Description: The domain and range of a transposition. (Contributed by NM, 10-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | tposf | ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → tpos 𝐹 : ( 𝐵 × 𝐴 ) ⟶ 𝐶 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relxp | ⊢ Rel ( 𝐴 × 𝐵 ) | |
2 | tposf2 | ⊢ ( Rel ( 𝐴 × 𝐵 ) → ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → tpos 𝐹 : ◡ ( 𝐴 × 𝐵 ) ⟶ 𝐶 ) ) | |
3 | 1 2 | ax-mp | ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → tpos 𝐹 : ◡ ( 𝐴 × 𝐵 ) ⟶ 𝐶 ) |
4 | cnvxp | ⊢ ◡ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) | |
5 | 4 | feq2i | ⊢ ( tpos 𝐹 : ◡ ( 𝐴 × 𝐵 ) ⟶ 𝐶 ↔ tpos 𝐹 : ( 𝐵 × 𝐴 ) ⟶ 𝐶 ) |
6 | 3 5 | sylib | ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → tpos 𝐹 : ( 𝐵 × 𝐴 ) ⟶ 𝐶 ) |