Theorem oelim2 7030

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 4778	. . . . . 6 |- ( ( B e. C /\ Lim B ) -> B e. On )
2		0ellim 4777	. . . . . . 7 |- ( Lim B -> (/) e. B )
3	2	adantl 463	. . . . . 6 |- ( ( B e. C /\ Lim B ) -> (/) e. B )
4		oe0m1 6957	. . . . . . 7 |- ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
5	4	biimpa 481	. . . . . 6 |- ( ( B e. On /\ (/) e. B ) -> ( (/) ^o B ) = (/) )
6	1, 3, 5	syl2anc 656	. . . . 5 |- ( ( B e. C /\ Lim B ) -> ( (/) ^o B ) = (/) )
7		eldif 3335	. . . . . . . . 9 |- ( x e. ( B \ 1o ) <-> ( x e. B /\ -. x e. 1o ) )
8		limord 4774	. . . . . . . . . . . 12 |- ( Lim B -> Ord B )
9		ordelon 4739	. . . . . . . . . . . 12 |- ( ( Ord B /\ x e. B ) -> x e. On )
10	8, 9	sylan 468	. . . . . . . . . . 11 |- ( ( Lim B /\ x e. B ) -> x e. On )
11		on0eln0 4770	. . . . . . . . . . . . 13 |- ( x e. On -> ( (/) e. x <-> x =/= (/) ) )
12		el1o 6935	. . . . . . . . . . . . . 14 |- ( x e. 1o <-> x = (/) )
13	12	necon3bbii 2637	. . . . . . . . . . . . 13 |- ( -. x e. 1o <-> x =/= (/) )
14	11, 13	syl6bbr 263	. . . . . . . . . . . 12 |- ( x e. On -> ( (/) e. x <-> -. x e. 1o ) )
15		oe0m1 6957	. . . . . . . . . . . . 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 616	. . . . . . . . 9 |- ( ( Lim B /\ ( x e. B /\ -. x e. 1o ) ) -> ( (/) ^o x ) = (/) )
20	7, 19	sylan2b 472	. . . . . . . 8 |- ( ( Lim B /\ x e. ( B \ 1o ) ) -> ( (/) ^o x ) = (/) )
21	20	iuneq2dv 4189	. . . . . . 7 |- ( Lim B -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = U_ x e. ( B \ 1o ) (/) )
22		df-1o 6916	. . . . . . . . . . 11 |- 1o = suc (/)
23		limsuc 6459	. . . . . . . . . . . 12 |- ( Lim B -> ( (/) e. B <-> suc (/) e. B ) )
24	2, 23	mpbid 210	. . . . . . . . . . 11 |- ( Lim B -> suc (/) e. B )
25	22, 24	syl5eqel 2525	. . . . . . . . . 10 |- ( Lim B -> 1o e. B )
26		1on 6923	. . . . . . . . . . 11 |- 1o e. On
27	26	onirri 4821	. . . . . . . . . 10 |- -. 1o e. 1o
28	25, 27	jctir 535	. . . . . . . . 9 |- ( Lim B -> ( 1o e. B /\ -. 1o e. 1o ) )
29		eldif 3335	. . . . . . . . 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 3640	. . . . . . . 8 |- ( 1o e. ( B \ 1o ) -> ( B \ 1o ) =/= (/) )
32		iunconst 4176	. . . . . . . 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 2473	. . . . . 6 |- ( Lim B -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = (/) )
35	34	adantl 463	. . . . 5 |- ( ( B e. C /\ Lim B ) -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = (/) )
36	6, 35	eqtr4d 2476	. . . 4 |- ( ( B e. C /\ Lim B ) -> ( (/) ^o B ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) )
37		oveq1 6097	. . . . 5 |- ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
38		oveq1 6097	. . . . . 6 |- ( A = (/) -> ( A ^o x ) = ( (/) ^o x ) )
39	38	iuneq2d 4194	. . . . 5 |- ( A = (/) -> U_ x e. ( B \ 1o ) ( A ^o x ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) )
40	37, 39	eqeq12d 2455	. . . 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 6970	. . 3 |- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ y e. B ( A ^o y ) )
44		limsuc 6459	. . . . . . . . . . . . 13 |- ( Lim B -> ( y e. B <-> suc y e. B ) )
45	44	biimpa 481	. . . . . . . . . . . 12 |- ( ( Lim B /\ y e. B ) -> suc y e. B )
46		nsuceq0 4795	. . . . . . . . . . . . 13 |- suc y =/= (/)
47	46	a1i 11	. . . . . . . . . . . 12 |- ( ( Lim B /\ y e. B ) -> suc y =/= (/) )
48		dif1o 6936	. . . . . . . . . . . 12 |- ( suc y e. ( B \ 1o ) <-> ( suc y e. B /\ suc y =/= (/) ) )
49	45, 47, 48	sylanbrc 659	. . . . . . . . . . 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 721	. . . . . . . . 9 |- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> suc y e. ( B \ 1o ) ) )
52		sssucid 4792	. . . . . . . . . . 11 |- y C_ suc y
53		ordelon 4739	. . . . . . . . . . . . . . . . 17 |- ( ( Ord B /\ y e. B ) -> y e. On )
54	8, 53	sylan 468	. . . . . . . . . . . . . . . 16 |- ( ( Lim B /\ y e. B ) -> y e. On )
55		suceloni 6423	. . . . . . . . . . . . . . . . 17 |- ( y e. On -> suc y e. On )
56	55	ancli 548	. . . . . . . . . . . . . . . 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 1182	. . . . . . . . . . . . . . . 16 |- ( ( ( y e. On /\ suc y e. On ) /\ A e. On ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
60	59	ancoms 450	. . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . . 14 |- ( ( A e. On /\ ( Lim B /\ y e. B ) ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
62	61	anassrs 643	. . . . . . . . . . . . 13 |- ( ( ( A e. On /\ Lim B ) /\ y e. B ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
63		oewordi 7026	. . . . . . . . . . . . 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 468	. . . . . . . . . . . 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 797	. . . . . . . . . . 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 530	. . . . . . . 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 6098	. . . . . . . . . 10 |- ( x = suc y -> ( A ^o x ) = ( A ^o suc y ) )
70	69	sseq2d 3381	. . . . . . . . 9 |- ( x = suc y -> ( ( A ^o y ) C_ ( A ^o x ) <-> ( A ^o y ) C_ ( A ^o suc y ) ) )
71	70	rspcev 3070	. . . . . . . 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 2796	. . . . . 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 4212	. . . . . 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 3480	. . . . . . . 8 |- ( B \ 1o ) C_ B
77		iunss1 4179	. . . . . . . 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 6098	. . . . . . . 8 |- ( x = y -> ( A ^o x ) = ( A ^o y ) )
80	79	cbviunv 4206	. . . . . . 7 |- U_ x e. B ( A ^o x ) = U_ y e. B ( A ^o y )
81	78, 80	sseqtri 3385	. . . . . 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 3370	. . . 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 714	. . 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 2473	. 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 6949	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 960   = wceq 1364   e. wcel 1761   =/= wne 2604   A.wral 2713   E.wrex 2714   \ cdif 3322   C_ wss 3325   (/)c0 3634   U_ciun 4168   Ord word 4714   Oncon0 4715   Lim wlim 4716   suc csuc 4717  (class class class)co 6090   1oc1o 6909   ^o coe 6915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-recs 6828  df-rdg 6862  df-1o 6916  df-2o 6917  df-oadd 6920  df-omul 6921  df-oexp 6922

This theorem is referenced by:  oelimcl  7035  oaabs2  7080  omabs  7082