Theorem funcofd

Description: Composition of two functions as a function with domain and codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Proof shortened by AV, 20-Sep-2024)

	Ref	Expression
Hypotheses	funcofd.1	⊢ ( 𝜑 → Fun 𝐹 )
	funcofd.2	⊢ ( 𝜑 → Fun 𝐺 )
Assertion	funcofd	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ dom 𝐹 ) ⟶ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		funcofd.1	⊢ ( 𝜑 → Fun 𝐹 )
2		funcofd.2	⊢ ( 𝜑 → Fun 𝐺 )
3		fdmrn	⊢ ( Fun 𝐹 ↔ 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
4	1 3	sylib	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
5		fcof	⊢ ( ( 𝐹 : dom 𝐹 ⟶ ran 𝐹 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ dom 𝐹 ) ⟶ ran 𝐹 )
6	4 2 5	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ dom 𝐹 ) ⟶ ran 𝐹 )