Metamath Proof Explorer

Theorem fnco

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

Ref Expression
Assertion fnco ⊢ F Fn A ∧ G Fn B ∧ ran ⁡ G ⊆ A → F ∘ G Fn B

Proof

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