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