Metamath Proof Explorer

Theorem swapfida

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

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 swapfida.b 
 |-  B = ( Base ` S )
7 swapfida.x 
 |-  ( ph -> X e. B )
8 swapfida.1 
 |-  .1. = ( Id ` S )
9 swapfida.i 
 |-  I = ( Id ` T )
10 eqid 
 |-  ( Base ` C ) = ( Base ` C )
11 eqid 
 |-  ( Base ` D ) = ( Base ` D )
12 3 10 11 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` S )
13 6 12 eqtr4i 
 |-  B = ( ( Base ` C ) X. ( Base ` D ) )
14 7 13 eleqtrdi 
 |-  ( ph -> X e. ( ( Base ` C ) X. ( Base ` D ) ) )
15 xp1st 
 |-  ( X e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( 1st ` X ) e. ( Base ` C ) )
16 14 15 syl 
 |-  ( ph -> ( 1st ` X ) e. ( Base ` C ) )
17 xp2nd 
 |-  ( X e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( 2nd ` X ) e. ( Base ` D ) )
18 14 17 syl 
 |-  ( ph -> ( 2nd ` X ) e. ( Base ` D ) )
19 1 2 3 4 5 16 18 8 9 swapfid 
 |-  ( ph -> ( ( <. ( 1st ` X ) , ( 2nd ` X ) >. P <. ( 1st ` X ) , ( 2nd ` X ) >. ) ` ( .1. ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) ) = ( I ` ( O ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) ) )
20 1st2nd2 
 |-  ( X e. ( ( Base ` C ) X. ( Base ` D ) ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
21 14 20 syl 
 |-  ( ph -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
22 21 21 oveq12d 
 |-  ( ph -> ( X P X ) = ( <. ( 1st ` X ) , ( 2nd ` X ) >. P <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
23 21 fveq2d 
 |-  ( ph -> ( .1. ` X ) = ( .1. ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
24 22 23 fveq12d 
 |-  ( ph -> ( ( X P X ) ` ( .1. ` X ) ) = ( ( <. ( 1st ` X ) , ( 2nd ` X ) >. P <. ( 1st ` X ) , ( 2nd ` X ) >. ) ` ( .1. ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) ) )
25 21 fveq2d 
 |-  ( ph -> ( O ` X ) = ( O ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
26 25 fveq2d 
 |-  ( ph -> ( I ` ( O ` X ) ) = ( I ` ( O ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) ) )
27 19 24 26 3eqtr4d 
 |-  ( ph -> ( ( X P X ) ` ( .1. ` X ) ) = ( I ` ( O ` X ) ) )