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 𝐴 → Ord suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ordtr	⊢ ( Ord 𝐴 → Tr 𝐴 )
2		suctr	⊢ ( Tr 𝐴 → Tr suc 𝐴 )
3	1 2	syl	⊢ ( Ord 𝐴 → Tr suc 𝐴 )
4		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
5		ordsson	⊢ ( Ord 𝐴 → 𝐴 ⊆ On )
6		elon2	⊢ ( 𝐴 ∈ On ↔ ( Ord 𝐴 ∧ 𝐴 ∈ V ) )
7		snssi	⊢ ( 𝐴 ∈ On → { 𝐴 } ⊆ On )
8	6 7	sylbir	⊢ ( ( Ord 𝐴 ∧ 𝐴 ∈ V ) → { 𝐴 } ⊆ On )
9		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
10	9	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
11		0ss	⊢ ∅ ⊆ On
12	10 11	eqsstrdi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } ⊆ On )
13	12	adantl	⊢ ( ( Ord 𝐴 ∧ ¬ 𝐴 ∈ V ) → { 𝐴 } ⊆ On )
14	8 13	pm2.61dan	⊢ ( Ord 𝐴 → { 𝐴 } ⊆ On )
15	5 14	unssd	⊢ ( Ord 𝐴 → ( 𝐴 ∪ { 𝐴 } ) ⊆ On )
16	4 15	eqsstrid	⊢ ( Ord 𝐴 → suc 𝐴 ⊆ On )
17		ordon	⊢ Ord On
18	17	a1i	⊢ ( Ord 𝐴 → Ord On )
19		trssord	⊢ ( ( Tr suc 𝐴 ∧ suc 𝐴 ⊆ On ∧ Ord On ) → Ord suc 𝐴 )
20	3 16 18 19	syl3anc	⊢ ( Ord 𝐴 → Ord suc 𝐴 )