This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) → 𝐴 ≈ ω )