This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ◡ 𝐴 ) )