Metamath Proof Explorer

Theorem dfswapf2

Description: Alternate definition of swapF ( df-swapf ). (Contributed by Zhi Wang, 9-Oct-2025)

Ref Expression
Assertion dfswapf2 
|- swapF = ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. )

Proof

Step Hyp Ref Expression
1 df-swapf 
 |-  swapF = ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. )
2 fvex 
 |-  ( Base ` ( c Xc. d ) ) e. _V
3 id 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> b = ( Base ` ( c Xc. d ) ) )
4 eqid 
 |-  ( c Xc. d ) = ( c Xc. d )
5 eqid 
 |-  ( Base ` c ) = ( Base ` c )
6 eqid 
 |-  ( Base ` d ) = ( Base ` d )
7 4 5 6 xpcbas 
 |-  ( ( Base ` c ) X. ( Base ` d ) ) = ( Base ` ( c Xc. d ) )
8 3 7 eqtr4di 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> b = ( ( Base ` c ) X. ( Base ` d ) ) )
9 8 mpteq1d 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> ( x e. b |-> U. `' { x } ) = ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) )
10 eqidd 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> ( f e. ( u h v ) |-> U. `' { f } ) = ( f e. ( u h v ) |-> U. `' { f } ) )
11 8 8 10 mpoeq123dv 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) = ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u h v ) |-> U. `' { f } ) ) )
12 9 11 opeq12d 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. = <. ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. )
13 12 csbeq2dv 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. = [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. )
14 2 13 csbie 
 |-  [_ ( Base ` ( c Xc. d ) ) / b ]_ [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. = [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >.
15 ovex 
 |-  ( c Xc. d ) e. _V
16 fveq2 
 |-  ( s = ( c Xc. d ) -> ( Base ` s ) = ( Base ` ( c Xc. d ) ) )
17 fveq2 
 |-  ( s = ( c Xc. d ) -> ( Hom ` s ) = ( Hom ` ( c Xc. d ) ) )
18 17 csbeq1d 
 |-  ( s = ( c Xc. d ) -> [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. = [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. )
19 16 18 csbeq12dv 
 |-  ( s = ( c Xc. d ) -> [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. = [_ ( Base ` ( c Xc. d ) ) / b ]_ [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. )
20 15 19 csbie 
 |-  [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. = [_ ( Base ` ( c Xc. d ) ) / b ]_ [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >.
21 17 csbeq1d 
 |-  ( s = ( c Xc. d ) -> [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. = [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. )
22 16 21 csbeq12dv 
 |-  ( s = ( c Xc. d ) -> [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. = [_ ( Base ` ( c Xc. d ) ) / b ]_ [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. )
23 15 22 csbie 
 |-  [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. = [_ ( Base ` ( c Xc. d ) ) / b ]_ [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >.
24 8 reseq2d 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> ( tpos _I |` b ) = ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) )
25 eqidd 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> ( tpos _I |` ( u h v ) ) = ( tpos _I |` ( u h v ) ) )
26 8 8 25 mpoeq123dv 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) = ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u h v ) ) ) )
27 24 26 opeq12d 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. = <. ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u h v ) ) ) >. )
28 27 csbeq2dv 
 |-  ( b = ( Base ` ( c Xc. d ) ) -> [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. = [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u h v ) ) ) >. )
29 2 28 csbie 
 |-  [_ ( Base ` ( c Xc. d ) ) / b ]_ [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. = [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u h v ) ) ) >.
30 eqid 
 |-  ( ( Base ` c ) X. ( Base ` d ) ) = ( ( Base ` c ) X. ( Base ` d ) )
31 30 tposideq2 
 |-  ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) = ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } )
32 eqid 
 |-  ( ( ( 1st ` u ) ( Hom ` c ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` d ) ( 2nd ` v ) ) ) = ( ( ( 1st ` u ) ( Hom ` c ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` d ) ( 2nd ` v ) ) )
33 32 tposideq2 
 |-  ( tpos _I |` ( ( ( 1st ` u ) ( Hom ` c ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` d ) ( 2nd ` v ) ) ) ) = ( f e. ( ( ( 1st ` u ) ( Hom ` c ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` d ) ( 2nd ` v ) ) ) |-> U. `' { f } )
34 eqid 
 |-  ( Hom ` c ) = ( Hom ` c )
35 eqid 
 |-  ( Hom ` d ) = ( Hom ` d )
36 eqid 
 |-  ( Hom ` ( c Xc. d ) ) = ( Hom ` ( c Xc. d ) )
37 simpl 
 |-  ( ( u e. ( ( Base ` c ) X. ( Base ` d ) ) /\ v e. ( ( Base ` c ) X. ( Base ` d ) ) ) -> u e. ( ( Base ` c ) X. ( Base ` d ) ) )
38 simpr 
 |-  ( ( u e. ( ( Base ` c ) X. ( Base ` d ) ) /\ v e. ( ( Base ` c ) X. ( Base ` d ) ) ) -> v e. ( ( Base ` c ) X. ( Base ` d ) ) )
39 4 7 34 35 36 37 38 xpchom 
 |-  ( ( u e. ( ( Base ` c ) X. ( Base ` d ) ) /\ v e. ( ( Base ` c ) X. ( Base ` d ) ) ) -> ( u ( Hom ` ( c Xc. d ) ) v ) = ( ( ( 1st ` u ) ( Hom ` c ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` d ) ( 2nd ` v ) ) ) )
40 39 reseq2d 
 |-  ( ( u e. ( ( Base ` c ) X. ( Base ` d ) ) /\ v e. ( ( Base ` c ) X. ( Base ` d ) ) ) -> ( tpos _I |` ( u ( Hom ` ( c Xc. d ) ) v ) ) = ( tpos _I |` ( ( ( 1st ` u ) ( Hom ` c ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` d ) ( 2nd ` v ) ) ) ) )
41 39 mpteq1d 
 |-  ( ( u e. ( ( Base ` c ) X. ( Base ` d ) ) /\ v e. ( ( Base ` c ) X. ( Base ` d ) ) ) -> ( f e. ( u ( Hom ` ( c Xc. d ) ) v ) |-> U. `' { f } ) = ( f e. ( ( ( 1st ` u ) ( Hom ` c ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` d ) ( 2nd ` v ) ) ) |-> U. `' { f } ) )
42 33 40 41 3eqtr4a 
 |-  ( ( u e. ( ( Base ` c ) X. ( Base ` d ) ) /\ v e. ( ( Base ` c ) X. ( Base ` d ) ) ) -> ( tpos _I |` ( u ( Hom ` ( c Xc. d ) ) v ) ) = ( f e. ( u ( Hom ` ( c Xc. d ) ) v ) |-> U. `' { f } ) )
43 42 mpoeq3ia 
 |-  ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u ( Hom ` ( c Xc. d ) ) v ) ) ) = ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u ( Hom ` ( c Xc. d ) ) v ) |-> U. `' { f } ) )
44 31 43 opeq12i 
 |-  <. ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u ( Hom ` ( c Xc. d ) ) v ) ) ) >. = <. ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u ( Hom ` ( c Xc. d ) ) v ) |-> U. `' { f } ) ) >.
45 fvex 
 |-  ( Hom ` ( c Xc. d ) ) e. _V
46 oveq 
 |-  ( h = ( Hom ` ( c Xc. d ) ) -> ( u h v ) = ( u ( Hom ` ( c Xc. d ) ) v ) )
47 46 reseq2d 
 |-  ( h = ( Hom ` ( c Xc. d ) ) -> ( tpos _I |` ( u h v ) ) = ( tpos _I |` ( u ( Hom ` ( c Xc. d ) ) v ) ) )
48 47 mpoeq3dv 
 |-  ( h = ( Hom ` ( c Xc. d ) ) -> ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u h v ) ) ) = ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u ( Hom ` ( c Xc. d ) ) v ) ) ) )
49 48 opeq2d 
 |-  ( h = ( Hom ` ( c Xc. d ) ) -> <. ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u h v ) ) ) >. = <. ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u ( Hom ` ( c Xc. d ) ) v ) ) ) >. )
50 45 49 csbie 
 |-  [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u h v ) ) ) >. = <. ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u ( Hom ` ( c Xc. d ) ) v ) ) ) >.
