Theorem oaass 3163

Description: Ordinal addition is associative. Theorem 25 of [Suppes] p. 211.

Assertion

Ref	Expression
oaass	|- ((A e. On /\ B e. On /\ C e. On) -> ((A +o B) +o C) = (A +o (B +o C)))

Proof of Theorem oaass

Step	Hyp	Ref	Expression
1		opreq2 3007	. . . . . 6 |- (x = (/) -> ((A +o B) +o x) = ((A +o B) +o (/)))
2		opreq2 3007	. . . . . . 7 |- (x = (/) -> (B +o x) = (B +o (/)))
3	2	opreq2d 3013	. . . . . 6 |- (x = (/) -> (A +o (B +o x)) = (A +o (B +o (/))))
4	1, 3	cleq12d 1115	. . . . 5 |- (x = (/) -> (((A +o B) +o x) = (A +o (B +o x)) <-> ((A +o B) +o (/)) = (A +o (B +o (/)))))
5		opreq2 3007	. . . . . 6 |- (x = y -> ((A +o B) +o x) = ((A +o B) +o y))
6		opreq2 3007	. . . . . . 7 |- (x = y -> (B +o x) = (B +o y))
7	6	opreq2d 3013	. . . . . 6 |- (x = y -> (A +o (B +o x)) = (A +o (B +o y)))
8	5, 7	cleq12d 1115	. . . . 5 |- (x = y -> (((A +o B) +o x) = (A +o (B +o x)) <-> ((A +o B) +o y) = (A +o (B +o y))))
9		opreq2 3007	. . . . . 6 |- (x = suc y -> ((A +o B) +o x) = ((A +o B) +o suc y))
10		opreq2 3007	. . . . . . 7 |- (x = suc y -> (B +o x) = (B +o suc y))
11	10	opreq2d 3013	. . . . . 6 |- (x = suc y -> (A +o (B +o x)) = (A +o (B +o suc y)))
12	9, 11	cleq12d 1115	. . . . 5 |- (x = suc y -> (((A +o B) +o x) = (A +o (B +o x)) <-> ((A +o B) +o suc y) = (A +o (B +o suc y))))
13		opreq2 3007	. . . . . 6 |- (x = C -> ((A +o B) +o x) = ((A +o B) +o C))
14		opreq2 3007	. . . . . . 7 |- (x = C -> (B +o x) = (B +o C))
15	14	opreq2d 3013	. . . . . 6 |- (x = C -> (A +o (B +o x)) = (A +o (B +o C)))
16	13, 15	cleq12d 1115	. . . . 5 |- (x = C -> (((A +o B) +o x) = (A +o (B +o x)) <-> ((A +o B) +o C) = (A +o (B +o C))))
17		oacl 3138	. . . . . . 7 |- ((A e. On /\ B e. On) -> (A +o B) e. On)
18		oa0 3124	. . . . . . 7 |- ((A +o B) e. On -> ((A +o B) +o (/)) = (A +o B))
19	17, 18	syl 12	. . . . . 6 |- ((A e. On /\ B e. On) -> ((A +o B) +o (/)) = (A +o B))
20		oa0 3124	. . . . . . . 8 |- (B e. On -> (B +o (/)) = B)
21	20	opreq2d 3013	. . . . . . 7 |- (B e. On -> (A +o (B +o (/))) = (A +o B))
22	21	adantl 305	. . . . . 6 |- ((A e. On /\ B e. On) -> (A +o (B +o (/))) = (A +o B))
23	19, 22	eqtr4d 1131	. . . . 5 |- ((A e. On /\ B e. On) -> ((A +o B) +o (/)) = (A +o (B +o (/))))
24		oasuc 3131	. . . . . . . . . 10 |- (((A +o B) e. On /\ y e. On) -> ((A +o B) +o suc y) = suc ((A +o B) +o y))
25	24, 17	sylan 343	. . . . . . . . 9 |- (((A e. On /\ B e. On) /\ y e. On) -> ((A +o B) +o suc y) = suc ((A +o B) +o y))
26		oasuc 3131	. . . . . . . . . . . . 13 |- ((B e. On /\ y e. On) -> (B +o suc y) = suc (B +o y))
27	26	opreq2d 3013	. . . . . . . . . . . 12 |- ((B e. On /\ y e. On) -> (A +o (B +o suc y)) = (A +o suc (B +o y)))
28	27	adantl 305	. . . . . . . . . . 11 |- ((A e. On /\ (B e. On /\ y e. On)) -> (A +o (B +o suc y)) = (A +o suc (B +o y)))
29		oasuc 3131	. . . . . . . . . . . 12 |- ((A e. On /\ (B +o y) e. On) -> (A +o suc (B +o y)) = suc (A +o (B +o y)))
30		oacl 3138	. . . . . . . . . . . 12 |- ((B e. On /\ y e. On) -> (B +o y) e. On)
31	29, 30	sylan2 346	. . . . . . . . . . 11 |- ((A e. On /\ (B e. On /\ y e. On)) -> (A +o suc (B +o y)) = suc (A +o (B +o y)))
32	28, 31	eqtrd 1128	. . . . . . . . . 10 |- ((A e. On /\ (B e. On /\ y e. On)) -> (A +o (B +o suc y)) = suc (A +o (B +o y)))
33	32	anassrs 338	. . . . . . . . 9 |- (((A e. On /\ B e. On) /\ y e. On) -> (A +o (B +o suc y)) = suc (A +o (B +o y)))
34	25, 33	cleq12d 1115	. . . . . . . 8 |- (((A e. On /\ B e. On) /\ y e. On) -> (((A +o B) +o suc y) = (A +o (B +o suc y)) <-> suc ((A +o B) +o y) = suc (A +o (B +o y))))
35		suceq 2288	. . . . . . . 8 |- (((A +o B) +o y) = (A +o (B +o y)) -> suc ((A +o B) +o y) = suc (A +o (B +o y)))
36	34, 35	syl5bir 184	. . . . . . 7 |- (((A e. On /\ B e. On) /\ y e. On) -> (((A +o B) +o y) = (A +o (B +o y)) -> ((A +o B) +o suc y) = (A +o (B +o suc y))))
37	36	exp 291	. . . . . 6 |- ((A e. On /\ B e. On) -> (y e. On -> (((A +o B) +o y) = (A +o (B +o y)) -> ((A +o B) +o suc y) = (A +o (B +o suc y)))))
38	37	com12 13	. . . . 5 |- (y e. On -> ((A e. On /\ B e. On) -> (((A +o B) +o y) = (A +o (B +o y)) -> ((A +o B) +o suc y) = (A +o (B +o suc y)))))
39		iuneq2 2006	. . . . . . . 8 |- (A.y e. x ((A +o B) +o y) = (A +o (B +o y)) -> U.y e. x ((A +o B) +o y) = U.y e. x (A +o (B +o y)))
40	39	adantl 305	. . . . . . 7 |- (((Lim x /\ (A e. On /\ B e. On)) /\ A.y e. x ((A +o B) +o y) = (A +o (B +o y))) -> U.y e. x ((A +o B) +o y) = U.y e. x (A +o (B +o y)))
41		visset 1350	. . . . . . . . . . 11 |- x e. V
42		oalim 3135	. . . . . . . . . . 11 |- (((A +o B) e. On /\ (x e. V /\ Lim x)) -> ((A +o B) +o x) = U.y e. x ((A +o B) +o y))
43	41, 42	mpan21 531	. . . . . . . . . 10 |- (((A +o B) e. On /\ Lim x) -> ((A +o B) +o x) = U.y e. x ((A +o B) +o y))
44	43, 17	sylan 343	. . . . . . . . 9 |- (((A e. On /\ B e. On) /\ Lim x) -> ((A +o B) +o x) = U.y e. x ((A +o B) +o y))
45	44	ancoms 334	. . . . . . . 8 |- ((Lim x /\ (A e. On /\ B e. On)) -> ((A +o B) +o x) = U.y e. x ((A +o B) +o y))
46	45	adantr 306	. . . . . . 7 |- (((Lim x /\ (A e. On /\ B e. On)) /\ A.y e. x ((A +o B) +o y) = (A +o (B +o y))) -> ((A +o B) +o x) = U.y e. x ((A +o B) +o y))
47		oprex 3018	. . . . . . . . . . . 12 |- (B +o x) e. V
48		oalim 3135	. . . . . . . . . . . 12 |- ((A e. On /\ ((B +o x) e. V /\ Lim (B +o x))) -> (A +o (B +o x)) = U.z e. (B +o x)(A +o z))
49	47, 48	mpan21 531	. . . . . . . . . . 11 |- ((A e. On /\ Lim (B +o x)) -> (A +o (B +o x)) = U.z e. (B +o x)(A +o z))
50		oalimcl 3162	. . . . . . . . . . . . 13 |- ((B e. On /\ (x e. V /\ Lim x)) -> Lim (B +o x))
51	41, 50	mpan21 531	. . . . . . . . . . . 12 |- ((B e. On /\ Lim x) -> Lim (B +o x))
52	51	ancoms 334	. . . . . . . . . . 11 |- ((Lim x /\ B e. On) -> Lim (B +o x))
53	49, 52	sylan2 346	. . . . . . . . . 10 |- ((A e. On /\ (Lim x /\ B e. On)) -> (A +o (B +o x)) = U.z e. (B +o x)(A +o z))
54		limelon 2286	. . . . . . . . . . . . . . . . . 18 |- ((x e. V /\ Lim x) -> x e. On)
55	41, 54	mpan 518	. . . . . . . . . . . . . . . . 17 |- (Lim x -> x e. On)
56		oacl 3138	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((B e. On /\ x e. On) -> (B +o x) e. On)
57	56	ancoms 334	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. On /\ B e. On) -> (B +o x) e. On)
58		onelon 2223	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((B +o x) e. On /\ z e. (B +o x)) -> z e. On)
59	58	exp 291	. . . . . . . . . . . . . . . . . . . . . 22 |- ((B +o x) e. On -> (z e. (B +o x) -> z e. On))
60	57, 59	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. On /\ B e. On) -> (z e. (B +o x) -> z e. On))
61	60	adantld 307	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. On /\ B e. On) -> ((A e. On /\ z e. (B +o x)) -> z e. On))
62	61	adantl 305	. . . . . . . . . . . . . . . . . . 19 |- ((