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

Metamath Proof Explorer

Theorem limuni3

Description: The union of a nonempty class of limit ordinals is a limit ordinal. (Contributed by NM, 1-Feb-2005)

Ref Expression
Assertion limuni3 ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Lim 𝑥 ) → Lim ∪ 𝐴 )

Proof

Step Hyp Ref Expression
1 limeq ⊢ ( 𝑥 = 𝑧 → ( Lim 𝑥 ↔ Lim 𝑧 ) )
2 1 rspcv ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → Lim 𝑧 ) )
3 vex ⊢ 𝑧 ∈ V
4 limelon ⊢ ( ( 𝑧 ∈ V ∧ Lim 𝑧 ) → 𝑧 ∈ On )
5 3 4 mpan ⊢ ( Lim 𝑧 → 𝑧 ∈ On )
6 2 5 syl6com ⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ On ) )
7 6 ssrdv ⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → 𝐴 ⊆ On )
8 ssorduni ⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
9 7 8 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → Ord ∪ 𝐴 )
10 9 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Lim 𝑥 ) → Ord ∪ 𝐴 )
11 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
12 0ellim ⊢ ( Lim 𝑧 → ∅ ∈ 𝑧 )
13 elunii ⊢ ( ( ∅ ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → ∅ ∈ ∪ 𝐴 )
14 13 expcom ⊢ ( 𝑧 ∈ 𝐴 → ( ∅ ∈ 𝑧 → ∅ ∈ ∪ 𝐴 ) )
15 12 14 syl5 ⊢ ( 𝑧 ∈ 𝐴 → ( Lim 𝑧 → ∅ ∈ ∪ 𝐴 ) )
16 2 15 syld ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴 ) )
17 16 exlimiv ⊢ ( ∃ 𝑧 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴 ) )
18 11 17 sylbi ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴 ) )
19 18 imp ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Lim 𝑥 ) → ∅ ∈ ∪ 𝐴 )
20 eluni2 ⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 )
21 1 rspccv ⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ( 𝑧 ∈ 𝐴 → Lim 𝑧 ) )
22 limsuc ⊢ ( Lim 𝑧 → ( 𝑦 ∈ 𝑧 ↔ suc 𝑦 ∈ 𝑧 ) )
23 22 anbi1d ⊢ ( Lim 𝑧 → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) ↔ ( suc 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) ) )
24 elunii ⊢ ( ( suc 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → suc 𝑦 ∈ ∪ 𝐴 )
25 23 24 biimtrdi ⊢ ( Lim 𝑧 → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → suc 𝑦 ∈ ∪ 𝐴 ) )
26 25 expd ⊢ ( Lim 𝑧 → ( 𝑦 ∈ 𝑧 → ( 𝑧 ∈ 𝐴 → suc 𝑦 ∈ ∪ 𝐴 ) ) )
27 26 com3r ⊢ ( 𝑧 ∈ 𝐴 → ( Lim 𝑧 → ( 𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴 ) ) )
28 21 27 sylcom ⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ( 𝑧 ∈ 𝐴 → ( 𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴 ) ) )
29 28 rexlimdv ⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ( ∃ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴 ) )
30 20 29 biimtrid ⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ( 𝑦 ∈ ∪ 𝐴 → suc 𝑦 ∈ ∪ 𝐴 ) )
31 30 ralrimiv ⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ∀ 𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴 )
32 31 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Lim 𝑥 ) → ∀ 𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴 )
33 dflim4 ⊢ ( Lim ∪ 𝐴 ↔ ( Ord ∪ 𝐴 ∧ ∅ ∈ ∪ 𝐴 ∧ ∀ 𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴 ) )
34 10 19 32 33 syl3anbrc ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Lim 𝑥 ) → Lim ∪ 𝐴 )