Theorem oaass 4193

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 3967	. . . . 5 |- (x = (/) -> ((A +o B) +o x) = ((A +o B) +o (/)))
2		opreq2 3967	. . . . . 6 |- (x = (/) -> (B +o x) = (B +o (/)))
3	2	opreq2d 3974	. . . . 5 |- (x = (/) -> (A +o (B +o x)) = (A +o (B +o (/))))
4	1, 3	eqeq12d 1488	. . . 4 |- (x = (/) -> (((A +o B) +o x) = (A +o (B +o x)) <-> ((A +o B) +o (/)) = (A +o (B +o (/)))))
5		opreq2 3967	. . . . 5 |- (x = y -> ((A +o B) +o x) = ((A +o B) +o y))
6		opreq2 3967	. . . . . 6 |- (x = y -> (B +o x) = (B +o y))
7	6	opreq2d 3974	. . . . 5 |- (x = y -> (A +o (B +o x)) = (A +o (B +o y)))
8	5, 7	eqeq12d 1488	. . . 4 |- (x = y -> (((A +o B) +o x) = (A +o (B +o x)) <-> ((A +o B) +o y) = (A +o (B +o y))))
9		opreq2 3967	. . . . 5 |- (x = suc y -> ((A +o B) +o x) = ((A +o B) +o suc y))
10		opreq2 3967	. . . . . 6 |- (x = suc y -> (B +o x) = (B +o suc y))
11	10	opreq2d 3974	. . . . 5 |- (x = suc y -> (A +o (B +o x)) = (A +o (B +o suc y)))
12	9, 11	eqeq12d 1488	. . . 4 |- (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 3967	. . . . 5 |- (x = C -> ((A +o B) +o x) = ((A +o B) +o C))
14		opreq2 3967	. . . . . 6 |- (x = C -> (B +o x) = (B +o C))
15	14	opreq2d 3974	. . . . 5 |- (x = C -> (A +o (B +o x)) = (A +o (B +o C)))
16	13, 15	eqeq12d 1488	. . . 4 |- (x = C -> (((A +o B) +o x) = (A +o (B +o x)) <-> ((A +o B) +o C) = (A +o (B +o C))))
17		oacl 4168	. . . . . 6 |- ((A e. On /\ B e. On) -> (A +o B) e. On)
18		oa0 4153	. . . . . 6 |- ((A +o B) e. On -> ((A +o B) +o (/)) = (A +o B))
19	17, 18	syl 10	. . . . 5 |- ((A e. On /\ B e. On) -> ((A +o B) +o (/)) = (A +o B))
20		oa0 4153	. . . . . . 7 |- (B e. On -> (B +o (/)) = B)
21	20	opreq2d 3974	. . . . . 6 |- (B e. On -> (A +o (B +o (/))) = (A +o B))
22	21	adantl 388	. . . . 5 |- ((A e. On /\ B e. On) -> (A +o (B +o (/))) = (A +o B))
23	19, 22	eqtr4d 1509	. . . 4 |- ((A e. On /\ B e. On) -> ((A +o B) +o (/)) = (A +o (B +o (/))))
24		oasuc 4161	. . . . . . . 8 |- (((A +o B) e. On /\ y e. On) -> ((A +o B) +o suc y) = suc ((A +o B) +o y))
25	24, 17	sylan 448	. . . . . . 7 |- (((A e. On /\ B e. On) /\ y e. On) -> ((A +o B) +o suc y) = suc ((A +o B) +o y))
26		oasuc 4161	. . . . . . . . . . 11 |- ((B e. On /\ y e. On) -> (B +o suc y) = suc (B +o y))
27	26	opreq2d 3974	. . . . . . . . . 10 |- ((B e. On /\ y e. On) -> (A +o (B +o suc y)) = (A +o suc (B +o y)))
28	27	adantl 388	. . . . . . . . 9 |- ((A e. On /\ (B e. On /\ y e. On)) -> (A +o (B +o suc y)) = (A +o suc (B +o y)))
29		oasuc 4161	. . . . . . . . . 10 |- ((A e. On /\ (B +o y) e. On) -> (A +o suc (B +o y)) = suc (A +o (B +o y)))
30		oacl 4168	. . . . . . . . . 10 |- ((B e. On /\ y e. On) -> (B +o y) e. On)
31	29, 30	sylan2 451	. . . . . . . . 9 |- ((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 1506	. . . . . . . 8 |- ((A e. On /\ (B e. On /\ y e. On)) -> (A +o (B +o suc y)) = suc (A +o (B +o y)))
33	32	anassrs 441	. . . . . . 7 |- (((A e. On /\ B e. On) /\ y e. On) -> (A +o (B +o suc y)) = suc (A +o (B +o y)))
34	25, 33	eqeq12d 1488	. . . . . 6 |- (((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 3032	. . . . . 6 |- (((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 210	. . . . 5 |- (((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	expcom 374	. . . 4 |- (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)))))
38		iuneq2 2576	. . . . . . 7 |- (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)))
39	38	adantl 388	. . . . . 6 |- (((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)))
40		visset 1811	. . . . . . . . . 10 |- x e. V
41		oalim 4165	. . . . . . . . . 10 |- (((A +o B) e. On /\ (x e. V /\ Lim x)) -> ((A +o B) +o x) = U_y e. x ((A +o B) +o y))
42	40, 41	mpanr1 709	. . . . . . . . 9 |- (((A +o B) e. On /\ Lim x) -> ((A +o B) +o x) = U_y e. x ((A +o B) +o y))
43	42, 17	sylan 448	. . . . . . . 8 |- (((A e. On /\ B e. On) /\ Lim x) -> ((A +o B) +o x) = U_y e. x ((A +o B) +o y))
44	43	ancoms 436	. . . . . . 7 |- ((Lim x /\ (A e. On /\ B e. On)) -> ((A +o B) +o x) = U_y e. x ((A +o B) +o y))
45	44	adantr 389	. . . . . 6 |- (((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))
46		oprex 3981	. . . . . . . . . . 11 |- (B +o x) e. V
47		oalim 4165	. . . . . . . . . . 11 |- ((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))
48	46, 47	mpanr1 709	. . . . . . . . . 10 |- ((A e. On /\ Lim (B +o x)) -> (A +o (B +o x)) = U_z e. (B +o x)(A +o z))
49		oalimcl 4192	. . . . . . . . . . . 12 |- ((B e. On /\ (x e. V /\ Lim x)) -> Lim (B +o x))
50	40, 49	mpanr1 709	. . . . . . . . . . 11 |- ((B e. On /\ Lim x) -> Lim (B +o x))
51	50	ancoms 436	. . . . . . . . . 10 |- ((Lim x /\ B e. On) -> Lim (B +o x))
52	48, 51	sylan2 451	. . . . . . . . 9 |- ((A e. On /\ (Lim x /\ B e. On)) -> (A +o (B +o x)) = U_z e. (B +o x)(A +o z))
53		limelon 3030	. . . . . . . . . . . . . . . . 17 |- ((x e. V /\ Lim x) -> x e. On)
54	40, 53	mpan 695	. . . . . . . . . . . . . . . 16 |- (Lim x -> x e. On)
55		oacl 4168	. . . . . . . . . . . . . . . . . . . . . 22 |- ((B e. On /\ x e. On) -> (B +o x) e. On)
56	55	ancoms 436	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. On /\ B e. On) -> (B +o x) e. On)
57		onelon 2970	. . . . . . . . . . . . . . . . . . . . . 22 |- (((B +o x) e. On /\ z e. (B +o x)) -> z e. On)
58	57	ex 373	. . . . . . . . . . . . . . . . . . . . 21 |- ((B +o x) e. On -> (z e. (B +o x) -> z e. On))
59	56, 58	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. On /\ B e. On) -> (z e. (B +o x) -> z e. On))
60	59	adantld 390	. . . . . . . . . . . . . . . . . . 19 |- ((x e. On /\ B e. On) -> ((A e. On /\ z e. (B +o x)) -> z e. On))
61	60	adantl 388	. . . . . . . . . . . . . . . . . 18 |- ((Lim x /\ (x e.