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

Metamath Proof Explorer

Theorem unbnn2

Description: Version of unbnn that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004)

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

Proof

Step Hyp Ref Expression
1 peano2 ⊢ ( 𝑧 ∈ ω → suc 𝑧 ∈ ω )
2 sseq1 ⊢ ( 𝑥 = suc 𝑧 → ( 𝑥 ⊆ 𝑦 ↔ suc 𝑧 ⊆ 𝑦 ) )
3 2 rexbidv ⊢ ( 𝑥 = suc 𝑧 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 suc 𝑧 ⊆ 𝑦 ) )
4 3 rspcv ⊢ ( suc 𝑧 ∈ ω → ( ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 → ∃ 𝑦 ∈ 𝐴 suc 𝑧 ⊆ 𝑦 ) )
5 sucssel ⊢ ( 𝑧 ∈ V → ( suc 𝑧 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) )
6 5 elv ⊢ ( suc 𝑧 ⊆ 𝑦 → 𝑧 ∈ 𝑦 )
7 6 reximi ⊢ ( ∃ 𝑦 ∈ 𝐴 suc 𝑧 ⊆ 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 )
8 4 7 syl6com ⊢ ( ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 → ( suc 𝑧 ∈ ω → ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
9 1 8 syl5 ⊢ ( ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 → ( 𝑧 ∈ ω → ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
10 9 ralrimiv ⊢ ( ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 → ∀ 𝑧 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 )
11 unbnn ⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀ 𝑧 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) → 𝐴 ≈ ω )
12 10 11 syl3an3 ⊢ ( ( ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) → 𝐴 ≈ ω )