Theorem numinfctb

Description: A numerable infinite set contains a countable subset.MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015)

	Ref	Expression
Assertion	numinfctb	⊢ ( ( 𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin ) → ω ≼ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		omelon	⊢ ω ∈ On
2		onenon	⊢ ( ω ∈ On → ω ∈ dom card )
3	1 2	ax-mp	⊢ ω ∈ dom card
4		domtri2	⊢ ( ( ω ∈ dom card ∧ 𝑆 ∈ dom card ) → ( ω ≼ 𝑆 ↔ ¬ 𝑆 ≺ ω ) )
5	3 4	mpan	⊢ ( 𝑆 ∈ dom card → ( ω ≼ 𝑆 ↔ ¬ 𝑆 ≺ ω ) )
6		isfinite	⊢ ( 𝑆 ∈ Fin ↔ 𝑆 ≺ ω )
7	6	notbii	⊢ ( ¬ 𝑆 ∈ Fin ↔ ¬ 𝑆 ≺ ω )
8	5 7	bitr4di	⊢ ( 𝑆 ∈ dom card → ( ω ≼ 𝑆 ↔ ¬ 𝑆 ∈ Fin ) )
9	8	biimpar	⊢ ( ( 𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin ) → ω ≼ 𝑆 )