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	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ 𝐻 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )