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

Metamath Proof Explorer

Theorem offn

Description: The function operation produces a function. (Contributed by Mario Carneiro, 22-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
Assertion offn ⊢ φ → F R f G Fn S

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 ovex ⊢ F ⁡ x R G ⁡ x ∈ V
7 eqid ⊢ x ∈ S ⟼ F ⁡ x R G ⁡ x = x ∈ S ⟼ F ⁡ x R G ⁡ x
8 6 7 fnmpti ⊢ x ∈ S ⟼ F ⁡ x R G ⁡ x Fn S
9 eqidd ⊢ φ ∧ x ∈ A → F ⁡ x = F ⁡ x
10 eqidd ⊢ φ ∧ x ∈ B → G ⁡ x = G ⁡ x
11 1 2 3 4 5 9 10 offval ⊢ φ → F R f G = x ∈ S ⟼ F ⁡ x R G ⁡ x
12 11 fneq1d ⊢ φ → F R f G Fn S ↔ x ∈ S ⟼ F ⁡ x R G ⁡ x Fn S
13 8 12 mpbiri ⊢ φ → F R f G Fn S