Metamath Proof Explorer

Theorem cofuswapf1

Description: The object part of a bifunctor pre-composed with a swap functor. (Contributed by Zhi Wang, 9-Oct-2025)

Ref Expression
Hypotheses cofuswapf1.c 
|- ( ph -> C e. Cat )
cofuswapf1.d 
|- ( ph -> D e. Cat )
cofuswapf1.f 
|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
cofuswapf1.g 
|- ( ph -> G = ( F o.func ( C swapF D ) ) )
cofuswapf1.a 
|- A = ( Base ` C )
cofuswapf1.b 
|- B = ( Base ` D )
cofuswapf1.x 
|- ( ph -> X e. A )
cofuswapf1.y 
|- ( ph -> Y e. B )
Assertion cofuswapf1 
|- ( ph -> ( X ( 1st ` G ) Y ) = ( Y ( 1st ` F ) X ) )

Proof

Step Hyp Ref Expression
1 cofuswapf1.c 
 |-  ( ph -> C e. Cat )
2 cofuswapf1.d 
 |-  ( ph -> D e. Cat )
3 cofuswapf1.f 
 |-  ( ph -> F e. ( ( D Xc. C ) Func E ) )
4 cofuswapf1.g 
 |-  ( ph -> G = ( F o.func ( C swapF D ) ) )
5 cofuswapf1.a 
 |-  A = ( Base ` C )
6 cofuswapf1.b 
 |-  B = ( Base ` D )
7 cofuswapf1.x 
 |-  ( ph -> X e. A )
8 cofuswapf1.y 
 |-  ( ph -> Y e. B )
9 df-ov 
 |-  ( X ( 1st ` G ) Y ) = ( ( 1st ` G ) ` <. X , Y >. )
10 4 fveq2d 
 |-  ( ph -> ( 1st ` G ) = ( 1st ` ( F o.func ( C swapF D ) ) ) )
11 10 fveq1d 
 |-  ( ph -> ( ( 1st ` G ) ` <. X , Y >. ) = ( ( 1st ` ( F o.func ( C swapF D ) ) ) ` <. X , Y >. ) )
12 9 11 eqtrid 
 |-  ( ph -> ( X ( 1st ` G ) Y ) = ( ( 1st ` ( F o.func ( C swapF D ) ) ) ` <. X , Y >. ) )
13 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
14 13 5 6 xpcbas 
 |-  ( A X. B ) = ( Base ` ( C Xc. D ) )
15 eqid 
 |-  ( D Xc. C ) = ( D Xc. C )
16 1 2 13 15 swapffunca 
 |-  ( ph -> ( C swapF D ) e. ( ( C Xc. D ) Func ( D Xc. C ) ) )
17 7 8 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( A X. B ) )
18 14 16 3 17 cofu1 
 |-  ( ph -> ( ( 1st ` ( F o.func ( C swapF D ) ) ) ` <. X , Y >. ) = ( ( 1st ` F ) ` ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ) )
19 df-ov 
 |-  ( X ( 1st ` ( C swapF D ) ) Y ) = ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. )
20 1 2 swapfelvv 
 |-  ( ph -> ( C swapF D ) e. ( _V X. _V ) )
21 1st2nd2 
 |-  ( ( C swapF D ) e. ( _V X. _V ) -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. )
22 20 21 syl 
 |-  ( ph -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. )
23 7 5 eleqtrdi 
 |-  ( ph -> X e. ( Base ` C ) )
24 8 6 eleqtrdi 
 |-  ( ph -> Y e. ( Base ` D ) )
25 22 23 24 swapf1 
 |-  ( ph -> ( X ( 1st ` ( C swapF D ) ) Y ) = <. Y , X >. )
26 19 25 eqtr3id 
 |-  ( ph -> ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) = <. Y , X >. )
27 26 fveq2d 
 |-  ( ph -> ( ( 1st ` F ) ` ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ) = ( ( 1st ` F ) ` <. Y , X >. ) )
28 12 18 27 3eqtrd 
 |-  ( ph -> ( X ( 1st ` G ) Y ) = ( ( 1st ` F ) ` <. Y , X >. ) )
29 df-ov 
 |-  ( Y ( 1st ` F ) X ) = ( ( 1st ` F ) ` <. Y , X >. )
30 28 29 eqtr4di 
 |-  ( ph -> ( X ( 1st ` G ) Y ) = ( Y ( 1st ` F ) X ) )