Theorem tposf2

Description: The domain and range 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 𝐹 : ◡ 𝐴 ⟶ 𝐵 ) )