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 AOnsucAS
Assertion ordtoplem OrdAAAAS

Proof

Step Hyp Ref Expression
1 ordtoplem.1 AOnsucAS
2 df-ne AA¬A=A
3 ordeleqon OrdAAOnA=On
4 unon On=On
5 4 eqcomi On=On
6 id A=OnA=On
7 unieq A=OnA=On
8 5 6 7 3eqtr4a A=OnA=A
9 8 orim2i AOnA=OnAOnA=A
10 3 9 sylbi OrdAAOnA=A
11 10 orcomd OrdAA=AAOn
12 11 ord OrdA¬A=AAOn
13 orduniorsuc OrdAA=AA=sucA
14 13 ord OrdA¬A=AA=sucA
15 onuni AOnAOn
16 eleq1a sucASA=sucAAS
17 15 1 16 3syl AOnA=sucAAS
18 12 14 17 syl6c OrdA¬A=AAS
19 2 18 biimtrid OrdAAAAS