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=xB,yAA𝑜x+𝑜y
omf1o.2 G=xB,yAB𝑜y+𝑜x
Assertion omf1o AOnBOnGF-1:A𝑜B1-1 ontoB𝑜A

Proof

Step Hyp Ref Expression
1 omf1o.1 F=xB,yAA𝑜x+𝑜y
2 omf1o.2 G=xB,yAB𝑜y+𝑜x
3 eqid yA,xBB𝑜y+𝑜x=yA,xBB𝑜y+𝑜x
4 3 omxpenlem BOnAOnyA,xBB𝑜y+𝑜x:A×B1-1 ontoB𝑜A
5 4 ancoms AOnBOnyA,xBB𝑜y+𝑜x:A×B1-1 ontoB𝑜A
6 eqid zB×Az-1=zB×Az-1
7 6 xpcomf1o zB×Az-1:B×A1-1 ontoA×B
8 f1oco yA,xBB𝑜y+𝑜x:A×B1-1 ontoB𝑜AzB×Az-1:B×A1-1 ontoA×ByA,xBB𝑜y+𝑜xzB×Az-1:B×A1-1 ontoB𝑜A
9 5 7 8 sylancl AOnBOnyA,xBB𝑜y+𝑜xzB×Az-1:B×A1-1 ontoB𝑜A
10 6 3 xpcomco yA,xBB𝑜y+𝑜xzB×Az-1=xB,yAB𝑜y+𝑜x
11 2 10 eqtr4i G=yA,xBB𝑜y+𝑜xzB×Az-1
12 f1oeq1 G=yA,xBB𝑜y+𝑜xzB×Az-1G:B×A1-1 ontoB𝑜AyA,xBB𝑜y+𝑜xzB×Az-1:B×A1-1 ontoB𝑜A
13 11 12 ax-mp G:B×A1-1 ontoB𝑜AyA,xBB𝑜y+𝑜xzB×Az-1:B×A1-1 ontoB𝑜A
14 9 13 sylibr AOnBOnG:B×A1-1 ontoB𝑜A
15 1 omxpenlem AOnBOnF:B×A1-1 ontoA𝑜B
16 f1ocnv F:B×A1-1 ontoA𝑜BF-1:A𝑜B1-1 ontoB×A
17 15 16 syl AOnBOnF-1:A𝑜B1-1 ontoB×A
18 f1oco G:B×A1-1 ontoB𝑜AF-1:A𝑜B1-1 ontoB×AGF-1:A𝑜B1-1 ontoB𝑜A
19 14 17 18 syl2anc AOnBOnGF-1:A𝑜B1-1 ontoB𝑜A