Metamath Proof Explorer

Theorem swapfffth

Description: The swap functor is a fully faithful 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 swapfffth 
|- ( ph -> O ( ( S Full T ) i^i ( S Faith 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 1 2 3 4 5 swapffunc 
 |-  ( ph -> O ( S Func T ) P )
7 5 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( C swapF D ) = <. O , P >. )
8 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
9 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> x e. ( Base ` S ) )
12 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> y e. ( Base ` S ) )
13 7 3 4 8 9 10 11 12 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 ) ) )
14 13 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( x P y ) : ( x ( Hom ` S ) y ) -1-1-onto-> ( ( O ` x ) ( Hom ` T ) ( O ` y ) ) )
15 10 8 9 isffth2 
 |-  ( O ( ( S Full T ) i^i ( S Faith T ) ) P <-> ( O ( S Func T ) P /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( x P y ) : ( x ( Hom ` S ) y ) -1-1-onto-> ( ( O ` x ) ( Hom ` T ) ( O ` y ) ) ) )
16 6 14 15 sylanbrc 
 |-  ( ph -> O ( ( S Full T ) i^i ( S Faith T ) ) P )