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 ⊢ A ≠ ∅ ∧ ∀ x ∈ A Lim ⁡ x → Lim ⁡ ⋃ A

Proof

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