Theorem ordsuci

Description: The successor of an ordinal class is an ordinal class. Remark 1.5 of Schloeder p. 1. (Contributed by NM, 6-Jun-1994) Extract and adapt from a subproof of onsuc . (Revised by BTernaryTau, 6-Jan-2025) (Proof shortened by BJ, 11-Jan-2025)

	Ref	Expression
Assertion	ordsuci	|- ( Ord A -> Ord suc A )

Proof

Step	Hyp	Ref	Expression
1		ordtr	|- ( Ord A -> Tr A )
2		suctr	|- ( Tr A -> Tr suc A )
3	1 2	syl	|- ( Ord A -> Tr suc A )
4		df-suc	|- suc A = ( A u. { A } )
5		ordsson	|- ( Ord A -> A C_ On )
6		elon2	|- ( A e. On <-> ( Ord A /\ A e. _V ) )
7		snssi	|- ( A e. On -> { A } C_ On )
8	6 7	sylbir	|- ( ( Ord A /\ A e. _V ) -> { A } C_ On )
9		snprc	|- ( -. A e. _V <-> { A } = (/) )
10	9	biimpi	|- ( -. A e. _V -> { A } = (/) )
11		0ss	|- (/) C_ On
12	10 11	eqsstrdi	|- ( -. A e. _V -> { A } C_ On )
13	12	adantl	|- ( ( Ord A /\ -. A e. _V ) -> { A } C_ On )
14	8 13	pm2.61dan	|- ( Ord A -> { A } C_ On )
15	5 14	unssd	|- ( Ord A -> ( A u. { A } ) C_ On )
16	4 15	eqsstrid	|- ( Ord A -> suc A C_ On )
17		ordon	|- Ord On
18	17	a1i	|- ( Ord A -> Ord On )
19		trssord	|- ( ( Tr suc A /\ suc A C_ On /\ Ord On ) -> Ord suc A )
20	3 16 18 19	syl3anc	|- ( Ord A -> Ord suc A )