Step 
Hyp 
Ref 
Expression 
1 

dff 
⊢ ( 𝐹 : 𝐵 ⟶ 𝐶 ↔ ( 𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) ) 
2 

dff 
⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 ↔ ( 𝐺 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 

dff 
⊢ ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ↔ ( ( 𝐹 ∘ 𝐺 ) Fn 𝐴 ∧ ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐶 ) ) 
14 
12 13

sylibr 
⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ) 