Metamath Proof Explorer


Theorem dfsucon

Description: A is called a successor ordinal if it is not a limit ordinal and not the empty set. (Contributed by RP, 11-Nov-2023)

Ref Expression
Assertion dfsucon OrdA¬LimAAxOnA=sucx

Proof

Step Hyp Ref Expression
1 3ancomb OrdA¬LimAAOrdAA¬LimA
2 df-3an OrdAA¬LimAOrdAA¬LimA
3 df-ne A¬A=
4 3 anbi2i OrdAAOrdA¬A=
5 4 imbi1i OrdAAxOnA=sucxOrdA¬A=xOnA=sucx
6 pm5.6 OrdA¬A=xOnA=sucxOrdAA=xOnA=sucx
7 iman OrdAA=xOnA=sucx¬OrdA¬A=xOnA=sucx
8 5 6 7 3bitrri ¬OrdA¬A=xOnA=sucxOrdAAxOnA=sucx
9 dflim3 LimAOrdA¬A=xOnA=sucx
10 8 9 xchnxbir ¬LimAOrdAAxOnA=sucx
11 10 anbi2i OrdAA¬LimAOrdAAOrdAAxOnA=sucx
12 1 2 11 3bitri OrdA¬LimAAOrdAAOrdAAxOnA=sucx
13 pm3.35 OrdAAOrdAAxOnA=sucxxOnA=sucx
14 12 13 sylbi OrdA¬LimAAxOnA=sucx
15 eloni xOnOrdx
16 ordsuc OrdxOrdsucx
17 15 16 sylib xOnOrdsucx
18 nlimsucg xOn¬Limsucx
19 nsuceq0 sucx
20 19 a1i xOnsucx
21 17 18 20 3jca xOnOrdsucx¬Limsucxsucx
22 ordeq A=sucxOrdAOrdsucx
23 limeq A=sucxLimALimsucx
24 23 notbid A=sucx¬LimA¬Limsucx
25 neeq1 A=sucxAsucx
26 22 24 25 3anbi123d A=sucxOrdA¬LimAAOrdsucx¬Limsucxsucx
27 21 26 syl5ibrcom xOnA=sucxOrdA¬LimAA
28 27 rexlimiv xOnA=sucxOrdA¬LimAA
29 14 28 impbii OrdA¬LimAAxOnA=sucx