Theorem fnresfnco

Description: Composition of two functions, similar to fnco . (Contributed by Alexander van der Vekens, 25-Jul-2017)

	Ref	Expression
Assertion	fnresfnco	⊢ ( ( ( 𝐹 ↾ ran 𝐺 ) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 ∘ 𝐺 ) Fn 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fnfun	⊢ ( ( 𝐹 ↾ ran 𝐺 ) Fn ran 𝐺 → Fun ( 𝐹 ↾ ran 𝐺 ) )
2		fnfun	⊢ ( 𝐺 Fn 𝐵 → Fun 𝐺 )
3		funresfunco	⊢ ( ( Fun ( 𝐹 ↾ ran 𝐺 ) ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )
4	1 2 3	syl2an	⊢ ( ( ( 𝐹 ↾ ran 𝐺 ) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵 ) → Fun ( 𝐹 ∘ 𝐺 ) )
5		fndm	⊢ ( ( 𝐹 ↾ ran 𝐺 ) Fn ran 𝐺 → dom ( 𝐹 ↾ ran 𝐺 ) = ran 𝐺 )
6		dmres	⊢ dom ( 𝐹 ↾ ran 𝐺 ) = ( ran 𝐺 ∩ dom 𝐹 )
7	6	eqeq1i	⊢ ( dom ( 𝐹 ↾ ran 𝐺 ) = ran 𝐺 ↔ ( ran 𝐺 ∩ dom 𝐹 ) = ran 𝐺 )
8		dfss2	⊢ ( ran 𝐺 ⊆ dom 𝐹 ↔ ( ran 𝐺 ∩ dom 𝐹 ) = ran 𝐺 )
9	7 8	sylbb2	⊢ ( dom ( 𝐹 ↾ ran 𝐺 ) = ran 𝐺 → ran 𝐺 ⊆ dom 𝐹 )
10	5 9	syl	⊢ ( ( 𝐹 ↾ ran 𝐺 ) Fn ran 𝐺 → ran 𝐺 ⊆ dom 𝐹 )
11	10	adantr	⊢ ( ( ( 𝐹 ↾ ran 𝐺 ) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵 ) → ran 𝐺 ⊆ dom 𝐹 )
12		dmcosseq	⊢ ( ran 𝐺 ⊆ dom 𝐹 → dom ( 𝐹 ∘ 𝐺 ) = dom 𝐺 )
13	11 12	syl	⊢ ( ( ( 𝐹 ↾ ran 𝐺 ) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵 ) → dom ( 𝐹 ∘ 𝐺 ) = dom 𝐺 )
14		fndm	⊢ ( 𝐺 Fn 𝐵 → dom 𝐺 = 𝐵 )
15	14	adantl	⊢ ( ( ( 𝐹 ↾ ran 𝐺 ) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵 ) → dom 𝐺 = 𝐵 )
16	13 15	eqtrd	⊢ ( ( ( 𝐹 ↾ ran 𝐺 ) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵 ) → dom ( 𝐹 ∘ 𝐺 ) = 𝐵 )
17		df-fn	⊢ ( ( 𝐹 ∘ 𝐺 ) Fn 𝐵 ↔ ( Fun ( 𝐹 ∘ 𝐺 ) ∧ dom ( 𝐹 ∘ 𝐺 ) = 𝐵 ) )
18	4 16 17	sylanbrc	⊢ ( ( ( 𝐹 ↾ ran 𝐺 ) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 ∘ 𝐺 ) Fn 𝐵 )