Theorem xpmapenlem4 3394

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
xpmapenlem4	|- (((y = <.U.dom {y}, U.ran {y}>. /\ (U.dom {y}:C-->A /\ U.ran {y}:C-->B)) /\ x = S) -> (x:C-->(A X. B) /\ y = <.D, R>.))

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 xpmapenlem4

Step	Hyp	Ref	Expression
1		xpmapenlem.6	. . . . . . 7 |- S = {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}
2		cleqtr 1118	. . . . . . . 8 |- ((x = S /\ S = {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}) -> x = {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)})
3		feq1 2748	. . . . . . . 8 |- (x = {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)} -> (x:C-->(A X. B) <-> {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}:C-->(A X. B)))
4	2, 3	syl 12	. . . . . . 7 |- ((x = S /\ S = {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}) -> (x:C-->(A X. B) <-> {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}:C-->(A X. B)))
5	1, 4	mpan2 519	. . . . . 6 |- (x = S -> (x:C-->(A X. B) <-> {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}:C-->(A X. B)))
6		fvex 2838	. . . . . . . . 9 |- (U.ran {y}` z) e. V
7	6	opelxp 2452	. . . . . . . 8 |- (<.(U.dom {y}` z), (U.ran {y}` z)>. e. (A X. B) <-> ((U.dom {y}` z) e. A /\ (U.ran {y}` z) e. B))
8	7	biral 1223	. . . . . . 7 |- (A.z e. C <.(U.dom {y}` z), (U.ran {y}` z)>. e. (A X. B) <-> A.z e. C ((U.dom {y}` z) e. A /\ (U.ran {y}` z) e. B))
9		cleqid 1102	. . . . . . . 8 |- {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)} = {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}
10	9	fopab2 2891	. . . . . . 7 |- (A.z e. C <.(U.dom {y}` z), (U.ran {y}` z)>. e. (A X. B) <-> {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}:C-->(A X. B))
11		r19.26 1289	. . . . . . 7 |- (A.z e. C ((U.dom {y}` z) e. A /\ (U.ran {y}` z) e. B) <-> (A.z e. C (U.dom {y}` z) e. A /\ A.z e. C (U.ran {y}` z) e. B))
12	8, 10, 11	3bitr3r 157	. . . . . 6 |- ((A.z e. C (U.dom {y}` z) e. A /\ A.z e. C (U.ran {y}` z) e. B) <-> {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}:C-->(A X. B))
13	5, 12	syl6rbbr 417	. . . . 5 |- (x = S -> ((A.z e. C (U.dom {y}` z) e. A /\ A.z e. C (U.ran {y}` z) e. B) <-> x:C-->(A X. B)))
14	13	biimpac 326	. . . 4 |- (((A.z e. C (U.dom {y}` z) e. A /\ A.z e. C (U.ran {y}` z) e. B) /\ x = S) -> x:C-->(A X. B))
15		ffvrn 2890	. . . . . . 7 |- ((U.dom {y}:C-->A /\ z e. C) -> (U.dom {y}` z) e. A)
16	15	exp 291	. . . . . 6 |- (U.dom {y}:C-->A -> (z e. C -> (U.dom {y}` z) e. A))
17	16	r19.21aiv 1259	. . . . 5 |- (U.dom {y}:C-->A -> A.z e. C (U.dom {y}` z) e. A)
18		ffvrn 2890	. . . . . . 7 |- ((U.ran {y}:C-->B /\ z e. C) -> (U.ran {y}` z) e. B)
19	18	exp 291	. . . . . 6 |- (U.ran {y}:C-->B -> (z e. C -> (U.ran {y}` z) e. B))
20	19	r19.21aiv 1259	. . . . 5 |- (U.ran {y}:C-->B -> A.z e. C (U.ran {y}` z) e. B)
21	17, 20	anim12i 268	. . . 4 |- ((U.dom {y}:C-->A /\ U.ran {y}:C-->B) -> (A.z e. C (U.dom {y}` z) e. A /\ A.z e. C (U.ran {y}` z) e. B))
22	14, 21	sylan 343	. . 3 |- (((U.dom {y}:C-->A /\ U.ran {y}:C-->B) /\ x = S) -> x:C-->(A X. B))
23	22	adantll 309	. 2 |- (((y = <.U.dom {y}, U.ran {y}>. /\ (U.dom {y}:C-->A /\ U.ran {y}:C-->B)) /\ x = S) -> x:C-->(A X. B))
24		cleq1 1107	. . . . 5 |- (y = <.U.dom {y}, U.ran {y}>. -> (y = <.D, R>. <-> <.U.dom {y}, U.ran {y}>. = <.D, R>.))
25		fopabfv 2894	. . . . . . . . . 10 |- (U.dom {y}:C-->A <-> (U.dom {y} = {<.z, w>. | (z e. C /\ w = (U.dom {y}` z))} /\ A.z e. C (U.dom {y}` z) e. A))
26	25	pm3.26bd 259	. . . . . . . . 9 |- (U.dom {y}:C-->A -> U.dom {y} = {<.z, w>. | (z e. C /\ w = (U.dom {y}` z))})
27		hbopab1 2112	. . . . . . . . . . . . 13 |- (x e. {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)} -> A.z x e. {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)})
28	1	eleq2i 1153	. . . . . . . . . . . . 13 |- (x e. S <-> x e. {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)})
29	28	bial 695	. . . . . . . . . . . . 13 |- (A.z x e. S <-> A.z x e. {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)})
30	27, 28, 29	3imtr4 192	. . . . . . . . . . . 12 |- (x e. S -> A.z x e. S)
31	30	hbeleq 1173	. . . . . . . . . . 11 |- (x = S -> A.z x = S)
32		hbopab2 2113	. . . . . . . . . . . . 13 |- (x e. {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)} -> A.w x e. {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)})
33	28	bial 695	. . . . . . . . . . . . 13 |- (A.w x e. S <-> A.w x e. {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)})
34	32, 28, 33	3imtr4 192	. . . . . . . . . . . 12 |- (x e. S -> A.w x e. S)
35	34	hbeleq 1173	. . . . . . . . . . 11 |- (x = S -> A.w x = S)
36	1, 2	mpan2 519	. . . . . . . . . . . . . . . . . . . 20 |- (x = S -> x = {<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)})
37	36	fveq1d 2834	. . . . . . . . . . . . . . . . . . 19 |- (x = S -> (x` z) = ({<.z, w>. | (z e. C /\ w = <.(U.dom {y}` z), (U.ran {y}` z)>.)}` z))
38		opex 1893	. . . . . . . . . . . . . . . . . . . 20 |- <.(U.dom {y}` z), (U.ran {y}` z)>.