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 ( ( 𝑥𝐴𝑦𝐵𝐶𝑉 ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )