Theorem oelim2 7055

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 4803	. . . . . 6 |- ( ( B e. C /\ Lim B ) -> B e. On )
2		0ellim 4802	. . . . . . 7 |- ( Lim B -> (/) e. B )
3	2	adantl 466	. . . . . 6 |- ( ( B e. C /\ Lim B ) -> (/) e. B )
4		oe0m1 6982	. . . . . . 7 |- ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
5	4	biimpa 484	. . . . . 6 |- ( ( B e. On /\ (/) e. B ) -> ( (/) ^o B ) = (/) )
6	1, 3, 5	syl2anc 661	. . . . 5 |- ( ( B e. C /\ Lim B ) -> ( (/) ^o B ) = (/) )
7		eldif 3359	. . . . . . . . 9 |- ( x e. ( B \ 1o ) <-> ( x e. B /\ -. x e. 1o ) )
8		limord 4799	. . . . . . . . . . . 12 |- ( Lim B -> Ord B )
9		ordelon 4764	. . . . . . . . . . . 12 |- ( ( Ord B /\ x e. B ) -> x e. On )
10	8, 9	sylan 471	. . . . . . . . . . 11 |- ( ( Lim B /\ x e. B ) -> x e. On )
11		on0eln0 4795	. . . . . . . . . . . . 13 |- ( x e. On -> ( (/) e. x <-> x =/= (/) ) )
12		el1o 6960	. . . . . . . . . . . . . 14 |- ( x e. 1o <-> x = (/) )
13	12	necon3bbii 2633	. . . . . . . . . . . . 13 |- ( -. x e. 1o <-> x =/= (/) )
14	11, 13	syl6bbr 263	. . . . . . . . . . . 12 |- ( x e. On -> ( (/) e. x <-> -. x e. 1o ) )
15		oe0m1 6982	. . . . . . . . . . . . 13 |- ( x e. On -> ( (/) e. x <-> ( (/) ^o x ) = (/) ) )
16	15	biimpd 207	. . . . . . . . . . . 12 |- ( x e. On -> ( (/) e. x -> ( (/) ^o x ) = (/) ) )
17	14, 16	sylbird 235	. . . . . . . . . . 11 |- ( x e. On -> ( -. x e. 1o -> ( (/) ^o x ) = (/) ) )
18	10, 17	syl 16	. . . . . . . . . 10 |- ( ( Lim B /\ x e. B ) -> ( -. x e. 1o -> ( (/) ^o x ) = (/) ) )
19	18	impr 619	. . . . . . . . 9 |- ( ( Lim B /\ ( x e. B /\ -. x e. 1o ) ) -> ( (/) ^o x ) = (/) )
20	7, 19	sylan2b 475	. . . . . . . 8 |- ( ( Lim B /\ x e. ( B \ 1o ) ) -> ( (/) ^o x ) = (/) )
21	20	iuneq2dv 4213	. . . . . . 7 |- ( Lim B -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = U_ x e. ( B \ 1o ) (/) )
22		df-1o 6941	. . . . . . . . . . 11 |- 1o = suc (/)
23		limsuc 6481	. . . . . . . . . . . 12 |- ( Lim B -> ( (/) e. B <-> suc (/) e. B ) )
24	2, 23	mpbid 210	. . . . . . . . . . 11 |- ( Lim B -> suc (/) e. B )
25	22, 24	syl5eqel 2527	. . . . . . . . . 10 |- ( Lim B -> 1o e. B )
26		1on 6948	. . . . . . . . . . 11 |- 1o e. On
27	26	onirri 4846	. . . . . . . . . 10 |- -. 1o e. 1o
28	25, 27	jctir 538	. . . . . . . . 9 |- ( Lim B -> ( 1o e. B /\ -. 1o e. 1o ) )
29		eldif 3359	. . . . . . . . 9 |- ( 1o e. ( B \ 1o ) <-> ( 1o e. B /\ -. 1o e. 1o ) )
30	28, 29	sylibr 212	. . . . . . . 8 |- ( Lim B -> 1o e. ( B \ 1o ) )
31		ne0i 3664	. . . . . . . 8 |- ( 1o e. ( B \ 1o ) -> ( B \ 1o ) =/= (/) )
32		iunconst 4200	. . . . . . . 8 |- ( ( B \ 1o ) =/= (/) -> U_ x e. ( B \ 1o ) (/) = (/) )
33	30, 31, 32	3syl 20	. . . . . . 7 |- ( Lim B -> U_ x e. ( B \ 1o ) (/) = (/) )
34	21, 33	eqtrd 2475	. . . . . 6 |- ( Lim B -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = (/) )
35	34	adantl 466	. . . . 5 |- ( ( B e. C /\ Lim B ) -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = (/) )
36	6, 35	eqtr4d 2478	. . . 4 |- ( ( B e. C /\ Lim B ) -> ( (/) ^o B ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) )
37		oveq1 6119	. . . . 5 |- ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
38		oveq1 6119	. . . . . 6 |- ( A = (/) -> ( A ^o x ) = ( (/) ^o x ) )
39	38	iuneq2d 4218	. . . . 5 |- ( A = (/) -> U_ x e. ( B \ 1o ) ( A ^o x ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) )
40	37, 39	eqeq12d 2457	. . . 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 221	. . 3 |- ( A = (/) -> ( ( B e. C /\ Lim B ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) ) )
42	41	impcom 430	. 2 |- ( ( ( B e. C /\ Lim B ) /\ A = (/) ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
43		oelim 6995	. . 3 |- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ y e. B ( A ^o y ) )
44		limsuc 6481	. . . . . . . . . . . . 13 |- ( Lim B -> ( y e. B <-> suc y e. B ) )
45	44	biimpa 484	. . . . . . . . . . . 12 |- ( ( Lim B /\ y e. B ) -> suc y e. B )
46		nsuceq0 4820	. . . . . . . . . . . . 13 |- suc y =/= (/)
47	46	a1i 11	. . . . . . . . . . . 12 |- ( ( Lim B /\ y e. B ) -> suc y =/= (/) )
48		dif1o 6961	. . . . . . . . . . . 12 |- ( suc y e. ( B \ 1o ) <-> ( suc y e. B /\ suc y =/= (/) ) )
49	45, 47, 48	sylanbrc 664	. . . . . . . . . . 11 |- ( ( Lim B /\ y e. B ) -> suc y e. ( B \ 1o ) )
50	49	ex 434	. . . . . . . . . 10 |- ( Lim B -> ( y e. B -> suc y e. ( B \ 1o ) ) )
51	50	ad2antlr 726	. . . . . . . . 9 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> suc y e. ( B \ 1o ) ) )
52		sssucid 4817	. . . . . . . . . . 11 |- y C_ suc y
53		ordelon 4764	. . . . . . . . . . . . . . . . 17 |- ( ( Ord B /\ y e. B ) -> y e. On )
54	8, 53	sylan 471	. . . . . . . . . . . . . . . 16 |- ( ( Lim B /\ y e. B ) -> y e. On )
55		suceloni 6445	. . . . . . . . . . . . . . . . 17 |- ( y e. On -> suc y e. On )
56	55	ancli 551	. . . . . . . . . . . . . . . 16 |- ( y e. On -> ( y e. On /\ suc y e. On ) )
57	54, 56	syl 16	. . . . . . . . . . . . . . 15 |- ( ( Lim B /\ y e. B ) -> ( y e. On /\ suc y e. On ) )
58		id 22	. . . . . . . . . . . . . . . . 17 |- ( ( y e. On /\ suc y e. On /\ A e. On ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
59	58	3expa 1187	. . . . . . . . . . . . . . . 16 |- ( ( ( y e. On /\ suc y e. On ) /\ A e. On ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
60	59	ancoms 453	. . . . . . . . . . . . . . 15 |- ( ( A e. On /\ ( y e. On /\ suc y e. On ) ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
61	57, 60	sylan2 474	. . . . . . . . . . . . . 14 |- ( ( A e. On /\ ( Lim B /\ y e. B ) ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
62	61	anassrs 648	. . . . . . . . . . . . 13 |- ( ( ( A e. On /\ Lim B ) /\ y e. B ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
63		oewordi 7051	. . . . . . . . . . . . 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 ) ) )
64	62, 63	sylan 471	. . . . . . . . . . . 12 |- ( ( ( ( A e. On /\ Lim B ) /\ y e. B ) /\ (/) e. A ) -> ( y C_ suc y -> ( A ^o y ) C_ ( A ^o suc y ) ) )
65	64	an32s 802	. . . . . . . . . . 11 |- ( ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) /\ y e. B ) -> ( y C_ suc y -> ( A ^o y ) C_ ( A ^o suc y ) ) )
66	52, 65	mpi 17	. . . . . . . . . 10 |- ( ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) /\ y e. B ) -> ( A ^o y ) C_ ( A ^o suc y ) )
67	66	ex 434	. . . . . . . . 9 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> ( A ^o y ) C_ ( A ^o suc y ) ) )
68	51, 67	jcad 533	. . . . . . . 8 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> ( suc y e. ( B \ 1o ) /\ ( A ^o y ) C_ ( A ^o suc y ) ) ) )
69		oveq2 6120	. . . . . . . . . 10 |- ( x = suc y -> ( A ^o x ) = ( A ^o suc y ) )
70	69	sseq2d 3405	. . . . . . . . 9 |- ( x = suc y -> ( ( A ^o y ) C_ ( A ^o x ) <-> ( A ^o y ) C_ ( A ^o suc y ) ) )
71	70	rspcev 3094	. . . . . . . 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 ) )
72	68, 71	syl6 33	. . . . . . 7 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> E. x e. ( B \ 1o ) ( A ^o y ) C_ ( A ^o x ) ) )
73	72	ralrimiv 2819	. . . . . 6 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> A. y e. B E. x e. ( B \ 1o ) ( A ^o y ) C_ ( A ^o x ) )
74		iunss2 4236	. . . . . 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 ) )
75	73, 74	syl 16	. . . . 5 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> U_ y e. B ( A ^o y ) C_ U_ x e. ( B \ 1o ) ( A ^o x ) )
76		difss 3504	. . . . . . . 8 |- ( B \ 1o ) C_ B
77		iunss1 4203	. . . . . . . 8 |- ( ( B \ 1o ) C_ B -> U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ x e. B ( A ^o x ) )
78	76, 77	ax-mp 5	. . . . . . 7 |- U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ x e. B ( A ^o x )
79		oveq2 6120	. . . . . . . 8 |- ( x = y -> ( A ^o x ) = ( A ^o y ) )
80	79	cbviunv 4230	. . . . . . 7 |- U_ x e. B ( A ^o x ) = U_ y e. B ( A ^o y )
81	78, 80	sseqtri 3409	. . . . . 6 |- U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ y e. B ( A ^o y )
82	81	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 ) )
83	75, 82	eqssd 3394	. . . 4 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> U_ y e. B ( A ^o y ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
84	83	adantlrl 719	. . 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 ) )
85	43, 84	eqtrd 2475	. 2 |- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
86	42, 85	oe0lem 6974	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 369   /\ w3a 965   = wceq 1369   e. wcel 1756   =/= wne 2620   A.wral 2736   E.wrex 2737   \ cdif 3346   C_ wss 3349   (/)c0 3658   U_ciun 4192   Ord word 4739   Oncon0 4740   Lim wlim 4741   suc csuc 4742  (class class class)co 6112   1oc1o 6934   ^o coe 6940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-recs 6853  df-rdg 6887  df-1o 6941  df-2o 6942  df-oadd 6945  df-omul 6946  df-oexp 6947

This theorem is referenced by:  oelimcl  7060  oaabs2  7105  omabs  7107