Metamath Proof Explorer

Theorem swapfiso

Description: The swap functor is an isomorphism between product categories. (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 )
swapfiso.e 
|- E = ( CatCat ` U )
swapfiso.u 
|- ( ph -> U e. V )
swapfiso.s 
|- ( ph -> S e. U )
swapfiso.t 
|- ( ph -> T e. U )
swapfiso.i 
|- I = ( Iso ` E )
Assertion swapfiso 
|- ( ph -> ( C swapF D ) e. ( S I T ) )

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 swapfiso.e 
 |-  E = ( CatCat ` U )
6 swapfiso.u 
 |-  ( ph -> U e. V )
7 swapfiso.s 
 |-  ( ph -> S e. U )
8 swapfiso.t 
 |-  ( ph -> T e. U )
9 swapfiso.i 
 |-  I = ( Iso ` E )
10 1 2 swapfelvv 
 |-  ( ph -> ( C swapF D ) e. ( _V X. _V ) )
11 1st2nd2 
 |-  ( ( C swapF D ) e. ( _V X. _V ) -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. )
12 10 11 syl 
 |-  ( ph -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. )
13 1 2 3 4 12 swapfffth 
 |-  ( ph -> ( 1st ` ( C swapF D ) ) ( ( S Full T ) i^i ( S Faith T ) ) ( 2nd ` ( C swapF D ) ) )
14 df-br 
 |-  ( ( 1st ` ( C swapF D ) ) ( ( S Full T ) i^i ( S Faith T ) ) ( 2nd ` ( C swapF D ) ) <-> <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. e. ( ( S Full T ) i^i ( S Faith T ) ) )
15 13 14 sylib 
 |-  ( ph -> <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. e. ( ( S Full T ) i^i ( S Faith T ) ) )
16 12 15 eqeltrd 
 |-  ( ph -> ( C swapF D ) e. ( ( S Full T ) i^i ( S Faith T ) ) )
17 eqid 
 |-  ( Base ` S ) = ( Base ` S )
18 eqid 
 |-  ( Base ` T ) = ( Base ` T )
19 12 3 4 1 2 17 18 swapf1f1o 
 |-  ( ph -> ( 1st ` ( C swapF D ) ) : ( Base ` S ) -1-1-onto-> ( Base ` T ) )
20 eqid 
 |-  ( Base ` E ) = ( Base ` E )
21 3 1 2 xpccat 
 |-  ( ph -> S e. Cat )
22 7 21 elind 
 |-  ( ph -> S e. ( U i^i Cat ) )
23 5 20 6 catcbas 
 |-  ( ph -> ( Base ` E ) = ( U i^i Cat ) )
24 22 23 eleqtrrd 
 |-  ( ph -> S e. ( Base ` E ) )
25 4 2 1 xpccat 
 |-  ( ph -> T e. Cat )
26 8 25 elind 
 |-  ( ph -> T e. ( U i^i Cat ) )
27 26 23 eleqtrrd 
 |-  ( ph -> T e. ( Base ` E ) )
28 5 20 17 18 6 24 27 9 catciso 
 |-  ( ph -> ( ( C swapF D ) e. ( S I T ) <-> ( ( C swapF D ) e. ( ( S Full T ) i^i ( S Faith T ) ) /\ ( 1st ` ( C swapF D ) ) : ( Base ` S ) -1-1-onto-> ( Base ` T ) ) ) )
29 16 19 28 mpbir2and 
 |-  ( ph -> ( C swapF D ) e. ( S I T ) )