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