MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  limuni3 Structured version   Visualization version   GIF version

Theorem limuni3 7381
Description: The union of a nonempty class of limit ordinals is a limit ordinal. (Contributed by NM, 1-Feb-2005.)
Assertion
Ref Expression
limuni3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 Lim 𝑥) → Lim 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem limuni3
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limeq 6038 . . . . . . 7 (𝑥 = 𝑧 → (Lim 𝑥 ↔ Lim 𝑧))
21rspcv 3524 . . . . . 6 (𝑧𝐴 → (∀𝑥𝐴 Lim 𝑥 → Lim 𝑧))
3 vex 3411 . . . . . . 7 𝑧 ∈ V
4 limelon 6089 . . . . . . 7 ((𝑧 ∈ V ∧ Lim 𝑧) → 𝑧 ∈ On)
53, 4mpan 678 . . . . . 6 (Lim 𝑧𝑧 ∈ On)
62, 5syl6com 37 . . . . 5 (∀𝑥𝐴 Lim 𝑥 → (𝑧𝐴𝑧 ∈ On))
76ssrdv 3857 . . . 4 (∀𝑥𝐴 Lim 𝑥𝐴 ⊆ On)
8 ssorduni 7314 . . . 4 (𝐴 ⊆ On → Ord 𝐴)
97, 8syl 17 . . 3 (∀𝑥𝐴 Lim 𝑥 → Ord 𝐴)
109adantl 474 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 Lim 𝑥) → Ord 𝐴)
11 n0 4190 . . . 4 (𝐴 ≠ ∅ ↔ ∃𝑧 𝑧𝐴)
12 0ellim 6088 . . . . . . 7 (Lim 𝑧 → ∅ ∈ 𝑧)
13 elunii 4713 . . . . . . . 8 ((∅ ∈ 𝑧𝑧𝐴) → ∅ ∈ 𝐴)
1413expcom 406 . . . . . . 7 (𝑧𝐴 → (∅ ∈ 𝑧 → ∅ ∈ 𝐴))
1512, 14syl5 34 . . . . . 6 (𝑧𝐴 → (Lim 𝑧 → ∅ ∈ 𝐴))
162, 15syld 47 . . . . 5 (𝑧𝐴 → (∀𝑥𝐴 Lim 𝑥 → ∅ ∈ 𝐴))
1716exlimiv 1890 . . . 4 (∃𝑧 𝑧𝐴 → (∀𝑥𝐴 Lim 𝑥 → ∅ ∈ 𝐴))
1811, 17sylbi 209 . . 3 (𝐴 ≠ ∅ → (∀𝑥𝐴 Lim 𝑥 → ∅ ∈ 𝐴))
1918imp 398 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 Lim 𝑥) → ∅ ∈ 𝐴)
20 eluni2 4712 . . . . 5 (𝑦 𝐴 ↔ ∃𝑧𝐴 𝑦𝑧)
211rspccv 3525 . . . . . . 7 (∀𝑥𝐴 Lim 𝑥 → (𝑧𝐴 → Lim 𝑧))
22 limsuc 7378 . . . . . . . . . . 11 (Lim 𝑧 → (𝑦𝑧 ↔ suc 𝑦𝑧))
2322anbi1d 621 . . . . . . . . . 10 (Lim 𝑧 → ((𝑦𝑧𝑧𝐴) ↔ (suc 𝑦𝑧𝑧𝐴)))
24 elunii 4713 . . . . . . . . . 10 ((suc 𝑦𝑧𝑧𝐴) → suc 𝑦 𝐴)
2523, 24syl6bi 245 . . . . . . . . 9 (Lim 𝑧 → ((𝑦𝑧𝑧𝐴) → suc 𝑦 𝐴))
2625expd 408 . . . . . . . 8 (Lim 𝑧 → (𝑦𝑧 → (𝑧𝐴 → suc 𝑦 𝐴)))
2726com3r 87 . . . . . . 7 (𝑧𝐴 → (Lim 𝑧 → (𝑦𝑧 → suc 𝑦 𝐴)))
2821, 27sylcom 30 . . . . . 6 (∀𝑥𝐴 Lim 𝑥 → (𝑧𝐴 → (𝑦𝑧 → suc 𝑦 𝐴)))
2928rexlimdv 3221 . . . . 5 (∀𝑥𝐴 Lim 𝑥 → (∃𝑧𝐴 𝑦𝑧 → suc 𝑦 𝐴))
3020, 29syl5bi 234 . . . 4 (∀𝑥𝐴 Lim 𝑥 → (𝑦 𝐴 → suc 𝑦 𝐴))
3130ralrimiv 3124 . . 3 (∀𝑥𝐴 Lim 𝑥 → ∀𝑦 𝐴 suc 𝑦 𝐴)
3231adantl 474 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 Lim 𝑥) → ∀𝑦 𝐴 suc 𝑦 𝐴)
33 dflim4 7377 . 2 (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑦 𝐴 suc 𝑦 𝐴))
3410, 19, 32, 33syl3anbrc 1324 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 Lim 𝑥) → Lim 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wex 1743  wcel 2051  wne 2960  wral 3081  wrex 3082  Vcvv 3408  wss 3822  c0 4172   cuni 4708  Ord word 6025  Oncon0 6026  Lim wlim 6027  suc csuc 6028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-sep 5056  ax-nul 5063  ax-pr 5182  ax-un 7277
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-ral 3086  df-rex 3087  df-rab 3090  df-v 3410  df-sbc 3675  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-pss 3838  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-br 4926  df-opab 4988  df-tr 5027  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-we 5364  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator