Theorem oelim2 4280

Description: Ordinal exponentiation with a limit exponent. Part of Exercise 4.36 of [Mendelson] p. 250.

Assertion

Ref	Expression
oelim2	|- ((A e. On /\ (B e. C /\ Lim B)) -> (A ^o B) = U_x e. (B \ 1o)(A ^o x))

Distinct variable groups:   x,A   x,B

Proof of Theorem oelim2

Step	Hyp	Ref	Expression
1		opreq1 4026	. . . . 5 |- (A = (/) -> (A ^o B) = ((/) ^o B))
2		opreq1 4026	. . . . . . 7 |- (A = (/) -> (A ^o x) = ((/) ^o x))
3	2	adantr 398	. . . . . 6 |- ((A = (/) /\ x e. (B \ 1o)) -> (A ^o x) = ((/) ^o x))
4	3	iuneq2dv 2636	. . . . 5 |- (A = (/) -> U_x e. (B \ 1o)(A ^o x) = U_x e. (B \ 1o)((/) ^o x))
5	1, 4	eqeq12d 1536	. . . 4 |- (A = (/) -> ((A ^o B) = U_x e. (B \ 1o)(A ^o x) <-> ((/) ^o B) = U_x e. (B \ 1o)((/) ^o x)))
6		oe0m1 4218	. . . . . . 7 |- (B e. On -> ((/) e. B <-> ((/) ^o B) = (/)))
7	6	biimpa 425	. . . . . 6 |- ((B e. On /\ (/) e. B) -> ((/) ^o B) = (/))
8		limelon 3089	. . . . . 6 |- ((B e. C /\ Lim B) -> B e. On)
9		0ellim 3088	. . . . . . 7 |- (Lim B -> (/) e. B)
10	9	adantl 397	. . . . . 6 |- ((B e. C /\ Lim B) -> (/) e. B)
11	7, 8, 10	sylanc 482	. . . . 5 |- ((B e. C /\ Lim B) -> ((/) ^o B) = (/))
12		ordelon 3028	. . . . . . . . . . . . 13 |- ((Ord B /\ x e. B) -> x e. On)
13		limord 3085	. . . . . . . . . . . . 13 |- (Lim B -> Ord B)
14	12, 13	sylan 459	. . . . . . . . . . . 12 |- ((Lim B /\ x e. B) -> x e. On)
15		on0eln0 3081	. . . . . . . . . . . . . 14 |- (x e. On -> ((/) e. x <-> x =/= (/)))
16		el1o 4204	. . . . . . . . . . . . . . 15 |- (x e. 1o <-> x = (/))
17	16	necon3bbii 1644	. . . . . . . . . . . . . 14 |- (-. x e. 1o <-> x =/= (/))
18	15, 17	syl6bbr 549	. . . . . . . . . . . . 13 |- (x e. On -> ((/) e. x <-> -. x e. 1o))
19		oe0m1 4218	. . . . . . . . . . . . . 14 |- (x e. On -> ((/) e. x <-> ((/) ^o x) = (/)))
20	19	biimpd 160	. . . . . . . . . . . . 13 |- (x e. On -> ((/) e. x -> ((/) ^o x) = (/)))
21	18, 20	sylbird 212	. . . . . . . . . . . 12 |- (x e. On -> (-. x e. 1o -> ((/) ^o x) = (/)))
22	14, 21	syl 10	. . . . . . . . . . 11 |- ((Lim B /\ x e. B) -> (-. x e. 1o -> ((/) ^o x) = (/)))
23	22	ex 380	. . . . . . . . . 10 |- (Lim B -> (x e. B -> (-. x e. 1o -> ((/) ^o x) = (/))))
24	23	imp32 370	. . . . . . . . 9 |- ((Lim B /\ (x e. B /\ -. x e. 1o)) -> ((/) ^o x) = (/))
25		eldif 2108	. . . . . . . . 9 |- (x e. (B \ 1o) <-> (x e. B /\ -. x e. 1o))
26	24, 25	sylan2b 463	. . . . . . . 8 |- ((Lim B /\ x e. (B \ 1o)) -> ((/) ^o x) = (/))
27	26	iuneq2dv 2636	. . . . . . 7 |- (Lim B -> U_x e. (B \ 1o)((/) ^o x) = U_x e. (B \ 1o)(/))
28		limsuc 3177	. . . . . . . . . . . 12 |- (Lim B -> ((/) e. B <-> suc (/) e. B))
29	9, 28	mpbid 202	. . . . . . . . . . 11 |- (Lim B -> suc (/) e. B)
30		df-1o 4191	. . . . . . . . . . 11 |- 1o = suc (/)
31	29, 30	syl5eqel 1599	. . . . . . . . . 10 |- (Lim B -> 1o e. B)
32		1on 4196	. . . . . . . . . . 11 |- 1o e. On
33	32	onirri 3154	. . . . . . . . . 10 |- -. 1o e. 1o
34	31, 33	jctir 300	. . . . . . . . 9 |- (Lim B -> (1o e. B /\ -. 1o e. 1o))
35		eldif 2108	. . . . . . . . 9 |- (1o e. (B \ 1o) <-> (1o e. B /\ -. 1o e. 1o))
36	34, 35	sylibr 207	. . . . . . . 8 |- (Lim B -> 1o e. (B \ 1o))
37		ne0i 2337	. . . . . . . 8 |- (1o e. (B \ 1o) -> (B \ 1o) =/= (/))
38		iunconst 2626	. . . . . . . 8 |- ((B \ 1o) =/= (/) -> U_x e. (B \ 1o)(/) = (/))
39	36, 37, 38	3syl 20	. . . . . . 7 |- (Lim B -> U_x e. (B \ 1o)(/) = (/))
40	27, 39	eqtrd 1554	. . . . . 6 |- (Lim B -> U_x e. (B \ 1o)((/) ^o x) = (/))
41	40	adantl 397	. . . . 5 |- ((B e. C /\ Lim B) -> U_x e. (B \ 1o)((/) ^o x) = (/))
42	11, 41	eqtr4d 1557	. . . 4 |- ((B e. C /\ Lim B) -> ((/) ^o B) = U_x e. (B \ 1o)((/) ^o x))
43	5, 42	syl5bir 217	. . 3 |- (A = (/) -> ((B e. C /\ Lim B) -> (A ^o B) = U_x e. (B \ 1o)(A ^o x)))
44	43	impcom 358	. 2 |- (((B e. C /\ Lim B) /\ A = (/)) -> (A ^o B) = U_x e. (B \ 1o)(A ^o x))
45		oelim 4227	. . 3 |- (((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) -> (A ^o B) = U_y e. B (A ^o y))
46		limsuc 3177	. . . . . . . . . . . . . 14 |- (Lim B -> (y e. B <-> suc y e. B))
47	46	biimpa 425	. . . . . . . . . . . . 13 |- ((Lim B /\ y e. B) -> suc y e. B)
48		nsuceq0 3110	. . . . . . . . . . . . . 14 |- suc y =/= (/)
49		el1o 4204	. . . . . . . . . . . . . 14 |- (suc y e. 1o <-> suc y = (/))
50	48, 49	nemtbir 1688	. . . . . . . . . . . . 13 |- -. suc y e. 1o
51	47, 50	jctir 300	. . . . . . . . . . . 12 |- ((Lim B /\ y e. B) -> (suc y e. B /\ -. suc y e. 1o))
52		eldif 2108	. . . . . . . . . . . 12 |- (suc y e. (B \ 1o) <-> (suc y e. B /\ -. suc y e. 1o))
53	51, 52	sylibr 207	. . . . . . . . . . 11 |- ((Lim B /\ y e. B) -> suc y e. (B \ 1o))
54	53	ex 380	. . . . . . . . . 10 |- (Lim B -> (y e. B -> suc y e. (B \ 1o)))
55	54	ad2antlr 414	. . . . . . . . 9 |- (((A e. On /\ Lim B) /\ (/) e. A) -> (y e. B -> suc y e. (B \ 1o)))
56		sssucid 3104	. . . . . . . . . . 11 |- y (_ suc y
57		oewordi 4276	. . . . . . . . . . . . 13 |- (((y e. On /\ suc y e. On /\ A e. On) /\ (/) e. A) -> (y (_ suc y -> (A ^o y) (_ (A ^o suc y)))
58		id 59	. . . . . . . . . . . . . . . . 17 |- ((y e. On /\ suc y e. On /\ A e. On) -> (y e. On /\ suc y e. On /\ A e. On))
59	58	3expa 845	. . . . . . . . . . . . . . . 16 |- (((y e. On /\ suc y e. On) /\ A e. On) -> (y e. On /\ suc y e. On /\ A e. On))
60	59	ancoms 447	. . . . . . . . . . . . . . 15 |- ((A e. On /\ (y e. On /\ suc y e. On)) -> (y e. On /\ suc y e. On /\ A e. On))
61		ordelon 3028	. . . . . . . . . . . . . . . . 17 |- ((Ord B /\ y e. B) -> y e. On)
62	61, 13	sylan 459	. . . . . . . . . . . . . . . 16 |- ((Lim B /\ y e. B) -> y e. On)
63		suceloni 3119	. . . . . . . . . . . . . . . . 17 |- (y e. On -> suc y e. On)
64	63	ancli 303	. . . . . . . . . . . . . . . 16 |- (y e. On -> (y e. On /\ suc y e. On))
65	62, 64	syl 10	. . . . . . . . . . . . . . 15 |- ((Lim B /\ y e. B) -> (y e. On /\ suc y e. On))
66	60, 65	sylan2 462	. . . . . . . . . . . . . 14 |- ((A e. On /\ (Lim B /\ y e. B)) -> (y e. On /\ suc y e. On /\ A e. On))
67	66	anassrs 452	. . . . . . . . . . . . 13 |- (((A e. On /\ Lim B) /\ y e. B) -> (y e. On /\ suc y e. On /\ A e. On))
68	57, 67	sylan 459	. . . . . . . . . . . 12 |- ((((A e. On /\ Lim B) /\ y e. B) /\ (/) e. A) -> (y (_ suc y -> (A ^o y) (_ (A ^o suc y)))
69	68	an1rs 500	. . . . . . . . . . 11 |- ((((A e. On /\ Lim B) /\ (/) e. A) /\ y e. B) -> (y (_ suc y -> (A ^o y) (_ (A ^o suc y)))
70	56, 69	mpi 44	. . . . . . . . . 10 |- ((((A e. On /\ Lim B) /\ (/) e. A) /\ y e. B) -> (A ^o y) (_ (A ^o suc y))
71	70	ex 380	. . . . . . . . 9 |- (((A e. On /\ Lim B) /\ (/) e. A) -> (y e. B -> (A ^o y) (_ (A ^o suc y)))
72	55, 71	jcad 611	. . . . . . . 8 |- (((A e. On /\ Lim B) /\ (/) e. A) -> (y e. B -> (suc y e. (B \ 1o) /\ (A ^o y) (_ (A ^o suc y))))
73		opreq2 4027	. . . . . . . . . 10 |- (x = suc y -> (A ^o x) = (A ^o suc y))
74	73	sseq2d 2140	. . . . . . . . 9 |- (x = suc y -> ((A ^o y) (_ (A ^o x) <-> (A ^o y) (_ (A ^o suc y)))
75	74	rcla4ev 1924	. . . . . . . 8 |- ((suc y e. (B \ 1o) /\ (A ^o y) (_ (A ^o suc y)) -> E.x e. (B \ 1o)(A ^o y) (_ (A ^o x))
76	72, 75	syl6 22	. . . . . . 7 |- (((A e. On /\ Lim B) /\ (/) e. A) -> (y e. B -> E.x e. (B \ 1o)(A ^o y) (_ (A ^o x)))
77	76	r19.21aiv 1760	. . . . . 6 |- (((A e. On /\ Lim B) /\ (/) e. A) -> A.y e. B E.x e. (B \ 1o)(A ^o y) (_ (A ^o x))
78		iunss2 2649	. . . . . 6 |- (A.y e. B E.x e. (B \ 1o)(A ^o y) (_ (A ^o x) -> U_y e. B (A ^o y) (_ U_x e. (B \ 1o)(A ^o x))
79	77, 78	syl 10	. . . . 5 |- (((A e. On /\ Lim B) /\ (/) e. A) -> U_y e. B (A ^o y) (_ U_x e. (B \ 1o)(A ^o x))
80		difss 2218	. . . . . . . 8 |- (B \