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

Metamath Proof Explorer

Definition df-lim

Description: Define the limit ordinal predicate, which is true for a nonempty ordinal that is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of BellMachover p. 471 and Exercise 1 of TakeutiZaring p. 42. See dflim2 , dflim3 , and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994)

Ref Expression
Assertion df-lim 
|- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 0 wlim 
 |-  Lim A
2 0 word 
 |-  Ord A
3 c0 
 |-  (/)
4 0 3 wne 
 |-  A =/= (/)
5 0 cuni 
 |-  U. A
6 0 5 wceq 
 |-  A = U. A
7 2 4 6 w3a 
 |-  ( Ord A /\ A =/= (/) /\ A = U. A )
8 1 7 wb 
 |-  ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )