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 =/= (/) ) <-> E. x e. 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 =/= (/) ) -> E. x e. On A = suc x ) <-> ( ( Ord A /\ -. A = (/) ) -> E. x e. On A = suc x ) )
6 pm5.6 
 |-  ( ( ( Ord A /\ -. A = (/) ) -> E. x e. On A = suc x ) <-> ( Ord A -> ( A = (/) \/ E. x e. On A = suc x ) ) )
7 iman 
 |-  ( ( Ord A -> ( A = (/) \/ E. x e. On A = suc x ) ) <-> -. ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) )
8 5 6 7 3bitrri 
 |-  ( -. ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) <-> ( ( Ord A /\ A =/= (/) ) -> E. x e. On A = suc x ) )
9 dflim3 
 |-  ( Lim A <-> ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) )
10 8 9 xchnxbir 
 |-  ( -. Lim A <-> ( ( Ord A /\ A =/= (/) ) -> E. x e. On A = suc x ) )
11 10 anbi2i 
 |-  ( ( ( Ord A /\ A =/= (/) ) /\ -. Lim A ) <-> ( ( Ord A /\ A =/= (/) ) /\ ( ( Ord A /\ A =/= (/) ) -> E. x e. On A = suc x ) ) )
12 1 2 11 3bitri 
 |-  ( ( Ord A /\ -. Lim A /\ A =/= (/) ) <-> ( ( Ord A /\ A =/= (/) ) /\ ( ( Ord A /\ A =/= (/) ) -> E. x e. On A = suc x ) ) )
13 pm3.35 
 |-  ( ( ( Ord A /\ A =/= (/) ) /\ ( ( Ord A /\ A =/= (/) ) -> E. x e. On A = suc x ) ) -> E. x e. On A = suc x )
14 12 13 sylbi 
 |-  ( ( Ord A /\ -. Lim A /\ A =/= (/) ) -> E. x e. On A = suc x )
15 eloni 
 |-  ( x e. On -> Ord x )
16 ordsuc 
 |-  ( Ord x <-> Ord suc x )
17 15 16 sylib 
 |-  ( x e. On -> Ord suc x )
18 nlimsucg 
 |-  ( x e. On -> -. Lim suc x )
19 nsuceq0 
 |-  suc x =/= (/)
20 19 a1i 
 |-  ( x e. On -> suc x =/= (/) )
21 17 18 20 3jca 
 |-  ( x e. 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 e. On -> ( A = suc x -> ( Ord A /\ -. Lim A /\ A =/= (/) ) ) )
28 27 rexlimiv 
 |-  ( E. x e. On A = suc x -> ( Ord A /\ -. Lim A /\ A =/= (/) ) )
29 14 28 impbii 
 |-  ( ( Ord A /\ -. Lim A /\ A =/= (/) ) <-> E. x e. On A = suc x )