Metamath Proof Explorer

Theorem onsucf1olem

Description: The successor operation is bijective between the ordinals and the class of successor ordinals. Lemma 1.17 of Schloeder p. 2. (Contributed by RP, 18-Jan-2025)

Ref Expression
Assertion onsucf1olem 
|- ( ( A e. On /\ A =/= (/) /\ -. Lim A ) -> E! b e. On A = suc b )

Proof

Step Hyp Ref Expression
1 onuni 
 |-  ( A e. On -> U. A e. On )
2 1 3ad2ant1 
 |-  ( ( A e. On /\ A =/= (/) /\ -. Lim A ) -> U. A e. On )
3 eloni 
 |-  ( A e. On -> Ord A )
4 unizlim 
 |-  ( Ord A -> ( A = U. A <-> ( A = (/) \/ Lim A ) ) )
5 oran 
 |-  ( ( A = (/) \/ Lim A ) <-> -. ( -. A = (/) /\ -. Lim A ) )
6 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
7 6 anbi1i 
 |-  ( ( A =/= (/) /\ -. Lim A ) <-> ( -. A = (/) /\ -. Lim A ) )
8 5 7 xchbinxr 
 |-  ( ( A = (/) \/ Lim A ) <-> -. ( A =/= (/) /\ -. Lim A ) )
9 4 8 bitrdi 
 |-  ( Ord A -> ( A = U. A <-> -. ( A =/= (/) /\ -. Lim A ) ) )
10 3 9 syl 
 |-  ( A e. On -> ( A = U. A <-> -. ( A =/= (/) /\ -. Lim A ) ) )
11 pm2.21 
 |-  ( -. ( A =/= (/) /\ -. Lim A ) -> ( ( A =/= (/) /\ -. Lim A ) -> A = suc U. A ) )
12 10 11 biimtrdi 
 |-  ( A e. On -> ( A = U. A -> ( ( A =/= (/) /\ -. Lim A ) -> A = suc U. A ) ) )
13 12 com23 
 |-  ( A e. On -> ( ( A =/= (/) /\ -. Lim A ) -> ( A = U. A -> A = suc U. A ) ) )
14 13 3impib 
 |-  ( ( A e. On /\ A =/= (/) /\ -. Lim A ) -> ( A = U. A -> A = suc U. A ) )
15 idd 
 |-  ( ( A e. On /\ A =/= (/) /\ -. Lim A ) -> ( A = suc U. A -> A = suc U. A ) )
16 onuniorsuc 
 |-  ( A e. On -> ( A = U. A \/ A = suc U. A ) )
17 16 3ad2ant1 
 |-  ( ( A e. On /\ A =/= (/) /\ -. Lim A ) -> ( A = U. A \/ A = suc U. A ) )
18 14 15 17 mpjaod 
 |-  ( ( A e. On /\ A =/= (/) /\ -. Lim A ) -> A = suc U. A )
19 2 18 jca 
 |-  ( ( A e. On /\ A =/= (/) /\ -. Lim A ) -> ( U. A e. On /\ A = suc U. A ) )
20 eleq1 
 |-  ( b = U. A -> ( b e. On <-> U. A e. On ) )
21 suceq 
 |-  ( b = U. A -> suc b = suc U. A )
22 21 eqeq2d 
 |-  ( b = U. A -> ( A = suc b <-> A = suc U. A ) )
23 20 22 anbi12d 
 |-  ( b = U. A -> ( ( b e. On /\ A = suc b ) <-> ( U. A e. On /\ A = suc U. A ) ) )
24 2 19 23 spcedv 
 |-  ( ( A e. On /\ A =/= (/) /\ -. Lim A ) -> E. b ( b e. On /\ A = suc b ) )
25 onsucf1lem 
 |-  ( A e. On -> E* b e. On A = suc b )
26 25 3ad2ant1 
 |-  ( ( A e. On /\ A =/= (/) /\ -. Lim A ) -> E* b e. On A = suc b )
27 df-eu 
 |-  ( E! b ( b e. On /\ A = suc b ) <-> ( E. b ( b e. On /\ A = suc b ) /\ E* b ( b e. On /\ A = suc b ) ) )
28 df-reu 
 |-  ( E! b e. On A = suc b <-> E! b ( b e. On /\ A = suc b ) )
29 df-rmo 
 |-  ( E* b e. On A = suc b <-> E* b ( b e. On /\ A = suc b ) )
30 29 anbi2i 
 |-  ( ( E. b ( b e. On /\ A = suc b ) /\ E* b e. On A = suc b ) <-> ( E. b ( b e. On /\ A = suc b ) /\ E* b ( b e. On /\ A = suc b ) ) )
31 27 28 30 3bitr4i 
 |-  ( E! b e. On A = suc b <-> ( E. b ( b e. On /\ A = suc b ) /\ E* b e. On A = suc b ) )
32 24 26 31 sylanbrc 
 |-  ( ( A e. On /\ A =/= (/) /\ -. Lim A ) -> E! b e. On A = suc b )