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 e. A |-> ( B +o x ) ) u. `' ( x e. B |-> ( A +o x ) ) )
Assertion oacomf1o 
|- ( ( A e. On /\ B e. On ) -> F : ( A +o B ) -1-1-onto-> ( B +o A ) )

Proof

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