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 OrdAA=AA=LimA

Proof

Step Hyp Ref Expression
1 df-ne A¬A=
2 df-lim LimAOrdAAA=A
3 2 biimpri OrdAAA=ALimA
4 3 3exp OrdAAA=ALimA
5 1 4 syl5bir OrdA¬A=A=ALimA
6 5 com23 OrdAA=A¬A=LimA
7 6 imp OrdAA=A¬A=LimA
8 7 orrd OrdAA=AA=LimA
9 8 ex OrdAA=AA=LimA
10 uni0 =
11 10 eqcomi =
12 id A=A=
13 unieq A=A=
14 11 12 13 3eqtr4a A=A=A
15 limuni LimAA=A
16 14 15 jaoi A=LimAA=A
17 9 16 impbid1 OrdAA=AA=LimA