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 𝐹 = ( ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) )
Assertion oacomf1o ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 : ( 𝐴 +o 𝐵 ) –1-1-onto→ ( 𝐵 +o 𝐴 ) )

Proof

Step Hyp Ref Expression
1 oacomf1o.1 𝐹 = ( ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) )
2 eqid ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) = ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) )
3 2 oacomf1olem ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) : 𝐴1-1-onto→ ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∧ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∩ 𝐵 ) = ∅ ) )
4 3 simpld ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) : 𝐴1-1-onto→ ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) )
5 eqid ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) = ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) )
6 5 oacomf1olem ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : 𝐵1-1-onto→ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∧ ( ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∩ 𝐴 ) = ∅ ) )
7 6 ancoms ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : 𝐵1-1-onto→ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∧ ( ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∩ 𝐴 ) = ∅ ) )
8 7 simpld ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : 𝐵1-1-onto→ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) )
9 f1ocnv ( ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : 𝐵1-1-onto→ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) → ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) –1-1-onto𝐵 )
10 8 9 syl ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) –1-1-onto𝐵 )
11 incom ( 𝐴 ∩ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) = ( ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∩ 𝐴 )
12 7 simprd ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∩ 𝐴 ) = ∅ )
13 11 12 eqtrid ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∩ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) = ∅ )
14 3 simprd ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∩ 𝐵 ) = ∅ )
15 f1oun ( ( ( ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) : 𝐴1-1-onto→ ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∧ ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) –1-1-onto𝐵 ) ∧ ( ( 𝐴 ∩ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) = ∅ ∧ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∩ 𝐵 ) = ∅ ) ) → ( ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) : ( 𝐴 ∪ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) )
16 4 10 13 14 15 syl22anc ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) : ( 𝐴 ∪ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) )
17 f1oeq1 ( 𝐹 = ( ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) → ( 𝐹 : ( 𝐴 ∪ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) ↔ ( ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) : ( 𝐴 ∪ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) ) )
18 1 17 ax-mp ( 𝐹 : ( 𝐴 ∪ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) ↔ ( ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) : ( 𝐴 ∪ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) )
19 16 18 sylibr ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 : ( 𝐴 ∪ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) )
20 oarec ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ( 𝐴 ∪ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) )
21 20 f1oeq2d ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐹 : ( 𝐴 +o 𝐵 ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) ↔ 𝐹 : ( 𝐴 ∪ ran ( 𝑥𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) ) )
22 19 21 mpbird ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 : ( 𝐴 +o 𝐵 ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) )
23 oarec ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 +o 𝐴 ) = ( 𝐵 ∪ ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ) )
24 23 ancoms ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 +o 𝐴 ) = ( 𝐵 ∪ ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ) )
25 uncom ( 𝐵 ∪ ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ) = ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 )
26 24 25 eqtrdi ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 +o 𝐴 ) = ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) )
27 26 f1oeq3d ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐹 : ( 𝐴 +o 𝐵 ) –1-1-onto→ ( 𝐵 +o 𝐴 ) ↔ 𝐹 : ( 𝐴 +o 𝐵 ) –1-1-onto→ ( ran ( 𝑥𝐴 ↦ ( 𝐵 +o 𝑥 ) ) ∪ 𝐵 ) ) )
28 22 27 mpbird ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 : ( 𝐴 +o 𝐵 ) –1-1-onto→ ( 𝐵 +o 𝐴 ) )