Theorem oelim2 7304

Description: Ordinal exponentiation with a limit exponent. Part of Exercise 4.36 of [Mendelson] p. 250. (Contributed by NM, 6-Jan-2005.)

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

Allowed substitution hint:   C( x)

Proof of Theorem oelim2

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		limelon 5505	. . . . . 6 |- ( ( B e. C /\ Lim B ) -> B e. On )
2		0ellim 5504	. . . . . . 7 |- ( Lim B -> (/) e. B )
3	2	adantl 467	. . . . . 6 |- ( ( B e. C /\ Lim B ) -> (/) e. B )
4		oe0m1 7231	. . . . . . 7 |- ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
5	4	biimpa 486	. . . . . 6 |- ( ( B e. On /\ (/) e. B ) -> ( (/) ^o B ) = (/) )
6	1, 3, 5	syl2anc 665	. . . . 5 |- ( ( B e. C /\ Lim B ) -> ( (/) ^o B ) = (/) )
7		eldif 3452	. . . . . . . . 9 |- ( x e. ( B \ 1o ) <-> ( x e. B /\ -. x e. 1o ) )
8		limord 5501	. . . . . . . . . . . 12 |- ( Lim B -> Ord B )
9		ordelon 5466	. . . . . . . . . . . 12 |- ( ( Ord B /\ x e. B ) -> x e. On )
10	8, 9	sylan 473	. . . . . . . . . . 11 |- ( ( Lim B /\ x e. B ) -> x e. On )
11		on0eln0 5497	. . . . . . . . . . . . 13 |- ( x e. On -> ( (/) e. x <-> x =/= (/) ) )
12		el1o 7209	. . . . . . . . . . . . . 14 |- ( x e. 1o <-> x = (/) )
13	12	necon3bbii 2692	. . . . . . . . . . . . 13 |- ( -. x e. 1o <-> x =/= (/) )
14	11, 13	syl6bbr 266	. . . . . . . . . . . 12 |- ( x e. On -> ( (/) e. x <-> -. x e. 1o ) )
15		oe0m1 7231	. . . . . . . . . . . . 13 |- ( x e. On -> ( (/) e. x <-> ( (/) ^o x ) = (/) ) )
16	15	biimpd 210	. . . . . . . . . . . 12 |- ( x e. On -> ( (/) e. x -> ( (/) ^o x ) = (/) ) )
17	14, 16	sylbird 238	. . . . . . . . . . 11 |- ( x e. On -> ( -. x e. 1o -> ( (/) ^o x ) = (/) ) )
18	10, 17	syl 17	. . . . . . . . . 10 |- ( ( Lim B /\ x e. B ) -> ( -. x e. 1o -> ( (/) ^o x ) = (/) ) )
19	18	impr 623	. . . . . . . . 9 |- ( ( Lim B /\ ( x e. B /\ -. x e. 1o ) ) -> ( (/) ^o x ) = (/) )
20	7, 19	sylan2b 477	. . . . . . . 8 |- ( ( Lim B /\ x e. ( B \ 1o ) ) -> ( (/) ^o x ) = (/) )
21	20	iuneq2dv 4324	. . . . . . 7 |- ( Lim B -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = U_ x e. ( B \ 1o ) (/) )
22		df-1o 7190	. . . . . . . . . . 11 |- 1o = suc (/)
23		limsuc 6690	. . . . . . . . . . . 12 |- ( Lim B -> ( (/) e. B <-> suc (/) e. B ) )
24	2, 23	mpbid 213	. . . . . . . . . . 11 |- ( Lim B -> suc (/) e. B )
25	22, 24	syl5eqel 2521	. . . . . . . . . 10 |- ( Lim B -> 1o e. B )
26		1on 7197	. . . . . . . . . . 11 |- 1o e. On
27	26	onirri 5548	. . . . . . . . . 10 |- -. 1o e. 1o
28	25, 27	jctir 540	. . . . . . . . 9 |- ( Lim B -> ( 1o e. B /\ -. 1o e. 1o ) )
29		eldif 3452	. . . . . . . . 9 |- ( 1o e. ( B \ 1o ) <-> ( 1o e. B /\ -. 1o e. 1o ) )
30	28, 29	sylibr 215	. . . . . . . 8 |- ( Lim B -> 1o e. ( B \ 1o ) )
31		ne0i 3773	. . . . . . . 8 |- ( 1o e. ( B \ 1o ) -> ( B \ 1o ) =/= (/) )
32		iunconst 4311	. . . . . . . 8 |- ( ( B \ 1o ) =/= (/) -> U_ x e. ( B \ 1o ) (/) = (/) )
33	30, 31, 32	3syl 18	. . . . . . 7 |- ( Lim B -> U_ x e. ( B \ 1o ) (/) = (/) )
34	21, 33	eqtrd 2470	. . . . . 6 |- ( Lim B -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = (/) )
35	34	adantl 467	. . . . 5 |- ( ( B e. C /\ Lim B ) -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = (/) )
36	6, 35	eqtr4d 2473	. . . 4 |- ( ( B e. C /\ Lim B ) -> ( (/) ^o B ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) )
37		oveq1 6312	. . . . 5 |- ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
38		oveq1 6312	. . . . . 6 |- ( A = (/) -> ( A ^o x ) = ( (/) ^o x ) )
39	38	iuneq2d 4329	. . . . 5 |- ( A = (/) -> U_ x e. ( B \ 1o ) ( A ^o x ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) )
40	37, 39	eqeq12d 2451	. . . 4 |- ( A = (/) -> ( ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) <-> ( (/) ^o B ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) ) )
41	36, 40	syl5ibr 224	. . 3 |- ( A = (/) -> ( ( B e. C /\ Lim B ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) ) )
42	41	impcom 431	. 2 |- ( ( ( B e. C /\ Lim B ) /\ A = (/) ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
43		oelim 7244	. . 3 |- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ y e. B ( A ^o y ) )
44		limsuc 6690	. . . . . . . . . . . . 13 |- ( Lim B -> ( y e. B <-> suc y e. B ) )
45	44	biimpa 486	. . . . . . . . . . . 12 |- ( ( Lim B /\ y e. B ) -> suc y e. B )
46		nsuceq0 5522	. . . . . . . . . . . . 13 |- suc y =/= (/)
47	46	a1i 11	. . . . . . . . . . . 12 |- ( ( Lim B /\ y e. B ) -> suc y =/= (/) )
48		dif1o 7210	. . . . . . . . . . . 12 |- ( suc y e. ( B \ 1o ) <-> ( suc y e. B /\ suc y =/= (/) ) )
49	45, 47, 48	sylanbrc 668	. . . . . . . . . . 11 |- ( ( Lim B /\ y e. B ) -> suc y e. ( B \ 1o ) )
50	49	ex 435	. . . . . . . . . 10 |- ( Lim B -> ( y e. B -> suc y e. ( B \ 1o ) ) )
51	50	ad2antlr 731	. . . . . . . . 9 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> suc y e. ( B \ 1o ) ) )
52		sssucid 5519	. . . . . . . . . . 11 |- y C_ suc y
53		ordelon 5466	. . . . . . . . . . . . . . . . 17 |- ( ( Ord B /\ y e. B ) -> y e. On )
54	8, 53	sylan 473	. . . . . . . . . . . . . . . 16 |- ( ( Lim B /\ y e. B ) -> y e. On )
55		suceloni 6654	. . . . . . . . . . . . . . . 16 |- ( y e. On -> suc y e. On )
56	54, 55	jccir 541	. . . . . . . . . . . . . . 15 |- ( ( Lim B /\ y e. B ) -> ( y e. On /\ suc y e. On ) )
57		id 23	. . . . . . . . . . . . . . . . 17 |- ( ( y e. On /\ suc y e. On /\ A e. On ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
58	57	3expa 1205	. . . . . . . . . . . . . . . 16 |- ( ( ( y e. On /\ suc y e. On ) /\ A e. On ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
59	58	ancoms 454	. . . . . . . . . . . . . . 15 |- ( ( A e. On /\ ( y e. On /\ suc y e. On ) ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
60	56, 59	sylan2 476	. . . . . . . . . . . . . 14 |- ( ( A e. On /\ ( Lim B /\ y e. B ) ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
61	60	anassrs 652	. . . . . . . . . . . . 13 |- ( ( ( A e. On /\ Lim B ) /\ y e. B ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
62		oewordi 7300	. . . . . . . . . . . . 13 |- ( ( ( y e. On /\ suc y e. On /\ A e. On ) /\ (/) e. A ) -> ( y C_ suc y -> ( A ^o y ) C_ ( A ^o suc y ) ) )
63	61, 62	sylan 473	. . . . . . . . . . . 12 |- ( ( ( ( A e. On /\ Lim B ) /\ y e. B ) /\ (/) e. A ) -> ( y C_ suc y -> ( A ^o y ) C_ ( A ^o suc y ) ) )
64	63	an32s 811	. . . . . . . . . . 11 |- ( ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) /\ y e. B ) -> ( y C_ suc y -> ( A ^o y ) C_ ( A ^o suc y ) ) )
65	52, 64	mpi 21	. . . . . . . . . 10 |- ( ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) /\ y e. B ) -> ( A ^o y ) C_ ( A ^o suc y ) )
66	65	ex 435	. . . . . . . . 9 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> ( A ^o y ) C_ ( A ^o suc y ) ) )
67	51, 66	jcad 535	. . . . . . . 8 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> ( suc y e. ( B \ 1o ) /\ ( A ^o y ) C_ ( A ^o suc y ) ) ) )
68		oveq2 6313	. . . . . . . . . 10 |- ( x = suc y -> ( A ^o x ) = ( A ^o suc y ) )
69	68	sseq2d 3498	. . . . . . . . 9 |- ( x = suc y -> ( ( A ^o y ) C_ ( A ^o x ) <-> ( A ^o y ) C_ ( A ^o suc y ) ) )
70	69	rspcev 3188	. . . . . . . 8 |- ( ( suc y e. ( B \ 1o ) /\ ( A ^o y ) C_ ( A ^o suc y ) ) -> E. x e. ( B \ 1o ) ( A ^o y ) C_ ( A ^o x ) )
71	67, 70	syl6 34	. . . . . . 7 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> E. x e. ( B \ 1o ) ( A ^o y ) C_ ( A ^o x ) ) )
72	71	ralrimiv 2844	. . . . . 6 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> A. y e. B E. x e. ( B \ 1o ) ( A ^o y ) C_ ( A ^o x ) )
73		iunss2 4347	. . . . . 6 |- ( A. y e. B E. x e. ( B \ 1o ) ( A ^o y ) C_ ( A ^o x ) -> U_ y e. B ( A ^o y ) C_ U_ x e. ( B \ 1o ) ( A ^o x ) )
74	72, 73	syl 17	. . . . 5 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> U_ y e. B ( A ^o y ) C_ U_ x e. ( B \ 1o ) ( A ^o x ) )
75		difss 3598	. . . . . . . 8 |- ( B \ 1o ) C_ B
76		iunss1 4314	. . . . . . . 8 |- ( ( B \ 1o ) C_ B -> U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ x e. B ( A ^o x ) )
77	75, 76	ax-mp 5	. . . . . . 7 |- U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ x e. B ( A ^o x )
78		oveq2 6313	. . . . . . . 8 |- ( x = y -> ( A ^o x ) = ( A ^o y ) )
79	78	cbviunv 4341	. . . . . . 7 |- U_ x e. B ( A ^o x ) = U_ y e. B ( A ^o y )
80	77, 79	sseqtri 3502	. . . . . 6 |- U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ y e. B ( A ^o y )
81	80	a1i 11	. . . . 5 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ y e. B ( A ^o y ) )
82	74, 81	eqssd 3487	. . . 4 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> U_ y e. B ( A ^o y ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
83	82	adantlrl 724	. . 3 |- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> U_ y e. B ( A ^o y ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
84	43, 83	eqtrd 2470	. 2 |- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
85	42, 84	oe0lem 7223	1 |- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1870   =/= wne 2625   A.wral 2782   E.wrex 2783   \ cdif 3439   C_ wss 3442   (/)c0 3767   U_ciun 4302   Ord word 5441   Oncon0 5442   Lim wlim 5443   suc csuc 5444  (class class class)co 6305   1oc1o 7183   ^o coe 7189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-2o 7191  df-oadd 7194  df-omul 7195  df-oexp 7196

This theorem is referenced by:  oelimcl  7309  oaabs2  7354  omabs  7356