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→ ( 𝐵 × 𝐴 )