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