Theorem xpmapenlem5 3395

Description: Lemma for xpmapen 3396.

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 group(s):   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 3018	. 2 |- ((A X. B) ^m C) e. V
2		opex 1893	. . 3 |- <.D, R>. e. V
3	2	a1i 7	. 2 |- (x e. ((A X. B) ^m C) -> <.D, R>. e. V)
4		xpmapenlem.6	. . . 4 |- S = {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}
5		xpmapen.3	. . . . 5 |- C e. V
6		moeq 1431	. . . . . 6 |- E*w w = <.(U.dom {y}` z), (U.ran {y}` z)>.
7	6	a1i 7	. . . . 5 |- (z e. C -> E*w w = <.(U.dom {y}` z), (U.ran {y}` z)>.)
8	5, 7	funopabex 2742	. . . 4 |- {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)} e. V
9	4, 8	eqeltr 1159	. . 3 |- S e. V
10	9	a1i 7	. 2 |- (y e. ((A ^m C) X. (B ^m C)) -> S e. V)
11		xpmapenlem.4	. . . . . . . . . . . 12 |- D = {<.z, w>. | (z e. C /\ w = U.dom {(x` z)})}
12		moeq 1431	. . . . . . . . . . . . . 14 |- E*w w = U.dom {(x` z)}
13	12	a1i 7	. . . . . . . . . . . . 13 |- (z e. C -> E*w w = U.dom {(x` z)})
14	5, 13	funopabex 2742	. . . . . . . . . . . 12 |- {<.z, w>. | (z e. C /\ w = U.dom {(x` z)})} e. V
15	11, 14	eqeltr 1159	. . . . . . . . . . 11 |- D e. V
16		xpmapenlem.5	. . . . . . . . . . . 12 |- R = {<.z, w>. | (z e. C /\ w = U.ran {(x` z)})}
17		moeq 1431	. . . . . . . . . . . . . 14 |- E*w w = U.ran {(x` z)}
18	17	a1i 7	. . . . . . . . . . . . 13 |- (z e. C -> E*w w = U.ran {(x` z)})
19	5, 18	funopabex 2742	. . . . . . . . . . . 12 |- {<.z, w>. | (z e. C /\ w = U.ran {(x` z)})} e. V
20	16, 19	eqeltr 1159	. . . . . . . . . . 11 |- R e. V
21	15, 20	pm3.2i 234	. . . . . . . . . 10 |- (D e. V /\ R e. V)
22	20	opelxp 2452	. . . . . . . . . 10 |- (<.D, R>. e. (V X. V) <-> (D e. V /\ R e. V))
23	21, 22	mpbir 165	. . . . . . . . 9 |- <.D, R>. e. (V X. V)
24		eleq1 1149	. . . . . . . . 9 |- (y = <.D, R>. -> (y e. (V X. V) <-> <.D, R>. e. (V X. V)))
25	23, 24	mpbiri 169	. . . . . . . 8 |- (y = <.D, R>. -> y e. (V X. V))
26	25	adantl 305	. . . . . . 7 |- ((x:C-->(A X. B) /\ y = <.D, R>.) -> y e. (V X. V))
27		elxp4 2640	. . . . . . . 8 |- (y e. (V X. V) <-> (y = <.U.dom {y}, U.ran {y}>. /\ (U.dom {y} e. V /\ U.ran {y} e. V)))
28	27	pm3.26bd 259	. . . . . . 7 |- (y e. (V X. V) -> y = <.U.dom {y}, U.ran {y}>.)
29	26, 28	syl 12	. . . . . 6 |- ((x:C-->(A X. B) /\ y = <.D, R>.) -> y = <.U.dom {y}, U.ran {y}>.)
30		sneq 1816	. . . . . . . . . . . . . 14 |- (y = <.D, R>. -> {y} = {<.D, R>.})
31	30	dmeqd 2533	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> dom {y} = dom {<.D, R>.})
32	31	unieqd 1929	. . . . . . . . . . . 12 |- (y = <.D, R>. -> U.dom {y} = U.dom {<.D, R>.})
33	15	op1sta 2635	. . . . . . . . . . . 12 |- U.dom {<.D, R>.} = D
34	32, 33	syl6eq 1140	. . . . . . . . . . 11 |- (y = <.D, R>. -> U.dom {y} = D)
35		xpmapen.1	. . . . . . . . . . . . . . 15 |- A e. V
36		xpmapen.2	. . . . . . . . . . . . . . 15 |- B e. V
37	35, 36, 5, 11, 16, 4	xpmapenlem1 3391	. . . . . . . . . . . . . 14 |- ((y = <.D, R>. -> A.z y = <.D, R>.) /\ (y = <.D, R>. -> A.w y = <.D, R>.))
38	37	pm3.26i 257	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> A.z y = <.D, R>.)
39	37	pm3.27i 261	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> A.w y = <.D, R>.)
40	35, 36, 5, 11, 16, 4	xpmapenlem2 3392	. . . . . . . . . . . . . . . . 17 |- ((y = <.D, R>. /\ z e. C) -> ((U.dom {y}` z) = U.dom {(x` z)} /\ (U.ran {y}` z) = U.ran {(x` z)}))
41	40	pm3.26d 258	. . . . . . . . . . . . . . . 16 |- ((y = <.D, R>. /\ z e. C) -> (U.dom {y}` z) = U.dom {(x` z)})
42	41	cleq2d 1112	. . . . . . . . . . . . . . 15 |- ((y = <.D, R>. /\ z e. C) -> (w = (U.dom {y}` z) <-> w = U.dom {(x` z)}))
43	42	exp 291	. . . . . . . . . . . . . 14 |- (y = <.D, R>. -> (z e. C -> (w = (U.dom {y}` z) <-> w = U.dom {(x` z)})))
44	43	pm5.32d 491	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> ((z e. C /\ w = (U.dom {y}` z)) <-> (z e. C /\ w = U.dom {(x` z)})))
45	38, 39, 44	biopabd 2101	. . . . . . . . . . . 12 |- (y = <.D, R>. -> {<.z, w>. | (z e. C /\ w = (U.dom {y}` z))} = {<.z, w>. | (z e. C /\ w = U.dom {(x` z)})})
46	45, 11	syl6eqr 1142	. . . . . . . . . . 11 |- (y = <.D, R>. -> {<.z, w>. | (z e. C /\ w = (U.dom {y}` z))} = D)
47	34, 46	eqtr4d 1131	. . . . . . . . . 10 |- (y = <.D, R>. -> U.dom {y} = {<.z, w>. | (z e. C /\ w = (U.dom {y}` z))})
48	30	rneqd 2557	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> ran {y} = ran {<.D, R>.})
49	48	unieqd 1929	. . . . . . . . . . . 12 |- (y = <.D, R>. -> U.ran {y} = U.ran {<.D, R>.})
50	15, 20	op2nda 2639	. . . . . . . . . . . 12 |- U.ran {<.D, R>.} = R
51	49, 50	syl6eq 1140	. . . . . . . . . . 11 |- (y = <.D, R>. -> U.ran {y} = R)
52	40	pm3.27d 262	. . . . . . . . . . . . . . . 16 |- ((y = <.D, R>. /\ z e. C) -> (U.ran {y}` z) = U.ran {(x` z)})
53	52	cleq2d 1112	. . . . . . . . . . . . . . 15 |- ((y = <.D, R>. /\ z e. C) -> (w = (U.ran {y}` z) <-> w = U.ran {(x` z)}))
54	53	exp 291	. . . . . . . . . . . . . 14 |- (y = <.D, R>. -> (z e. C -> (w = (U.ran {y}` z) <-> w = U.ran {(x` z)})))
55	54	pm5.32d 491	. . . . . . . . . . . . 13 |- (y = <.D, R>. -> ((z e. C /\ w = (U.ran {y}` z)) <-> (z e. C /\ w = U.ran {(x` z)})))
56	38, 39, 55	biopabd 2101	. . . . . . . . . . . 12 |- (y = <.D, R>. -> {<.z, w>. | (z e. C /\ w = (U.ran {y}` z))} = {<.z, w>. | (z e. C /\ w = U.ran {(x` z)})})
57	56, 16	syl6eqr 1142	. . . . . . . . . . 11 |- (y = <.D, R>. -> {<.z, w>. | (z e. C /\ w = (U.ran {y}` z))} = R)
58	51, 57	eqtr4d 1131	. . . . . . . . . 10 |- (y = <.D, R>. -> U.ran {y} = {<.z, w>. | (z e. C /\ w = (U.ran {y}` z))})
59	47, 58	jca 236	. . . . . . . . 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))}))
60	59	adantl 305	. . . . . . . 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))}))
61		ffvrn 2890	. . . . . . . . . . . 12 |- ((x:C-->(A X. B) /\ z e. C) -> (x` z) e. (A X. B))
62	61	exp 291	. . . . . . . . . . 11 |- (x:C-->(A X. B) -> (z e. C -> (x` z) e. (A X. B)))
63	62	r19.21aiv 1259	. . . . . . . . . 10 |- (x:C-->(A X. B) -> A.z e. C (x` z) e. (A X. B))
64	63	adantr 306	. . . . . . . . 9 |- ((x:C-->(A X. B) /\ y = <.D, R>.) -> A.z e. C (x` z) e. (A X. B))
65		ax-17