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

Metamath Proof Explorer

Theorem ovmpox

Description: The value of an operation class abstraction. Variant of ovmpoga which does not require D and x to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 20-Dec-2013)

Ref Expression
Hypotheses ovmpox.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑅 = 𝑆 )
ovmpox.2 ⊢ ( 𝑥 = 𝐴 → 𝐷 = 𝐿 )
ovmpox.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
Assertion ovmpox ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ 𝐻 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 ovmpox.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑅 = 𝑆 )
2 ovmpox.2 ⊢ ( 𝑥 = 𝐴 → 𝐷 = 𝐿 )
3 ovmpox.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
4 elex ⊢ ( 𝑆 ∈ 𝐻 → 𝑆 ∈ V )
5 3 a1i ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ V ) → 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) )
6 1 adantl ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ V ) ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 )
7 2 adantl ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ V ) ∧ 𝑥 = 𝐴 ) → 𝐷 = 𝐿 )
8 simp1 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ V ) → 𝐴 ∈ 𝐶 )
9 simp2 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ V ) → 𝐵 ∈ 𝐿 )
10 simp3 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ V ) → 𝑆 ∈ V )
11 5 6 7 8 9 10 ovmpodx ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ V ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )
12 4 11 syl3an3 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ 𝐻 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )