Theorem xpmapenlem5 4486

Description: Lemma for xpmapen 4487.

Hypotheses

Ref	Expression
xpmapen.1	|- A e. V
xpmapen.2	|- B e. V
xpmapen.3	|- C e. V
xpmapenlem.4	|- D = {<.z, w>. | (z e. C /\ w = U.dom {(x` z)})}
xpmapenlem.5	|- R = {<.z, w>. | (z e. C /\ w = U.ran {(x` z)})}
xpmapenlem.6	|- S = {<.z, w>. | (z e. C /\ w = <.(U.dom { y}` z), (U.ran { y}` z)>.)}

Assertion

Ref	Expression
xpmapenlem5	|- ((A X. B) ^m C) ~~ ((A ^m C) X. (B ^m C))

Distinct variable groups:   x,y,z,w,A   x,B,y,z,w   x,C,y,z,w   y,D   y,R   x,S

Proof of Theorem xpmapenlem5

Step	Hyp	Ref	Expression
1		oprex 3974	. 2 |- ((A X. B) ^m C) e. V
2		opex 2777	. . 3 |- <.D, R>. e. V
3	2	a1i 8	. 2 |- (x e. ((A X. B) ^m C) -> <.D, R>. e. V)
4		xpmapen.3	. . . 4 |- C e. V
5		xpmapenlem.6	. . . 4 |- S = {<.z, w>. | (z e. C /\ w = <.(U.dom { y}` z), (U.ran { y}` z)>.)}
6	4, 5	fopabex2 3604	. . 3 |- S e. V
7	6	a1i 8	. 2 |- (y e. ((A ^m C) X. (B ^m C)) -> S e. V)
8		xpmapenlem.5	. . . . . . . . . . . 12 |- R = {<.z, w>. | (z e. C /\ w = U.ran {(x` z)})}
9	4, 8	fopabex2 3604	. . . . . . . . . . 11 |- R e. V
10	9	opelxp 3209	. . . . . . . . . 10 |- (<.D, R>. e. (V X. V) <-> (D e. V /\ R e. V))
11		xpmapenlem.4	. . . . . . . . . . 11 |- D = {<.z, w>. | (z e. C /\ w = U.dom {(x` z)})}
12	4, 11	fopabex2 3604	. . . . . . . . . 10 |- D e. V
13	10, 12, 9	mpbir2an 729	. . . . . . . . 9 |- <.D, R>. e. (V X. V)
14		eleq1 1531	. . . . . . . . 9 |- (y = <.D, R>. -> (y e. (V X. V) <-> <.D, R>. e. (V X. V)))
15	13, 14	mpbiri 194	. . . . . . . 8 |- (y = <.D, R>. -> y e. (V X. V))
16	15	adantl 388	. . . . . . 7 |- ((x:C-->(A X. B) /\ y = <.D, R>.) -> y e. (V X. V))
17		elxp4 3445	. . . . . . . 8 |- (y e. (V X. V) <-> (y = <.U.dom { y}, U.ran { y}>. /\ (U.dom { y} e. V /\ U.ran { y} e. V)))
18	17	pm3.26bi 322	. . . . . . 7 |- (y e. (V X. V) -> y = <.U.dom { y}, U.ran { y}>.)
19	16, 18	syl 10	. . . . . 6 |- ((x:C-->(A X. B) /\ y = <.D, R>.) -> y = <.U.dom { y}, U.ran { y}>.)
20	12	op1sta 3440	. . . . . . . . . . 11 |- U.dom {<.D, R>.} = D
21		sneq 2413	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> {y} = {<.D, R>.})
22	21	dmeqd 3308	. . . . . . . . . . . 12 |- (y = <.D, R>. -> dom { y} = dom {<.D, R>.})
23	22	unieqd 2507	. . . . . . . . . . 11 |- (y = <.D, R>. -> U.dom { y} = U.dom {<.D, R>.})
24		xpmapen.1	. . . . . . . . . . . . . . 15 |- A e. V
25		xpmapen.2	. . . . . . . . . . . . . . 15 |- B e. V
26	24, 25, 4, 11, 8, 5	xpmapenlem1 4482	. . . . . . . . . . . . . 14 |- ((y = <.D, R>. -> A.z y = <.D, R>.) /\ (y = <.D, R>. -> A.w y = <.D, R>.))
27	26	pm3.26i 320	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> A.z y = <.D, R>.)
28	26	pm3.27i 324	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> A.w y = <.D, R>.)
29	24, 25, 4, 11, 8, 5	xpmapenlem2 4483	. . . . . . . . . . . . . . . 16 |- ((y = <.D, R>. /\ z e. C) -> ((U.dom { y}` z) = U.dom {(x` z)} /\ (U.ran { y}` z) = U.ran {(x` z)}))
30	29	pm3.26d 321	. . . . . . . . . . . . . . 15 |- ((y = <.D, R>. /\ z e. C) -> (U.dom { y}` z) = U.dom {(x` z)})
31	30	eqeq2d 1483	. . . . . . . . . . . . . 14 |- ((y = <.D, R>. /\ z e. C) -> (w = (U.dom { y}` z) <-> w = U.dom {(x` z)}))
32	31	pm5.32da 648	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> ((z e. C /\ w = (U.dom { y}` z)) <-> (z e. C /\ w = U.dom {(x` z)})))
33	27, 28, 32	opabbid 2664	. . . . . . . . . . . 12 |- (y = <.D, R>. -> {<.z, w>. | (z e. C /\ w = (U.dom { y}` z))} = {<.z, w>. | (z e. C /\ w = U.dom {(x` z)})})
34	33, 11	syl6eqr 1522	. . . . . . . . . . 11 |- (y = <.D, R>. -> {<.z, w>. | (z e. C /\ w = (U.dom { y}` z))} = D)
35	20, 23, 34	3eqtr4a 1529	. . . . . . . . . 10 |- (y = <.D, R>. -> U.dom { y} = {<.z, w>. | (z e. C /\ w = (U.dom { y}` z))})
36	12, 9	op2nda 3444	. . . . . . . . . . 11 |- U.ran {<.D, R>.} = R
37	21	rneqd 3336	. . . . . . . . . . . 12 |- (y = <.D, R>. -> ran { y} = ran {<.D, R>.})
38	37	unieqd 2507	. . . . . . . . . . 11 |- (y = <.D, R>. -> U.ran { y} = U.ran {<.D, R>.})
39	29	pm3.27d 325	. . . . . . . . . . . . . . 15 |- ((y = <.D, R>. /\ z e. C) -> (U.ran { y}` z) = U.ran {(x` z)})
40	39	eqeq2d 1483	. . . . . . . . . . . . . 14 |- ((y = <.D, R>. /\ z e. C) -> (w = (U.ran { y}` z) <-> w = U.ran {(x` z)}))
41	40	pm5.32da 648	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> ((z e. C /\ w = (U.ran { y}` z)) <-> (z e. C /\ w = U.ran {(x` z)})))
42	27, 28, 41	opabbid 2664	. . . . . . . . . . . 12 |- (y = <.D, R>. -> {<.z, w>. | (z e. C /\ w = (U.ran { y}` z))} = {<.z, w>. | (z e. C /\ w = U.ran {(x` z)})})
43	42, 8	syl6eqr 1522	. . . . . . . . . . 11 |- (y = <.D, R>. -> {<.z, w>. | (z e. C /\ w = (U.ran { y}` z))} = R)
44	36, 38, 43	3eqtr4a 1529	. . . . . . . . . 10 |- (y = <.D, R>. -> U.ran { y} = {<.z, w>. | (z e. C /\ w = (U.ran { y}` z))})
45	35, 44	jca 288	. . . . . . . . 9 |- (y = <.D, R>. -> (U.dom { y} = {<.z, w>. | (z e. C /\ w = (U.dom { y}` z))} /\ U.ran { y} = {<.z, w>. | (z e. C /\ w = (U.ran { y}` z))}))
46	45	adantl 388	. . . . . . . 8 |- ((x:C-->(A X. B) /\ y = <.D, R>.) -> (U.dom { y} = {<.z, w>. | (z e. C /\ w = (U.dom { y}` z))} /\ U.ran { y} = {<.z, w>. | (z e. C /\ w = (U.ran { y}` z))}))
47		ffvelrn 3805	. . . . . . . . . . 11 |- ((x:C-->(A X. B) /\ z e. C) -> (x` z) e. (A X. B))
48	47	r19.21aiva 1711	. . . . . . . . . 10 |- (x:C-->(A X. B) -> A.z e. C (x` z) e. (A X. B))
49	48	adantr 389	. . . . . . . . 9 |- ((x:C-->(A X. B) /\ y = <.D, R>.) -> A.z e. C (x` z) e. (A X. B))
50		ax-17 969	. . . . . . . . . . . 12 |- (x:C-->(A X. B) -> A.z x:C-->(A X. B))
51	50, 27	hban 1007	. . . . . . . . . . 11 |- ((x:C-->(A X. B) /\ y = <.D, R>.) -> A.z(x:C-->(A X. B) /\ y = <.D, R>.))
52	24, 25, 4, 11, 8, 5	xpmapenlem3 4484	. . . . . . . . . . . . . . 15 |- ((x:C-->(A X. B) /\ y = <.D, R>.) -> x = S)
53	52	fveq1d 3717	. . . . . . . . . . . . . 14 |- ((x:C-->(A X. B) /\ y = <.D, R>.) -> (x` z) = (S` z))
54		opex 2777	. . . . . . . . . . . . . . . 16 |- <.(U.dom { y}` z), (U.ran { y}` z)>. e. V
55		fvopab2 3782	. . . . . . . . . . . . . . . 16 |- ((z e. C /\ <.(U.dom { y}` z), (U.ran { y}` z)>. e. V) -> ({<.z, w>. | (z e. C /\ w = <.(U.dom { y}` z), (U.ran { y}` z)>.)}` z) = <.(U.dom { y}` z), (U.ran { y}` z)>.)
56	54, 55	mpan2 695	. . . . . . . . . . . . . . 15 |- (z e. C -> ({<.z, w>. | (z e. C /\ w = <.(U.dom { y}` z), (U.ran { y}` z)>.)}` z) = <.(U.dom { y}` z), (U.ran { y}` z)>.)
57	5	fveq1i 3716	. . . . . . . . . . . . . . 15 |- (S` z) = ({<.z, w>. | (z e. C /\ w = <.(U.dom { y