Theorem fco

Description: Composition of two mappings. (Contributed by NM, 29-Aug-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Assertion	fco	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )

Proof

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