Metamath Proof Explorer

Theorem swapf1

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

Ref Expression
Hypotheses swapf1.o 
|- ( ph -> ( C swapF D ) = <. O , P >. )
swapf1.x 
|- ( ph -> X e. ( Base ` C ) )
swapf1.y 
|- ( ph -> Y e. ( Base ` D ) )
Assertion swapf1 
|- ( ph -> ( X O Y ) = <. Y , X >. )

Proof

Step Hyp Ref Expression
1 swapf1.o 
 |-  ( ph -> ( C swapF D ) = <. O , P >. )
2 swapf1.x 
 |-  ( ph -> X e. ( Base ` C ) )
3 swapf1.y 
 |-  ( ph -> Y e. ( Base ` D ) )
4 df-ov 
 |-  ( X O Y ) = ( O ` <. X , Y >. )
5 2 elfvexd 
 |-  ( ph -> C e. _V )
6 3 elfvexd 
 |-  ( ph -> D e. _V )
7 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 eqid 
 |-  ( Base ` D ) = ( Base ` D )
10 7 8 9 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` ( C Xc. D ) )
11 5 6 7 10 1 swapf1val 
 |-  ( ph -> O = ( x e. ( ( Base ` C ) X. ( Base ` D ) ) |-> U. `' { x } ) )
12 simpr 
 |-  ( ( ph /\ x = <. X , Y >. ) -> x = <. X , Y >. )
13 12 sneqd 
 |-  ( ( ph /\ x = <. X , Y >. ) -> { x } = { <. X , Y >. } )
14 13 cnveqd 
 |-  ( ( ph /\ x = <. X , Y >. ) -> `' { x } = `' { <. X , Y >. } )
15 14 unieqd 
 |-  ( ( ph /\ x = <. X , Y >. ) -> U. `' { x } = U. `' { <. X , Y >. } )
16 opswap 
 |-  U. `' { <. X , Y >. } = <. Y , X >.
17 15 16 eqtrdi 
 |-  ( ( ph /\ x = <. X , Y >. ) -> U. `' { x } = <. Y , X >. )
18 2 3 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
19 opex 
 |-  <. Y , X >. e. _V
20 19 a1i 
 |-  ( ph -> <. Y , X >. e. _V )
21 11 17 18 20 fvmptd 
 |-  ( ph -> ( O ` <. X , Y >. ) = <. Y , X >. )
22 4 21 eqtrid 
 |-  ( ph -> ( X O Y ) = <. Y , X >. )