Metamath Proof Explorer


Theorem ovmpox2

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 ovmpox2.1 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → 𝑅 = 𝑆 )
ovmpox2.2 ( 𝑦 = 𝐵𝐶 = 𝐿 )
ovmpox2.3 𝐹 = ( 𝑥𝐶 , 𝑦𝐷𝑅 )
Assertion ovmpox2 ( ( 𝐴𝐿𝐵𝐷𝑆𝐻 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 ovmpox2.1 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → 𝑅 = 𝑆 )
2 ovmpox2.2 ( 𝑦 = 𝐵𝐶 = 𝐿 )
3 ovmpox2.3 𝐹 = ( 𝑥𝐶 , 𝑦𝐷𝑅 )
4 3 a1i ( ( 𝐴𝐿𝐵𝐷𝑆𝐻 ) → 𝐹 = ( 𝑥𝐶 , 𝑦𝐷𝑅 ) )
5 1 adantl ( ( ( 𝐴𝐿𝐵𝐷𝑆𝐻 ) ∧ ( 𝑥 = 𝐴𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 )
6 2 adantl ( ( ( 𝐴𝐿𝐵𝐷𝑆𝐻 ) ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐿 )
7 simp1 ( ( 𝐴𝐿𝐵𝐷𝑆𝐻 ) → 𝐴𝐿 )
8 simp2 ( ( 𝐴𝐿𝐵𝐷𝑆𝐻 ) → 𝐵𝐷 )
9 simp3 ( ( 𝐴𝐿𝐵𝐷𝑆𝐻 ) → 𝑆𝐻 )
10 4 5 6 7 8 9 ovmpordx ( ( 𝐴𝐿𝐵𝐷𝑆𝐻 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )