Metamath Proof Explorer

Theorem swapf2f1oa

Description: The morphism part of the swap functor is a bijection between hom-sets. (Contributed by Zhi Wang, 9-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 )
swapf2f1oa.b 
|- B = ( Base ` S )
swapf2f1oa.x 
|- ( ph -> X e. B )
swapf2f1oa.y 
|- ( ph -> Y e. B )
Assertion swapf2f1oa 
|- ( ph -> ( X P Y ) : ( X H Y ) -1-1-onto-> ( ( O ` X ) J ( O ` Y ) ) )

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 swapf2f1oa.b 
 |-  B = ( Base ` S )
7 swapf2f1oa.x 
 |-  ( ph -> X e. B )
8 swapf2f1oa.y 
 |-  ( ph -> Y e. B )
9 eqid 
 |-  ( Base ` C ) = ( Base ` C )
10 eqid 
 |-  ( Base ` D ) = ( Base ` D )
11 2 9 10 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` S )
12 6 11 eqtr4i 
 |-  B = ( ( Base ` C ) X. ( Base ` D ) )
13 7 12 eleqtrdi 
 |-  ( ph -> X e. ( ( Base ` C ) X. ( Base ` D ) ) )
14 xp1st 
 |-  ( X e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( 1st ` X ) e. ( Base ` C ) )
15 13 14 syl 
 |-  ( ph -> ( 1st ` X ) e. ( Base ` C ) )
16 xp2nd 
 |-  ( X e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( 2nd ` X ) e. ( Base ` D ) )
17 13 16 syl 
 |-  ( ph -> ( 2nd ` X ) e. ( Base ` D ) )
18 8 12 eleqtrdi 
 |-  ( ph -> Y e. ( ( Base ` C ) X. ( Base ` D ) ) )
19 xp1st 
 |-  ( Y e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( 1st ` Y ) e. ( Base ` C ) )
20 18 19 syl 
 |-  ( ph -> ( 1st ` Y ) e. ( Base ` C ) )
21 xp2nd 
 |-  ( Y e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( 2nd ` Y ) e. ( Base ` D ) )
22 18 21 syl 
 |-  ( ph -> ( 2nd ` Y ) e. ( Base ` D ) )
23 1 2 3 4 5 15 17 20 22 swapf2f1o 
 |-  ( ph -> ( <. ( 1st ` X ) , ( 2nd ` X ) >. P <. ( 1st ` Y ) , ( 2nd ` Y ) >. ) : ( <. ( 1st ` X ) , ( 2nd ` X ) >. H <. ( 1st ` Y ) , ( 2nd ` Y ) >. ) -1-1-onto-> ( <. ( 2nd ` X ) , ( 1st ` X ) >. J <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) )
24 1st2nd2 
 |-  ( X e. ( ( Base ` C ) X. ( Base ` D ) ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
25 13 24 syl 
 |-  ( ph -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
26 1st2nd2 
 |-  ( Y e. ( ( Base ` C ) X. ( Base ` D ) ) -> Y = <. ( 1st ` Y ) , ( 2nd ` Y ) >. )
27 18 26 syl 
 |-  ( ph -> Y = <. ( 1st ` Y ) , ( 2nd ` Y ) >. )
28 25 27 oveq12d 
 |-  ( ph -> ( X P Y ) = ( <. ( 1st ` X ) , ( 2nd ` X ) >. P <. ( 1st ` Y ) , ( 2nd ` Y ) >. ) )
29 25 27 oveq12d 
 |-  ( ph -> ( X H Y ) = ( <. ( 1st ` X ) , ( 2nd ` X ) >. H <. ( 1st ` Y ) , ( 2nd ` Y ) >. ) )
30 1 2 6 7 swapf1a 
 |-  ( ph -> ( O ` X ) = <. ( 2nd ` X ) , ( 1st ` X ) >. )
31 1 2 6 8 swapf1a 
 |-  ( ph -> ( O ` Y ) = <. ( 2nd ` Y ) , ( 1st ` Y ) >. )
32 30 31 oveq12d 
 |-  ( ph -> ( ( O ` X ) J ( O ` Y ) ) = ( <. ( 2nd ` X ) , ( 1st ` X ) >. J <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) )
33 28 29 32 f1oeq123d 
 |-  ( ph -> ( ( X P Y ) : ( X H Y ) -1-1-onto-> ( ( O ` X ) J ( O ` Y ) ) <-> ( <. ( 1st ` X ) , ( 2nd ` X ) >. P <. ( 1st ` Y ) , ( 2nd ` Y ) >. ) : ( <. ( 1st ` X ) , ( 2nd ` X ) >. H <. ( 1st ` Y ) , ( 2nd ` Y ) >. ) -1-1-onto-> ( <. ( 2nd ` X ) , ( 1st ` X ) >. J <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) ) )
34 23 33 mpbird 
 |-  ( ph -> ( X P Y ) : ( X H Y ) -1-1-onto-> ( ( O ` X ) J ( O ` Y ) ) )