Theorem tposfn2

Description: The domain of a transposition. (Contributed by NM, 10-Sep-2015)

	Ref	Expression
Assertion	tposfn2	⊢ ( Rel 𝐴 → ( 𝐹 Fn 𝐴 → tpos 𝐹 Fn ◡ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		tposfun	⊢ ( Fun 𝐹 → Fun tpos 𝐹 )
2	1	a1i	⊢ ( Rel 𝐴 → ( Fun 𝐹 → Fun tpos 𝐹 ) )
3		dmtpos	⊢ ( Rel dom 𝐹 → dom tpos 𝐹 = ◡ dom 𝐹 )
4	3	a1i	⊢ ( dom 𝐹 = 𝐴 → ( Rel dom 𝐹 → dom tpos 𝐹 = ◡ dom 𝐹 ) )
5		releq	⊢ ( dom 𝐹 = 𝐴 → ( Rel dom 𝐹 ↔ Rel 𝐴 ) )
6		cnveq	⊢ ( dom 𝐹 = 𝐴 → ◡ dom 𝐹 = ◡ 𝐴 )
7	6	eqeq2d	⊢ ( dom 𝐹 = 𝐴 → ( dom tpos 𝐹 = ◡ dom 𝐹 ↔ dom tpos 𝐹 = ◡ 𝐴 ) )
8	4 5 7	3imtr3d	⊢ ( dom 𝐹 = 𝐴 → ( Rel 𝐴 → dom tpos 𝐹 = ◡ 𝐴 ) )
9	8	com12	⊢ ( Rel 𝐴 → ( dom 𝐹 = 𝐴 → dom tpos 𝐹 = ◡ 𝐴 ) )
10	2 9	anim12d	⊢ ( Rel 𝐴 → ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) → ( Fun tpos 𝐹 ∧ dom tpos 𝐹 = ◡ 𝐴 ) ) )
11		df-fn	⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
12		df-fn	⊢ ( tpos 𝐹 Fn ◡ 𝐴 ↔ ( Fun tpos 𝐹 ∧ dom tpos 𝐹 = ◡ 𝐴 ) )
13	10 11 12	3imtr4g	⊢ ( Rel 𝐴 → ( 𝐹 Fn 𝐴 → tpos 𝐹 Fn ◡ 𝐴 ) )