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

Metamath Proof Explorer

Theorem ellimits

Description: Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012)

Ref Expression
Hypothesis ellimits.1 
|- A e. _V
Assertion ellimits 
|- ( A e. Limits <-> Lim A )

Proof

Step Hyp Ref Expression
1 ellimits.1 
 |-  A e. _V
2 df-limits 
 |-  Limits = ( ( On i^i Fix Bigcup ) \ { (/) } )
3 2 eleq2i 
 |-  ( A e. Limits <-> A e. ( ( On i^i Fix Bigcup ) \ { (/) } ) )
4 eldif 
 |-  ( A e. ( ( On i^i Fix Bigcup ) \ { (/) } ) <-> ( A e. ( On i^i Fix Bigcup ) /\ -. A e. { (/) } ) )
5 3anan32 
 |-  ( ( Ord A /\ A =/= (/) /\ A = U. A ) <-> ( ( Ord A /\ A = U. A ) /\ A =/= (/) ) )
6 df-lim 
 |-  ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
7 elin 
 |-  ( A e. ( On i^i Fix Bigcup ) <-> ( A e. On /\ A e. Fix Bigcup ) )
8 1 elon 
 |-  ( A e. On <-> Ord A )
9 1 elfix 
 |-  ( A e. Fix Bigcup <-> A Bigcup A )
10 1 brbigcup 
 |-  ( A Bigcup A <-> U. A = A )
11 eqcom 
 |-  ( U. A = A <-> A = U. A )
12 9 10 11 3bitri 
 |-  ( A e. Fix Bigcup <-> A = U. A )
13 8 12 anbi12i 
 |-  ( ( A e. On /\ A e. Fix Bigcup ) <-> ( Ord A /\ A = U. A ) )
14 7 13 bitri 
 |-  ( A e. ( On i^i Fix Bigcup ) <-> ( Ord A /\ A = U. A ) )
15 1 elsn 
 |-  ( A e. { (/) } <-> A = (/) )
16 15 necon3bbii 
 |-  ( -. A e. { (/) } <-> A =/= (/) )
17 14 16 anbi12i 
 |-  ( ( A e. ( On i^i Fix Bigcup ) /\ -. A e. { (/) } ) <-> ( ( Ord A /\ A = U. A ) /\ A =/= (/) ) )
18 5 6 17 3bitr4ri 
 |-  ( ( A e. ( On i^i Fix Bigcup ) /\ -. A e. { (/) } ) <-> Lim A )
19 3 4 18 3bitri 
 |-  ( A e. Limits <-> Lim A )