Metamath Proof Explorer

Theorem naddsuc2

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

Ref Expression
Assertion naddsuc2 ⊢ A ∈ On ∧ B ∈ On → A + suc ⁡ B = suc ⁡ A + B

Proof

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