This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) )
omf1o.2 ⊢ 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) )
Assertion omf1o ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐺 ∘ ◡ 𝐹 ) : ( 𝐴 ·o 𝐵 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) )

Proof

Step Hyp Ref Expression
1 omf1o.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) )
2 omf1o.2 ⊢ 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) )
3 eqid ⊢ ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) = ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) )
4 3 omxpenlem ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) )
5 4 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) )
6 eqid ⊢ ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } ) = ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } )
7 6 xpcomf1o ⊢ ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 × 𝐵 )
8 f1oco ⊢ ( ( ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) ∧ ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 × 𝐵 ) ) → ( ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) ∘ ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } ) ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) )
9 5 7 8 sylancl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) ∘ ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } ) ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) )
10 6 3 xpcomco ⊢ ( ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) ∘ ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) )
11 2 10 eqtr4i ⊢ 𝐺 = ( ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) ∘ ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } ) )
12 f1oeq1 ⊢ ( 𝐺 = ( ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) ∘ ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } ) ) → ( 𝐺 : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) ↔ ( ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) ∘ ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } ) ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) ) )
13 11 12 ax-mp ⊢ ( 𝐺 : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) ↔ ( ( 𝑦 ∈ 𝐴 , 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ·o 𝑦 ) +o 𝑥 ) ) ∘ ( 𝑧 ∈ ( 𝐵 × 𝐴 ) ↦ ∪ ◡ { 𝑧 } ) ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) )
14 9 13 sylibr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐺 : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) )
15 1 omxpenlem ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 ·o 𝐵 ) )
16 f1ocnv ⊢ ( 𝐹 : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 ·o 𝐵 ) → ◡ 𝐹 : ( 𝐴 ·o 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 ) )
17 15 16 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ◡ 𝐹 : ( 𝐴 ·o 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 ) )
18 f1oco ⊢ ( ( 𝐺 : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) ∧ ◡ 𝐹 : ( 𝐴 ·o 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 ) ) → ( 𝐺 ∘ ◡ 𝐹 ) : ( 𝐴 ·o 𝐵 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) )
19 14 17 18 syl2anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐺 ∘ ◡ 𝐹 ) : ( 𝐴 ·o 𝐵 ) –1-1-onto→ ( 𝐵 ·o 𝐴 ) )