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