Theorem tposfun

Description: The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	tposfun	⊢ ( Fun 𝐹 → Fun tpos 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		funmpt	⊢ Fun ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
2		funco	⊢ ( ( Fun 𝐹 ∧ Fun ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) → Fun ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) )
3	1 2	mpan2	⊢ ( Fun 𝐹 → Fun ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) )
4		df-tpos	⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
5	4	funeqi	⊢ ( Fun tpos 𝐹 ↔ Fun ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) )
6	3 5	sylibr	⊢ ( Fun 𝐹 → Fun tpos 𝐹 )