Theorem oewordri 4219

Description: Weak ordering property of ordinal exponentiation. Proposition 8.35 of [TakeutiZaring] p. 68.

Assertion

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

Proof of Theorem oewordri

Step	Hyp	Ref	Expression
1		opreq2 3969	. . . . 5 |- (x = (/) -> (A ^o x) = (A ^o (/)))
2		opreq2 3969	. . . . 5 |- (x = (/) -> (B ^o x) = (B ^o (/)))
3	1, 2	sseq12d 2090	. . . 4 |- (x = (/) -> ((A ^o x) (_ (B ^o x) <-> (A ^o (/)) (_ (B ^o (/))))
4		opreq2 3969	. . . . 5 |- (x = y -> (A ^o x) = (A ^o y))
5		opreq2 3969	. . . . 5 |- (x = y -> (B ^o x) = (B ^o y))
6	4, 5	sseq12d 2090	. . . 4 |- (x = y -> ((A ^o x) (_ (B ^o x) <-> (A ^o y) (_ (B ^o y)))
7		opreq2 3969	. . . . 5 |- (x = suc y -> (A ^o x) = (A ^o suc y))
8		opreq2 3969	. . . . 5 |- (x = suc y -> (B ^o x) = (B ^o suc y))
9	7, 8	sseq12d 2090	. . . 4 |- (x = suc y -> ((A ^o x) (_ (B ^o x) <-> (A ^o suc y) (_ (B ^o suc y)))
10		opreq2 3969	. . . . 5 |- (x = C -> (A ^o x) = (A ^o C))
11		opreq2 3969	. . . . 5 |- (x = C -> (B ^o x) = (B ^o C))
12	10, 11	sseq12d 2090	. . . 4 |- (x = C -> ((A ^o x) (_ (B ^o x) <-> (A ^o C) (_ (B ^o C)))
13		onelon 2972	. . . . . . 7 |- ((B e. On /\ A e. B) -> A e. On)
14		oe0 4161	. . . . . . 7 |- (A e. On -> (A ^o (/)) = 1o)
15	13, 14	syl 10	. . . . . 6 |- ((B e. On /\ A e. B) -> (A ^o (/)) = 1o)
16		oe0 4161	. . . . . . 7 |- (B e. On -> (B ^o (/)) = 1o)
17	16	adantr 389	. . . . . 6 |- ((B e. On /\ A e. B) -> (B ^o (/)) = 1o)
18	15, 17	eqtr4d 1510	. . . . 5 |- ((B e. On /\ A e. B) -> (A ^o (/)) = (B ^o (/)))
19		eqimss 2109	. . . . 5 |- ((A ^o (/)) = (B ^o (/)) -> (A ^o (/)) (_ (B ^o (/)))
20	18, 19	syl 10	. . . 4 |- ((B e. On /\ A e. B) -> (A ^o (/)) (_ (B ^o (/)))
21		omwordri 4203	. . . . . . . . . . . . . 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)))
22		oecl 4172	. . . . . . . . . . . . . . 15 |- ((A e. On /\ y e. On) -> (A ^o y) e. On)
23	22	3adant2 798	. . . . . . . . . . . . . 14 |- ((A e. On /\ B e. On /\ y e. On) -> (A ^o y) e. On)
24		oecl 4172	. . . . . . . . . . . . . . 15 |- ((B e. On /\ y e. On) -> (B ^o y) e. On)
25	24	3adant1 797	. . . . . . . . . . . . . 14 |- ((A e. On /\ B e. On /\ y e. On) -> (B ^o y) e. On)
26		3simp1 788	. . . . . . . . . . . . . 14 |- ((A e. On /\ B e. On /\ y e. On) -> A e. On)
27	21, 23, 25, 26	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)))
28	27	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))
29	28	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))
30		omwordi 4202	. . . . . . . . . . . . . 14 |- ((A e. On /\ B e. On /\ (B ^o y) e. On) -> (A (_ B -> ((B ^o y) .o A) (_ ((B ^o y) .o B)))
31	30, 25	syld3an3 870	. . . . . . . . . . . . 13 |- ((A e. On /\ B e. On /\ y e. On) -> (A (_ B -> ((B ^o y) .o A) (_ ((B ^o y) .o B)))
32	31	imp 350	. . . . . . . . . . . 12 |- (((A e. On /\ B e. On /\ y e. On) /\ A (_ B) -> ((B ^o y) .o A) (_ ((B ^o y) .o B))
33	32	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))
34	29, 33	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))
35		oesuc 4166	. . . . . . . . . . . 12 |- ((A e. On /\ y e. On) -> (A ^o suc y) = ((A ^o y) .o A))
36	35	3adant2 798	. . . . . . . . . . 11 |- ((A e. On /\ B e. On /\ y e. On) -> (A ^o suc y) = ((A ^o y) .o A))
37	36	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))
38		oesuc 4166	. . . . . . . . . . . 12 |- ((B e. On /\ y e. On) -> (B ^o suc y) = ((B ^o y) .o B))
39	38	3adant1 797	. . . . . . . . . . 11 |- ((A e. On /\ B e. On /\ y e. On) -> (B ^o suc y) = ((B ^o y) .o B))
40	39	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))
41	34, 37, 40	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))
42	41	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))))
43	42	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))))))
44	43	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))))))
45	44	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))))
46		pm3.26 319	. . . . . . 7 |- ((B e. On /\ A e. B) -> B e. On)
47	13, 46	jca 288	. . . . . 6 |- ((B e. On /\ A e. B) -> (A e. On /\ B e. On))
48		onelsst 3000	. . . . . . 7 |- (B e. On -> (A e. B -> A (_ B))
49	48	imp 350	. . . . . 6 |- ((B e. On /\ A e. B) -> A (_ B)
50	47, 49	jca 288	. . . . 5 |- ((B e. On /\ A e. B) -> ((A e. On /\ B e. On) /\ A (_ B))
51	45, 50	syl5 21	. . . 4 |- (y e. On -> ((B e. On /\ A e. B) -> ((A ^o y) (_ (B ^o y) -> (A ^o suc y) (_ (B ^o suc y))))
52		opreq1 3968	. . . . . . . . . . 11 |- (A = (/) -> (A ^o x) = ((/) ^o x))
53	52	sseq1d 2088	. . . . . . . . . 10 |- (A = (/) -> ((A ^o x) (_ (B ^o x) <-> ((/) ^o x) (_ (B ^o x)))
54		oe0m1 4160	. . . . . . . . . . . . 13 |- (x e. On -> ((/) e. x <-> ((/) ^o x) = (/)))
55	54	biimpa 416	. . . . . . . . . . . 12 |- ((x e. On /\ (/) e. x) -> ((/) ^o x) = (/))
56		visset 1813	. . . . . . . . . . . . 13 |- x e. V
57		limelon 3032	. . . . . . . . . . . . 13 |- ((x e. V /\ Lim x) -> x e. On)
58	56, 57	mpan 695	. . . . . . . . . . . 12 |- (Lim x -> x e. On)
59		0ellim 3031	. . . . . . . . . . . 12 |- (Lim x -> (/) e. x)
60	55, 58, 59	sylanc 471	. . . . . . . . . . 11 |- (Lim x -> ((/) ^o x) = (/))
61		0ss 2301	. . . . . . . . . . . 12 |- (/) (_ (B ^o x)
62	61	a1i 8	. . . . . . . . . . 11 |- (Lim x -> (/) (_ (B ^o x))
63	60, 62	eqsstrd 2095	. . . . . . . . . 10 |- (Lim x -> ((/) ^o x) (_ (B ^o x))
64	53, 63	syl5bir 210	. . . . . . . . 9 |- (A = (/) -> (Lim x -> (A ^o x) (_ (B ^o x)))
65	64	adantl 388	. . . . . . . 8 |- (((B e. On /\ A e. B) /\ A = (/)) -> (Lim x -> (A ^o x) (_ (B ^o x)))
66	65	a1dd 42	. . . . . . 7 |- (((B e. On /\ A e. B) /\ A = (/)) -> (Lim x -> (A.y e. x (A ^o y) (_ (B ^o y) -> (A ^o x) (_ (B ^o x))))
67		oelim 4169	. . . . . . . . . . . . 13 |- (((A e. On /\ (x