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 syl5bb ( ( 𝜏 ∧ ( 𝐴𝑅𝐵𝑆𝐶𝐷 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ ( ( 𝐴𝑅𝐵𝑆 ) ∧ 𝜃 ) ) )
38 biidd ( ( 𝐴𝑅𝐵𝑆 ) → ( ( ( 𝐴𝑅𝐵𝑆 ) ∧ 𝜃 ) ↔ ( ( 𝐴𝑅𝐵𝑆 ) ∧ 𝜃 ) ) )
39 38 bianabs ( ( 𝐴𝑅𝐵𝑆 ) → ( ( ( 𝐴𝑅𝐵𝑆 ) ∧ 𝜃 ) ↔ 𝜃 ) )
40 39 3adant3 ( ( 𝐴𝑅𝐵𝑆𝐶𝐷 ) → ( ( ( 𝐴𝑅𝐵𝑆 ) ∧ 𝜃 ) ↔ 𝜃 ) )
41 40 adantl ( ( 𝜏 ∧ ( 𝐴𝑅𝐵𝑆𝐶𝐷 ) ) → ( ( ( 𝐴𝑅𝐵𝑆 ) ∧ 𝜃 ) ↔ 𝜃 ) )
42 37 41 bitrd ( ( 𝜏 ∧ ( 𝐴𝑅𝐵𝑆𝐶𝐷 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶𝜃 ) )