  We study cofinal systems of finite subsets of $\omega_1$. We show that while
such systems can be NIP, they cannot be defined in an NIP structure. We deduce
a positive answer to a question of Chernikov and Simon from 2013: in an NIP
theory, any uncountable externally definable set contains an infinite definable
subset. A similar result holds for larger cardinals.
