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∈ALim⁡x→Lim⁡⋃A

Proof

Step Hyp Ref Expression
1 limeq ⊢x=z→Lim⁡x↔Lim⁡z
2 1 rspcv ⊢z∈A→∀x∈ALim⁡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∈ALim⁡x→z∈A→z∈On
7 6 ssrdv ⊢∀x∈ALim⁡x→A⊆On
8 ssorduni ⊢A⊆On→Ord⁡⋃A
9 7 8 syl ⊢∀x∈ALim⁡x→Ord⁡⋃A
10 9 adantl ⊢A≠∅∧∀x∈ALim⁡x→Ord⁡⋃A
11 n0 ⊢A≠∅↔∃zz∈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∈ALim⁡x→∅∈⋃A
17 16 exlimiv ⊢∃zz∈A→∀x∈ALim⁡x→∅∈⋃A
18 11 17 sylbi ⊢A≠∅→∀x∈ALim⁡x→∅∈⋃A
19 18 imp ⊢A≠∅∧∀x∈ALim⁡x→∅∈⋃A
20 eluni2 ⊢y∈⋃A↔∃z∈Ay∈z
21 1 rspccv ⊢∀x∈ALim⁡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∈ALim⁡x→z∈A→y∈z→suc⁡y∈⋃A
29 28 rexlimdv ⊢∀x∈ALim⁡x→∃z∈Ay∈z→suc⁡y∈⋃A
30 20 29 biimtrid ⊢∀x∈ALim⁡x→y∈⋃A→suc⁡y∈⋃A
31 30 ralrimiv ⊢∀x∈ALim⁡x→∀y∈⋃Asuc⁡y∈⋃A
32 31 adantl ⊢A≠∅∧∀x∈ALim⁡x→∀y∈⋃Asuc⁡y∈⋃A
33 dflim4 ⊢Lim⁡⋃A↔Ord⁡⋃A∧∅∈⋃A∧∀y∈⋃Asuc⁡y∈⋃A
34 10 19 32 33 syl3anbrc ⊢A≠∅∧∀x∈ALim⁡x→Lim⁡⋃A