Theorem omwordri 4203

Description: Weak ordering property of ordinal multiplication. Proposition 8.21 of [TakeutiZaring] p. 63.

Assertion

Ref	Expression
omwordri	|- ((A e. On /\ B e. On /\ C e. On) -> (A (_ B -> (A .o C) (_ (B .o C)))

Proof of Theorem omwordri

Step	Hyp	Ref	Expression
1		opreq2 3969	. . . . . 6 |- (x = (/) -> (A .o x) = (A .o (/)))
2		opreq2 3969	. . . . . 6 |- (x = (/) -> (B .o x) = (B .o (/)))
3	1, 2	sseq12d 2090	. . . . 5 |- (x = (/) -> ((A .o x) (_ (B .o x) <-> (A .o (/)) (_ (B .o (/))))
4		opreq2 3969	. . . . . 6 |- (x = y -> (A .o x) = (A .o y))
5		opreq2 3969	. . . . . 6 |- (x = y -> (B .o x) = (B .o y))
6	4, 5	sseq12d 2090	. . . . 5 |- (x = y -> ((A .o x) (_ (B .o x) <-> (A .o y) (_ (B .o y)))
7		opreq2 3969	. . . . . 6 |- (x = suc y -> (A .o x) = (A .o suc y))
8		opreq2 3969	. . . . . 6 |- (x = suc y -> (B .o x) = (B .o suc y))
9	7, 8	sseq12d 2090	. . . . 5 |- (x = suc y -> ((A .o x) (_ (B .o x) <-> (A .o suc y) (_ (B .o suc y)))
10		opreq2 3969	. . . . . 6 |- (x = C -> (A .o x) = (A .o C))
11		opreq2 3969	. . . . . 6 |- (x = C -> (B .o x) = (B .o C))
12	10, 11	sseq12d 2090	. . . . 5 |- (x = C -> ((A .o x) (_ (B .o x) <-> (A .o C) (_ (B .o C)))
13		0ss 2301	. . . . . . 7 |- (/) (_ (B .o (/))
14		om0 4156	. . . . . . . 8 |- (A e. On -> (A .o (/)) = (/))
15	14	sseq1d 2088	. . . . . . 7 |- (A e. On -> ((A .o (/)) (_ (B .o (/)) <-> (/) (_ (B .o (/))))
16	13, 15	mpbiri 194	. . . . . 6 |- (A e. On -> (A .o (/)) (_ (B .o (/)))
17	16	ad2antrr 404	. . . . 5 |- (((A e. On /\ B e. On) /\ A (_ B) -> (A .o (/)) (_ (B .o (/)))
18		oawordri 4184	. . . . . . . . . . . . . 14 |- (((A .o y) e. On /\ (B .o y) e. On /\ A e. On) -> ((A .o y) (_ (B .o y) -> ((A .o y) +o A) (_ ((B .o y) +o A)))
19		omcl 4171	. . . . . . . . . . . . . . 15 |- ((A e. On /\ y e. On) -> (A .o y) e. On)
20	19	3adant2 798	. . . . . . . . . . . . . 14 |- ((A e. On /\ B e. On /\ y e. On) -> (A .o y) e. On)
21		omcl 4171	. . . . . . . . . . . . . . 15 |- ((B e. On /\ y e. On) -> (B .o y) e. On)
22	21	3adant1 797	. . . . . . . . . . . . . 14 |- ((A e. On /\ B e. On /\ y e. On) -> (B .o y) e. On)
23		3simp1 788	. . . . . . . . . . . . . 14 |- ((A e. On /\ B e. On /\ y e. On) -> A e. On)
24	18, 20, 22, 23	syl3anc 858	. . . . . . . . . . . . 13 |- ((A e. On /\ B e. On /\ y e. On) -> ((A .o y) (_ (B .o y) -> ((A .o y) +o A) (_ ((B .o y) +o A)))
25	24	imp 350	. . . . . . . . . . . 12 |- (((A e. On /\ B e. On /\ y e. On) /\ (A .o y) (_ (B .o y)) -> ((A .o y) +o A) (_ ((B .o y) +o A))
26	25	adantrl 394	. . . . . . . . . . 11 |- (((A e. On /\ B e. On /\ y e. On) /\ (A (_ B /\ (A .o y) (_ (B .o y))) -> ((A .o y) +o A) (_ ((B .o y) +o A))
27		oaword 4183	. . . . . . . . . . . . . 14 |- ((A e. On /\ B e. On /\ (B .o y) e. On) -> (A (_ B <-> ((B .o y) +o A) (_ ((B .o y) +o B)))
28	27, 22	syld3an3 870	. . . . . . . . . . . . 13 |- ((A e. On /\ B e. On /\ y e. On) -> (A (_ B <-> ((B .o y) +o A) (_ ((B .o y) +o B)))
29	28	biimpa 416	. . . . . . . . . . . 12 |- (((A e. On /\ B e. On /\ y e. On) /\ A (_ B) -> ((B .o y) +o A) (_ ((B .o y) +o B))
30	29	adantrr 395	. . . . . . . . . . 11 |- (((A e. On /\ B e. On /\ y e. On) /\ (A (_ B /\ (A .o y) (_ (B .o y))) -> ((B .o y) +o A) (_ ((B .o y) +o B))
31	26, 30	sstrd 2074	. . . . . . . . . 10 |- (((A e. On /\ B e. On /\ y e. On) /\ (A (_ B /\ (A .o y) (_ (B .o y))) -> ((A .o y) +o A) (_ ((B .o y) +o B))
32		omsuc 4165	. . . . . . . . . . . 12 |- ((A e. On /\ y e. On) -> (A .o suc y) = ((A .o y) +o A))
33	32	3adant2 798	. . . . . . . . . . 11 |- ((A e. On /\ B e. On /\ y e. On) -> (A .o suc y) = ((A .o y) +o A))
34	33	adantr 389	. . . . . . . . . 10 |- (((A e. On /\ B e. On /\ y e. On) /\ (A (_ B /\ (A .o y) (_ (B .o y))) -> (A .o suc y) = ((A .o y) +o A))
35		omsuc 4165	. . . . . . . . . . . 12 |- ((B e. On /\ y e. On) -> (B .o suc y) = ((B .o y) +o B))
36	35	3adant1 797	. . . . . . . . . . 11 |- ((A e. On /\ B e. On /\ y e. On) -> (B .o suc y) = ((B .o y) +o B))
37	36	adantr 389	. . . . . . . . . 10 |- (((A e. On /\ B e. On /\ y e. On) /\ (A (_ B /\ (A .o y) (_ (B .o y))) -> (B .o suc y) = ((B .o y) +o B))
38	31, 34, 37	3sstr4d 2104	. . . . . . . . 9 |- (((A e. On /\ B e. On /\ y e. On) /\ (A (_ B /\ (A .o y) (_ (B .o y))) -> (A .o suc y) (_ (B .o suc y))
39	38	exp32 377	. . . . . . . 8 |- ((A e. On /\ B e. On /\ y e. On) -> (A (_ B -> ((A .o y) (_ (B .o y) -> (A .o suc y) (_ (B .o suc y))))
40	39	3exp 832	. . . . . . 7 |- (A e. On -> (B e. On -> (y e. On -> (A (_ B -> ((A .o y) (_ (B .o y) -> (A .o suc y) (_ (B .o suc y))))))
41	40	com3r 35	. . . . . 6 |- (y e. On -> (A e. On -> (B e. On -> (A (_ B -> ((A .o y) (_ (B .o y) -> (A .o suc y) (_ (B .o suc y))))))
42	41	imp4c 366	. . . . 5 |- (y e. On -> (((A e. On /\ B e. On) /\ A (_ B) -> ((A .o y) (_ (B .o y) -> (A .o suc y) (_ (B .o suc y))))
43		visset 1813	. . . . . . . 8 |- x e. V
44		omlim 4168	. . . . . . . . . . . 12 |- ((A e. On /\ (x e. V /\ Lim x)) -> (A .o x) = U_y e. x (A .o y))
45	44	ad2ant2rl 411	. . . . . . . . . . 11 |- (((A e. On /\ (x e. V /\ Lim x)) /\ (B e. On /\ (x e. V /\ Lim x))) -> (A .o x) = U_y e. x (A .o y))
46		omlim 4168	. . . . . . . . . . . 12 |- ((B e. On /\ (x e. V /\ Lim x)) -> (B .o x) = U_y e. x (B .o y))
47	46	adantl 388	. . . . . . . . . . 11 |- (((A e. On /\ (x e. V /\ Lim x)) /\ (B e. On /\ (x e. V /\ Lim x))) -> (B .o x) = U_y e. x (B .o y))
48	45, 47	sseq12d 2090	. . . . . . . . . 10 |- (((A e. On /\ (x e. V /\ Lim x)) /\ (B e. On /\ (x e. V /\ Lim x))) -> ((A .o x) (_ (B .o x) <-> U_y e. x (A .o y) (_ U_y e. x (B .o y)))
49		ss2iun 2577	. . . . . . . . . 10 |- (A.y e. x (A .o y) (_ (B .o y) -> U_y e. x (A .o y) (_ U_y e. x (B .o y))
50	48, 49	syl5bir 210	. . . . . . . . 9 |- (((A e. On /\ (x e. V /\ Lim x)) /\ (B e. On /\ (x e. V /\ Lim x))) -> (A.y e. x (A .o y) (_ (B .o y) -> (A .o x) (_ (B .o x)))
51	50	anandirs 513	. . . . . . . 8 |- (((A e. On /\ B e. On) /\ (x e. V /\ Lim x)) -> (A.y e. x (A .o y) (_ (B .o y) -> (A .o x) (_ (B .o x)))
52	43, 51	mpanr1 709	. . . . . . 7 |- (((A e. On /\ B e. On) /\ Lim x) -> (A.y e. x (A .o y) (_ (B .o y) -> (A .o x) (_ (B .o x)))
53	52	expcom 374	. . . . . 6 |- (Lim x -> ((A e. On /\ B e. On) -> (A.y e. x (A .o y) (_ (B .o y) -> (A .o x) (_ (B .o x))))
54	53	adantrd 391	. . . . 5 |- (Lim x -> (((A e. On /\ B e. On) /\ A (_ B) -> (A.y e. x (A .o y) (_ (B .o y) -> (A .o x) (_ (B .o x))))
55	3, 6, 9, 12, 17, 42, 54	tfinds3 3166	. . . 4 |- (C e. On -> (((A e. On /\ B e. On) /\ A (_ B