Metamath Proof Explorer


Theorem naddcom

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

Ref Expression
Assertion naddcom ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ( 𝐵 +no 𝐴 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ( 𝑎 = 𝑐 → ( 𝑎 +no 𝑏 ) = ( 𝑐 +no 𝑏 ) )
2 oveq2 ( 𝑎 = 𝑐 → ( 𝑏 +no 𝑎 ) = ( 𝑏 +no 𝑐 ) )
3 1 2 eqeq12d ( 𝑎 = 𝑐 → ( ( 𝑎 +no 𝑏 ) = ( 𝑏 +no 𝑎 ) ↔ ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ) )
4 oveq2 ( 𝑏 = 𝑑 → ( 𝑐 +no 𝑏 ) = ( 𝑐 +no 𝑑 ) )
5 oveq1 ( 𝑏 = 𝑑 → ( 𝑏 +no 𝑐 ) = ( 𝑑 +no 𝑐 ) )
6 4 5 eqeq12d ( 𝑏 = 𝑑 → ( ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ↔ ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ) )
7 oveq1 ( 𝑎 = 𝑐 → ( 𝑎 +no 𝑑 ) = ( 𝑐 +no 𝑑 ) )
8 oveq2 ( 𝑎 = 𝑐 → ( 𝑑 +no 𝑎 ) = ( 𝑑 +no 𝑐 ) )
9 7 8 eqeq12d ( 𝑎 = 𝑐 → ( ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ↔ ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ) )
10 oveq1 ( 𝑎 = 𝐴 → ( 𝑎 +no 𝑏 ) = ( 𝐴 +no 𝑏 ) )
11 oveq2 ( 𝑎 = 𝐴 → ( 𝑏 +no 𝑎 ) = ( 𝑏 +no 𝐴 ) )
12 10 11 eqeq12d ( 𝑎 = 𝐴 → ( ( 𝑎 +no 𝑏 ) = ( 𝑏 +no 𝑎 ) ↔ ( 𝐴 +no 𝑏 ) = ( 𝑏 +no 𝐴 ) ) )
13 oveq2 ( 𝑏 = 𝐵 → ( 𝐴 +no 𝑏 ) = ( 𝐴 +no 𝐵 ) )
14 oveq1 ( 𝑏 = 𝐵 → ( 𝑏 +no 𝐴 ) = ( 𝐵 +no 𝐴 ) )
15 13 14 eqeq12d ( 𝑏 = 𝐵 → ( ( 𝐴 +no 𝑏 ) = ( 𝑏 +no 𝐴 ) ↔ ( 𝐴 +no 𝐵 ) = ( 𝐵 +no 𝐴 ) ) )
16 eleq1 ( ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) → ( ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) )
17 16 ralimi ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) → ∀ 𝑑𝑏 ( ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) )
18 ralbi ( ∀ 𝑑𝑏 ( ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) → ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) )
19 17 18 syl ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) → ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) )
20 19 3ad2ant3 ( ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) → ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) )
21 20 adantl ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) )
22 eleq1 ( ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) → ( ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) )
23 22 ralimi ( ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) → ∀ 𝑐𝑎 ( ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) )
24 ralbi ( ∀ 𝑐𝑎 ( ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) → ( ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) )
25 23 24 syl ( ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) → ( ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) )
26 25 3ad2ant2 ( ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) → ( ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) )
27 26 adantl ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) )
28 21 27 anbi12d ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ↔ ( ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ∧ ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) ) )
29 28 biancomd ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ↔ ( ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) ) )
30 29 rabbidv ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → { 𝑥 ∈ On ∣ ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) } )
31 30 inteqd ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → { 𝑥 ∈ On ∣ ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) } )
32 naddov2 ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑎 +no 𝑏 ) = { 𝑥 ∈ On ∣ ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) } )
33 32 adantr ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( 𝑎 +no 𝑏 ) = { 𝑥 ∈ On ∣ ( ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) } )
34 naddov2 ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( 𝑏 +no 𝑎 ) = { 𝑥 ∈ On ∣ ( ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) } )
35 34 ancoms ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑏 +no 𝑎 ) = { 𝑥 ∈ On ∣ ( ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) } )
36 35 adantr ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( 𝑏 +no 𝑎 ) = { 𝑥 ∈ On ∣ ( ∀ 𝑐𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) } )
37 31 33 36 3eqtr4d ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( 𝑎 +no 𝑏 ) = ( 𝑏 +no 𝑎 ) )
38 37 ex ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐𝑎𝑑𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) → ( 𝑎 +no 𝑏 ) = ( 𝑏 +no 𝑎 ) ) )
39 3 6 9 12 15 38 on2ind ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ( 𝐵 +no 𝐴 ) )