Metamath Proof Explorer

Theorem swapf2f1o

Description: The morphism part of the swap functor is a bijection between hom-sets. (Contributed by Zhi Wang, 8-Oct-2025)

Ref Expression
Hypotheses swapf1f1o.o 
|- ( ph -> ( C swapF D ) = <. O , P >. )
swapf1f1o.s 
|- S = ( C Xc. D )
swapf1f1o.t 
|- T = ( D Xc. C )
swapf2f1o.h 
|- H = ( Hom ` S )
swapf2f1o.j 
|- J = ( Hom ` T )
swapf2f1o.x 
|- ( ph -> X e. ( Base ` C ) )
swapf2f1o.y 
|- ( ph -> Y e. ( Base ` D ) )
swapf2f1o.z 
|- ( ph -> Z e. ( Base ` C ) )
swapf2f1o.w 
|- ( ph -> W e. ( Base ` D ) )
Assertion swapf2f1o 
|- ( ph -> ( <. X , Y >. P <. Z , W >. ) : ( <. X , Y >. H <. Z , W >. ) -1-1-onto-> ( <. Y , X >. J <. W , Z >. ) )

Proof

Step Hyp Ref Expression
1 swapf1f1o.o 
 |-  ( ph -> ( C swapF D ) = <. O , P >. )
2 swapf1f1o.s 
 |-  S = ( C Xc. D )
3 swapf1f1o.t 
 |-  T = ( D Xc. C )
4 swapf2f1o.h 
 |-  H = ( Hom ` S )
5 swapf2f1o.j 
 |-  J = ( Hom ` T )
6 swapf2f1o.x 
 |-  ( ph -> X e. ( Base ` C ) )
7 swapf2f1o.y 
 |-  ( ph -> Y e. ( Base ` D ) )
8 swapf2f1o.z 
 |-  ( ph -> Z e. ( Base ` C ) )
9 swapf2f1o.w 
 |-  ( ph -> W e. ( Base ` D ) )
10 eqid 
 |-  ( f e. ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) |-> U. `' { f } ) = ( f e. ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) |-> U. `' { f } )
11 10 xpcomf1o 
 |-  ( f e. ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) |-> U. `' { f } ) : ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) -1-1-onto-> ( ( Y ( Hom ` D ) W ) X. ( X ( Hom ` C ) Z ) )
12 4 a1i 
 |-  ( ph -> H = ( Hom ` S ) )
13 1 6 7 8 9 2 12 swapf2val 
 |-  ( ph -> ( <. X , Y >. P <. Z , W >. ) = ( f e. ( <. X , Y >. H <. Z , W >. ) |-> U. `' { f } ) )
14 eqid 
 |-  ( Base ` C ) = ( Base ` C )
15 eqid 
 |-  ( Base ` D ) = ( Base ` D )
16 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
17 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
18 2 14 15 16 17 6 7 8 9 4 xpchom2 
 |-  ( ph -> ( <. X , Y >. H <. Z , W >. ) = ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) )
19 18 mpteq1d 
 |-  ( ph -> ( f e. ( <. X , Y >. H <. Z , W >. ) |-> U. `' { f } ) = ( f e. ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) |-> U. `' { f } ) )
20 13 19 eqtrd 
 |-  ( ph -> ( <. X , Y >. P <. Z , W >. ) = ( f e. ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) |-> U. `' { f } ) )
21 3 15 14 17 16 7 6 9 8 5 xpchom2 
 |-  ( ph -> ( <. Y , X >. J <. W , Z >. ) = ( ( Y ( Hom ` D ) W ) X. ( X ( Hom ` C ) Z ) ) )
22 20 18 21 f1oeq123d 
 |-  ( ph -> ( ( <. X , Y >. P <. Z , W >. ) : ( <. X , Y >. H <. Z , W >. ) -1-1-onto-> ( <. Y , X >. J <. W , Z >. ) <-> ( f e. ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) |-> U. `' { f } ) : ( ( X ( Hom ` C ) Z ) X. ( Y ( Hom ` D ) W ) ) -1-1-onto-> ( ( Y ( Hom ` D ) W ) X. ( X ( Hom ` C ) Z ) ) ) )
23 11 22 mpbiri 
 |-  ( ph -> ( <. X , Y >. P <. Z , W >. ) : ( <. X , Y >. H <. Z , W >. ) -1-1-onto-> ( <. Y , X >. J <. W , Z >. ) )