Metamath Proof Explorer

Theorem naddsuc2

Description: Natural addition with successor. (Contributed by RP, 1-Jan-2025)

Ref Expression
Assertion naddsuc2 
|- ( ( A e. On /\ B e. On ) -> ( A +no suc B ) = suc ( A +no B ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = c -> ( a +no suc b ) = ( c +no suc b ) )
2 oveq1 
 |-  ( a = c -> ( a +no b ) = ( c +no b ) )
3 suceq 
 |-  ( ( a +no b ) = ( c +no b ) -> suc ( a +no b ) = suc ( c +no b ) )
4 2 3 syl 
 |-  ( a = c -> suc ( a +no b ) = suc ( c +no b ) )
5 1 4 eqeq12d 
 |-  ( a = c -> ( ( a +no suc b ) = suc ( a +no b ) <-> ( c +no suc b ) = suc ( c +no b ) ) )
6 suceq 
 |-  ( b = d -> suc b = suc d )
7 6 oveq2d 
 |-  ( b = d -> ( c +no suc b ) = ( c +no suc d ) )
8 oveq2 
 |-  ( b = d -> ( c +no b ) = ( c +no d ) )
9 suceq 
 |-  ( ( c +no b ) = ( c +no d ) -> suc ( c +no b ) = suc ( c +no d ) )
10 8 9 syl 
 |-  ( b = d -> suc ( c +no b ) = suc ( c +no d ) )
11 7 10 eqeq12d 
 |-  ( b = d -> ( ( c +no suc b ) = suc ( c +no b ) <-> ( c +no suc d ) = suc ( c +no d ) ) )
12 oveq1 
 |-  ( a = c -> ( a +no suc d ) = ( c +no suc d ) )
13 oveq1 
 |-  ( a = c -> ( a +no d ) = ( c +no d ) )
14 suceq 
 |-  ( ( a +no d ) = ( c +no d ) -> suc ( a +no d ) = suc ( c +no d ) )
15 13 14 syl 
 |-  ( a = c -> suc ( a +no d ) = suc ( c +no d ) )
16 12 15 eqeq12d 
 |-  ( a = c -> ( ( a +no suc d ) = suc ( a +no d ) <-> ( c +no suc d ) = suc ( c +no d ) ) )
17 oveq1 
 |-  ( a = A -> ( a +no suc b ) = ( A +no suc b ) )
18 oveq1 
 |-  ( a = A -> ( a +no b ) = ( A +no b ) )
19 suceq 
 |-  ( ( a +no b ) = ( A +no b ) -> suc ( a +no b ) = suc ( A +no b ) )
20 18 19 syl 
 |-  ( a = A -> suc ( a +no b ) = suc ( A +no b ) )
21 17 20 eqeq12d 
 |-  ( a = A -> ( ( a +no suc b ) = suc ( a +no b ) <-> ( A +no suc b ) = suc ( A +no b ) ) )
22 suceq 
 |-  ( b = B -> suc b = suc B )
23 22 oveq2d 
 |-  ( b = B -> ( A +no suc b ) = ( A +no suc B ) )
24 oveq2 
 |-  ( b = B -> ( A +no b ) = ( A +no B ) )
25 suceq 
 |-  ( ( A +no b ) = ( A +no B ) -> suc ( A +no b ) = suc ( A +no B ) )
26 24 25 syl 
 |-  ( b = B -> suc ( A +no b ) = suc ( A +no B ) )
27 23 26 eqeq12d 
 |-  ( b = B -> ( ( A +no suc b ) = suc ( A +no b ) <-> ( A +no suc B ) = suc ( A +no B ) ) )
28 simp2 
 |-  ( ( A. c e. a A. d e. b ( c +no suc d ) = suc ( c +no d ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) /\ A. d e. b ( a +no suc d ) = suc ( a +no d ) ) -> A. c e. a ( c +no suc b ) = suc ( c +no b ) )
29 28 a1i 
 |-  ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +no suc d ) = suc ( c +no d ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) /\ A. d e. b ( a +no suc d ) = suc ( a +no d ) ) -> A. c e. a ( c +no suc b ) = suc ( c +no b ) ) )
