Metamath Proof Explorer

Theorem nadd1suc

Description: Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024)

Ref Expression
Assertion nadd1suc 
|- ( A e. On -> ( A +no 1o ) = suc A )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = b -> ( a +no 1o ) = ( b +no 1o ) )
2 suceq 
 |-  ( a = b -> suc a = suc b )
3 1 2 eqeq12d 
 |-  ( a = b -> ( ( a +no 1o ) = suc a <-> ( b +no 1o ) = suc b ) )
4 oveq1 
 |-  ( a = A -> ( a +no 1o ) = ( A +no 1o ) )
5 suceq 
 |-  ( a = A -> suc a = suc A )
6 4 5 eqeq12d 
 |-  ( a = A -> ( ( a +no 1o ) = suc a <-> ( A +no 1o ) = suc A ) )
7 naddrid 
 |-  ( a e. On -> ( a +no (/) ) = a )
8 7 eleq1d 
 |-  ( a e. On -> ( ( a +no (/) ) e. x <-> a e. x ) )
9 8 anbi1d 
 |-  ( a e. On -> ( ( ( a +no (/) ) e. x /\ A. b e. a suc b e. x ) <-> ( a e. x /\ A. b e. a suc b e. x ) ) )
10 9 ad2antrr 
 |-  ( ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) /\ x e. On ) -> ( ( ( a +no (/) ) e. x /\ A. b e. a suc b e. x ) <-> ( a e. x /\ A. b e. a suc b e. x ) ) )
11 df1o2 
 |-  1o = { (/) }
12 11 raleqi 
 |-  ( A. y e. 1o ( a +no y ) e. x <-> A. y e. { (/) } ( a +no y ) e. x )
13 0ex 
 |-  (/) e. _V
14 oveq2 
 |-  ( y = (/) -> ( a +no y ) = ( a +no (/) ) )
15 14 eleq1d 
 |-  ( y = (/) -> ( ( a +no y ) e. x <-> ( a +no (/) ) e. x ) )
16 13 15 ralsn 
 |-  ( A. y e. { (/) } ( a +no y ) e. x <-> ( a +no (/) ) e. x )
17 12 16 bitri 
 |-  ( A. y e. 1o ( a +no y ) e. x <-> ( a +no (/) ) e. x )
18 17 a1i 
 |-  ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) -> ( A. y e. 1o ( a +no y ) e. x <-> ( a +no (/) ) e. x ) )
19 oveq1 
 |-  ( y = b -> ( y +no 1o ) = ( b +no 1o ) )
20 19 eleq1d 
 |-  ( y = b -> ( ( y +no 1o ) e. x <-> ( b +no 1o ) e. x ) )
21 20 cbvralvw 
 |-  ( A. y e. a ( y +no 1o ) e. x <-> A. b e. a ( b +no 1o ) e. x )
22 nfv 
 |-  F/ b a e. On
23 nfra1 
 |-  F/ b A. b e. a ( b +no 1o ) = suc b
24 22 23 nfan 
 |-  F/ b ( a e. On /\ A. b e. a ( b +no 1o ) = suc b )
25 simpr 
 |-  ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) -> A. b e. a ( b +no 1o ) = suc b )
26 25 r19.21bi 
 |-  ( ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) /\ b e. a ) -> ( b +no 1o ) = suc b )
27 26 eleq1d 
 |-  ( ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) /\ b e. a ) -> ( ( b +no 1o ) e. x <-> suc b e. x ) )
28 24 27 ralbida 
 |-  ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) -> ( A. b e. a ( b +no 1o ) e. x <-> A. b e. a suc b e. x ) )
29 21 28 bitrid 
 |-  ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) -> ( A. y e. a ( y +no 1o ) e. x <-> A. b e. a suc b e. x ) )
30 18 29 anbi12d 
 |-  ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) -> ( ( A. y e. 1o ( a +no y ) e. x /\ A. y e. a ( y +no 1o ) e. x ) <-> ( ( a +no (/) ) e. x /\ A. b e. a suc b e. x ) ) )
31 30 adantr 
 |-  ( ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) /\ x e. On ) -> ( ( A. y e. 1o ( a +no y ) e. x /\ A. y e. a ( y +no 1o ) e. x ) <-> ( ( a +no (/) ) e. x /\ A. b e. a suc b e. x ) ) )
32 onelon 
 |-  ( ( a e. On /\ b e. a ) -> b e. On )
33 32 ad4ant13 
 |-  ( ( ( ( a e. On /\ x e. On ) /\ b e. a ) /\ a e. x ) -> b e. On )
