# Metamath Proof Explorer

## Theorem ofval

Description: Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Hypotheses offval.1 $⊢ φ → F Fn A$
offval.2 $⊢ φ → G Fn B$
offval.3 $⊢ φ → A ∈ V$
offval.4 $⊢ φ → B ∈ W$
offval.5 $⊢ A ∩ B = S$
ofval.6 $⊢ φ ∧ X ∈ A → F ⁡ X = C$
ofval.7 $⊢ φ ∧ X ∈ B → G ⁡ X = D$
Assertion ofval $⊢ φ ∧ X ∈ S → F R f G ⁡ X = C R D$

### Proof

Step Hyp Ref Expression
1 offval.1 $⊢ φ → F Fn A$
2 offval.2 $⊢ φ → G Fn B$
3 offval.3 $⊢ φ → A ∈ V$
4 offval.4 $⊢ φ → B ∈ W$
5 offval.5 $⊢ A ∩ B = S$
6 ofval.6 $⊢ φ ∧ X ∈ A → F ⁡ X = C$
7 ofval.7 $⊢ φ ∧ X ∈ B → G ⁡ X = D$
8 eqidd $⊢ φ ∧ x ∈ A → F ⁡ x = F ⁡ x$
9 eqidd $⊢ φ ∧ x ∈ B → G ⁡ x = G ⁡ x$
10 1 2 3 4 5 8 9 offval $⊢ φ → F R f G = x ∈ S ⟼ F ⁡ x R G ⁡ x$
11 10 fveq1d $⊢ φ → F R f G ⁡ X = x ∈ S ⟼ F ⁡ x R G ⁡ x ⁡ X$
12 11 adantr $⊢ φ ∧ X ∈ S → F R f G ⁡ X = x ∈ S ⟼ F ⁡ x R G ⁡ x ⁡ X$
13 fveq2 $⊢ x = X → F ⁡ x = F ⁡ X$
14 fveq2 $⊢ x = X → G ⁡ x = G ⁡ X$
15 13 14 oveq12d $⊢ x = X → F ⁡ x R G ⁡ x = F ⁡ X R G ⁡ X$
16 eqid $⊢ x ∈ S ⟼ F ⁡ x R G ⁡ x = x ∈ S ⟼ F ⁡ x R G ⁡ x$
17 ovex $⊢ F ⁡ X R G ⁡ X ∈ V$
18 15 16 17 fvmpt $⊢ X ∈ S → x ∈ S ⟼ F ⁡ x R G ⁡ x ⁡ X = F ⁡ X R G ⁡ X$
19 18 adantl $⊢ φ ∧ X ∈ S → x ∈ S ⟼ F ⁡ x R G ⁡ x ⁡ X = F ⁡ X R G ⁡ X$
20 inss1 $⊢ A ∩ B ⊆ A$
21 5 20 eqsstrri $⊢ S ⊆ A$
22 21 sseli $⊢ X ∈ S → X ∈ A$
23 22 6 sylan2 $⊢ φ ∧ X ∈ S → F ⁡ X = C$
24 inss2 $⊢ A ∩ B ⊆ B$
25 5 24 eqsstrri $⊢ S ⊆ B$
26 25 sseli $⊢ X ∈ S → X ∈ B$
27 26 7 sylan2 $⊢ φ ∧ X ∈ S → G ⁡ X = D$
28 23 27 oveq12d $⊢ φ ∧ X ∈ S → F ⁡ X R G ⁡ X = C R D$
29 12 19 28 3eqtrd $⊢ φ ∧ X ∈ S → F R f G ⁡ X = C R D$