Metamath Proof Explorer

Theorem swapf1vala

Description: The object part of the swap functor. See also swapf1val . (Contributed by Zhi Wang, 7-Oct-2025)

Ref Expression
Hypotheses swapfval.c 
|- ( ph -> C e. U )
swapfval.d 
|- ( ph -> D e. V )
swapf2fvala.s 
|- S = ( C Xc. D )
swapf2fvala.b 
|- B = ( Base ` S )
Assertion swapf1vala 
|- ( ph -> ( 1st ` ( C swapF D ) ) = ( x e. B |-> U. `' { x } ) )

Proof

Step Hyp Ref Expression
1 swapfval.c 
 |-  ( ph -> C e. U )
2 swapfval.d 
 |-  ( ph -> D e. V )
3 swapf2fvala.s 
 |-  S = ( C Xc. D )
4 swapf2fvala.b 
 |-  B = ( Base ` S )
5 eqidd 
 |-  ( ph -> ( Hom ` S ) = ( Hom ` S ) )
6 1 2 3 4 5 swapfval 
 |-  ( ph -> ( C swapF D ) = <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) >. )
7 6 fveq2d 
 |-  ( ph -> ( 1st ` ( C swapF D ) ) = ( 1st ` <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) >. ) )
8 4 fvexi 
 |-  B e. _V
9 8 mptex 
 |-  ( x e. B |-> U. `' { x } ) e. _V
10 8 8 mpoex 
 |-  ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) e. _V
11 9 10 op1st 
 |-  ( 1st ` <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) >. ) = ( x e. B |-> U. `' { x } )
12 7 11 eqtrdi 
 |-  ( ph -> ( 1st ` ( C swapF D ) ) = ( x e. B |-> U. `' { x } ) )