Metamath Proof Explorer

Theorem swapf2f1oaALT

Description: Alternate proof of swapf2f1oa . (Contributed by Zhi Wang, 8-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses swapf1f1o.o 
|- ( ph -> ( C swapF D ) = <. O , P >. )
swapf1f1o.s 
|- S = ( C Xc. D )
swapf1f1o.t 
|- T = ( D Xc. C )
swapf2f1o.h 
|- H = ( Hom ` S )
swapf2f1o.j 
|- J = ( Hom ` T )
swapf2f1oa.b 
|- B = ( Base ` S )
swapf2f1oa.x 
|- ( ph -> X e. B )
swapf2f1oa.y 
|- ( ph -> Y e. B )
Assertion swapf2f1oaALT 
|- ( ph -> ( X P Y ) : ( X H Y ) -1-1-onto-> ( ( O ` X ) J ( O ` Y ) ) )

Proof

Step Hyp Ref Expression
1 swapf1f1o.o 
 |-  ( ph -> ( C swapF D ) = <. O , P >. )
2 swapf1f1o.s 
 |-  S = ( C Xc. D )
3 swapf1f1o.t 
 |-  T = ( D Xc. C )
4 swapf2f1o.h 
 |-  H = ( Hom ` S )
5 swapf2f1o.j 
 |-  J = ( Hom ` T )
6 swapf2f1oa.b 
 |-  B = ( Base ` S )
7 swapf2f1oa.x 
 |-  ( ph -> X e. B )
8 swapf2f1oa.y 
 |-  ( ph -> Y e. B )
9 eqid 
 |-  ( f e. ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) |-> U. `' { f } ) = ( f e. ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) |-> U. `' { f } )
10 9 xpcomf1o 
 |-  ( f e. ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) |-> U. `' { f } ) : ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) -1-1-onto-> ( ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) X. ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) )
11 4 a1i 
 |-  ( ph -> H = ( Hom ` S ) )
12 1 2 6 7 8 11 swapf2vala 
 |-  ( ph -> ( X P Y ) = ( f e. ( X H Y ) |-> U. `' { f } ) )
13 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
14 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
15 2 6 13 14 4 7 8 xpchom 
 |-  ( ph -> ( X H Y ) = ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) )
16 15 mpteq1d 
 |-  ( ph -> ( f e. ( X H Y ) |-> U. `' { f } ) = ( f e. ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) |-> U. `' { f } ) )
17 12 16 eqtrd 
 |-  ( ph -> ( X P Y ) = ( f e. ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) |-> U. `' { f } ) )
18 eqid 
 |-  ( Base ` T ) = ( Base ` T )
19 2 6 7 elxpcbasex1 
 |-  ( ph -> C e. _V )
20 2 6 7 elxpcbasex2 
 |-  ( ph -> D e. _V )
21 1 2 3 19 20 6 18 swapf1f1o 
 |-  ( ph -> O : B -1-1-onto-> ( Base ` T ) )
22 f1of 
 |-  ( O : B -1-1-onto-> ( Base ` T ) -> O : B --> ( Base ` T ) )
23 21 22 syl 
 |-  ( ph -> O : B --> ( Base ` T ) )
24 23 7 ffvelcdmd 
 |-  ( ph -> ( O ` X ) e. ( Base ` T ) )
25 23 8 ffvelcdmd 
 |-  ( ph -> ( O ` Y ) e. ( Base ` T ) )
26 3 18 14 13 5 24 25 xpchom 
 |-  ( ph -> ( ( O ` X ) J ( O ` Y ) ) = ( ( ( 1st ` ( O ` X ) ) ( Hom ` D ) ( 1st ` ( O ` Y ) ) ) X. ( ( 2nd ` ( O ` X ) ) ( Hom ` C ) ( 2nd ` ( O ` Y ) ) ) ) )
27 1 2 6 7 swapf1a 
 |-  ( ph -> ( O ` X ) = <. ( 2nd ` X ) , ( 1st ` X ) >. )