30 df-suc 
 |-  suc b = ( b u. { b } )
31 30 a1i 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> suc b = ( b u. { b } ) )
32 31 raleqdv 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. suc b ( a +no d ) e. x <-> A. d e. ( b u. { b } ) ( a +no d ) e. x ) )
33 vex 
 |-  b e. _V
34 33 a1i 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> b e. _V )
35 oveq2 
 |-  ( d = b -> ( a +no d ) = ( a +no b ) )
36 35 eleq1d 
 |-  ( d = b -> ( ( a +no d ) e. x <-> ( a +no b ) e. x ) )
37 36 ralunsn 
 |-  ( b e. _V -> ( A. d e. ( b u. { b } ) ( a +no d ) e. x <-> ( A. d e. b ( a +no d ) e. x /\ ( a +no b ) e. x ) ) )
38 34 37 syl 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. ( b u. { b } ) ( a +no d ) e. x <-> ( A. d e. b ( a +no d ) e. x /\ ( a +no b ) e. x ) ) )
39 38 biancomd 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. ( b u. { b } ) ( a +no d ) e. x <-> ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) ) )
40 32 39 bitrd 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. suc b ( a +no d ) e. x <-> ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) ) )
41 nfv 
 |-  F/ c ( a e. On /\ b e. On )
42 nfra1 
 |-  F/ c A. c e. a ( c +no suc b ) = suc ( c +no b )
43 41 42 nfan 
 |-  F/ c ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) )
44 nfv 
 |-  F/ c x e. On
45 43 44 nfan 
 |-  F/ c ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On )
46 simplr 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> A. c e. a ( c +no suc b ) = suc ( c +no b ) )
47 46 r19.21bi 
 |-  ( ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) /\ c e. a ) -> ( c +no suc b ) = suc ( c +no b ) )
48 47 eleq1d 
 |-  ( ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) /\ c e. a ) -> ( ( c +no suc b ) e. x <-> suc ( c +no b ) e. x ) )
49 45 48 ralbida 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. c e. a ( c +no suc b ) e. x <-> A. c e. a suc ( c +no b ) e. x ) )
50 40 49 anbi12d 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) <-> ( ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) /\ A. c e. a suc ( c +no b ) e. x ) ) )
51 anass 
 |-  ( ( ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) /\ A. c e. a suc ( c +no b ) e. x ) <-> ( ( a +no b ) e. x /\ ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) )
52 simpll3 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> x e. On )
53 simpr 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> d e. b )
54 simpll2 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> b e. On )
55 onelon 
 |-  ( ( b e. On /\ d e. b ) -> d e. On )
56 54 53 55 syl2anc 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> d e. On )
57 simpll1 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> a e. On )
58 naddel2 
 |-  ( ( d e. On /\ b e. On /\ a e. On ) -> ( d e. b <-> ( a +no d ) e. ( a +no b ) ) )
59 56 54 57 58 syl3anc 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( d e. b <-> ( a +no d ) e. ( a +no b ) ) )
60 53 59 mpbid 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( a +no d ) e. ( a +no b ) )
61 simplr 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( a +no b ) e. x )
62 60 61 jca 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( ( a +no d ) e. ( a +no b ) /\ ( a +no b ) e. x ) )
63 ontr1 
 |-  ( x e. On -> ( ( ( a +no d ) e. ( a +no b ) /\ ( a +no b ) e. x ) -> ( a +no d ) e. x ) )
64 52 62 63 sylc 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( a +no d ) e. x )
65 64 ralrimiva 
 |-  ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) -> A. d e. b ( a +no d ) e. x )
