Metamath Proof Explorer

Theorem 1stfval

Description: Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses 1stfval.t 
|- T = ( C Xc. D )
1stfval.b 
|- B = ( Base ` T )
1stfval.h 
|- H = ( Hom ` T )
1stfval.c 
|- ( ph -> C e. Cat )
1stfval.d 
|- ( ph -> D e. Cat )
1stfval.p 
|- P = ( C 1stF D )
Assertion 1stfval 
|- ( ph -> P = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. )

Proof

Step Hyp Ref Expression
1 1stfval.t 
 |-  T = ( C Xc. D )
2 1stfval.b 
 |-  B = ( Base ` T )
3 1stfval.h 
 |-  H = ( Hom ` T )
4 1stfval.c 
 |-  ( ph -> C e. Cat )
5 1stfval.d 
 |-  ( ph -> D e. Cat )
6 1stfval.p 
 |-  P = ( C 1stF D )
7 fvex 
 |-  ( Base ` c ) e. _V
8 fvex 
 |-  ( Base ` d ) e. _V
9 7 8 xpex 
 |-  ( ( Base ` c ) X. ( Base ` d ) ) e. _V
10 9 a1i 
 |-  ( ( c = C /\ d = D ) -> ( ( Base ` c ) X. ( Base ` d ) ) e. _V )
11 simpl 
 |-  ( ( c = C /\ d = D ) -> c = C )
12 11 fveq2d 
 |-  ( ( c = C /\ d = D ) -> ( Base ` c ) = ( Base ` C ) )
13 simpr 
 |-  ( ( c = C /\ d = D ) -> d = D )
14 13 fveq2d 
 |-  ( ( c = C /\ d = D ) -> ( Base ` d ) = ( Base ` D ) )
15 12 14 xpeq12d 
 |-  ( ( c = C /\ d = D ) -> ( ( Base ` c ) X. ( Base ` d ) ) = ( ( Base ` C ) X. ( Base ` D ) ) )
16 eqid 
 |-  ( Base ` C ) = ( Base ` C )
17 eqid 
 |-  ( Base ` D ) = ( Base ` D )
18 1 16 17 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` T )
19 18 2 eqtr4i 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = B
20 15 19 eqtrdi 
 |-  ( ( c = C /\ d = D ) -> ( ( Base ` c ) X. ( Base ` d ) ) = B )
21 simpr 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> b = B )
22 21 reseq2d 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> ( 1st |` b ) = ( 1st |` B ) )
23 simpll 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> c = C )
24 simplr 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> d = D )
25 23 24 oveq12d 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> ( c Xc. d ) = ( C Xc. D ) )
26 25 1 eqtr4di 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> ( c Xc. d ) = T )
27 26 fveq2d 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> ( Hom ` ( c Xc. d ) ) = ( Hom ` T ) )
28 27 3 eqtr4di 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> ( Hom ` ( c Xc. d ) ) = H )
29 28 oveqd 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> ( x ( Hom ` ( c Xc. d ) ) y ) = ( x H y ) )
30 29 reseq2d 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> ( 1st |` ( x ( Hom ` ( c Xc. d ) ) y ) ) = ( 1st |` ( x H y ) ) )
31 21 21 30 mpoeq123dv 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( c Xc. d ) ) y ) ) ) = ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) )
32 22 31 opeq12d 
 |-  ( ( ( c = C /\ d = D ) /\ b = B ) -> <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( c Xc. d ) ) y ) ) ) >. = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. )
33 10 20 32 csbied2 
 |-  ( ( c = C /\ d = D ) -> [_ ( ( Base ` c ) X. ( Base ` d ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( c Xc. d ) ) y ) ) ) >. = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. )
34 df-1stf 
 |-  1stF = ( c e. Cat , d e. Cat |-> [_ ( ( Base ` c ) X. ( Base ` d ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( c Xc. d ) ) y ) ) ) >. )
35 opex 
 |-  <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. e. _V
36 33 34 35 ovmpoa 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( C 1stF D ) = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. )
37 4 5 36 syl2anc 
 |-  ( ph -> ( C 1stF D ) = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. )
38 6 37 eqtrid 
 |-  ( ph -> P = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. )