ov

Description: The value of an operation class abstraction. (Contributed by NM, 16-May-1995) (Revised by David Abernethy, 19-Jun-2012)

	Ref	Expression
Hypotheses	ov.1	⊢ 𝐶 ∈ V
	ov.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	ov.3	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	ov.4	⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
	ov.5	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃! 𝑧 𝜑 )
	ov.6	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) }
Assertion	ov	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		ov.1	⊢ 𝐶 ∈ V
2		ov.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		ov.3	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
4		ov.4	⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
5		ov.5	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃! 𝑧 𝜑 )
6		ov.6	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) }
7		df-ov	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
8	6	fveq1i	⊢ ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ )
9	7 8	eqtri	⊢ ( 𝐴 𝐹 𝐵 ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ )
10	9	eqeq1i	⊢ ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 )
11	5	fnoprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) }
12		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑅 ↔ 𝐴 ∈ 𝑅 ) )
13	12	anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ) )
14		eleq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆 ) )
15	14	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) )
16	13 15	opelopabg	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) )
17	16	ibir	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } )
18		fnopfvb	⊢ ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ) → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) )
19	11 17 18	sylancr	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) )
20	13 2	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜓 ) ) )
21	15 3	anbi12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜓 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜒 ) ) )
22	4	anbi2d	⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜒 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
23	20 21 22	eloprabg	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ V ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
24	1 23	mp3an3	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
25	19 24	bitrd	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
26	10 25	bitrid	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
27	26	bianabs	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ 𝜃 ) )

Metamath Proof Explorer

Theorem ov

Proof