Theorem fcof

Description: Composition of a function with domain and codomain and a function as a function with domain and codomain. Generalization of fco . (Contributed by AV, 18-Sep-2024)

	Ref	Expression
Assertion	fcof	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
2		fncofn	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) )
3	2	ex	⊢ ( 𝐹 Fn 𝐴 → ( Fun 𝐺 → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ) )
4	3	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) → ( Fun 𝐺 → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ) )
5		rncoss	⊢ ran ( 𝐹 ∘ 𝐺 ) ⊆ ran 𝐹
6		sstr	⊢ ( ( ran ( 𝐹 ∘ 𝐺 ) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 )
7	5 6	mpan	⊢ ( ran 𝐹 ⊆ 𝐵 → ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 )
8	7	adantl	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) → ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 )
9	4 8	jctird	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) → ( Fun 𝐺 → ( ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ∧ ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 ) ) )
10	9	imp	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ∧ Fun 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ∧ ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 ) )
11	1 10	sylanb	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ∧ ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 ) )
12		df-f	⊢ ( ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) ⟶ 𝐵 ↔ ( ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ∧ ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 ) )
13	11 12	sylibr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) ⟶ 𝐵 )