This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )