Theorem orduniorsuc

Description: An ordinal class is either its union or the successor of its union. If we adopt the view that zero is a limit ordinal, this means every ordinal class is either a limit or a successor. (Contributed by NM, 13-Sep-2003)

	Ref	Expression
Assertion	orduniorsuc	|- ( Ord A -> ( A = U. A \/ A = suc U. A ) )

Proof

Step	Hyp	Ref	Expression
1		orduniss	|- ( Ord A -> U. A C_ A )
2		orduni	|- ( Ord A -> Ord U. A )
3		ordelssne	|- ( ( Ord U. A /\ Ord A ) -> ( U. A e. A <-> ( U. A C_ A /\ U. A =/= A ) ) )
4	2 3	mpancom	|- ( Ord A -> ( U. A e. A <-> ( U. A C_ A /\ U. A =/= A ) ) )
5	4	biimprd	|- ( Ord A -> ( ( U. A C_ A /\ U. A =/= A ) -> U. A e. A ) )
6	1 5	mpand	|- ( Ord A -> ( U. A =/= A -> U. A e. A ) )
7		ordsucss	|- ( Ord A -> ( U. A e. A -> suc U. A C_ A ) )
8	6 7	syld	|- ( Ord A -> ( U. A =/= A -> suc U. A C_ A ) )
9		ordsucuni	|- ( Ord A -> A C_ suc U. A )
10	8 9	jctild	|- ( Ord A -> ( U. A =/= A -> ( A C_ suc U. A /\ suc U. A C_ A ) ) )
11		df-ne	|- ( A =/= U. A <-> -. A = U. A )
12		necom	|- ( A =/= U. A <-> U. A =/= A )
13	11 12	bitr3i	|- ( -. A = U. A <-> U. A =/= A )
14		eqss	|- ( A = suc U. A <-> ( A C_ suc U. A /\ suc U. A C_ A ) )
15	10 13 14	3imtr4g	|- ( Ord A -> ( -. A = U. A -> A = suc U. A ) )
16	15	orrd	|- ( Ord A -> ( A = U. A \/ A = suc U. A ) )