oelim2

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

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

Proof

Step	Hyp	Ref	Expression
1		limelon	\|- ( ( B e. C /\ Lim B ) -> B e. On )
2		0ellim	\|- ( Lim B -> (/) e. B )
3	2	adantl	\|- ( ( B e. C /\ Lim B ) -> (/) e. B )
4		oe0m1	\|- ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
5	4	biimpa	\|- ( ( B e. On /\ (/) e. B ) -> ( (/) ^o B ) = (/) )
6	1 3 5	syl2anc	\|- ( ( B e. C /\ Lim B ) -> ( (/) ^o B ) = (/) )
7		eldif	\|- ( x e. ( B \ 1o ) <-> ( x e. B /\ -. x e. 1o ) )
8		limord	\|- ( Lim B -> Ord B )
9		ordelon	\|- ( ( Ord B /\ x e. B ) -> x e. On )
10	8 9	sylan	\|- ( ( Lim B /\ x e. B ) -> x e. On )
11		on0eln0	\|- ( x e. On -> ( (/) e. x <-> x =/= (/) ) )
12		el1o	\|- ( x e. 1o <-> x = (/) )
13	12	necon3bbii	\|- ( -. x e. 1o <-> x =/= (/) )
14	11 13	bitr4di	\|- ( x e. On -> ( (/) e. x <-> -. x e. 1o ) )
15		oe0m1	\|- ( x e. On -> ( (/) e. x <-> ( (/) ^o x ) = (/) ) )
16	15	biimpd	\|- ( x e. On -> ( (/) e. x -> ( (/) ^o x ) = (/) ) )
17	14 16	sylbird	\|- ( x e. On -> ( -. x e. 1o -> ( (/) ^o x ) = (/) ) )
18	10 17	syl	\|- ( ( Lim B /\ x e. B ) -> ( -. x e. 1o -> ( (/) ^o x ) = (/) ) )
19	18	impr	\|- ( ( Lim B /\ ( x e. B /\ -. x e. 1o ) ) -> ( (/) ^o x ) = (/) )
20	7 19	sylan2b	\|- ( ( Lim B /\ x e. ( B \ 1o ) ) -> ( (/) ^o x ) = (/) )
21	20	iuneq2dv	\|- ( Lim B -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = U_ x e. ( B \ 1o ) (/) )
22		df-1o	\|- 1o = suc (/)
23		limsuc	\|- ( Lim B -> ( (/) e. B <-> suc (/) e. B ) )
24	2 23	mpbid	\|- ( Lim B -> suc (/) e. B )
25	22 24	eqeltrid	\|- ( Lim B -> 1o e. B )
26		1on	\|- 1o e. On
27	26	onirri	\|- -. 1o e. 1o
28		eldif	\|- ( 1o e. ( B \ 1o ) <-> ( 1o e. B /\ -. 1o e. 1o ) )
29	25 27 28	sylanblrc	\|- ( Lim B -> 1o e. ( B \ 1o ) )
30		ne0i	\|- ( 1o e. ( B \ 1o ) -> ( B \ 1o ) =/= (/) )
31		iunconst	\|- ( ( B \ 1o ) =/= (/) -> U_ x e. ( B \ 1o ) (/) = (/) )
32	29 30 31	3syl	\|- ( Lim B -> U_ x e. ( B \ 1o ) (/) = (/) )
33	21 32	eqtrd	\|- ( Lim B -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = (/) )
34	33	adantl	\|- ( ( B e. C /\ Lim B ) -> U_ x e. ( B \ 1o ) ( (/) ^o x ) = (/) )
35	6 34	eqtr4d	\|- ( ( B e. C /\ Lim B ) -> ( (/) ^o B ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) )
36		oveq1	\|- ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
37		oveq1	\|- ( A = (/) -> ( A ^o x ) = ( (/) ^o x ) )
38	37	iuneq2d	\|- ( A = (/) -> U_ x e. ( B \ 1o ) ( A ^o x ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) )
39	36 38	eqeq12d	\|- ( A = (/) -> ( ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) <-> ( (/) ^o B ) = U_ x e. ( B \ 1o ) ( (/) ^o x ) ) )
40	35 39	imbitrrid	\|- ( A = (/) -> ( ( B e. C /\ Lim B ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) ) )
41	40	impcom	\|- ( ( ( B e. C /\ Lim B ) /\ A = (/) ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
42		oelim	\|- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ y e. B ( A ^o y ) )
43		limsuc	\|- ( Lim B -> ( y e. B <-> suc y e. B ) )
44	43	biimpa	\|- ( ( Lim B /\ y e. B ) -> suc y e. B )
45		nsuceq0	\|- suc y =/= (/)
46		dif1o	\|- ( suc y e. ( B \ 1o ) <-> ( suc y e. B /\ suc y =/= (/) ) )
47	44 45 46	sylanblrc	\|- ( ( Lim B /\ y e. B ) -> suc y e. ( B \ 1o ) )
48	47	ex	\|- ( Lim B -> ( y e. B -> suc y e. ( B \ 1o ) ) )
49	48	ad2antlr	\|- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> suc y e. ( B \ 1o ) ) )
50		sssucid	\|- y C_ suc y
51		ordelon	\|- ( ( Ord B /\ y e. B ) -> y e. On )
52	8 51	sylan	\|- ( ( Lim B /\ y e. B ) -> y e. On )
53		onsuc	\|- ( y e. On -> suc y e. On )
54	52 53	jccir	\|- ( ( Lim B /\ y e. B ) -> ( y e. On /\ suc y e. On ) )
55		id	\|- ( ( y e. On /\ suc y e. On /\ A e. On ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
56	55	3expa	\|- ( ( ( y e. On /\ suc y e. On ) /\ A e. On ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
57	56	ancoms	\|- ( ( A e. On /\ ( y e. On /\ suc y e. On ) ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
58	54 57	sylan2	\|- ( ( A e. On /\ ( Lim B /\ y e. B ) ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
59	58	anassrs	\|- ( ( ( A e. On /\ Lim B ) /\ y e. B ) -> ( y e. On /\ suc y e. On /\ A e. On ) )
60		oewordi	\|- ( ( ( y e. On /\ suc y e. On /\ A e. On ) /\ (/) e. A ) -> ( y C_ suc y -> ( A ^o y ) C_ ( A ^o suc y ) ) )
61	59 60	sylan	\|- ( ( ( ( A e. On /\ Lim B ) /\ y e. B ) /\ (/) e. A ) -> ( y C_ suc y -> ( A ^o y ) C_ ( A ^o suc y ) ) )
62	61	an32s	\|- ( ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) /\ y e. B ) -> ( y C_ suc y -> ( A ^o y ) C_ ( A ^o suc y ) ) )
63	50 62	mpi	\|- ( ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) /\ y e. B ) -> ( A ^o y ) C_ ( A ^o suc y ) )
64	63	ex	\|- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> ( A ^o y ) C_ ( A ^o suc y ) ) )
65	49 64	jcad	\|- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> ( suc y e. ( B \ 1o ) /\ ( A ^o y ) C_ ( A ^o suc y ) ) ) )
66		oveq2	\|- ( x = suc y -> ( A ^o x ) = ( A ^o suc y ) )
67	66	sseq2d	\|- ( x = suc y -> ( ( A ^o y ) C_ ( A ^o x ) <-> ( A ^o y ) C_ ( A ^o suc y ) ) )
68	67	rspcev	\|- ( ( 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 ) )
69	65 68	syl6	\|- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> ( y e. B -> E. x e. ( B \ 1o ) ( A ^o y ) C_ ( A ^o x ) ) )
70	69	ralrimiv	\|- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> A. y e. B E. x e. ( B \ 1o ) ( A ^o y ) C_ ( A ^o x ) )
71		iunss2	\|- ( 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 ) )
72	70 71	syl	\|- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> U_ y e. B ( A ^o y ) C_ U_ x e. ( B \ 1o ) ( A ^o x ) )
73		difss	\|- ( B \ 1o ) C_ B
74		iunss1	\|- ( ( B \ 1o ) C_ B -> U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ x e. B ( A ^o x ) )
75	73 74	ax-mp	\|- U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ x e. B ( A ^o x )
76		oveq2	\|- ( x = y -> ( A ^o x ) = ( A ^o y ) )
77	76	cbviunv	\|- U_ x e. B ( A ^o x ) = U_ y e. B ( A ^o y )
78	75 77	sseqtri	\|- U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ y e. B ( A ^o y )
79	78	a1i	\|- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> U_ x e. ( B \ 1o ) ( A ^o x ) C_ U_ y e. B ( A ^o y ) )
80	72 79	eqssd	\|- ( ( ( A e. On /\ Lim B ) /\ (/) e. A ) -> U_ y e. B ( A ^o y ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
81	80	adantlrl	\|- ( ( ( 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 ) )
82	42 81	eqtrd	\|- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
83	41 82	oe0lem	\|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) )

Metamath Proof Explorer

Theorem oelim2

Proof