66 simpll1 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> a e. On )
67 simpr 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> c e. a )
68 onelon 
 |-  ( ( a e. On /\ c e. a ) -> c e. On )
69 66 67 68 syl2anc 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> c e. On )
70 simpll2 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> b e. On )
71 69 66 70 3jca 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( c e. On /\ a e. On /\ b e. On ) )
72 naddelim 
 |-  ( ( c e. On /\ a e. On /\ b e. On ) -> ( c e. a -> ( c +no b ) e. ( a +no b ) ) )
73 71 67 72 sylc 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( c +no b ) e. ( a +no b ) )
74 simplr 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( a +no b ) e. x )
75 elunii 
 |-  ( ( ( c +no b ) e. ( a +no b ) /\ ( a +no b ) e. x ) -> ( c +no b ) e. U. x )
76 73 74 75 syl2anc 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( c +no b ) e. U. x )
77 simpll3 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> x e. On )
78 eloni 
 |-  ( x e. On -> Ord x )
79 77 78 syl 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> Ord x )
80 ordsucuniel 
 |-  ( Ord x -> ( ( c +no b ) e. U. x <-> suc ( c +no b ) e. x ) )
81 79 80 syl 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( ( c +no b ) e. U. x <-> suc ( c +no b ) e. x ) )
82 76 81 mpbid 
 |-  ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> suc ( c +no b ) e. x )
83 82 ralrimiva 
 |-  ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) -> A. c e. a suc ( c +no b ) e. x )
84 65 83 jca 
 |-  ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) -> ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) )
85 84 ex 
 |-  ( ( a e. On /\ b e. On /\ x e. On ) -> ( ( a +no b ) e. x -> ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) )
86 85 ad4ant124 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( a +no b ) e. x -> ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) )
87 86 pm4.71d 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( a +no b ) e. x <-> ( ( a +no b ) e. x /\ ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) ) )
88 51 87 bitr4id 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) /\ A. c e. a suc ( c +no b ) e. x ) <-> ( a +no b ) e. x ) )
89 50 88 bitrd 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) <-> ( a +no b ) e. x ) )
90 89 rabbidva 
 |-  ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } = { x e. On | ( a +no b ) e. x } )
91 90 inteqd 
 |-  ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } = |^| { x e. On | ( a +no b ) e. x } )
92 onsuc 
 |-  ( b e. On -> suc b e. On )
93 naddov2 
 |-  ( ( a e. On /\ suc b e. On ) -> ( a +no suc b ) = |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } )
94 92 93 sylan2 
 |-  ( ( a e. On /\ b e. On ) -> ( a +no suc b ) = |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } )
95 94 adantr 
 |-  ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> ( a +no suc b ) = |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } )
96 naddcl 
 |-  ( ( a e. On /\ b e. On ) -> ( a +no b ) e. On )
97 onsucmin 
 |-  ( ( a +no b ) e. On -> suc ( a +no b ) = |^| { x e. On | ( a +no b ) e. x } )
98 96 97 syl 
 |-  ( ( a e. On /\ b e. On ) -> suc ( a +no b ) = |^| { x e. On | ( a +no b ) e. x } )
99 98 adantr 
 |-  ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> suc ( a +no b ) = |^| { x e. On | ( a +no b ) e. x } )
100 91 95 99 3eqtr4d 
 |-  ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> ( a +no suc b ) = suc ( a +no b ) )
101 100 ex 
 |-  ( ( a e. On /\ b e. On ) -> ( A. c e. a ( c +no suc b ) = suc ( c +no b ) -> ( a +no suc b ) = suc ( a +no b ) ) )
102 29 101 syld 
 |-  ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +no suc d ) = suc ( c +no d ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) /\ A. d e. b ( a +no suc d ) = suc ( a +no d ) ) -> ( a +no suc b ) = suc ( a +no b ) ) )
103 5 11 16 21 27 102 on2ind 
 |-  ( ( A e. On /\ B e. On ) -> ( A +no suc B ) = suc ( A +no B ) )