Metamath Proof Explorer

Theorem swapfval

Description: Value of the swap functor. (Contributed by Zhi Wang, 7-Oct-2025)

Ref Expression
Hypotheses swapfval.c 
|- ( ph -> C e. U )
swapfval.d 
|- ( ph -> D e. V )
swapfval.s 
|- S = ( C Xc. D )
swapfval.b 
|- B = ( Base ` S )
swapfval.h 
|- ( ph -> H = ( Hom ` S ) )
Assertion swapfval 
|- ( ph -> ( C swapF D ) = <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. )

Proof

Step Hyp Ref Expression
1 swapfval.c 
 |-  ( ph -> C e. U )
2 swapfval.d 
 |-  ( ph -> D e. V )
3 swapfval.s 
 |-  S = ( C Xc. D )
4 swapfval.b 
 |-  B = ( Base ` S )
5 swapfval.h 
 |-  ( ph -> H = ( Hom ` S ) )
6 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 } ) ) >. )
7 6 a1i 
 |-  ( ph -> 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 } ) ) >. ) )
8 ovexd 
 |-  ( ( ph /\ ( c = C /\ d = D ) ) -> ( c Xc. d ) e. _V )
9 simprl 
 |-  ( ( ph /\ ( c = C /\ d = D ) ) -> c = C )
10 simprr 
 |-  ( ( ph /\ ( c = C /\ d = D ) ) -> d = D )
11 9 10 oveq12d 
 |-  ( ( ph /\ ( c = C /\ d = D ) ) -> ( c Xc. d ) = ( C Xc. D ) )
12 11 3 eqtr4di 
 |-  ( ( ph /\ ( c = C /\ d = D ) ) -> ( c Xc. d ) = S )
13 fvexd 
 |-  ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) -> ( Base ` s ) e. _V )
14 simpr 
 |-  ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) -> s = S )
15 14 fveq2d 
 |-  ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) -> ( Base ` s ) = ( Base ` S ) )
16 15 4 eqtr4di 
 |-  ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) -> ( Base ` s ) = B )
17 fvexd 
 |-  ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) -> ( Hom ` s ) e. _V )
18 simplr 
 |-  ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) -> s = S )
19 18 fveq2d 
 |-  ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) -> ( Hom ` s ) = ( Hom ` S ) )
20 5 ad3antrrr 
 |-  ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) -> H = ( Hom ` S ) )
21 19 20 eqtr4d 
 |-  ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) -> ( Hom ` s ) = H )
22 simplr 
 |-  ( ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) /\ h = H ) -> b = B )
23 22 mpteq1d 
 |-  ( ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) /\ h = H ) -> ( x e. b |-> U. `' { x } ) = ( x e. B |-> U. `' { x } ) )
24 simpr 
 |-  ( ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) /\ h = H ) -> h = H )
25 24 oveqd 
 |-  ( ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) /\ h = H ) -> ( u h v ) = ( u H v ) )
26 25 mpteq1d 
 |-  ( ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) /\ h = H ) -> ( f e. ( u h v ) |-> U. `' { f } ) = ( f e. ( u H v ) |-> U. `' { f } ) )
27 22 22 26 mpoeq123dv 
 |-  ( ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) /\ h = H ) -> ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) = ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) )
28 23 27 opeq12d 
 |-  ( ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) /\ h = H ) -> <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. = <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. )
29 17 21 28 csbied2 
 |-  ( ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = S ) /\ b = B ) -> [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. = <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. )
30 13 16 29 csbied2 
 |-  ( ( ( ph /\ ( c = C /\ d = D ) ) /\ s = 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 } ) ) >. = <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. )
31 8 12 30 csbied2 
 |-  ( ( ph /\ ( c = C /\ d = D ) ) -> [_ ( 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 } ) ) >. = <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. )
32 1 elexd 
 |-  ( ph -> C e. _V )
33 2 elexd 
 |-  ( ph -> D e. _V )
34 opex 
 |-  <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. e. _V
35 34 a1i 
 |-  ( ph -> <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. e. _V )
36 7 31 32 33 35 ovmpod 
 |-  ( ph -> ( C swapF D ) = <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. )