Theorem oeordi 4272

Description: Ordering law for ordinal exponentiation. Proposition 8.33 of [TakeutiZaring] p. 67.

Assertion

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

Proof of Theorem oeordi

Step	Hyp	Ref	Expression
1		opreq2 4027	. . . . . . . 8 |- (x = suc A -> (C ^o x) = (C ^o suc A))
2	1	eleq2d 1588	. . . . . . 7 |- (x = suc A -> ((C ^o A) e. (C ^o x) <-> (C ^o A) e. (C ^o suc A)))
3	2	imbi2d 623	. . . . . 6 |- (x = suc A -> (((C e. On /\ 1o e. C) -> (C ^o A) e. (C ^o x)) <-> ((C e. On /\ 1o e. C) -> (C ^o A) e. (C ^o suc A))))
4		opreq2 4027	. . . . . . . 8 |- (x = y -> (C ^o x) = (C ^o y))
5	4	eleq2d 1588	. . . . . . 7 |- (x = y -> ((C ^o A) e. (C ^o x) <-> (C ^o A) e. (C ^o y)))
6	5	imbi2d 623	. . . . . 6 |- (x = y -> (((C e. On /\ 1o e. C) -> (C ^o A) e. (C ^o x)) <-> ((C e. On /\ 1o e. C) -> (C ^o A) e. (C ^o y))))
7		opreq2 4027	. . . . . . . 8 |- (x = suc y -> (C ^o x) = (C ^o suc y))
8	7	eleq2d 1588	. . . . . . 7 |- (x = suc y -> ((C ^o A) e. (C ^o x) <-> (C ^o A) e. (C ^o suc y)))
9	8	imbi2d 623	. . . . . 6 |- (x = suc y -> (((C e. On /\ 1o e. C) -> (C ^o A) e. (C ^o x)) <-> ((C e. On /\ 1o e. C) -> (C ^o A) e. (C ^o suc y))))
10		opreq2 4027	. . . . . . . 8 |- (x = B -> (C ^o x) = (C ^o B))
11	10	eleq2d 1588	. . . . . . 7 |- (x = B -> ((C ^o A) e. (C ^o x) <-> (C ^o A) e. (C ^o B)))
12	11	imbi2d 623	. . . . . 6 |- (x = B -> (((C e. On /\ 1o e. C) -> (C ^o A) e. (C ^o x)) <-> ((C e. On /\ 1o e. C) -> (C ^o A) e. (C ^o B))))
13		0lt1o 4205	. . . . . . . . . . . . . 14 |- (/) e. 1o
14		ontr1 3060	. . . . . . . . . . . . . 14 |- (C e. On -> (((/) e. 1o /\ 1o e. C) -> (/) e. C))
15	13, 14	mpani 710	. . . . . . . . . . . . 13 |- (C e. On -> (1o e. C -> (/) e. C))
16	15	adantr 398	. . . . . . . . . . . 12 |- ((C e. On /\ A e. On) -> (1o e. C -> (/) e. C))
17		oen0 4271	. . . . . . . . . . . . 13 |- (((C e. On /\ A e. On) /\ (/) e. C) -> (/) e. (C ^o A))
18	17	ex 380	. . . . . . . . . . . 12 |- ((C e. On /\ A e. On) -> ((/) e. C -> (/) e. (C ^o A)))
19	16, 18	syld 27	. . . . . . . . . . 11 |- ((C e. On /\ A e. On) -> (1o e. C -> (/) e. (C ^o A)))
20		pm3.26 326	. . . . . . . . . . . 12 |- ((C e. On /\ A e. On) -> C e. On)
21		oecl 4230	. . . . . . . . . . . 12 |- ((C e. On /\ A e. On) -> (C ^o A) e. On)
22	20, 21	jca 295	. . . . . . . . . . 11 |- ((C e. On /\ A e. On) -> (C e. On /\ (C ^o A) e. On))
23	19, 22	jctild 612	. . . . . . . . . 10 |- ((C e. On /\ A e. On) -> (1o e. C -> ((C e. On /\ (C ^o A) e. On) /\ (/) e. (C ^o A))))
24		omordi 4255	. . . . . . . . . 10 |- (((C e. On /\ (C ^o A) e. On) /\ (/) e. (C ^o A)) -> (1o e. C -> ((C ^o A) .o 1o) e. ((C ^o A) .o C)))
25	23, 24	syli 54	. . . . . . . . 9 |- ((C e. On /\ A e. On) -> (1o e. C -> ((C ^o A) .o 1o) e. ((C ^o A) .o C)))
26		om1 4234	. . . . . . . . . . . 12 |- ((C ^o A) e. On -> ((C ^o A) .o 1o) = (C ^o A))
27	21, 26	syl 10	. . . . . . . . . . 11 |- ((C e. On /\ A e. On) -> ((C ^o A) .o 1o) = (C ^o A))
28	27	eleq1d 1587	. . . . . . . . . 10 |- ((C e. On /\ A e. On) -> (((C ^o A) .o 1o) e. ((C ^o A) .o C) <-> (C ^o A) e. ((C ^o A) .o C)))
29		oesuc 4224	. . . . . . . . . . 11 |- ((C e. On /\ A e. On) -> (C ^o suc A) = ((C ^o A) .o C))
30	29	eleq2d 1588	. . . . . . . . . 10 |- ((C e. On /\ A e. On) -> ((C ^o A) e. (C ^o suc A) <-> (C ^o A) e. ((C ^o A) .o C)))
31	28, 30	bitr4d 542	. . . . . . . . 9 |- ((C e. On /\ A e. On) -> (((C ^o A) .o 1o) e. ((C ^o A) .o C) <-> (C ^o A) e. (C ^o suc A)))
32	25, 31	sylibd 209	. . . . . . . 8 |- ((C e. On /\ A e. On) -> (1o e. C -> (C ^o A) e. (C ^o suc A)))
33	32	expcom 381	. . . . . . 7 |- (A e. On -> (C e. On -> (1o e. C -> (C ^o A) e. (C ^o suc A))))
34	33	imp3a 368	. . . . . 6 |- (A e. On -> ((C e. On /\ 1o e. C) -> (C ^o A) e. (C ^o suc A)))
35	15	adantr 398	. . . . . . . . . . . . . . 15 |- ((C e. On /\ y e. On) -> (1o e. C -> (/) e. C))
36		oen0 4271	. . . . . . . . . . . . . . . 16 |- (((C e. On /\ y e. On) /\ (/) e. C) -> (/) e. (C ^o y))
37	36	ex 380	. . . . . . . . . . . . . . 15 |- ((C e. On /\ y e. On) -> ((/) e. C -> (/) e. (C ^o y)))
38	35, 37	syld 27	. . . . . . . . . . . . . 14 |- ((C e. On /\ y e. On) -> (1o e. C -> (/) e. (C ^o y)))
39		pm3.26 326	. . . . . . . . . . . . . . 15 |- ((C e. On /\ y e. On) -> C e. On)
40		oecl 4230	. . . . . . . . . . . . . . 15 |- ((C e. On /\ y e. On) -> (C ^o y) e. On)
41	39, 40	jca 295	. . . . . . . . . . . . . 14 |- ((C e. On /\ y e. On) -> (C e. On /\ (C ^o y) e. On))
42	38, 41	jctild 612	. . . . . . . . . . . . 13 |- ((C e. On /\ y e. On) -> (1o e. C -> ((C e. On /\ (C ^o y) e. On) /\ (/) e. (C ^o y))))
43		omordi 4255	. . . . . . . . . . . . 13 |- (((C e. On /\ (C ^o y) e. On) /\ (/) e. (C ^o y)) -> (1o e. C -> ((C ^o y) .o 1o) e. ((C ^o y) .o C)))
44	42, 43	syli 54	. . . . . . . . . . . 12 |- ((C e. On /\ y e. On) -> (1o e. C -> ((C ^o y) .o 1o) e. ((C ^o y) .o C)))
45		om1 4234	. . . . . . . . . . . . . . 15 |- ((C ^o y) e. On -> ((C ^o y) .o 1o) = (C ^o y))
46	40, 45	syl 10	. . . . . . . . . . . . . 14 |- ((C e. On /\ y e. On) -> ((C ^o y) .o 1o) = (C ^o y))
47	46	eleq1d 1587	. . . . . . . . . . . . 13 |- ((C e. On /\ y e. On) -> (((C ^o y) .o 1o) e. ((C ^o y) .o C) <-> (C ^o y) e. ((C ^o y) .o C)))
48		oesuc 4224	. . . . . . . . . . . . . 14 |- ((C e. On /\ y e. On) -> (C ^o suc y) = ((C ^o y) .o C))
49	48	eleq2d 1588	. . . . . . . . . . . . 13 |- ((C e. On /\ y e. On) -> ((C ^o y) e. (C ^o suc y) <-> (C ^o y) e. ((C ^o y) .o C)))
50	47, 49	bitr4d 542	. . . . . . . . . . . 12 |- ((C e. On /\ y e. On) -> (((C ^o y) .o 1o) e. ((C ^o y) .o C) <-> (C ^o y) e. (C ^o suc y)))
51	44, 50	sylibd 209	. . . . . . . . . . 11 |- ((C e. On /\ y e. On) -> (1o e. C -> (C ^o y) e. (C ^o suc y)))
52		oecl 4230	. . . . . . . . . . . . . . 15 |- ((C e. On /\ suc y e. On) -> (C ^o suc y) e. On)
53		sucelon 3125	. . . . . . . . . . . . . . 15 |- (y e. On <-> suc y e. On)
54	52, 53	sylan2b 463	. . . . . . . . . . . . . 14 |- ((C e. On /\ y e. On) -> (C ^o suc y) e. On)
55		ontr1 3060	. . . . . . . . . . . . . 14 |- ((C ^o suc y) e. On -> (((C ^o A) e. (C ^o y) /\ (C ^o y) e. (C ^o suc y)) -> (C ^o A) e. (C ^o suc y)))
56	54, 55	syl 10	. . . . . . . . . . . . 13 |- ((C e. On /\ y e. On) -> (((C ^o A) e. (C ^o y) /\ (C ^o y) e. (C ^o suc y)) -> (C ^o A) e. (C ^o suc y)))
57	56	exp3a 383	. . . . . . . . . . . 12 |- ((C e. On /\ y e. On) -> ((C ^o A) e. (C ^o y) -> ((C ^o y) e. (C ^o suc y) -> (C ^o A) e. (C ^o suc y))))
58	57	com23 32	. . . . . . . . . . 11 |- ((C e. On /\ y e. On) -> ((C ^o y) e. (C ^o suc y) -> ((C ^o A) e. (C ^o y) -> (C ^o A) e. (C ^o suc y))))
59	51, 58	syld 27	. . . . . . . . . 10 |- ((C e. On /\ y e. On) -> (1o e. C -> ((C ^o A) e. (C ^o y) -> (C ^o A) e. (C ^o suc y))))
60	59	expcom 381	. . . . . . . . 9 |- (y e. On