Theorem omordi 4197

Description: Ordering property of ordinal multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63.

Assertion

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

Proof of Theorem omordi

Step	Hyp	Ref	Expression
1		onelon 2972	. . . . . 6 |- ((B e. On /\ A e. B) -> A e. On)
2	1	ex 373	. . . . 5 |- (B e. On -> (A e. B -> A e. On))
3		eleq2 1535	. . . . . . . . . 10 |- (x = (/) -> (A e. x <-> A e. (/)))
4		opreq2 3969	. . . . . . . . . . 11 |- (x = (/) -> (C .o x) = (C .o (/)))
5	4	eleq2d 1541	. . . . . . . . . 10 |- (x = (/) -> ((C .o A) e. (C .o x) <-> (C .o A) e. (C .o (/))))
6	3, 5	imbi12d 626	. . . . . . . . 9 |- (x = (/) -> ((A e. x -> (C .o A) e. (C .o x)) <-> (A e. (/) -> (C .o A) e. (C .o (/)))))
7		eleq2 1535	. . . . . . . . . 10 |- (x = y -> (A e. x <-> A e. y))
8		opreq2 3969	. . . . . . . . . . 11 |- (x = y -> (C .o x) = (C .o y))
9	8	eleq2d 1541	. . . . . . . . . 10 |- (x = y -> ((C .o A) e. (C .o x) <-> (C .o A) e. (C .o y)))
10	7, 9	imbi12d 626	. . . . . . . . 9 |- (x = y -> ((A e. x -> (C .o A) e. (C .o x)) <-> (A e. y -> (C .o A) e. (C .o y))))
11		eleq2 1535	. . . . . . . . . 10 |- (x = suc y -> (A e. x <-> A e. suc y))
12		opreq2 3969	. . . . . . . . . . 11 |- (x = suc y -> (C .o x) = (C .o suc y))
13	12	eleq2d 1541	. . . . . . . . . 10 |- (x = suc y -> ((C .o A) e. (C .o x) <-> (C .o A) e. (C .o suc y)))
14	11, 13	imbi12d 626	. . . . . . . . 9 |- (x = suc y -> ((A e. x -> (C .o A) e. (C .o x)) <-> (A e. suc y -> (C .o A) e. (C .o suc y))))
15		eleq2 1535	. . . . . . . . . 10 |- (x = B -> (A e. x <-> A e. B))
16		opreq2 3969	. . . . . . . . . . 11 |- (x = B -> (C .o x) = (C .o B))
17	16	eleq2d 1541	. . . . . . . . . 10 |- (x = B -> ((C .o A) e. (C .o x) <-> (C .o A) e. (C .o B)))
18	15, 17	imbi12d 626	. . . . . . . . 9 |- (x = B -> ((A e. x -> (C .o A) e. (C .o x)) <-> (A e. B -> (C .o A) e. (C .o B))))
19		noel 2284	. . . . . . . . . . 11 |- -. A e. (/)
20	19	pm2.21i 77	. . . . . . . . . 10 |- (A e. (/) -> (C .o A) e. (C .o (/)))
21	20	a1i 8	. . . . . . . . 9 |- (((A e. On /\ C e. On) /\ (/) e. C) -> (A e. (/) -> (C .o A) e. (C .o (/))))
22		oaword1 4186	. . . . . . . . . . . . . . . . . . . . 21 |- (((C .o y) e. On /\ C e. On) -> (C .o y) (_ ((C .o y) +o C))
23	22	sseld 2067	. . . . . . . . . . . . . . . . . . . 20 |- (((C .o y) e. On /\ C e. On) -> ((C .o A) e. (C .o y) -> (C .o A) e. ((C .o y) +o C)))
24	23	imim2d 25	. . . . . . . . . . . . . . . . . . 19 |- (((C .o y) e. On /\ C e. On) -> ((A e. y -> (C .o A) e. (C .o y)) -> (A e. y -> (C .o A) e. ((C .o y) +o C))))
25	24	imp 350	. . . . . . . . . . . . . . . . . 18 |- ((((C .o y) e. On /\ C e. On) /\ (A e. y -> (C .o A) e. (C .o y))) -> (A e. y -> (C .o A) e. ((C .o y) +o C)))
26	25	adantrl 394	. . . . . . . . . . . . . . . . 17 |- ((((C .o y) e. On /\ C e. On) /\ ((/) e. C /\ (A e. y -> (C .o A) e. (C .o y)))) -> (A e. y -> (C .o A) e. ((C .o y) +o C)))
27		opreq2 3969	. . . . . . . . . . . . . . . . . . . 20 |- (A = y -> (C .o A) = (C .o y))
28	27	eleq1d 1540	. . . . . . . . . . . . . . . . . . 19 |- (A = y -> ((C .o A) e. ((C .o y) +o C) <-> (C .o y) e. ((C .o y) +o C)))
29		oaord1 4185	. . . . . . . . . . . . . . . . . . . 20 |- (((C .o y) e. On /\ C e. On) -> ((/) e. C <-> (C .o y) e. ((C .o y) +o C)))
30	29	biimpa 416	. . . . . . . . . . . . . . . . . . 19 |- ((((C .o y) e. On /\ C e. On) /\ (/) e. C) -> (C .o y) e. ((C .o y) +o C))
31	28, 30	syl5cbir 211	. . . . . . . . . . . . . . . . . 18 |- ((((C .o y) e. On /\ C e. On) /\ (/) e. C) -> (A = y -> (C .o A) e. ((C .o y) +o C)))
32	31	adantrr 395	. . . . . . . . . . . . . . . . 17 |- ((((C .o y) e. On /\ C e. On) /\ ((/) e. C /\ (A e. y -> (C .o A) e. (C .o y)))) -> (A = y -> (C .o A) e. ((C .o y) +o C)))
33	26, 32	jaod 424	. . . . . . . . . . . . . . . 16 |- ((((C .o y) e. On /\ C e. On) /\ ((/) e. C /\ (A e. y -> (C .o A) e. (C .o y)))) -> ((A e. y \/ A = y) -> (C .o A) e. ((C .o y) +o C)))
34		omcl 4171	. . . . . . . . . . . . . . . . 17 |- ((C e. On /\ y e. On) -> (C .o y) e. On)
35		pm3.26 319	. . . . . . . . . . . . . . . . 17 |- ((C e. On /\ y e. On) -> C e. On)
36	34, 35	jca 288	. . . . . . . . . . . . . . . 16 |- ((C e. On /\ y e. On) -> ((C .o y) e. On /\ C e. On))
37	33, 36	sylan 448	. . . . . . . . . . . . . . 15 |- (((C e. On /\ y e. On) /\ ((/) e. C /\ (A e. y -> (C .o A) e. (C .o y)))) -> ((A e. y \/ A = y) -> (C .o A) e. ((C .o y) +o C)))
38		elsuci 3035	. . . . . . . . . . . . . . 15 |- (A e. suc y -> (A e. y \/ A = y))
39	37, 38	syl5 21	. . . . . . . . . . . . . 14 |- (((C e. On /\ y e. On) /\ ((/) e. C /\ (A e. y -> (C .o A) e. (C .o y)))) -> (A e. suc y -> (C .o A) e. ((C .o y) +o C)))
40		omsuc 4165	. . . . . . . . . . . . . . . 16 |- ((C e. On /\ y e. On) -> (C .o suc y) = ((C .o y) +o C))
41	40	eleq2d 1541	. . . . . . . . . . . . . . 15 |- ((C e. On /\ y e. On) -> ((C .o A) e. (C .o suc y) <-> (C .o A) e. ((C .o y) +o C)))
42	41	adantr 389	. . . . . . . . . . . . . 14 |- (((C e. On /\ y e. On) /\ ((/) e. C /\ (A e. y -> (C .o A) e. (C .o y)))) -> ((C .o A) e. (C .o suc y) <-> (C .o A) e. ((C .o y) +o C)))
43	39, 42	sylibrd 204	. . . . . . . . . . . . 13 |- (((C e. On /\ y e. On) /\ ((/) e. C /\ (A e. y -> (C .o A) e. (C .o y)))) -> (A e. suc y -> (C .o A) e. (C .o suc y)))
44	43	exp43 384	. . . . . . . . . . . 12 |- (C e. On -> (y e. On -> ((/) e. C -> ((A e. y -> (C .o A) e. (C .o y)) -> (A e. suc y -> (C .o A) e. (C .o suc y))))))
45	44	com12 11	. . . . . . . . . . 11 |- (y e. On -> (C e. On -> ((/) e. C -> ((A e. y -> (C .o A) e. (C .o y)) -> (A e. suc y -> (C .o A) e. (C .o suc y))))))
46	45	adantld 390	. . . . . . . . . 10 |- (y e. On -> ((A e. On /\ C e. On) -> ((/) e. C -> ((A e. y -> (C .o A) e. (C .o y)) -> (A e. suc y -> (C .o A) e. (C .o suc y))))))
47	46	imp3a 361	. . . . . . . . 9 |- (y e. On -> (((A e. On /\ C e. On) /\ (/) e. C) -> ((A e. y -> (C .o A) e. (C .o y)) -> (A e. suc y -> (C .o A) e. (C .o suc y)))))
48		limsuc 3120	. . . . . . . . . . . . . . . . . . . 20 |- (Lim x -> (A e. x <-> suc A e. x))
49	48	biimpa 416	. . . . . . . . . . . . . . . . . . 19 |- ((Lim x /\ A e. x) -> suc A e. x)
50		opreq2 3969	. . . . . . . . . . . . . . . . . . . 20 |- (y = suc A -> (C .o y) = (C .o suc A))
51	50	ssiun2s 2594	. . . . . . . . . . . . . . . . . . 19 |- (suc A e. x -> (C .o suc A) (_ U_y e. x (C .o y))
52	49, 51	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((Lim x /\ A e. x) -> (C .o suc A) (_ U_y e. x (C .o y))
53	52	adantll 392	. . . . . . . . . . . . . . . . 17 |- (((C e. On /\ Lim x) /\ A e. x) -> (C .o suc A) (_ U_y e. x (C .o y))
54		visset 1813	. . . . . . . . . . . . . . . . . . 19 |- x e. V
55		omlim 4168	. . . . . . . . . . . . . . . . . . 19 |- ((C e. On /\ (x e. V /\ Lim x)) -> (C .o x) = U_y e. x (C .o y))
56	54, 55	mpanr1 709	. . . . . . . . . . . . . . . . . 18 |- ((C e. On /\ Lim x) -> (C .o x) = U_y e. x (C .o y))
57	56	adantr 389	. . . . . . . . . . . . . . . . 17 |- (((C e. On