Metamath Proof Explorer

Theorem swapffunc

Description: The swap functor is a functor. (Contributed by Zhi Wang, 8-Oct-2025)

Ref Expression
Hypotheses swapfid.c 
|- ( ph -> C e. Cat )
swapfid.d 
|- ( ph -> D e. Cat )
swapfid.s 
|- S = ( C Xc. D )
swapfid.t 
|- T = ( D Xc. C )
swapfid.o 
|- ( ph -> ( C swapF D ) = <. O , P >. )
Assertion swapffunc 
|- ( ph -> O ( S Func T ) P )

Proof

Step Hyp Ref Expression
1 swapfid.c 
 |-  ( ph -> C e. Cat )
2 swapfid.d 
 |-  ( ph -> D e. Cat )
3 swapfid.s 
 |-  S = ( C Xc. D )
4 swapfid.t 
 |-  T = ( D Xc. C )
5 swapfid.o 
 |-  ( ph -> ( C swapF D ) = <. O , P >. )
6 eqid 
 |-  ( Base ` S ) = ( Base ` S )
7 eqid 
 |-  ( Base ` T ) = ( Base ` T )
8 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
9 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
10 eqid 
 |-  ( Id ` S ) = ( Id ` S )
11 eqid 
 |-  ( Id ` T ) = ( Id ` T )
12 eqid 
 |-  ( comp ` S ) = ( comp ` S )
13 eqid 
 |-  ( comp ` T ) = ( comp ` T )
14 3 1 2 xpccat 
 |-  ( ph -> S e. Cat )
15 4 2 1 xpccat 
 |-  ( ph -> T e. Cat )
16 5 3 4 1 2 6 7 swapf1f1o 
 |-  ( ph -> O : ( Base ` S ) -1-1-onto-> ( Base ` T ) )
17 f1of 
 |-  ( O : ( Base ` S ) -1-1-onto-> ( Base ` T ) -> O : ( Base ` S ) --> ( Base ` T ) )
18 16 17 syl 
 |-  ( ph -> O : ( Base ` S ) --> ( Base ` T ) )
19 1 2 3 6 5 swapf2fn 
 |-  ( ph -> P Fn ( ( Base ` S ) X. ( Base ` S ) ) )
20 5 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( C swapF D ) = <. O , P >. )
21 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> x e. ( Base ` S ) )
22 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> y e. ( Base ` S ) )
23 20 3 4 8 9 6 21 22 swapf2f1oa 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x P y ) : ( x ( Hom ` S ) y ) -1-1-onto-> ( ( O ` x ) ( Hom ` T ) ( O ` y ) ) )
24 f1of 
 |-  ( ( x P y ) : ( x ( Hom ` S ) y ) -1-1-onto-> ( ( O ` x ) ( Hom ` T ) ( O ` y ) ) -> ( x P y ) : ( x ( Hom ` S ) y ) --> ( ( O ` x ) ( Hom ` T ) ( O ` y ) ) )
25 23 24 syl 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x P y ) : ( x ( Hom ` S ) y ) --> ( ( O ` x ) ( Hom ` T ) ( O ` y ) ) )
26 1 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> C e. Cat )
27 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> D e. Cat )
28 5 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( C swapF D ) = <. O , P >. )
29 simpr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> x e. ( Base ` S ) )
30 26 27 3 4 28 6 29 10 11 swapfida 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( x P x ) ` ( ( Id ` S ) ` x ) ) = ( ( Id ` T ) ` ( O ` x ) ) )
31 1 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> C e. Cat )
32 2 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> D e. Cat )
33 5 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> ( C swapF D ) = <. O , P >. )
34 simp21 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> x e. ( Base ` S ) )
35 simp22 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> y e. ( Base ` S ) )
36 simp23 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> z e. ( Base ` S ) )
37 simp3l 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> m e. ( x ( Hom ` S ) y ) )
38 simp3r 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> n e. ( y ( Hom ` S ) z ) )
39 31 32 3 4 33 6 34 35 36 8 37 38 12 13 swapfcoa 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> ( ( x P z ) ` ( n ( <. x , y >. ( comp ` S ) z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. ( comp ` T ) ( O ` z ) ) ( ( x P y ) ` m ) ) )
40 6 7 8 9 10 11 12 13 14 15 18 19 25 30 39 isfuncd 
 |-  ( ph -> O ( S Func T ) P )