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