Metamath Proof Explorer

Theorem swapfelvv

Description: A swap functor is an ordered pair. (Contributed by Zhi Wang, 7-Oct-2025)

Ref Expression
Hypotheses swapfval.c 
|- ( ph -> C e. U )
swapfval.d 
|- ( ph -> D e. V )
Assertion swapfelvv 
|- ( ph -> ( C swapF D ) e. ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 swapfval.c 
 |-  ( ph -> C e. U )
2 swapfval.d 
 |-  ( ph -> D e. V )
3 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
4 eqid 
 |-  ( Base ` ( C Xc. D ) ) = ( Base ` ( C Xc. D ) )
5 eqidd 
 |-  ( ph -> ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) ) )
6 1 2 3 4 5 swapfval 
 |-  ( ph -> ( C swapF D ) = <. ( x e. ( Base ` ( C Xc. D ) ) |-> U. `' { x } ) , ( u e. ( Base ` ( C Xc. D ) ) , v e. ( Base ` ( C Xc. D ) ) |-> ( f e. ( u ( Hom ` ( C Xc. D ) ) v ) |-> U. `' { f } ) ) >. )
7 fvex 
 |-  ( Base ` ( C Xc. D ) ) e. _V
8 7 mptex 
 |-  ( x e. ( Base ` ( C Xc. D ) ) |-> U. `' { x } ) e. _V
9 7 7 mpoex 
 |-  ( u e. ( Base ` ( C Xc. D ) ) , v e. ( Base ` ( C Xc. D ) ) |-> ( f e. ( u ( Hom ` ( C Xc. D ) ) v ) |-> U. `' { f } ) ) e. _V
10 8 9 opelvv 
 |-  <. ( x e. ( Base ` ( C Xc. D ) ) |-> U. `' { x } ) , ( u e. ( Base ` ( C Xc. D ) ) , v e. ( Base ` ( C Xc. D ) ) |-> ( f e. ( u ( Hom ` ( C Xc. D ) ) v ) |-> U. `' { f } ) ) >. e. ( _V X. _V )
11 6 10 eqeltrdi 
 |-  ( ph -> ( C swapF D ) e. ( _V X. _V ) )