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 ) )