Theorem oelim2 7246

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 5443	. . . . . 6 |- ( ( B e. C /\ Lim B ) -> B e. On )
2		0ellim 5442	. . . . . . 7 |- ( Lim B -> (/) e. B )
3	2	adantl 467	. . . . . 6 |- ( ( B e. C /\ Lim B ) -> (/) e. B )
4		oe0m1 7173	. . . . . . 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 3384	. . . . . . . . 9 |- ( x e. ( B \ 1o ) <-> ( x e. B /\ -. x e. 1o ) )
8		limord 5439	. . . . . . . . . . . 12 |- ( Lim B -> Ord B )
9		ordelon 5404	. . . . . . . . . . . 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 5435	. . . . . . . . . . . . 13 |- ( x e. On -> ( (/) e. x <-> x =/= (/) ) )
12		el1o 7151	. . . . . . . . . . . . . 14 |- ( x e. 1o <-> x = (/) )
13	12	necon3bbii 2643	. . . . . . . . . . . . 13 |- ( -. x e. 1o <-> x =/= (/) )
14	11, 13	syl6bbr 266	. . . . . . . . . . . 12 |- ( x e. On -> ( (/) e. x <-> -. x e. 1o ) )
15		oe0m1 7173	. . . . . . . . . . . . 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 4259	. . . . . . 7 |- ( Lim B -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = U_ x e. ( B \ 1o ) (/) )
22		df-1o 7132	. . . . . . . . . . 11 |- 1o = suc (/)
23		limsuc 6629	. . . . . . . . . . . 12 |- ( Lim B -> ( (/) e. B <-> suc (/) e. B ) )
24	2, 23	mpbid 213	. . . . . . . . . . 11 |- ( Lim B -> suc (/) e. B )
25	22, 24	syl5eqel 2505	. . . . . . . . . 10 |- ( Lim B -> 1o e. B )
26		1on 7139	. . . . . . . . . . 11 |- 1o e. On
27	26	onirri 5486	. . . . . . . . . 10 |- -. 1o e. 1o
28	25, 27	jctir 540	. . . . . . . . 9 |- ( Lim B -> ( 1o e. B /\ -. 1o e. 1o ) )
29		eldif 3384	. . . . . . . . 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 3705	. . . . . . . 8 |- ( 1o e. ( B \ 1o ) -> ( B \ 1o ) =/= (/) )
32		iunconst 4246	. . . . . . . 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 2457	. . . . . 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 2460	. . . 4 |- ( ( B e. C /\ Lim B ) -> ( (/) ^o B ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) )
37		oveq1 6251	. . . . 5 |- ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
38		oveq1 6251	. . . . . 6 |- ( A = (/) -> ( A ^o x ) = ( (/) ^o x ) )
39	38	iuneq2d 4264	. . . . 5 |- ( A = (/) -> U_ x e. ( B \ 1o ) ( A ^o x ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) )
40	37, 39	eqeq12d 2438	. . . 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 7186	. . 3 |- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ y e. B ( A ^o y ) )
44		limsuc 6629	. . . . . . . . . . . . 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 5460	. . . . . . . . . . . . 13 |- suc y =/= (/)
47	46	a1i 11	. . . . . . . . . . . 12 |- ( ( Lim B /\ y e. B ) -> suc y =/= (/) )
48		dif1o 7152	. . . . . . . . . . . 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 5457	. . . . . . . . . . 11 |- y C_ suc y
53		ordelon 5404	. . . . . . . . . . . . . . . . 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 6593	. . . . . . . . . . . . . . . 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 22	. . . . . . . . . . . . . . . . 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 7242	. . . . . . . . . . . . 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 20	. . . . . . . . . 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 6252	. . . . . . . . . 10 |- ( x = suc y -> ( A ^o x ) = ( A ^o suc y ) )
69	68	sseq2d 3430	. . . . . . . . 9 |- ( x = suc y -> ( ( A ^o y ) C_ ( A ^o x ) <-> ( A ^o y ) C_ ( A ^o suc y ) ) )
70	69	rspcev 3120	. . . . . . . 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 2772	. . . . . 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 4282	. . . . . 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 3530	. . . . . . . 8 |- ( B \ 1o ) C_ B
76		iunss1 4249	. . . . . . . 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 6252	. . . . . . . 8 |- ( x = y -> ( A ^o x ) = ( A ^o y ) )
79	78	cbviunv 4276	. . . . . . 7 |- U_ x e. B ( A ^o x ) = U_ y e. B ( A ^o y )
80	77, 79	sseqtri 3434	. . . . . 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 3419	. . . 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 2457	. 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 7165	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 1872   =/= wne 2594   A.wral 2709   E.wrex 2710   \ cdif 3371   C_ wss 3374   (/)c0 3699   U_ciun 4237   Ord word 5379   Oncon0 5380   Lim wlim 5381   suc csuc 5382  (class class class)co 6244   1oc1o 7125   ^o coe 7131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536

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 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-omul 7137  df-oexp 7138

This theorem is referenced by:  oelimcl  7251  oaabs2  7296  omabs  7298