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

Metamath Proof Explorer

Theorem offvalfv

Description: The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019)

Ref Expression
Hypotheses offvalfv.a ⊢ φ → A ∈ V
offvalfv.f ⊢ φ → F Fn A
offvalfv.g ⊢ φ → G Fn A
Assertion offvalfv ⊢ φ → F R f G = x ∈ A ⟼ F ⁡ x R G ⁡ x

Proof

Step Hyp Ref Expression
1 offvalfv.a ⊢ φ → A ∈ V
2 offvalfv.f ⊢ φ → F Fn A
3 offvalfv.g ⊢ φ → G Fn A
4 fnfvelrn ⊢ F Fn A ∧ x ∈ A → F ⁡ x ∈ ran ⁡ F
5 2 4 sylan ⊢ φ ∧ x ∈ A → F ⁡ x ∈ ran ⁡ F
6 fnfvelrn ⊢ G Fn A ∧ x ∈ A → G ⁡ x ∈ ran ⁡ G
7 3 6 sylan ⊢ φ ∧ x ∈ A → G ⁡ x ∈ ran ⁡ G
8 dffn5 ⊢ F Fn A ↔ F = x ∈ A ⟼ F ⁡ x
9 2 8 sylib ⊢ φ → F = x ∈ A ⟼ F ⁡ x
10 dffn5 ⊢ G Fn A ↔ G = x ∈ A ⟼ G ⁡ x
11 3 10 sylib ⊢ φ → G = x ∈ A ⟼ G ⁡ x
12 1 5 7 9 11 offval2 ⊢ φ → F R f G = x ∈ A ⟼ F ⁡ x R G ⁡ x