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

Metamath Proof Explorer

Theorem ovmpt4g

Description: Value of a function given by the maps-to notation. (This is the operation analogue of fvmpt2 .) (Contributed by NM, 21-Feb-2004) (Revised by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypothesis ovmpt4g.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion ovmpt4g ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 ovmpt4g.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2 elisset ⊢ ( 𝐶 ∈ 𝑉 → ∃ 𝑧 𝑧 = 𝐶 )
3 moeq ⊢ ∃* 𝑧 𝑧 = 𝐶
4 3 a1i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑧 𝑧 = 𝐶 )
5 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
6 1 5 eqtri ⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
7 4 6 ovidi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = 𝐶 → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) )
8 eqeq2 ⊢ ( 𝑧 = 𝐶 → ( ( 𝑥 𝐹 𝑦 ) = 𝑧 ↔ ( 𝑥 𝐹 𝑦 ) = 𝐶 ) )
9 7 8 mpbidi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = 𝐶 → ( 𝑥 𝐹 𝑦 ) = 𝐶 ) )
10 9 exlimdv ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑧 𝑧 = 𝐶 → ( 𝑥 𝐹 𝑦 ) = 𝐶 ) )
11 2 10 syl5 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐶 ∈ 𝑉 → ( 𝑥 𝐹 𝑦 ) = 𝐶 ) )
12 11 3impia ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )