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 pairF G )
prfval.b 
|- B = ( Base ` C )
prfval.h 
|- H = ( Hom ` C )
prfval.c 
|- ( ph -> F e. ( C Func D ) )
prfval.d 
|- ( ph -> G e. ( C Func E ) )
Assertion prfval 
|- ( ph -> P = <. ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. )

Proof

Step Hyp Ref Expression
1 prfval.k 
 |-  P = ( F pairF G )
2 prfval.b 
 |-  B = ( Base ` C )
3 prfval.h 
 |-  H = ( Hom ` C )
4 prfval.c 
 |-  ( ph -> F e. ( C Func D ) )
5 prfval.d 
 |-  ( ph -> G e. ( C Func E ) )
6 df-prf 
 |-  pairF = ( f e. _V , g e. _V |-> [_ dom ( 1st ` f ) / b ]_ <. ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) , ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) >. )
7 6 a1i 
 |-  ( ph -> pairF = ( f e. _V , g e. _V |-> [_ dom ( 1st ` f ) / b ]_ <. ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) , ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) >. ) )
8 fvex 
 |-  ( 1st ` f ) e. _V
9 8 dmex 
 |-  dom ( 1st ` f ) e. _V
10 9 a1i 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> dom ( 1st ` f ) e. _V )
11 simprl 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> f = F )
12 11 fveq2d 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> ( 1st ` f ) = ( 1st ` F ) )
13 12 dmeqd 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> dom ( 1st ` f ) = dom ( 1st ` F ) )
14 eqid 
 |-  ( Base ` D ) = ( Base ` D )
15 relfunc 
 |-  Rel ( C Func D )
16 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
17 15 4 16 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
18 2 14 17 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> ( Base ` D ) )
19 18 fdmd 
 |-  ( ph -> dom ( 1st ` F ) = B )
20 19 adantr 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> dom ( 1st ` F ) = B )
21 13 20 eqtrd 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> dom ( 1st ` f ) = B )
22 simpr 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> b = B )
23 simplrl 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> f = F )
24 23 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> ( 1st ` f ) = ( 1st ` F ) )
25 24 fveq1d 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> ( ( 1st ` f ) ` x ) = ( ( 1st ` F ) ` x ) )
26 simplrr 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> g = G )
27 26 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> ( 1st ` g ) = ( 1st ` G ) )
28 27 fveq1d 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> ( ( 1st ` g ) ` x ) = ( ( 1st ` G ) ` x ) )
29 25 28 opeq12d 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. = <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. )
30 22 29 mpteq12dv 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) = ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) )
31 eqidd 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) = ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) )
32 22 22 31 mpoeq123dv 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) = ( x e. B , y e. B |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) )
33 23 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> f = F )
34 33 fveq2d 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> ( 2nd ` f ) = ( 2nd ` F ) )
35 34 oveqd 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> ( x ( 2nd ` f ) y ) = ( x ( 2nd ` F ) y ) )
36 35 dmeqd 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> dom ( x ( 2nd ` f ) y ) = dom ( x ( 2nd ` F ) y ) )
37 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
38 17 ad4antr 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
39 simplr 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> x e. B )
40 simpr 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> y e. B )
41 2 3 37 38 39 40 funcf2 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> ( x ( 2nd ` F ) y ) : ( x H y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
42 41 fdmd 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> dom ( x ( 2nd ` F ) y ) = ( x H y ) )
43 36 42 eqtrd 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> dom ( x ( 2nd ` f ) y ) = ( x H y ) )
44 35 fveq1d 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> ( ( x ( 2nd ` f ) y ) ` h ) = ( ( x ( 2nd ` F ) y ) ` h ) )
45 26 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> g = G )
46 45 fveq2d 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> ( 2nd ` g ) = ( 2nd ` G ) )
47 46 oveqd 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> ( x ( 2nd ` g ) y ) = ( x ( 2nd ` G ) y ) )
48 47 fveq1d 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> ( ( x ( 2nd ` g ) y ) ` h ) = ( ( x ( 2nd ` G ) y ) ` h ) )
49 44 48 opeq12d 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. = <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. )
50 43 49 mpteq12dv 
 |-  ( ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B ) /\ y e. B ) -> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) = ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) )
51 50 3impa 
 |-  ( ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) /\ x e. B /\ y e. B ) -> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) = ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) )
52 51 mpoeq3dva 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> ( x e. B , y e. B |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) = ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) )
53 32 52 eqtrd 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) = ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) )
54 30 53 opeq12d 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ b = B ) -> <. ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) , ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) >. = <. ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. )
55 10 21 54 csbied2 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> [_ dom ( 1st ` f ) / b ]_ <. ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) , ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) >. = <. ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. )
56 4 elexd 
 |-  ( ph -> F e. _V )
57 5 elexd 
 |-  ( ph -> G e. _V )
58 opex 
 |-  <. ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. e. _V
59 58 a1i 
 |-  ( ph -> <. ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. e. _V )
60 7 55 56 57 59 ovmpod 
 |-  ( ph -> ( F pairF G ) = <. ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. )
61 1 60 syl5eq 
 |-  ( ph -> P = <. ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. )