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