Theorem fncofn

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

	Ref	Expression
Assertion	fncofn	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
2		funco	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )
3	1 2	sylan	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )
4	3	funfnd	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) Fn dom ( 𝐹 ∘ 𝐺 ) )
5		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6	5	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → dom 𝐹 = 𝐴 )
7	6	eqcomd	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → 𝐴 = dom 𝐹 )
8	7	imaeq2d	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( ◡ 𝐺 “ 𝐴 ) = ( ◡ 𝐺 “ dom 𝐹 ) )
9		dmco	⊢ dom ( 𝐹 ∘ 𝐺 ) = ( ◡ 𝐺 “ dom 𝐹 )
10	8 9	eqtr4di	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( ◡ 𝐺 “ 𝐴 ) = dom ( 𝐹 ∘ 𝐺 ) )
11	10	fneq2d	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ↔ ( 𝐹 ∘ 𝐺 ) Fn dom ( 𝐹 ∘ 𝐺 ) ) )
12	4 11	mpbird	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) )