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

Metamath Proof Explorer

Theorem ovg

Description: The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010)

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

Proof

Step Hyp Ref Expression
1 ovg.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 ovg.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3 ovg.3 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
4 ovg.4 ⊢ ( ( 𝜏 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ) → ∃! 𝑧 𝜑 )
5 ovg.5 ⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) }
6 df-ov ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
7 5 fveq1i ⊢ ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ )
8 6 7 eqtri ⊢ ( 𝐴 𝐹 𝐵 ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ )
9 8 eqeq1i ⊢ ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 )
10 eqeq2 ⊢ ( 𝑐 = 𝐶 → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑐 ↔ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ) )
11 opeq2 ⊢ ( 𝑐 = 𝐶 → ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑐 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ )
12 11 eleq1d ⊢ ( 𝑐 = 𝐶 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑐 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) )
13 10 12 bibi12d ⊢ ( 𝑐 = 𝐶 → ( ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑐 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑐 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ↔ ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) )
14 13 imbi2d ⊢ ( 𝑐 = 𝐶 → ( ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑐 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑐 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) ↔ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) ) )
15 4 ex ⊢ ( 𝜏 → ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃! 𝑧 𝜑 ) )
16 15 alrimivv ⊢ ( 𝜏 → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃! 𝑧 𝜑 ) )
17 fnoprabg ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃! 𝑧 𝜑 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } )
18 16 17 syl ⊢ ( 𝜏 → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } )
19 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑅 ↔ 𝐴 ∈ 𝑅 ) )
20 19 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ) )
21 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆 ) )
22 21 anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) )
23 20 22 opelopabg ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) )
24 23 ibir ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } )
25 fnopfvb ⊢ ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ) → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑐 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑐 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) )
26 18 24 25 syl2an ⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑐 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑐 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) )
27 14 26 vtoclg ⊢ ( 𝐶 ∈ 𝐷 → ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) )
28 27 com12 ⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐶 ∈ 𝐷 → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) )
29 28 exp32 ⊢ ( 𝜏 → ( 𝐴 ∈ 𝑅 → ( 𝐵 ∈ 𝑆 → ( 𝐶 ∈ 𝐷 → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) ) ) ) )
30 29 3imp2 ⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ) )
31 20 1 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜓 ) ) )
32 22 2 anbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜓 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜒 ) ) )
33 3 anbi2d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜒 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
34 31 32 33 eloprabg ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
35 34 adantl ⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
36 30 35 bitrd ⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
37 9 36 bitrid ⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
38 biidd ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ) )
39 38 bianabs ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ↔ 𝜃 ) )
40 39 3adant3 ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ↔ 𝜃 ) )
41 40 adantl ⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝜃 ) ↔ 𝜃 ) )
42 37 41 bitrd ⊢ ( ( 𝜏 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ 𝜃 ) )