Theorem omordi 3164

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 2223	. . . . . 6 |- ((B e. On /\ A e. B) -> A e. On)
2	1	exp 291	. . . . 5 |- (B e. On -> (A e. B -> A e. On))
3		eleq2 1150	. . . . . . . . . 10 |- (x = (/) -> (A e. x <-> A e. (/)))
4		opreq2 3007	. . . . . . . . . . 11 |- (x = (/) -> (C .o x) = (C .o (/)))
5	4	eleq2d 1156	. . . . . . . . . 10 |- (x = (/) -> ((C .o A) e. (C .o x) <-> (C .o A) e. (C .o (/))))
6	3, 5	imbi12d 474	. . . . . . . . 9 |- (x = (/) -> ((A e. x -> (C .o A) e. (C .o x)) <-> (A e. (/) -> (C .o A) e. (C .o (/)))))
7		eleq2 1150	. . . . . . . . . 10 |- (x = y -> (A e. x <-> A e. y))
8		opreq2 3007	. . . . . . . . . . 11 |- (x = y -> (C .o x) = (C .o y))
9	8	eleq2d 1156	. . . . . . . . . 10 |- (x = y -> ((C .o A) e. (C .o x) <-> (C .o A) e. (C .o y)))
10	7, 9	imbi12d 474	. . . . . . . . 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 1150	. . . . . . . . . 10 |- (x = suc y -> (A e. x <-> A e. suc y))
12		opreq2 3007	. . . . . . . . . . 11 |- (x = suc y -> (C .o x) = (C .o suc y))
13	12	eleq2d 1156	. . . . . . . . . 10 |- (x = suc y -> ((C .o A) e. (C .o x) <-> (C .o A) e. (C .o suc y)))
14	11, 13	imbi12d 474	. . . . . . . . 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 1150	. . . . . . . . . 10 |- (x = B -> (A e. x <-> A e. B))
16		opreq2 3007	. . . . . . . . . . 11 |- (x = B -> (C .o x) = (C .o B))
17	16	eleq2d 1156	. . . . . . . . . 10 |- (x = B -> ((C .o A) e. (C .o x) <-> (C .o A) e. (C .o B)))
18	15, 17	imbi12d 474	. . . . . . . . 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 1711	. . . . . . . . . . 11 |- -. A e. (/)
20	19	pm2.21i 73	. . . . . . . . . 10 |- (A e. (/) -> (C .o A) e. (C .o (/)))
21	20	a1i 7	. . . . . . . . 9 |- (((A e. On /\ C e. On) /\ (/) e. C) -> (A e. (/) -> (C .o A) e. (C .o (/))))
22		oaword1 3154	. . . . . . . . . . . . . . . . . . . . 21 |- (((C .o y) e. On /\ C e. On) -> (C .o y) (_ ((C .o y) +o C))
23	22	sseld 1506	. . . . . . . . . . . . . . . . . . . 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	syl3d 26	. . . . . . . . . . . . . . . . . . 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 277	. . . . . . . . . . . . . . . . . 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 311	. . . . . . . . . . . . . . . . 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 3007	. . . . . . . . . . . . . . . . . . . . 21 |- (A = y -> (C .o A) = (C .o y))
28	27	eleq1d 1155	. . . . . . . . . . . . . . . . . . . 20 |- (A = y -> ((C .o A) e. ((C .o y) +o C) <-> (C .o y) e. ((C .o y) +o C)))
29		oaord1 3153	. . . . . . . . . . . . . . . . . . . . 21 |- (((C .o y) e. On /\ C e. On) -> ((/) e. C <-> (C .o y) e. ((C .o y) +o C)))
30	29	biimpa 324	. . . . . . . . . . . . . . . . . . . 20 |- ((((C .o y) e. On /\ C e. On) /\ (/) e. C) -> (C .o y) e. ((C .o y) +o C))
31	28, 30	syl5bir 184	. . . . . . . . . . . . . . . . . . 19 |- (A = y -> ((((C .o y) e. On /\ C e. On) /\ (/) e. C) -> (C .o A) e. ((C .o y) +o C)))
32	31	com12 13	. . . . . . . . . . . . . . . . . 18 |- ((((C .o y) e. On /\ C e. On) /\ (/) e. C) -> (A = y -> (C .o A) e. ((C .o y) +o C)))
33	32	adantrr 312	. . . . . . . . . . . . . . . . 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)))
34	26, 33	jaod 329	. . . . . . . . . . . . . . . 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)))
35		omcl 3139	. . . . . . . . . . . . . . . . 17 |- ((C e. On /\ y e. On) -> (C .o y) e. On)
36		pm3.26 256	. . . . . . . . . . . . . . . . 17 |- ((C e. On /\ y e. On) -> C e. On)
37	35, 36	jca 236	. . . . . . . . . . . . . . . 16 |- ((C e. On /\ y e. On) -> ((C .o y) e. On /\ C e. On))
38	34, 37	sylan 343	. . . . . . . . . . . . . . 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)))
39		elsuci 2289	. . . . . . . . . . . . . . 15 |- (A e. suc y -> (A e. y \/ A = y))
40	38, 39	syl5 22	. . . . . . . . . . . . . 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)))
41		omsuc 3133	. . . . . . . . . . . . . . . 16 |- ((C e. On /\ y e. On) -> (C .o suc y) = ((C .o y) +o C))
42	41	eleq2d 1156	. . . . . . . . . . . . . . 15 |- ((C e. On /\ y e. On) -> ((C .o A) e. (C .o suc y) <-> (C .o A) e. ((C .o y) +o C)))
43	42	adantr 306	. . . . . . . . . . . . . 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)))
44	40, 43	sylibrd 179	. . . . . . . . . . . . 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)))
45	44	exp43 301	. . . . . . . . . . . 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))))))
46	45	com12 13	. . . . . . . . . . 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))))))
47	46	adantld 307	. . . . . . . . . 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))))))
48	47	imp3a 279	. . . . . . . . 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)))))
49		limsuc 2361	. . . . . . . . . . . . . . . . . . . 20 |- (Lim x -> (A e. x <-> suc A e. x))
50	49	biimpa 324	. . . . . . . . . . . . . . . . . . 19 |- ((Lim x /\ A e. x) -> suc A e. x)
51		opreq2 3007	. . . . . . . . . . . . . . . . . . . 20 |- (y = suc A -> (C .o y) = (C .o suc A))
52	51	ssiun2s 2020	. . . . . . . . . . . . . . . . . . 19 |- (suc A e. x -> (C .o suc A) (_ U.y e. x (C .o y))
53	50, 52	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((Lim x /\ A e. x) -> (C .o suc A) (_ U.y e. x (C .o y))
54	53	adantll 309	. . . . . . . . . . . . . . . . 17 |- (((C e. On /\ Lim x) /\ A e. x) -> (C .o suc A) (_ U.y e. x (C .o y))
55		visset 1350	. . . . . . . . . . . . . . . . . . 19 |- x e. V
56		omlim 3136	. . . . . . . . . . . . . . . . . . 19 |- ((C e. On /\ (x e. V /\ Lim x)) -> (C .o x) = U.y e. x (C .o y))
57	55, 56	mpan21 531	. . . . . . . . . . . . . . . . . 18 |- ((C e. On /\ Lim x) -> (C .o x) = U.y e. x (C .o y))
58	57	adantr 306	. . . . . . . . . . . . . . . . 17 |- (((C e. On /\ Lim x) /\ A e. x) -> (C .o x) = U.y e.