Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ellimits Structured version   Visualization version   GIF version

Theorem ellimits 35744
Description: Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
Hypothesis
Ref Expression
ellimits.1 𝐴 ∈ V
Assertion
Ref Expression
ellimits (𝐴 Limits ↔ Lim 𝐴)

Proof of Theorem ellimits
StepHypRef Expression
1 df-limits 35694 . . 3 Limits = ((On ∩ Fix Bigcup ) ∖ {∅})
21eleq2i 2818 . 2 (𝐴 Limits 𝐴 ∈ ((On ∩ Fix Bigcup ) ∖ {∅}))
3 eldif 3956 . 2 (𝐴 ∈ ((On ∩ Fix Bigcup ) ∖ {∅}) ↔ (𝐴 ∈ (On ∩ Fix Bigcup ) ∧ ¬ 𝐴 ∈ {∅}))
4 3anan32 1094 . . 3 ((Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴) ↔ ((Ord 𝐴𝐴 = 𝐴) ∧ 𝐴 ≠ ∅))
5 df-lim 6370 . . 3 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
6 elin 3962 . . . . 5 (𝐴 ∈ (On ∩ Fix Bigcup ) ↔ (𝐴 ∈ On ∧ 𝐴 Fix Bigcup ))
7 ellimits.1 . . . . . . 7 𝐴 ∈ V
87elon 6374 . . . . . 6 (𝐴 ∈ On ↔ Ord 𝐴)
97elfix 35737 . . . . . . 7 (𝐴 Fix Bigcup 𝐴 Bigcup 𝐴)
107brbigcup 35732 . . . . . . 7 (𝐴 Bigcup 𝐴 𝐴 = 𝐴)
11 eqcom 2733 . . . . . . 7 ( 𝐴 = 𝐴𝐴 = 𝐴)
129, 10, 113bitri 296 . . . . . 6 (𝐴 Fix Bigcup 𝐴 = 𝐴)
138, 12anbi12i 626 . . . . 5 ((𝐴 ∈ On ∧ 𝐴 Fix Bigcup ) ↔ (Ord 𝐴𝐴 = 𝐴))
146, 13bitri 274 . . . 4 (𝐴 ∈ (On ∩ Fix Bigcup ) ↔ (Ord 𝐴𝐴 = 𝐴))
157elsn 4638 . . . . 5 (𝐴 ∈ {∅} ↔ 𝐴 = ∅)
1615necon3bbii 2978 . . . 4 𝐴 ∈ {∅} ↔ 𝐴 ≠ ∅)
1714, 16anbi12i 626 . . 3 ((𝐴 ∈ (On ∩ Fix Bigcup ) ∧ ¬ 𝐴 ∈ {∅}) ↔ ((Ord 𝐴𝐴 = 𝐴) ∧ 𝐴 ≠ ∅))
184, 5, 173bitr4ri 303 . 2 ((𝐴 ∈ (On ∩ Fix Bigcup ) ∧ ¬ 𝐴 ∈ {∅}) ↔ Lim 𝐴)
192, 3, 183bitri 296 1 (𝐴 Limits ↔ Lim 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wne 2930  Vcvv 3462  cdif 3943  cin 3945  c0 4322  {csn 4623   cuni 4905   class class class wbr 5143  Ord word 6364  Oncon0 6365  Lim wlim 6366   Bigcup cbigcup 35668   Fix cfix 35669   Limits climits 35670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7735
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-symdif 4241  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ord 6368  df-on 6369  df-lim 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fo 6549  df-fv 6551  df-1st 7992  df-2nd 7993  df-txp 35688  df-bigcup 35692  df-fix 35693  df-limits 35694
This theorem is referenced by:  dfom5b  35746  dfrdg4  35785
  Copyright terms: Public domain W3C validator