Metamath Proof Explorer

Theorem swapf2

Description: The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025)

Ref Expression
Hypotheses swapf1.o 
|- ( ph -> ( C swapF D ) = <. O , P >. )
swapf1.x 
|- ( ph -> X e. ( Base ` C ) )
swapf1.y 
|- ( ph -> Y e. ( Base ` D ) )
swapf2.z 
|- ( ph -> Z e. ( Base ` C ) )
swapf2.w 
|- ( ph -> W e. ( Base ` D ) )
swapf2.f 
|- ( ph -> F e. ( X ( Hom ` C ) Z ) )
swapf2.g 
|- ( ph -> G e. ( Y ( Hom ` D ) W ) )
Assertion swapf2 
|- ( ph -> ( F ( <. X , Y >. P <. Z , W >. ) G ) = <. G , F >. )

Proof

Step Hyp Ref Expression
1 swapf1.o 
 |-  ( ph -> ( C swapF D ) = <. O , P >. )
2 swapf1.x 
 |-  ( ph -> X e. ( Base ` C ) )
3 swapf1.y 
 |-  ( ph -> Y e. ( Base ` D ) )
4 swapf2.z 
 |-  ( ph -> Z e. ( Base ` C ) )
5 swapf2.w 
 |-  ( ph -> W e. ( Base ` D ) )
6 swapf2.f 
 |-  ( ph -> F e. ( X ( Hom ` C ) Z ) )
7 swapf2.g 
 |-  ( ph -> G e. ( Y ( Hom ` D ) W ) )
8 df-ov 
 |-  ( F ( <. X , Y >. P <. Z , W >. ) G ) = ( ( <. X , Y >. P <. Z , W >. ) ` <. F , G >. )
9 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
10 eqidd 
 |-  ( ph -> ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) ) )
11 1 2 3 4 5 9 10 swapf2val 
 |-  ( ph -> ( <. X , Y >. P <. Z , W >. ) = ( f e. ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) |-> U. `' { f } ) )
12 simpr 
 |-  ( ( ph /\ f = <. F , G >. ) -> f = <. F , G >. )
13 12 sneqd 
 |-  ( ( ph /\ f = <. F , G >. ) -> { f } = { <. F , G >. } )
14 13 cnveqd 
 |-  ( ( ph /\ f = <. F , G >. ) -> `' { f } = `' { <. F , G >. } )
15 14 unieqd 
 |-  ( ( ph /\ f = <. F , G >. ) -> U. `' { f } = U. `' { <. F , G >. } )
16 opswap 
 |-  U. `' { <. F , G >. } = <. G , F >.
17 15 16 eqtrdi 
 |-  ( ( ph /\ f = <. F , G >. ) -> U. `' { f } = <. G , F >. )
18 6 7 opelxpd 
 |-  ( ph -> <. F , G >. e. ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) )
19 eqid 
 |-  ( Base ` C ) = ( Base ` C )
20 eqid 
 |-  ( Base ` D ) = ( Base ` D )
21 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
22 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
23 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
24 9 19 20 21 22 2 3 4 5 23 xpchom2 
 |-  ( ph -> ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) = ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) )
25 18 24 eleqtrrd 
 |-  ( ph -> <. F , G >. e. ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) )
26 opex 
 |-  <. G , F >. e. _V
27 26 a1i 
 |-  ( ph -> <. G , F >. e. _V )
28 11 17 25 27 fvmptd 
 |-  ( ph -> ( ( <. X , Y >. P <. Z , W >. ) ` <. F , G >. ) = <. G , F >. )
29 8 28 eqtrid 
 |-  ( ph -> ( F ( <. X , Y >. P <. Z , W >. ) G ) = <. G , F >. )