Metamath Proof Explorer


Theorem xpcomf1o

Description: The canonical bijection from ( A X. B ) to ( B X. A ) . (Contributed by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypothesis xpcomf1o.1 𝐹 = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ { 𝑥 } )
Assertion xpcomf1o 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 )

Proof

Step Hyp Ref Expression
1 xpcomf1o.1 𝐹 = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ { 𝑥 } )
2 relxp Rel ( 𝐴 × 𝐵 )
3 cnvf1o ( Rel ( 𝐴 × 𝐵 ) → ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ { 𝑥 } ) : ( 𝐴 × 𝐵 ) –1-1-onto ( 𝐴 × 𝐵 ) )
4 2 3 ax-mp ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ { 𝑥 } ) : ( 𝐴 × 𝐵 ) –1-1-onto ( 𝐴 × 𝐵 )
5 f1oeq1 ( 𝐹 = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ { 𝑥 } ) → ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ { 𝑥 } ) : ( 𝐴 × 𝐵 ) –1-1-onto ( 𝐴 × 𝐵 ) ) )
6 1 5 ax-mp ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ { 𝑥 } ) : ( 𝐴 × 𝐵 ) –1-1-onto ( 𝐴 × 𝐵 ) )
7 4 6 mpbir 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto ( 𝐴 × 𝐵 )
8 cnvxp ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 )
9 f1oeq3 ( ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) → ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto ( 𝐴 × 𝐵 ) ↔ 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 ) ) )
10 8 9 ax-mp ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto ( 𝐴 × 𝐵 ) ↔ 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 ) )
11 7 10 mpbi 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 )