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

Metamath Proof Explorer

Theorem ofres

Description: Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Hypotheses ofres.1 ⊢ φ → F Fn A
ofres.2 ⊢ φ → G Fn B
ofres.3 ⊢ φ → A ∈ V
ofres.4 ⊢ φ → B ∈ W
ofres.5 ⊢ A ∩ B = C
Assertion ofres ⊢ φ → F R f G = F ↾ C R f G ↾ C

Proof

Step Hyp Ref Expression
1 ofres.1 ⊢ φ → F Fn A
2 ofres.2 ⊢ φ → G Fn B
3 ofres.3 ⊢ φ → A ∈ V
4 ofres.4 ⊢ φ → B ∈ W
5 ofres.5 ⊢ A ∩ B = C
6 eqidd ⊢ φ ∧ x ∈ A → F ⁡ x = F ⁡ x
7 eqidd ⊢ φ ∧ x ∈ B → G ⁡ x = G ⁡ x
8 1 2 3 4 5 6 7 offval ⊢ φ → F R f G = x ∈ C ⟼ F ⁡ x R G ⁡ x
9 inss1 ⊢ A ∩ B ⊆ A
10 5 9 eqsstrri ⊢ C ⊆ A
11 fnssres ⊢ F Fn A ∧ C ⊆ A → F ↾ C Fn C
12 1 10 11 sylancl ⊢ φ → F ↾ C Fn C
13 inss2 ⊢ A ∩ B ⊆ B
14 5 13 eqsstrri ⊢ C ⊆ B
15 fnssres ⊢ G Fn B ∧ C ⊆ B → G ↾ C Fn C
16 2 14 15 sylancl ⊢ φ → G ↾ C Fn C
17 ssexg ⊢ C ⊆ A ∧ A ∈ V → C ∈ V
18 10 3 17 sylancr ⊢ φ → C ∈ V
19 inidm ⊢ C ∩ C = C
20 fvres ⊢ x ∈ C → F ↾ C ⁡ x = F ⁡ x
21 20 adantl ⊢ φ ∧ x ∈ C → F ↾ C ⁡ x = F ⁡ x
22 fvres ⊢ x ∈ C → G ↾ C ⁡ x = G ⁡ x
23 22 adantl ⊢ φ ∧ x ∈ C → G ↾ C ⁡ x = G ⁡ x
24 12 16 18 18 19 21 23 offval ⊢ φ → F ↾ C R f G ↾ C = x ∈ C ⟼ F ⁡ x R G ⁡ x
25 8 24 eqtr4d ⊢ φ → F R f G = F ↾ C R f G ↾ C