Theorem xpmapenlem4 4485

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
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 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 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		eqtrt 1489	. . . . . . . 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	2	feq1d 3616	. . . . . . 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)))
4	1, 3	mpan2 695	. . . . . 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)))
5		fvex 3723	. . . . . . . . 9 |- (U.ran { y}` z) e. V
6	5	opelxp 3209	. . . . . . . 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))
7	6	ralbii 1664	. . . . . . 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))
8		eqid 1473	. . . . . . . 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)>.)}
9	8	fopab2 3814	. . . . . . 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))
10		r19.26 1747	. . . . . . 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))
11	7, 9, 10	3bitr3r 182	. . . . . 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))
12	4, 11	syl6rbbr 538	. . . . 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)))
13	12	biimpac 418	. . . 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))
14		ffvelrn 3805	. . . . . 6 |- ((U.dom { y}:C-->A /\ z e. C) -> (U.dom { y}` z) e. A)
15	14	r19.21aiva 1711	. . . . 5 |- (U.dom { y}:C-->A -> A.z e. C (U.dom { y}` z) e. A)
16		ffvelrn 3805	. . . . . 6 |- ((U.ran { y}:C-->B /\ z e. C) -> (U.ran { y}` z) e. B)
17	16	r19.21aiva 1711	. . . . 5 |- (U.ran { y}:C-->B -> A.z e. C (U.ran { y}` z) e. B)
18	15, 17	anim12i 333	. . . 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))
19	13, 18	sylan 448	. . 3 |- (((U.dom { y}:C-->A /\ U.ran { y}:C-->B) /\ x = S) -> x:C-->(A X. B))
20	19	adantll 392	. 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))
21		eqeq1 1478	. . . . 5 |- (y = <.U.dom { y}, U.ran { y}>. -> (y = <.D, R>. <-> <.U.dom { y}, U.ran { y}>. = <.D, R>.))
22		fopabfv 3822	. . . . . . . . 9 |- (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))
23	22	pm3.26bi 322	. . . . . . . 8 |- (U.dom { y}:C-->A -> U.dom { y} = {<.z, w>. | (z e. C /\ w = (U.dom { y}` z))})
24		hbopab1 2808	. . . . . . . . . . . 12 |- (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)>.)})
25	1, 24	hbxfr 1560	. . . . . . . . . . 11 |- (x e. S -> A.z x e. S)
26	25	hbeleq 1564	. . . . . . . . . 10 |- (x = S -> A.z x = S)
27		hbopab2 2809	. . . . . . . . . . . 12 |- (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)>.)})
28	1, 27	hbxfr 1560	. . . . . . . . . . 11 |- (x e. S -> A.w x e. S)
29	28	hbeleq 1564	. . . . . . . . . 10 |- (x = S -> A.w x = S)
30	1, 2	mpan2 695	. . . . . . . . . . . . . . . . . 18 |- (x = S -> x = {<.z, w>. | (z e. C /\ w = <.(U.dom { y}` z), (U.ran { y}` z)>.)})
31	30	fveq1d 3717	. . . . . . . . . . . . . . . . 17 |- (x = S -> (x` z) = ({<.z, w>. | (z e. C /\ w = <.(U.dom { y}` z), (U.ran { y}` z)>.)}` z))
32		opex 2777	. . . . . . . . . . . . . . . . . 18 |- <.(U.dom { y}` z), (U.ran { y}` z)>. e. V
33		fvopab2 3782	. . . . . . . . . . . . . . . . . 18 |- ((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)>.)
34	32, 33	mpan2 695	. . . . . . . . . . . . . . . . 17 |- (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)>.)
35	31, 34	sylan9eq 1524	. . . . . . . . . . . . . . . 16 |- ((x = S /\ z e. C) -> (x` z) = <.(U.dom { y}` z), (U.ran { y}` z)>.)
36	35	sneqd 2415	. . . . . . . . . . . . . . 15 |- ((x = S /\ z e. C) -> {(x` z)} = {<.(U.dom { y}` z), (U.ran { y}` z)>.})
37	36	dmeqd 3308	. . . . . . . . . . . . . 14 |- ((x = S /\ z e. C) -> dom {(x