Metamath Proof Explorer


Theorem prfval

Description: Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses prfval.k P=F⟨,⟩FG
prfval.b B=BaseC
prfval.h H=HomC
prfval.c φFCFuncD
prfval.d φGCFuncE
Assertion prfval φP=xB1stFx1stGxxB,yBhxHyx2ndFyhx2ndGyh

Proof

Step Hyp Ref Expression
1 prfval.k P=F⟨,⟩FG
2 prfval.b B=BaseC
3 prfval.h H=HomC
4 prfval.c φFCFuncD
5 prfval.d φGCFuncE
6 df-prf ⟨,⟩F=fV,gVdom1stf/bxb1stfx1stgxxb,ybhdomx2ndfyx2ndfyhx2ndgyh
7 6 a1i φ⟨,⟩F=fV,gVdom1stf/bxb1stfx1stgxxb,ybhdomx2ndfyx2ndfyhx2ndgyh
8 fvex 1stfV
9 8 dmex dom1stfV
10 9 a1i φf=Fg=Gdom1stfV
11 simprl φf=Fg=Gf=F
12 11 fveq2d φf=Fg=G1stf=1stF
13 12 dmeqd φf=Fg=Gdom1stf=dom1stF
14 eqid BaseD=BaseD
15 relfunc RelCFuncD
16 1st2ndbr RelCFuncDFCFuncD1stFCFuncD2ndF
17 15 4 16 sylancr φ1stFCFuncD2ndF
18 2 14 17 funcf1 φ1stF:BBaseD
19 18 fdmd φdom1stF=B
20 19 adantr φf=Fg=Gdom1stF=B
21 13 20 eqtrd φf=Fg=Gdom1stf=B
22 simpr φf=Fg=Gb=Bb=B
23 simplrl φf=Fg=Gb=Bf=F
24 23 fveq2d φf=Fg=Gb=B1stf=1stF
25 24 fveq1d φf=Fg=Gb=B1stfx=1stFx
26 simplrr φf=Fg=Gb=Bg=G
27 26 fveq2d φf=Fg=Gb=B1stg=1stG
28 27 fveq1d φf=Fg=Gb=B1stgx=1stGx
29 25 28 opeq12d φf=Fg=Gb=B1stfx1stgx=1stFx1stGx
30 22 29 mpteq12dv φf=Fg=Gb=Bxb1stfx1stgx=xB1stFx1stGx
31 eqidd φf=Fg=Gb=Bhdomx2ndfyx2ndfyhx2ndgyh=hdomx2ndfyx2ndfyhx2ndgyh
32 22 22 31 mpoeq123dv φf=Fg=Gb=Bxb,ybhdomx2ndfyx2ndfyhx2ndgyh=xB,yBhdomx2ndfyx2ndfyhx2ndgyh
33 23 ad2antrr φf=Fg=Gb=BxByBf=F
34 33 fveq2d φf=Fg=Gb=BxByB2ndf=2ndF
35 34 oveqd φf=Fg=Gb=BxByBx2ndfy=x2ndFy
36 35 dmeqd φf=Fg=Gb=BxByBdomx2ndfy=domx2ndFy
37 eqid HomD=HomD
38 17 ad4antr φf=Fg=Gb=BxByB1stFCFuncD2ndF
39 simplr φf=Fg=Gb=BxByBxB
40 simpr φf=Fg=Gb=BxByByB
41 2 3 37 38 39 40 funcf2 φf=Fg=Gb=BxByBx2ndFy:xHy1stFxHomD1stFy
42 41 fdmd φf=Fg=Gb=BxByBdomx2ndFy=xHy
43 36 42 eqtrd φf=Fg=Gb=BxByBdomx2ndfy=xHy
44 35 fveq1d φf=Fg=Gb=BxByBx2ndfyh=x2ndFyh
45 26 ad2antrr φf=Fg=Gb=BxByBg=G
46 45 fveq2d φf=Fg=Gb=BxByB2ndg=2ndG
47 46 oveqd φf=Fg=Gb=BxByBx2ndgy=x2ndGy
48 47 fveq1d φf=Fg=Gb=BxByBx2ndgyh=x2ndGyh
49 44 48 opeq12d φf=Fg=Gb=BxByBx2ndfyhx2ndgyh=x2ndFyhx2ndGyh
50 43 49 mpteq12dv φf=Fg=Gb=BxByBhdomx2ndfyx2ndfyhx2ndgyh=hxHyx2ndFyhx2ndGyh
51 50 3impa φf=Fg=Gb=BxByBhdomx2ndfyx2ndfyhx2ndgyh=hxHyx2ndFyhx2ndGyh
52 51 mpoeq3dva φf=Fg=Gb=BxB,yBhdomx2ndfyx2ndfyhx2ndgyh=xB,yBhxHyx2ndFyhx2ndGyh
53 32 52 eqtrd φf=Fg=Gb=Bxb,ybhdomx2ndfyx2ndfyhx2ndgyh=xB,yBhxHyx2ndFyhx2ndGyh
54 30 53 opeq12d φf=Fg=Gb=Bxb1stfx1stgxxb,ybhdomx2ndfyx2ndfyhx2ndgyh=xB1stFx1stGxxB,yBhxHyx2ndFyhx2ndGyh
55 10 21 54 csbied2 φf=Fg=Gdom1stf/bxb1stfx1stgxxb,ybhdomx2ndfyx2ndfyhx2ndgyh=xB1stFx1stGxxB,yBhxHyx2ndFyhx2ndGyh
56 4 elexd φFV
57 5 elexd φGV
58 opex xB1stFx1stGxxB,yBhxHyx2ndFyhx2ndGyhV
59 58 a1i φxB1stFx1stGxxB,yBhxHyx2ndFyhx2ndGyhV
60 7 55 56 57 59 ovmpod φF⟨,⟩FG=xB1stFx1stGxxB,yBhxHyx2ndFyhx2ndGyh
61 1 60 eqtrid φP=xB1stFx1stGxxB,yBhxHyx2ndFyhx2ndGyh