Metamath Proof Explorer

Theorem swapfid

Description: Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfida . (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 >. )
swapfid.x 
|- ( ph -> X e. ( Base ` C ) )
swapfid.y 
|- ( ph -> Y e. ( Base ` D ) )
swapfid.1 
|- .1. = ( Id ` S )
swapfid.i 
|- I = ( Id ` T )
Assertion swapfid 
|- ( ph -> ( ( <. X , Y >. P <. X , Y >. ) ` ( .1. ` <. X , Y >. ) ) = ( I ` ( O ` <. X , Y >. ) ) )

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 swapfid.x 
 |-  ( ph -> X e. ( Base ` C ) )
7 swapfid.y 
 |-  ( ph -> Y e. ( Base ` D ) )
8 swapfid.1 
 |-  .1. = ( Id ` S )
9 swapfid.i 
 |-  I = ( Id ` T )
10 eqid 
 |-  ( Base ` D ) = ( Base ` D )
11 eqid 
 |-  ( Base ` C ) = ( Base ` C )
12 eqid 
 |-  ( Id ` D ) = ( Id ` D )
13 eqid 
 |-  ( Id ` C ) = ( Id ` C )
14 4 2 1 10 11 12 13 9 7 6 xpcid 
 |-  ( ph -> ( I ` <. Y , X >. ) = <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. )
15 df-ov 
 |-  ( X O Y ) = ( O ` <. X , Y >. )
16 5 6 7 swapf1 
 |-  ( ph -> ( X O Y ) = <. Y , X >. )
17 15 16 eqtr3id 
 |-  ( ph -> ( O ` <. X , Y >. ) = <. Y , X >. )
18 17 fveq2d 
 |-  ( ph -> ( I ` ( O ` <. X , Y >. ) ) = ( I ` <. Y , X >. ) )
19 3 1 2 11 10 13 12 8 6 7 xpcid 
 |-  ( ph -> ( .1. ` <. X , Y >. ) = <. ( ( Id ` C ) ` X ) , ( ( Id ` D ) ` Y ) >. )
20 19 fveq2d 
 |-  ( ph -> ( ( <. X , Y >. P <. X , Y >. ) ` ( .1. ` <. X , Y >. ) ) = ( ( <. X , Y >. P <. X , Y >. ) ` <. ( ( Id ` C ) ` X ) , ( ( Id ` D ) ` Y ) >. ) )
21 df-ov 
 |-  ( ( ( Id ` C ) ` X ) ( <. X , Y >. P <. X , Y >. ) ( ( Id ` D ) ` Y ) ) = ( ( <. X , Y >. P <. X , Y >. ) ` <. ( ( Id ` C ) ` X ) , ( ( Id ` D ) ` Y ) >. )
22 21 a1i 
 |-  ( ph -> ( ( ( Id ` C ) ` X ) ( <. X , Y >. P <. X , Y >. ) ( ( Id ` D ) ` Y ) ) = ( ( <. X , Y >. P <. X , Y >. ) ` <. ( ( Id ` C ) ` X ) , ( ( Id ` D ) ` Y ) >. ) )
23 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
24 11 23 13 1 6 catidcl 
 |-  ( ph -> ( ( Id ` C ) ` X ) e. ( X ( Hom ` C ) X ) )
25 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
26 10 25 12 2 7 catidcl 
 |-  ( ph -> ( ( Id ` D ) ` Y ) e. ( Y ( Hom ` D ) Y ) )
27 5 6 7 6 7 24 26 swapf2 
 |-  ( ph -> ( ( ( Id ` C ) ` X ) ( <. X , Y >. P <. X , Y >. ) ( ( Id ` D ) ` Y ) ) = <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. )
28 20 22 27 3eqtr2d 
 |-  ( ph -> ( ( <. X , Y >. P <. X , Y >. ) ` ( .1. ` <. X , Y >. ) ) = <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. )
29 14 18 28 3eqtr4rd 
 |-  ( ph -> ( ( <. X , Y >. P <. X , Y >. ) ` ( .1. ` <. X , Y >. ) ) = ( I ` ( O ` <. X , Y >. ) ) )