This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnco

Description: Composition of two functions with domains as a function with domain. (Contributed by NM, 22-May-2006) (Proof shortened by AV, 20-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 fnfun ⊢ G Fn B → Fun ⁡ G
2 fncofn ⊢ F Fn A ∧ Fun ⁡ G → F ∘ G Fn G -1 A
3 1 2 sylan2 ⊢ F Fn A ∧ G Fn B → F ∘ G Fn G -1 A
4 3 3adant3 ⊢ F Fn A ∧ G Fn B ∧ ran ⁡ G ⊆ A → F ∘ G Fn G -1 A
5 cnvimassrndm ⊢ ran ⁡ G ⊆ A → G -1 A = dom ⁡ G
6 5 3ad2ant3 ⊢ F Fn A ∧ G Fn B ∧ ran ⁡ G ⊆ A → G -1 A = dom ⁡ G
7 fndm ⊢ G Fn B → dom ⁡ G = B
8 7 3ad2ant2 ⊢ F Fn A ∧ G Fn B ∧ ran ⁡ G ⊆ A → dom ⁡ G = B
9 6 8 eqtr2d ⊢ F Fn A ∧ G Fn B ∧ ran ⁡ G ⊆ A → B = G -1 A
10 9 fneq2d ⊢ F Fn A ∧ G Fn B ∧ ran ⁡ G ⊆ A → F ∘ G Fn B ↔ F ∘ G Fn G -1 A
11 4 10 mpbird ⊢ F Fn A ∧ G Fn B ∧ ran ⁡ G ⊆ A → F ∘ G Fn B