naddass

Description: Natural ordinal addition is associative. (Contributed by Scott Fenton, 20-Jan-2025)

		Ref	Expression
	Assertion	naddass	$⊢ (A \in On \land B \in On \land C \in On) \to (A + B) + C = A + (B + C)$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ a = x \to a + b = x + b$
2	1	oveq1d	$⊢ a = x \to (a + b) + c = (x + b) + c$
3		oveq1	$⊢ a = x \to a + (b + c) = x + (b + c)$
4	2 3	eqeq12d	$⊢ a = x \to ((a + b) + c = a + (b + c) \leftrightarrow (x + b) + c = x + (b + c))$
5		oveq2	$⊢ b = y \to x + b = x + y$
6	5	oveq1d	$⊢ b = y \to (x + b) + c = (x + y) + c$
7		oveq1	$⊢ b = y \to b + c = y + c$
8	7	oveq2d	$⊢ b = y \to x + (b + c) = x + (y + c)$
9	6 8	eqeq12d	$⊢ b = y \to ((x + b) + c = x + (b + c) \leftrightarrow (x + y) + c = x + (y + c))$
10		oveq2	$⊢ c = z \to (x + y) + c = (x + y) + z$
11		oveq2	$⊢ c = z \to y + c = y + z$
12	11	oveq2d	$⊢ c = z \to x + (y + c) = x + (y + z)$
13	10 12	eqeq12d	$⊢ c = z \to ((x + y) + c = x + (y + c) \leftrightarrow (x + y) + z = x + (y + z))$
14		oveq1	$⊢ a = x \to a + y = x + y$
15	14	oveq1d	$⊢ a = x \to (a + y) + z = (x + y) + z$
16		oveq1	$⊢ a = x \to a + (y + z) = x + (y + z)$
17	15 16	eqeq12d	$⊢ a = x \to ((a + y) + z = a + (y + z) \leftrightarrow (x + y) + z = x + (y + z))$
18		oveq2	$⊢ b = y \to a + b = a + y$
19	18	oveq1d	$⊢ b = y \to (a + b) + z = (a + y) + z$
20		oveq1	$⊢ b = y \to b + z = y + z$
21	20	oveq2d	$⊢ b = y \to a + (b + z) = a + (y + z)$
22	19 21	eqeq12d	$⊢ b = y \to ((a + b) + z = a + (b + z) \leftrightarrow (a + y) + z = a + (y + z))$
23	5	oveq1d	$⊢ b = y \to (x + b) + z = (x + y) + z$
24	20	oveq2d	$⊢ b = y \to x + (b + z) = x + (y + z)$
25	23 24	eqeq12d	$⊢ b = y \to ((x + b) + z = x + (b + z) \leftrightarrow (x + y) + z = x + (y + z))$
26		oveq2	$⊢ c = z \to (a + y) + c = (a + y) + z$
27	11	oveq2d	$⊢ c = z \to a + (y + c) = a + (y + z)$
28	26 27	eqeq12d	$⊢ c = z \to ((a + y) + c = a + (y + c) \leftrightarrow (a + y) + z = a + (y + z))$
29		oveq1	$⊢ a = A \to a + b = A + b$
30	29	oveq1d	$⊢ a = A \to (a + b) + c = (A + b) + c$
31		oveq1	$⊢ a = A \to a + (b + c) = A + (b + c)$
32	30 31	eqeq12d	$⊢ a = A \to ((a + b) + c = a + (b + c) \leftrightarrow (A + b) + c = A + (b + c))$
33		oveq2	$⊢ b = B \to A + b = A + B$
34	33	oveq1d	$⊢ b = B \to (A + b) + c = (A + B) + c$
35		oveq1	$⊢ b = B \to b + c = B + c$
36	35	oveq2d	$⊢ b = B \to A + (b + c) = A + (B + c)$
37	34 36	eqeq12d	$⊢ b = B \to ((A + b) + c = A + (b + c) \leftrightarrow (A + B) + c = A + (B + c))$
38		oveq2	$⊢ c = C \to (A + B) + c = (A + B) + C$
39		oveq2	$⊢ c = C \to B + c = B + C$
40	39	oveq2d	$⊢ c = C \to A + (B + c) = A + (B + C)$
41	38 40	eqeq12d	$⊢ c = C \to ((A + B) + c = A + (B + c) \leftrightarrow (A + B) + C = A + (B + C))$
42		simpr21	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to \forall x \in a (x + b) + c = x + (b + c)$
43		eleq1	$⊢ (x + b) + c = x + (b + c) \to ((x + b) + c \in w \leftrightarrow x + (b + c) \in w)$
44	43	ralimi	$⊢ \forall x \in a (x + b) + c = x + (b + c) \to \forall x \in a ((x + b) + c \in w \leftrightarrow x + (b + c) \in w)$
45		ralbi	$⊢ \forall x \in a ((x + b) + c \in w \leftrightarrow x + (b + c) \in w) \to (\forall x \in a (x + b) + c \in w \leftrightarrow \forall x \in a x + (b + c) \in w)$
46	42 44 45	3syl	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to (\forall x \in a (x + b) + c \in w \leftrightarrow \forall x \in a x + (b + c) \in w)$
47		simpr23	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to \forall y \in b (a + y) + c = a + (y + c)$
48		eleq1	$⊢ (a + y) + c = a + (y + c) \to ((a + y) + c \in w \leftrightarrow a + (y + c) \in w)$
49	48	ralimi	$⊢ \forall y \in b (a + y) + c = a + (y + c) \to \forall y \in b ((a + y) + c \in w \leftrightarrow a + (y + c) \in w)$
50		ralbi	$⊢ \forall y \in b ((a + y) + c \in w \leftrightarrow a + (y + c) \in w) \to (\forall y \in b (a + y) + c \in w \leftrightarrow \forall y \in b a + (y + c) \in w)$
51	47 49 50	3syl	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to (\forall y \in b (a + y) + c \in w \leftrightarrow \forall y \in b a + (y + c) \in w)$
52		simpr3	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to \forall z \in c (a + b) + z = a + (b + z)$
53		eleq1	$⊢ (a + b) + z = a + (b + z) \to ((a + b) + z \in w \leftrightarrow a + (b + z) \in w)$
54	53	ralimi	$⊢ \forall z \in c (a + b) + z = a + (b + z) \to \forall z \in c ((a + b) + z \in w \leftrightarrow a + (b + z) \in w)$
55		ralbi	$⊢ \forall z \in c ((a + b) + z \in w \leftrightarrow a + (b + z) \in w) \to (\forall z \in c (a + b) + z \in w \leftrightarrow \forall z \in c a + (b + z) \in w)$
56	52 54 55	3syl	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to (\forall z \in c (a + b) + z \in w \leftrightarrow \forall z \in c a + (b + z) \in w)$
57	46 51 56	3anbi123d	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to ((\forall x \in a (x + b) + c \in w \land \forall y \in b (a + y) + c \in w \land \forall z \in c (a + b) + z \in w) \leftrightarrow (\forall x \in a x + (b + c) \in w \land \forall y \in b a + (y + c) \in w \land \forall z \in c a + (b + z) \in w))$
58	57	rabbidv	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to \{w \in On \| (\forall x \in a (x + b) + c \in w \land \forall y \in b (a + y) + c \in w \land \forall z \in c (a + b) + z \in w)\} = \{w \in On \| (\forall x \in a x + (b + c) \in w \land \forall y \in b a + (y + c) \in w \land \forall z \in c a + (b + z) \in w)\}$
59	58	inteqd	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to ⋂ \{w \in On \| (\forall x \in a (x + b) + c \in w \land \forall y \in b (a + y) + c \in w \land \forall z \in c (a + b) + z \in w)\} = ⋂ \{w \in On \| (\forall x \in a x + (b + c) \in w \land \forall y \in b a + (y + c) \in w \land \forall z \in c a + (b + z) \in w)\}$
60		naddasslem1	$⊢ (a \in On \land b \in On \land c \in On) \to (a + b) + c = ⋂ \{w \in On \| (\forall x \in a (x + b) + c \in w \land \forall y \in b (a + y) + c \in w \land \forall z \in c (a + b) + z \in w)\}$
61	60	adantr	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to (a + b) + c = ⋂ \{w \in On \| (\forall x \in a (x + b) + c \in w \land \forall y \in b (a + y) + c \in w \land \forall z \in c (a + b) + z \in w)\}$
62		naddasslem2	$⊢ (a \in On \land b \in On \land c \in On) \to a + (b + c) = ⋂ \{w \in On \| (\forall x \in a x + (b + c) \in w \land \forall y \in b a + (y + c) \in w \land \forall z \in c a + (b + z) \in w)\}$
63	62	adantr	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to a + (b + c) = ⋂ \{w \in On \| (\forall x \in a x + (b + c) \in w \land \forall y \in b a + (y + c) \in w \land \forall z \in c a + (b + z) \in w)\}$
64	59 61 63	3eqtr4d	$⊢ ((a \in On \land b \in On \land c \in On) \land ((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z))) \to (a + b) + c = a + (b + c)$
65	64	ex	$⊢ (a \in On \land b \in On \land c \in On) \to (((\forall x \in a \forall y \in b \forall z \in c (x + y) + z = x + (y + z) \land \forall x \in a \forall y \in b (x + y) + c = x + (y + c) \land \forall x \in a \forall z \in c (x + b) + z = x + (b + z)) \land (\forall x \in a (x + b) + c = x + (b + c) \land \forall y \in b \forall z \in c (a + y) + z = a + (y + z) \land \forall y \in b (a + y) + c = a + (y + c)) \land \forall z \in c (a + b) + z = a + (b + z)) \to (a + b) + c = a + (b + c))$
66	4 9 13 17 22 25 28 32 37 41 65	on3ind	$⊢ (A \in On \land B \in On \land C \in On) \to (A + B) + C = A + (B + C)$

Metamath Proof Explorer

Theorem naddass

Proof