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 Ord A ¬ Lim A A x On A = suc x

Proof

Step Hyp Ref Expression
1 3ancomb Ord A ¬ Lim A A Ord A A ¬ Lim A
2 df-3an Ord A A ¬ Lim A Ord A A ¬ Lim A
3 df-ne A ¬ A =
4 3 anbi2i Ord A A Ord A ¬ A =
5 4 imbi1i Ord A A x On A = suc x Ord A ¬ A = x On A = suc x
6 pm5.6 Ord A ¬ A = x On A = suc x Ord A A = x On A = suc x
7 iman Ord A A = x On A = suc x ¬ Ord A ¬ A = x On A = suc x
8 5 6 7 3bitrri ¬ Ord A ¬ A = x On A = suc x Ord A A x On A = suc x
9 dflim3 Lim A Ord A ¬ A = x On A = suc x
10 8 9 xchnxbir ¬ Lim A Ord A A x On A = suc x
11 10 anbi2i Ord A A ¬ Lim A Ord A A Ord A A x On A = suc x
12 1 2 11 3bitri Ord A ¬ Lim A A Ord A A Ord A A x On A = suc x
13 pm3.35 Ord A A Ord A A x On A = suc x x On A = suc x
14 12 13 sylbi Ord A ¬ Lim A A x On A = suc x
15 eloni x On Ord x
16 ordsuc Ord x Ord suc x
17 15 16 sylib x On Ord suc x
18 nlimsucg x On ¬ Lim suc x
19 nsuceq0 suc x
20 19 a1i x On suc x
21 17 18 20 3jca x On Ord suc x ¬ Lim suc x suc x
22 ordeq A = suc x Ord A Ord suc x
23 limeq A = suc x Lim A Lim suc x
24 23 notbid A = suc x ¬ Lim A ¬ Lim suc x
25 neeq1 A = suc x A suc x
26 22 24 25 3anbi123d A = suc x Ord A ¬ Lim A A Ord suc x ¬ Lim suc x suc x
27 21 26 syl5ibrcom x On A = suc x Ord A ¬ Lim A A
28 27 rexlimiv x On A = suc x Ord A ¬ Lim A A
29 14 28 impbii Ord A ¬ Lim A A x On A = suc x