28 27 fveq2d 
 |-  ( ph -> ( 1st ` ( O ` X ) ) = ( 1st ` <. ( 2nd ` X ) , ( 1st ` X ) >. ) )
29 fvex 
 |-  ( 2nd ` X ) e. _V
30 fvex 
 |-  ( 1st ` X ) e. _V
31 29 30 op1st 
 |-  ( 1st ` <. ( 2nd ` X ) , ( 1st ` X ) >. ) = ( 2nd ` X )
32 28 31 eqtrdi 
 |-  ( ph -> ( 1st ` ( O ` X ) ) = ( 2nd ` X ) )
33 1 2 6 8 swapf1a 
 |-  ( ph -> ( O ` Y ) = <. ( 2nd ` Y ) , ( 1st ` Y ) >. )
34 33 fveq2d 
 |-  ( ph -> ( 1st ` ( O ` Y ) ) = ( 1st ` <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) )
35 fvex 
 |-  ( 2nd ` Y ) e. _V
36 fvex 
 |-  ( 1st ` Y ) e. _V
37 35 36 op1st 
 |-  ( 1st ` <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) = ( 2nd ` Y )
38 34 37 eqtrdi 
 |-  ( ph -> ( 1st ` ( O ` Y ) ) = ( 2nd ` Y ) )
39 32 38 oveq12d 
 |-  ( ph -> ( ( 1st ` ( O ` X ) ) ( Hom ` D ) ( 1st ` ( O ` Y ) ) ) = ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) )
40 27 fveq2d 
 |-  ( ph -> ( 2nd ` ( O ` X ) ) = ( 2nd ` <. ( 2nd ` X ) , ( 1st ` X ) >. ) )
41 29 30 op2nd 
 |-  ( 2nd ` <. ( 2nd ` X ) , ( 1st ` X ) >. ) = ( 1st ` X )
42 40 41 eqtrdi 
 |-  ( ph -> ( 2nd ` ( O ` X ) ) = ( 1st ` X ) )
43 33 fveq2d 
 |-  ( ph -> ( 2nd ` ( O ` Y ) ) = ( 2nd ` <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) )
44 35 36 op2nd 
 |-  ( 2nd ` <. ( 2nd ` Y ) , ( 1st ` Y ) >. ) = ( 1st ` Y )
45 43 44 eqtrdi 
 |-  ( ph -> ( 2nd ` ( O ` Y ) ) = ( 1st ` Y ) )
46 42 45 oveq12d 
 |-  ( ph -> ( ( 2nd ` ( O ` X ) ) ( Hom ` C ) ( 2nd ` ( O ` Y ) ) ) = ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) )
47 39 46 xpeq12d 
 |-  ( ph -> ( ( ( 1st ` ( O ` X ) ) ( Hom ` D ) ( 1st ` ( O ` Y ) ) ) X. ( ( 2nd ` ( O ` X ) ) ( Hom ` C ) ( 2nd ` ( O ` Y ) ) ) ) = ( ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) X. ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) ) )
48 26 47 eqtrd 
 |-  ( ph -> ( ( O ` X ) J ( O ` Y ) ) = ( ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) X. ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) ) )
49 17 15 48 f1oeq123d 
 |-  ( ph -> ( ( X P Y ) : ( X H Y ) -1-1-onto-> ( ( O ` X ) J ( O ` Y ) ) <-> ( f e. ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) |-> U. `' { f } ) : ( ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) ) -1-1-onto-> ( ( ( 2nd ` X ) ( Hom ` D ) ( 2nd ` Y ) ) X. ( ( 1st ` X ) ( Hom ` C ) ( 1st ` Y ) ) ) ) )
50 10 49 mpbiri 
 |-  ( ph -> ( X P Y ) : ( X H Y ) -1-1-onto-> ( ( O ` X ) J ( O ` Y ) ) )