This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omf1o

Description: Construct an explicit bijection from A .o B to B .o A . (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypotheses omf1o.1 
|- F = ( x e. B , y e. A |-> ( ( A .o x ) +o y ) )
omf1o.2 
|- G = ( x e. B , y e. A |-> ( ( B .o y ) +o x ) )
Assertion omf1o 
|- ( ( A e. On /\ B e. On ) -> ( G o. `' F ) : ( A .o B ) -1-1-onto-> ( B .o A ) )

Proof

Step Hyp Ref Expression
1 omf1o.1 
 |-  F = ( x e. B , y e. A |-> ( ( A .o x ) +o y ) )
2 omf1o.2 
 |-  G = ( x e. B , y e. A |-> ( ( B .o y ) +o x ) )
3 eqid 
 |-  ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) = ( y e. A , x e. B |-> ( ( B .o y ) +o x ) )
4 3 omxpenlem 
 |-  ( ( B e. On /\ A e. On ) -> ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) : ( A X. B ) -1-1-onto-> ( B .o A ) )
5 4 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) : ( A X. B ) -1-1-onto-> ( B .o A ) )
6 eqid 
 |-  ( z e. ( B X. A ) |-> U. `' { z } ) = ( z e. ( B X. A ) |-> U. `' { z } )
7 6 xpcomf1o 
 |-  ( z e. ( B X. A ) |-> U. `' { z } ) : ( B X. A ) -1-1-onto-> ( A X. B )
8 f1oco 
 |-  ( ( ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) : ( A X. B ) -1-1-onto-> ( B .o A ) /\ ( z e. ( B X. A ) |-> U. `' { z } ) : ( B X. A ) -1-1-onto-> ( A X. B ) ) -> ( ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) o. ( z e. ( B X. A ) |-> U. `' { z } ) ) : ( B X. A ) -1-1-onto-> ( B .o A ) )
9 5 7 8 sylancl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) o. ( z e. ( B X. A ) |-> U. `' { z } ) ) : ( B X. A ) -1-1-onto-> ( B .o A ) )
10 6 3 xpcomco 
 |-  ( ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) o. ( z e. ( B X. A ) |-> U. `' { z } ) ) = ( x e. B , y e. A |-> ( ( B .o y ) +o x ) )
11 2 10 eqtr4i 
 |-  G = ( ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) o. ( z e. ( B X. A ) |-> U. `' { z } ) )
12 f1oeq1 
 |-  ( G = ( ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) o. ( z e. ( B X. A ) |-> U. `' { z } ) ) -> ( G : ( B X. A ) -1-1-onto-> ( B .o A ) <-> ( ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) o. ( z e. ( B X. A ) |-> U. `' { z } ) ) : ( B X. A ) -1-1-onto-> ( B .o A ) ) )
13 11 12 ax-mp 
 |-  ( G : ( B X. A ) -1-1-onto-> ( B .o A ) <-> ( ( y e. A , x e. B |-> ( ( B .o y ) +o x ) ) o. ( z e. ( B X. A ) |-> U. `' { z } ) ) : ( B X. A ) -1-1-onto-> ( B .o A ) )
14 9 13 sylibr 
 |-  ( ( A e. On /\ B e. On ) -> G : ( B X. A ) -1-1-onto-> ( B .o A ) )
15 1 omxpenlem 
 |-  ( ( A e. On /\ B e. On ) -> F : ( B X. A ) -1-1-onto-> ( A .o B ) )
16 f1ocnv 
 |-  ( F : ( B X. A ) -1-1-onto-> ( A .o B ) -> `' F : ( A .o B ) -1-1-onto-> ( B X. A ) )
17 15 16 syl 
 |-  ( ( A e. On /\ B e. On ) -> `' F : ( A .o B ) -1-1-onto-> ( B X. A ) )
18 f1oco 
 |-  ( ( G : ( B X. A ) -1-1-onto-> ( B .o A ) /\ `' F : ( A .o B ) -1-1-onto-> ( B X. A ) ) -> ( G o. `' F ) : ( A .o B ) -1-1-onto-> ( B .o A ) )
19 14 17 18 syl2anc 
 |-  ( ( A e. On /\ B e. On ) -> ( G o. `' F ) : ( A .o B ) -1-1-onto-> ( B .o A ) )