Theorem ordtoplem

Description: Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015)

	Ref	Expression
Hypothesis	ordtoplem.1	|- ( U. A e. On -> suc U. A e. S )
Assertion	ordtoplem	|- ( Ord A -> ( A =/= U. A -> A e. S ) )

Proof

Step	Hyp	Ref	Expression
1		ordtoplem.1	|- ( U. A e. On -> suc U. A e. S )
2		df-ne	|- ( A =/= U. A <-> -. A = U. A )
3		ordeleqon	|- ( Ord A <-> ( A e. On \/ A = On ) )
4		unon	|- U. On = On
5	4	eqcomi	|- On = U. On
6		id	|- ( A = On -> A = On )
7		unieq	|- ( A = On -> U. A = U. On )
8	5 6 7	3eqtr4a	|- ( A = On -> A = U. A )
9	8	orim2i	|- ( ( A e. On \/ A = On ) -> ( A e. On \/ A = U. A ) )
10	3 9	sylbi	|- ( Ord A -> ( A e. On \/ A = U. A ) )
11	10	orcomd	|- ( Ord A -> ( A = U. A \/ A e. On ) )
12	11	ord	|- ( Ord A -> ( -. A = U. A -> A e. On ) )
13		orduniorsuc	|- ( Ord A -> ( A = U. A \/ A = suc U. A ) )
14	13	ord	|- ( Ord A -> ( -. A = U. A -> A = suc U. A ) )
15		onuni	|- ( A e. On -> U. A e. On )
16		eleq1a	|- ( suc U. A e. S -> ( A = suc U. A -> A e. S ) )
17	15 1 16	3syl	|- ( A e. On -> ( A = suc U. A -> A e. S ) )
18	12 14 17	syl6c	|- ( Ord A -> ( -. A = U. A -> A e. S ) )
19	2 18	syl5bi	|- ( Ord A -> ( A =/= U. A -> A e. S ) )