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

Metamath Proof Explorer

Theorem tposf2

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

Ref Expression
Assertion tposf2 ( Rel 𝐴 → ( 𝐹 : 𝐴 ⟶ 𝐵 → tpos 𝐹 : ◡ 𝐴 ⟶ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 tposfo2 ⊢ ( Rel 𝐴 → ( 𝐹 : 𝐴 –onto→ ran 𝐹 → tpos 𝐹 : ◡ 𝐴 –onto→ ran 𝐹 ) )
2 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
3 dffn4 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 )
4 2 3 sylib ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –onto→ ran 𝐹 )
5 1 4 impel ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → tpos 𝐹 : ◡ 𝐴 –onto→ ran 𝐹 )
6 fof ⊢ ( tpos 𝐹 : ◡ 𝐴 –onto→ ran 𝐹 → tpos 𝐹 : ◡ 𝐴 ⟶ ran 𝐹 )
7 5 6 syl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → tpos 𝐹 : ◡ 𝐴 ⟶ ran 𝐹 )
8 frn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ran 𝐹 ⊆ 𝐵 )
9 8 adantl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ran 𝐹 ⊆ 𝐵 )
10 7 9 fssd ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → tpos 𝐹 : ◡ 𝐴 ⟶ 𝐵 )
11 10 ex ⊢ ( Rel 𝐴 → ( 𝐹 : 𝐴 ⟶ 𝐵 → tpos 𝐹 : ◡ 𝐴 ⟶ 𝐵 ) )