Metamath Proof Explorer

Theorem ofco

Description: The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014)

Ref Expression
Hypotheses ofco.1 ⊢ φ → F Fn A
ofco.2 ⊢ φ → G Fn B
ofco.3 ⊢ φ → H : D ⟶ C
ofco.4 ⊢ φ → A ∈ V
ofco.5 ⊢ φ → B ∈ W
ofco.6 ⊢ φ → D ∈ X
ofco.7 ⊢ A ∩ B = C
Assertion ofco ⊢ φ → F R f G ∘ H = F ∘ H R f G ∘ H

Proof

Step Hyp Ref Expression
1 ofco.1 ⊢ φ → F Fn A
2 ofco.2 ⊢ φ → G Fn B
3 ofco.3 ⊢ φ → H : D ⟶ C
4 ofco.4 ⊢ φ → A ∈ V
5 ofco.5 ⊢ φ → B ∈ W
6 ofco.6 ⊢ φ → D ∈ X
7 ofco.7 ⊢ A ∩ B = C
8 3 ffvelrnda ⊢ φ ∧ x ∈ D → H ⁡ x ∈ C
9 3 feqmptd ⊢ φ → H = x ∈ D ⟼ H ⁡ x
10 eqidd ⊢ φ ∧ y ∈ A → F ⁡ y = F ⁡ y
11 eqidd ⊢ φ ∧ y ∈ B → G ⁡ y = G ⁡ y
12 1 2 4 5 7 10 11 offval ⊢ φ → F R f G = y ∈ C ⟼ F ⁡ y R G ⁡ y
13 fveq2 ⊢ y = H ⁡ x → F ⁡ y = F ⁡ H ⁡ x
14 fveq2 ⊢ y = H ⁡ x → G ⁡ y = G ⁡ H ⁡ x
15 13 14 oveq12d ⊢ y = H ⁡ x → F ⁡ y R G ⁡ y = F ⁡ H ⁡ x R G ⁡ H ⁡ x
16 8 9 12 15 fmptco ⊢ φ → F R f G ∘ H = x ∈ D ⟼ F ⁡ H ⁡ x R G ⁡ H ⁡ x
17 inss1 ⊢ A ∩ B ⊆ A
18 7 17 eqsstrri ⊢ C ⊆ A
19 fss ⊢ H : D ⟶ C ∧ C ⊆ A → H : D ⟶ A
20 3 18 19 sylancl ⊢ φ → H : D ⟶ A
21 fnfco ⊢ F Fn A ∧ H : D ⟶ A → F ∘ H Fn D
22 1 20 21 syl2anc ⊢ φ → F ∘ H Fn D
23 inss2 ⊢ A ∩ B ⊆ B
24 7 23 eqsstrri ⊢ C ⊆ B
25 fss ⊢ H : D ⟶ C ∧ C ⊆ B → H : D ⟶ B
26 3 24 25 sylancl ⊢ φ → H : D ⟶ B
27 fnfco ⊢ G Fn B ∧ H : D ⟶ B → G ∘ H Fn D
28 2 26 27 syl2anc ⊢ φ → G ∘ H Fn D
29 inidm ⊢ D ∩ D = D
30 3 ffnd ⊢ φ → H Fn D
31 fvco2 ⊢ H Fn D ∧ x ∈ D → F ∘ H ⁡ x = F ⁡ H ⁡ x
32 30 31 sylan ⊢ φ ∧ x ∈ D → F ∘ H ⁡ x = F ⁡ H ⁡ x
33 fvco2 ⊢ H Fn D ∧ x ∈ D → G ∘ H ⁡ x = G ⁡ H ⁡ x
34 30 33 sylan ⊢ φ ∧ x ∈ D → G ∘ H ⁡ x = G ⁡ H ⁡ x
35 22 28 6 6 29 32 34 offval ⊢ φ → F ∘ H R f G ∘ H = x ∈ D ⟼ F ⁡ H ⁡ x R G ⁡ H ⁡ x
36 16 35 eqtr4d ⊢ φ → F R f G ∘ H = F ∘ H R f G ∘ H