34 onsuc 
 |-  ( b e. On -> suc b e. On )
35 33 34 syl 
 |-  ( ( ( ( a e. On /\ x e. On ) /\ b e. a ) /\ a e. x ) -> suc b e. On )
36 simpllr 
 |-  ( ( ( ( a e. On /\ x e. On ) /\ b e. a ) /\ a e. x ) -> x e. On )
37 35 36 jca 
 |-  ( ( ( ( a e. On /\ x e. On ) /\ b e. a ) /\ a e. x ) -> ( suc b e. On /\ x e. On ) )
38 eloni 
 |-  ( a e. On -> Ord a )
39 38 ad3antrrr 
 |-  ( ( ( ( a e. On /\ x e. On ) /\ b e. a ) /\ a e. x ) -> Ord a )
40 simplr 
 |-  ( ( ( ( a e. On /\ x e. On ) /\ b e. a ) /\ a e. x ) -> b e. a )
41 ordsucss 
 |-  ( Ord a -> ( b e. a -> suc b C_ a ) )
42 39 40 41 sylc 
 |-  ( ( ( ( a e. On /\ x e. On ) /\ b e. a ) /\ a e. x ) -> suc b C_ a )
43 simpr 
 |-  ( ( ( ( a e. On /\ x e. On ) /\ b e. a ) /\ a e. x ) -> a e. x )
44 42 43 jca 
 |-  ( ( ( ( a e. On /\ x e. On ) /\ b e. a ) /\ a e. x ) -> ( suc b C_ a /\ a e. x ) )
45 ontr2 
 |-  ( ( suc b e. On /\ x e. On ) -> ( ( suc b C_ a /\ a e. x ) -> suc b e. x ) )
46 37 44 45 sylc 
 |-  ( ( ( ( a e. On /\ x e. On ) /\ b e. a ) /\ a e. x ) -> suc b e. x )
47 46 ex 
 |-  ( ( ( a e. On /\ x e. On ) /\ b e. a ) -> ( a e. x -> suc b e. x ) )
48 47 ralrimdva 
 |-  ( ( a e. On /\ x e. On ) -> ( a e. x -> A. b e. a suc b e. x ) )
49 48 pm4.71d 
 |-  ( ( a e. On /\ x e. On ) -> ( a e. x <-> ( a e. x /\ A. b e. a suc b e. x ) ) )
50 49 adantlr 
 |-  ( ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) /\ x e. On ) -> ( a e. x <-> ( a e. x /\ A. b e. a suc b e. x ) ) )
51 10 31 50 3bitr4d 
 |-  ( ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) /\ x e. On ) -> ( ( A. y e. 1o ( a +no y ) e. x /\ A. y e. a ( y +no 1o ) e. x ) <-> a e. x ) )
52 51 rabbidva 
 |-  ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) -> { x e. On | ( A. y e. 1o ( a +no y ) e. x /\ A. y e. a ( y +no 1o ) e. x ) } = { x e. On | a e. x } )
53 52 inteqd 
 |-  ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) -> |^| { x e. On | ( A. y e. 1o ( a +no y ) e. x /\ A. y e. a ( y +no 1o ) e. x ) } = |^| { x e. On | a e. x } )
54 1on 
 |-  1o e. On
55 naddov2 
 |-  ( ( a e. On /\ 1o e. On ) -> ( a +no 1o ) = |^| { x e. On | ( A. y e. 1o ( a +no y ) e. x /\ A. y e. a ( y +no 1o ) e. x ) } )
56 54 55 mpan2 
 |-  ( a e. On -> ( a +no 1o ) = |^| { x e. On | ( A. y e. 1o ( a +no y ) e. x /\ A. y e. a ( y +no 1o ) e. x ) } )
57 56 adantr 
 |-  ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) -> ( a +no 1o ) = |^| { x e. On | ( A. y e. 1o ( a +no y ) e. x /\ A. y e. a ( y +no 1o ) e. x ) } )
58 onsucmin 
 |-  ( a e. On -> suc a = |^| { x e. On | a e. x } )
59 58 adantr 
 |-  ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) -> suc a = |^| { x e. On | a e. x } )
60 53 57 59 3eqtr4d 
 |-  ( ( a e. On /\ A. b e. a ( b +no 1o ) = suc b ) -> ( a +no 1o ) = suc a )
61 60 ex 
 |-  ( a e. On -> ( A. b e. a ( b +no 1o ) = suc b -> ( a +no 1o ) = suc a ) )
62 3 6 61 tfis3 
 |-  ( A e. On -> ( A +no 1o ) = suc A )