Theorem naddcom

Description: Natural addition is commutative. (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 𝐴 ) )