Theorem fnco

Description: Composition of two functions. (Contributed by NM, 22-May-2006)

	Ref	Expression
Assertion	fnco	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → ( 𝐹 ∘ 𝐺 ) Fn 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
2		fnfun	⊢ ( 𝐺 Fn 𝐵 → Fun 𝐺 )
3		funco	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → Fun ( 𝐹 ∘ 𝐺 ) )
5	4	3adant3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → Fun ( 𝐹 ∘ 𝐺 ) )
6		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
7	6	sseq2d	⊢ ( 𝐹 Fn 𝐴 → ( ran 𝐺 ⊆ dom 𝐹 ↔ ran 𝐺 ⊆ 𝐴 ) )
8	7	biimpar	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐴 ) → ran 𝐺 ⊆ dom 𝐹 )
9		dmcosseq	⊢ ( ran 𝐺 ⊆ dom 𝐹 → dom ( 𝐹 ∘ 𝐺 ) = dom 𝐺 )
10	8 9	syl	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐴 ) → dom ( 𝐹 ∘ 𝐺 ) = dom 𝐺 )
11	10	3adant2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → dom ( 𝐹 ∘ 𝐺 ) = dom 𝐺 )
12		fndm	⊢ ( 𝐺 Fn 𝐵 → dom 𝐺 = 𝐵 )
13	12	3ad2ant2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → dom 𝐺 = 𝐵 )
14	11 13	eqtrd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → dom ( 𝐹 ∘ 𝐺 ) = 𝐵 )
15		df-fn	⊢ ( ( 𝐹 ∘ 𝐺 ) Fn 𝐵 ↔ ( Fun ( 𝐹 ∘ 𝐺 ) ∧ dom ( 𝐹 ∘ 𝐺 ) = 𝐵 ) )
16	5 14 15	sylanbrc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → ( 𝐹 ∘ 𝐺 ) Fn 𝐵 )