Theorem tposfn

Description: Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Assertion	tposfn	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → tpos 𝐹 Fn ( 𝐵 × 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		tposf	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ V → tpos 𝐹 : ( 𝐵 × 𝐴 ) ⟶ V )
2		dffn2	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ↔ 𝐹 : ( 𝐴 × 𝐵 ) ⟶ V )
3		dffn2	⊢ ( tpos 𝐹 Fn ( 𝐵 × 𝐴 ) ↔ tpos 𝐹 : ( 𝐵 × 𝐴 ) ⟶ V )
4	1 2 3	3imtr4i	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → tpos 𝐹 Fn ( 𝐵 × 𝐴 ) )