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 syl5bir
 |-  ( 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 ) ) )