Metamath Proof Explorer


Theorem ovid

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

Ref Expression
Hypotheses ovid.1 ( ( 𝑥𝑅𝑦𝑆 ) → ∃! 𝑧 𝜑 )
ovid.2 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝑅𝑦𝑆 ) ∧ 𝜑 ) }
Assertion ovid ( ( 𝑥𝑅𝑦𝑆 ) → ( ( 𝑥 𝐹 𝑦 ) = 𝑧𝜑 ) )

Proof

Step Hyp Ref Expression
1 ovid.1 ( ( 𝑥𝑅𝑦𝑆 ) → ∃! 𝑧 𝜑 )
2 ovid.2 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝑅𝑦𝑆 ) ∧ 𝜑 ) }
3 df-ov ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4 3 eqeq1i ( ( 𝑥 𝐹 𝑦 ) = 𝑧 ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 )
5 1 fnoprab { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝑅𝑦𝑆 ) ∧ 𝜑 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝑅𝑦𝑆 ) }
6 2 fneq1i ( 𝐹 Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝑅𝑦𝑆 ) } ↔ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝑅𝑦𝑆 ) ∧ 𝜑 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝑅𝑦𝑆 ) } )
7 5 6 mpbir 𝐹 Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝑅𝑦𝑆 ) }
8 opabidw ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝑅𝑦𝑆 ) } ↔ ( 𝑥𝑅𝑦𝑆 ) )
9 8 biimpri ( ( 𝑥𝑅𝑦𝑆 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝑅𝑦𝑆 ) } )
10 fnopfvb ( ( 𝐹 Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝑅𝑦𝑆 ) } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝑅𝑦𝑆 ) } ) → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 ) )
11 7 9 10 sylancr ( ( 𝑥𝑅𝑦𝑆 ) → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 ) )
12 2 eleq2i ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝑅𝑦𝑆 ) ∧ 𝜑 ) } )
13 oprabidw ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝑅𝑦𝑆 ) ∧ 𝜑 ) } ↔ ( ( 𝑥𝑅𝑦𝑆 ) ∧ 𝜑 ) )
14 12 13 bitri ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 ↔ ( ( 𝑥𝑅𝑦𝑆 ) ∧ 𝜑 ) )
15 14 baib ( ( 𝑥𝑅𝑦𝑆 ) → ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹𝜑 ) )
16 11 15 bitrd ( ( 𝑥𝑅𝑦𝑆 ) → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧𝜑 ) )
17 4 16 syl5bb ( ( 𝑥𝑅𝑦𝑆 ) → ( ( 𝑥 𝐹 𝑦 ) = 𝑧𝜑 ) )