Theorem unbnn

Description: Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. Part of the proof of Theorem 42 of Suppes p. 151. See unbnn3 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003)

	Ref	Expression
Assertion	unbnn	⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) → 𝐴 ≈ ω )

Proof

Step	Hyp	Ref	Expression
1		ssdomg	⊢ ( ω ∈ V → ( 𝐴 ⊆ ω → 𝐴 ≼ ω ) )
2	1	imp	⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ) → 𝐴 ≼ ω )
3	2	3adant3	⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) → 𝐴 ≼ ω )
4		simp1	⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) → ω ∈ V )
5		ssexg	⊢ ( ( 𝐴 ⊆ ω ∧ ω ∈ V ) → 𝐴 ∈ V )
6	5	ancoms	⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ) → 𝐴 ∈ V )
7	6	3adant3	⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) → 𝐴 ∈ V )
8		eqid	⊢ ( rec ( ( 𝑧 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑧 ) ) , ∩ 𝐴 ) ↾ ω ) = ( rec ( ( 𝑧 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑧 ) ) , ∩ 𝐴 ) ↾ ω )
9	8	unblem4	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) → ( rec ( ( 𝑧 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑧 ) ) , ∩ 𝐴 ) ↾ ω ) : ω –1-1→ 𝐴 )
10	9	3adant1	⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) → ( rec ( ( 𝑧 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑧 ) ) , ∩ 𝐴 ) ↾ ω ) : ω –1-1→ 𝐴 )
11		f1dom2g	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ V ∧ ( rec ( ( 𝑧 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑧 ) ) , ∩ 𝐴 ) ↾ ω ) : ω –1-1→ 𝐴 ) → ω ≼ 𝐴 )
12	4 7 10 11	syl3anc	⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) → ω ≼ 𝐴 )
13		sbth	⊢ ( ( 𝐴 ≼ ω ∧ ω ≼ 𝐴 ) → 𝐴 ≈ ω )
14	3 12 13	syl2anc	⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) → 𝐴 ≈ ω )