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

Metamath Proof Explorer

Theorem unizlim

Description: An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003)

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

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
2 df-lim 
 |-  ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
3 2 biimpri 
 |-  ( ( Ord A /\ A =/= (/) /\ A = U. A ) -> Lim A )
4 3 3exp 
 |-  ( Ord A -> ( A =/= (/) -> ( A = U. A -> Lim A ) ) )
5 1 4 biimtrrid 
 |-  ( Ord A -> ( -. A = (/) -> ( A = U. A -> Lim A ) ) )
6 5 com23 
 |-  ( Ord A -> ( A = U. A -> ( -. A = (/) -> Lim A ) ) )
7 6 imp 
 |-  ( ( Ord A /\ A = U. A ) -> ( -. A = (/) -> Lim A ) )
8 7 orrd 
 |-  ( ( Ord A /\ A = U. A ) -> ( A = (/) \/ Lim A ) )
9 8 ex 
 |-  ( Ord A -> ( A = U. A -> ( A = (/) \/ Lim A ) ) )
10 uni0 
 |-  U. (/) = (/)
11 10 eqcomi 
 |-  (/) = U. (/)
12 id 
 |-  ( A = (/) -> A = (/) )
13 unieq 
 |-  ( A = (/) -> U. A = U. (/) )
14 11 12 13 3eqtr4a 
 |-  ( A = (/) -> A = U. A )
15 limuni 
 |-  ( Lim A -> A = U. A )
16 14 15 jaoi 
 |-  ( ( A = (/) \/ Lim A ) -> A = U. A )
17 9 16 impbid1 
 |-  ( Ord A -> ( A = U. A <-> ( A = (/) \/ Lim A ) ) )