Metamath Proof Explorer


Theorem oacomf1o

Description: Define a bijection from A +o B to B +o A . Thus, the two are equinumerous even if they are not equal (which sometimes occurs, e.g., oancom ). (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypothesis oacomf1o.1 F = x A B + 𝑜 x x B A + 𝑜 x -1
Assertion oacomf1o A On B On F : A + 𝑜 B 1-1 onto B + 𝑜 A

Proof

Step Hyp Ref Expression
1 oacomf1o.1 F = x A B + 𝑜 x x B A + 𝑜 x -1
2 eqid x A B + 𝑜 x = x A B + 𝑜 x
3 2 oacomf1olem A On B On x A B + 𝑜 x : A 1-1 onto ran x A B + 𝑜 x ran x A B + 𝑜 x B =
4 3 simpld A On B On x A B + 𝑜 x : A 1-1 onto ran x A B + 𝑜 x
5 eqid x B A + 𝑜 x = x B A + 𝑜 x
6 5 oacomf1olem B On A On x B A + 𝑜 x : B 1-1 onto ran x B A + 𝑜 x ran x B A + 𝑜 x A =
7 6 ancoms A On B On x B A + 𝑜 x : B 1-1 onto ran x B A + 𝑜 x ran x B A + 𝑜 x A =
8 7 simpld A On B On x B A + 𝑜 x : B 1-1 onto ran x B A + 𝑜 x
9 f1ocnv x B A + 𝑜 x : B 1-1 onto ran x B A + 𝑜 x x B A + 𝑜 x -1 : ran x B A + 𝑜 x 1-1 onto B
10 8 9 syl A On B On x B A + 𝑜 x -1 : ran x B A + 𝑜 x 1-1 onto B
11 incom A ran x B A + 𝑜 x = ran x B A + 𝑜 x A
12 7 simprd A On B On ran x B A + 𝑜 x A =
13 11 12 eqtrid A On B On A ran x B A + 𝑜 x =
14 3 simprd A On B On ran x A B + 𝑜 x B =
15 f1oun x A B + 𝑜 x : A 1-1 onto ran x A B + 𝑜 x x B A + 𝑜 x -1 : ran x B A + 𝑜 x 1-1 onto B A ran x B A + 𝑜 x = ran x A B + 𝑜 x B = x A B + 𝑜 x x B A + 𝑜 x -1 : A ran x B A + 𝑜 x 1-1 onto ran x A B + 𝑜 x B
16 4 10 13 14 15 syl22anc A On B On x A B + 𝑜 x x B A + 𝑜 x -1 : A ran x B A + 𝑜 x 1-1 onto ran x A B + 𝑜 x B
17 f1oeq1 F = x A B + 𝑜 x x B A + 𝑜 x -1 F : A ran x B A + 𝑜 x 1-1 onto ran x A B + 𝑜 x B x A B + 𝑜 x x B A + 𝑜 x -1 : A ran x B A + 𝑜 x 1-1 onto ran x A B + 𝑜 x B
18 1 17 ax-mp F : A ran x B A + 𝑜 x 1-1 onto ran x A B + 𝑜 x B x A B + 𝑜 x x B A + 𝑜 x -1 : A ran x B A + 𝑜 x 1-1 onto ran x A B + 𝑜 x B
19 16 18 sylibr A On B On F : A ran x B A + 𝑜 x 1-1 onto ran x A B + 𝑜 x B
20 oarec A On B On A + 𝑜 B = A ran x B A + 𝑜 x
21 20 f1oeq2d A On B On F : A + 𝑜 B 1-1 onto ran x A B + 𝑜 x B F : A ran x B A + 𝑜 x 1-1 onto ran x A B + 𝑜 x B
22 19 21 mpbird A On B On F : A + 𝑜 B 1-1 onto ran x A B + 𝑜 x B
23 oarec B On A On B + 𝑜 A = B ran x A B + 𝑜 x
24 23 ancoms A On B On B + 𝑜 A = B ran x A B + 𝑜 x
25 uncom B ran x A B + 𝑜 x = ran x A B + 𝑜 x B
26 24 25 eqtrdi A On B On B + 𝑜 A = ran x A B + 𝑜 x B
27 26 f1oeq3d A On B On F : A + 𝑜 B 1-1 onto B + 𝑜 A F : A + 𝑜 B 1-1 onto ran x A B + 𝑜 x B
28 22 27 mpbird A On B On F : A + 𝑜 B 1-1 onto B + 𝑜 A