Metamath Proof Explorer

Theorem naddcom

Description: Natural addition is commutative. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Assertion naddcom ⊢ A ∈ On ∧ B ∈ On → A + B = B + A

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ a = c → a + b = c + b
2 oveq2 ⊢ a = c → b + a = b + c
3 1 2 eqeq12d ⊢ a = c → a + b = b + a ↔ c + b = b + c
4 oveq2 ⊢ b = d → c + b = c + d
5 oveq1 ⊢ b = d → b + c = d + c
6 4 5 eqeq12d ⊢ b = d → c + b = b + c ↔ c + d = d + c
7 oveq1 ⊢ a = c → a + d = c + d
8 oveq2 ⊢ a = c → d + a = d + c
9 7 8 eqeq12d ⊢ a = c → a + d = d + a ↔ c + d = d + c
10 oveq1 ⊢ a = A → a + b = A + b
11 oveq2 ⊢ a = A → b + a = b + A
12 10 11 eqeq12d ⊢ a = A → a + b = b + a ↔ A + b = b + A
13 oveq2 ⊢ b = B → A + b = A + B
14 oveq1 ⊢ b = B → b + A = B + A
15 13 14 eqeq12d ⊢ b = B → A + b = b + A ↔ A + B = B + A
16 eleq1 ⊢ a + d = d + a → a + d ∈ x ↔ d + a ∈ x
17 16 ralimi ⊢ ∀ d ∈ b a + d = d + a → ∀ d ∈ b a + d ∈ x ↔ d + a ∈ x
18 ralbi ⊢ ∀ d ∈ b a + d ∈ x ↔ d + a ∈ x → ∀ d ∈ b a + d ∈ x ↔ ∀ d ∈ b d + a ∈ x
19 17 18 syl ⊢ ∀ d ∈ b a + d = d + a → ∀ d ∈ b a + d ∈ x ↔ ∀ d ∈ b d + a ∈ x
20 19 3ad2ant3 ⊢ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → ∀ d ∈ b a + d ∈ x ↔ ∀ d ∈ b d + a ∈ x
21 20 adantl ⊢ a ∈ On ∧ b ∈ On ∧ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → ∀ d ∈ b a + d ∈ x ↔ ∀ d ∈ b d + a ∈ x
22 eleq1 ⊢ c + b = b + c → c + b ∈ x ↔ b + c ∈ x
23 22 ralimi ⊢ ∀ c ∈ a c + b = b + c → ∀ c ∈ a c + b ∈ x ↔ b + c ∈ x
24 ralbi ⊢ ∀ c ∈ a c + b ∈ x ↔ b + c ∈ x → ∀ c ∈ a c + b ∈ x ↔ ∀ c ∈ a b + c ∈ x
25 23 24 syl ⊢ ∀ c ∈ a c + b = b + c → ∀ c ∈ a c + b ∈ x ↔ ∀ c ∈ a b + c ∈ x
26 25 3ad2ant2 ⊢ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → ∀ c ∈ a c + b ∈ x ↔ ∀ c ∈ a b + c ∈ x
27 26 adantl ⊢ a ∈ On ∧ b ∈ On ∧ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → ∀ c ∈ a c + b ∈ x ↔ ∀ c ∈ a b + c ∈ x
28 21 27 anbi12d ⊢ a ∈ On ∧ b ∈ On ∧ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → ∀ d ∈ b a + d ∈ x ∧ ∀ c ∈ a c + b ∈ x ↔ ∀ d ∈ b d + a ∈ x ∧ ∀ c ∈ a b + c ∈ x
29 28 biancomd ⊢ a ∈ On ∧ b ∈ On ∧ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → ∀ d ∈ b a + d ∈ x ∧ ∀ c ∈ a c + b ∈ x ↔ ∀ c ∈ a b + c ∈ x ∧ ∀ d ∈ b d + a ∈ x
30 29 rabbidv ⊢ a ∈ On ∧ b ∈ On ∧ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → x ∈ On | ∀ d ∈ b a + d ∈ x ∧ ∀ c ∈ a c + b ∈ x = x ∈ On | ∀ c ∈ a b + c ∈ x ∧ ∀ d ∈ b d + a ∈ x
31 30 inteqd ⊢ a ∈ On ∧ b ∈ On ∧ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → ⋂ x ∈ On | ∀ d ∈ b a + d ∈ x ∧ ∀ c ∈ a c + b ∈ x = ⋂ x ∈ On | ∀ c ∈ a b + c ∈ x ∧ ∀ d ∈ b d + a ∈ x
32 naddov2 ⊢ a ∈ On ∧ b ∈ On → a + b = ⋂ x ∈ On | ∀ d ∈ b a + d ∈ x ∧ ∀ c ∈ a c + b ∈ x
33 32 adantr ⊢ a ∈ On ∧ b ∈ On ∧ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → a + b = ⋂ x ∈ On | ∀ d ∈ b a + d ∈ x ∧ ∀ c ∈ a c + b ∈ x
34 naddov2 ⊢ b ∈ On ∧ a ∈ On → b + a = ⋂ x ∈ On | ∀ c ∈ a b + c ∈ x ∧ ∀ d ∈ b d + a ∈ x
35 34 ancoms ⊢ a ∈ On ∧ b ∈ On → b + a = ⋂ x ∈ On | ∀ c ∈ a b + c ∈ x ∧ ∀ d ∈ b d + a ∈ x
36 35 adantr ⊢ a ∈ On ∧ b ∈ On ∧ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → b + a = ⋂ x ∈ On | ∀ c ∈ a b + c ∈ x ∧ ∀ d ∈ b d + a ∈ x
37 31 33 36 3eqtr4d ⊢ a ∈ On ∧ b ∈ On ∧ ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → a + b = b + a
38 37 ex ⊢ a ∈ On ∧ b ∈ On → ∀ c ∈ a ∀ d ∈ b c + d = d + c ∧ ∀ c ∈ a c + b = b + c ∧ ∀ d ∈ b a + d = d + a → a + b = b + a
39 3 6 9 12 15 38 on2ind ⊢ A ∈ On ∧ B ∈ On → A + B = B + A