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