Metamath Proof Explorer


Theorem dflim2

Description: An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 df-lim
 |-  ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
2 ord0eln0
 |-  ( Ord A -> ( (/) e. A <-> A =/= (/) ) )
3 2 anbi1d
 |-  ( Ord A -> ( ( (/) e. A /\ A = U. A ) <-> ( A =/= (/) /\ A = U. A ) ) )
4 3 pm5.32i
 |-  ( ( Ord A /\ ( (/) e. A /\ A = U. A ) ) <-> ( Ord A /\ ( A =/= (/) /\ A = U. A ) ) )
5 3anass
 |-  ( ( Ord A /\ (/) e. A /\ A = U. A ) <-> ( Ord A /\ ( (/) e. A /\ A = U. A ) ) )
6 3anass
 |-  ( ( Ord A /\ A =/= (/) /\ A = U. A ) <-> ( Ord A /\ ( A =/= (/) /\ A = U. A ) ) )
7 4 5 6 3bitr4i
 |-  ( ( Ord A /\ (/) e. A /\ A = U. A ) <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
8 1 7 bitr4i
 |-  ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )