# Metamath Proof Explorer

## 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 ( ( 𝐹 : 𝐵𝐶𝐺 : 𝐴𝐵 ) → ( 𝐹𝐺 ) : 𝐴𝐶 )