Theorem suceloni

Description: The successor of an ordinal number is an ordinal number. Proposition 7.24 of TakeutiZaring p. 41. (Contributed by NM, 6-Jun-1994)

	Ref	Expression
Assertion	suceloni	|- ( A e. On -> suc A e. On )

Proof

Step	Hyp	Ref	Expression
1		onelss	|- ( A e. On -> ( x e. A -> x C_ A ) )
2		velsn	|- ( x e. { A } <-> x = A )
3		eqimss	|- ( x = A -> x C_ A )
4	2 3	sylbi	|- ( x e. { A } -> x C_ A )
5	4	a1i	|- ( A e. On -> ( x e. { A } -> x C_ A ) )
6	1 5	orim12d	|- ( A e. On -> ( ( x e. A \/ x e. { A } ) -> ( x C_ A \/ x C_ A ) ) )
7		df-suc	|- suc A = ( A u. { A } )
8	7	eleq2i	|- ( x e. suc A <-> x e. ( A u. { A } ) )
9		elun	|- ( x e. ( A u. { A } ) <-> ( x e. A \/ x e. { A } ) )
10	8 9	bitr2i	|- ( ( x e. A \/ x e. { A } ) <-> x e. suc A )
11		oridm	|- ( ( x C_ A \/ x C_ A ) <-> x C_ A )
12	6 10 11	3imtr3g	|- ( A e. On -> ( x e. suc A -> x C_ A ) )
13		sssucid	|- A C_ suc A
14		sstr2	|- ( x C_ A -> ( A C_ suc A -> x C_ suc A ) )
15	12 13 14	syl6mpi	|- ( A e. On -> ( x e. suc A -> x C_ suc A ) )
16	15	ralrimiv	|- ( A e. On -> A. x e. suc A x C_ suc A )
17		dftr3	|- ( Tr suc A <-> A. x e. suc A x C_ suc A )
18	16 17	sylibr	|- ( A e. On -> Tr suc A )
19		onss	|- ( A e. On -> A C_ On )
20		snssi	|- ( A e. On -> { A } C_ On )
21	19 20	unssd	|- ( A e. On -> ( A u. { A } ) C_ On )
22	7 21	eqsstrid	|- ( A e. On -> suc A C_ On )
23		ordon	|- Ord On
24		trssord	|- ( ( Tr suc A /\ suc A C_ On /\ Ord On ) -> Ord suc A )
25	24	3exp	|- ( Tr suc A -> ( suc A C_ On -> ( Ord On -> Ord suc A ) ) )
26	23 25	mpii	|- ( Tr suc A -> ( suc A C_ On -> Ord suc A ) )
27	18 22 26	sylc	|- ( A e. On -> Ord suc A )
28		sucexg	|- ( A e. On -> suc A e. _V )
29		elong	|- ( suc A e. _V -> ( suc A e. On <-> Ord suc A ) )
30	28 29	syl	|- ( A e. On -> ( suc A e. On <-> Ord suc A ) )
31	27 30	mpbird	|- ( A e. On -> suc A e. On )