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