Metamath Proof Explorer


Theorem ordtoplem

Description: Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015)

Ref Expression
Hypothesis ordtoplem.1 ( 𝐴 ∈ On → suc 𝐴𝑆 )
Assertion ordtoplem ( Ord 𝐴 → ( 𝐴 𝐴𝐴𝑆 ) )

Proof

Step Hyp Ref Expression
1 ordtoplem.1 ( 𝐴 ∈ On → suc 𝐴𝑆 )
2 df-ne ( 𝐴 𝐴 ↔ ¬ 𝐴 = 𝐴 )
3 ordeleqon ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
4 unon On = On
5 4 eqcomi On = On
6 id ( 𝐴 = On → 𝐴 = On )
7 unieq ( 𝐴 = On → 𝐴 = On )
8 5 6 7 3eqtr4a ( 𝐴 = On → 𝐴 = 𝐴 )
9 8 orim2i ( ( 𝐴 ∈ On ∨ 𝐴 = On ) → ( 𝐴 ∈ On ∨ 𝐴 = 𝐴 ) )
10 3 9 sylbi ( Ord 𝐴 → ( 𝐴 ∈ On ∨ 𝐴 = 𝐴 ) )
11 10 orcomd ( Ord 𝐴 → ( 𝐴 = 𝐴𝐴 ∈ On ) )
12 11 ord ( Ord 𝐴 → ( ¬ 𝐴 = 𝐴𝐴 ∈ On ) )
13 orduniorsuc ( Ord 𝐴 → ( 𝐴 = 𝐴𝐴 = suc 𝐴 ) )
14 13 ord ( Ord 𝐴 → ( ¬ 𝐴 = 𝐴𝐴 = suc 𝐴 ) )
15 onuni ( 𝐴 ∈ On → 𝐴 ∈ On )
16 eleq1a ( suc 𝐴𝑆 → ( 𝐴 = suc 𝐴𝐴𝑆 ) )
17 15 1 16 3syl ( 𝐴 ∈ On → ( 𝐴 = suc 𝐴𝐴𝑆 ) )
18 12 14 17 syl6c ( Ord 𝐴 → ( ¬ 𝐴 = 𝐴𝐴𝑆 ) )
19 2 18 syl5bi ( Ord 𝐴 → ( 𝐴 𝐴𝐴𝑆 ) )