Metamath Proof Explorer

Theorem swapf2a

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

Ref Expression
Hypotheses swapf1a.o 
|- ( ph -> ( C swapF D ) = <. O , P >. )
swapf1a.s 
|- S = ( C Xc. D )
swapf1a.b 
|- B = ( Base ` S )
swapf1a.x 
|- ( ph -> X e. B )
swapf2a.y 
|- ( ph -> Y e. B )
swapf2a.h 
|- ( ph -> H = ( Hom ` S ) )
swapf2a.f 
|- ( ph -> F e. ( X H Y ) )
Assertion swapf2a 
|- ( ph -> ( ( X P Y ) ` F ) = <. ( 2nd ` F ) , ( 1st ` F ) >. )

Proof

Step Hyp Ref Expression
1 swapf1a.o 
 |-  ( ph -> ( C swapF D ) = <. O , P >. )
2 swapf1a.s 
 |-  S = ( C Xc. D )
3 swapf1a.b 
 |-  B = ( Base ` S )
4 swapf1a.x 
 |-  ( ph -> X e. B )
5 swapf2a.y 
 |-  ( ph -> Y e. B )
6 swapf2a.h 
 |-  ( ph -> H = ( Hom ` S ) )
7 swapf2a.f 
 |-  ( ph -> F e. ( X H Y ) )
8 1 2 3 4 5 6 swapf2vala 
 |-  ( ph -> ( X P Y ) = ( f e. ( X H Y ) |-> U. `' { f } ) )
9 simpr 
 |-  ( ( ph /\ f = F ) -> f = F )
10 9 sneqd 
 |-  ( ( ph /\ f = F ) -> { f } = { F } )
11 10 cnveqd 
 |-  ( ( ph /\ f = F ) -> `' { f } = `' { F } )
12 11 unieqd 
 |-  ( ( ph /\ f = F ) -> U. `' { f } = U. `' { F } )
13 6 oveqd 
 |-  ( ph -> ( X H Y ) = ( X ( Hom ` S ) Y ) )
14 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
15 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
16 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
17 2 3 14 15 16 4 5 xpchom 
 |-  ( ph -> ( X ( Hom ` S ) Y ) = ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) )
18 13 17 eqtrd 
 |-  ( ph -> ( X H Y ) = ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) )
19 7 18 eleqtrd 
 |-  ( ph -> F e. ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) )
20 2nd1st 
 |-  ( F e. ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) -> U. `' { F } = <. ( 2nd ` F ) , ( 1st ` F ) >. )
21 19 20 syl 
 |-  ( ph -> U. `' { F } = <. ( 2nd ` F ) , ( 1st ` F ) >. )
22 21 adantr 
 |-  ( ( ph /\ f = F ) -> U. `' { F } = <. ( 2nd ` F ) , ( 1st ` F ) >. )
23 12 22 eqtrd 
 |-  ( ( ph /\ f = F ) -> U. `' { f } = <. ( 2nd ` F ) , ( 1st ` F ) >. )
24 opex 
 |-  <. ( 2nd ` F ) , ( 1st ` F ) >. e. _V
25 24 a1i 
 |-  ( ph -> <. ( 2nd ` F ) , ( 1st ` F ) >. e. _V )
26 8 23 7 25 fvmptd 
 |-  ( ph -> ( ( X P Y ) ` F ) = <. ( 2nd ` F ) , ( 1st ` F ) >. )