51 46 mpteq1d 
 |-  ( h = ( Hom ` ( c Xc. d ) ) -> ( f e. ( u h v ) |-> U. `' { f } ) = ( f e. ( u ( Hom ` ( c Xc. d ) ) v ) |-> U. `' { f } ) )
52 51 mpoeq3dv 
 |-  ( h = ( Hom ` ( c Xc. d ) ) -> ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u h v ) |-> U. `' { f } ) ) = ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u ( Hom ` ( c Xc. d ) ) v ) |-> U. `' { f } ) ) )
53 52 opeq2d 
 |-  ( h = ( Hom ` ( c Xc. d ) ) -> <. ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. = <. ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u ( Hom ` ( c Xc. d ) ) v ) |-> U. `' { f } ) ) >. )
54 45 53 csbie 
 |-  [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. = <. ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u ( Hom ` ( c Xc. d ) ) v ) |-> U. `' { f } ) ) >.
55 44 50 54 3eqtr4i 
 |-  [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( tpos _I |` ( ( Base ` c ) X. ( Base ` d ) ) ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( tpos _I |` ( u h v ) ) ) >. = [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >.
56 23 29 55 3eqtri 
 |-  [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. = [_ ( Hom ` ( c Xc. d ) ) / h ]_ <. ( x e. ( ( Base ` c ) X. ( Base ` d ) ) |-> U. `' { x } ) , ( u e. ( ( Base ` c ) X. ( Base ` d ) ) , v e. ( ( Base ` c ) X. ( Base ` d ) ) |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >.
57 14 20 56 3eqtr4ri 
 |-  [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. = [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >.
58 57 a1i 
 |-  ( ( c e. _V /\ d e. _V ) -> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. = [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. )
59 58 mpoeq3ia 
 |-  ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. ) = ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. )
60 1 59 eqtr4i 
 |-  swapF = ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. )