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

Metamath Proof Explorer

Theorem dflim4

Description: An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005)

Ref Expression
Assertion dflim4 
|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A. x e. A suc x e. A ) )

Proof

Step Hyp Ref Expression
1 dflim2 
 |-  ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
2 ordunisuc2 
 |-  ( Ord A -> ( A = U. A <-> A. x e. A suc x e. A ) )
3 2 anbi2d 
 |-  ( Ord A -> ( ( (/) e. A /\ A = U. A ) <-> ( (/) e. A /\ A. x e. A suc x e. A ) ) )
4 3 pm5.32i 
 |-  ( ( Ord A /\ ( (/) e. A /\ A = U. A ) ) <-> ( Ord A /\ ( (/) e. A /\ A. x e. A suc x e. A ) ) )
5 3anass 
 |-  ( ( Ord A /\ (/) e. A /\ A = U. A ) <-> ( Ord A /\ ( (/) e. A /\ A = U. A ) ) )
6 3anass 
 |-  ( ( Ord A /\ (/) e. A /\ A. x e. A suc x e. A ) <-> ( Ord A /\ ( (/) e. A /\ A. x e. A suc x e. A ) ) )
7 4 5 6 3bitr4i 
 |-  ( ( Ord A /\ (/) e. A /\ A = U. A ) <-> ( Ord A /\ (/) e. A /\ A. x e. A suc x e. A ) )
8 1 7 bitri 
 |-  ( Lim A <-> ( Ord A /\ (/) e. A /\ A. x e. A suc x e. A ) )