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 x = A φ ψ
ovg.2 y = B ψ χ
ovg.3 z = C χ θ
ovg.4 τ x R y S ∃! z φ
ovg.5 F = x y z | x R y S φ
Assertion ovg τ A R B S C D A F B = C θ

Proof

Step Hyp Ref Expression
1 ovg.1 x = A φ ψ
2 ovg.2 y = B ψ χ
3 ovg.3 z = C χ θ
4 ovg.4 τ x R y S ∃! z φ
5 ovg.5 F = x y z | x R y S φ
6 df-ov A F B = F A B
7 5 fveq1i F A B = x y z | x R y S φ A B
8 6 7 eqtri A F B = x y z | x R y S φ A B
9 8 eqeq1i A F B = C x y z | x R y S φ A B = C
10 eqeq2 c = C x y z | x R y S φ A B = c x y z | x R y S φ A B = C
11 opeq2 c = C A B c = A B C
12 11 eleq1d c = C A B c x y z | x R y S φ A B C x y z | x R y S φ
13 10 12 bibi12d c = C x y z | x R y S φ A B = c A B c x y z | x R y S φ x y z | x R y S φ A B = C A B C x y z | x R y S φ
14 13 imbi2d c = C τ A R B S x y z | x R y S φ A B = c A B c x y z | x R y S φ τ A R B S x y z | x R y S φ A B = C A B C x y z | x R y S φ
15 4 ex τ x R y S ∃! z φ
16 15 alrimivv τ x y x R y S ∃! z φ
17 fnoprabg x y x R y S ∃! z φ x y z | x R y S φ Fn x y | x R y S
18 16 17 syl τ x y z | x R y S φ Fn x y | x R y S
19 eleq1 x = A x R A R
20 19 anbi1d x = A x R y S A R y S
21 eleq1 y = B y S B S
22 21 anbi2d y = B A R y S A R B S
23 20 22 opelopabg A R B S A B x y | x R y S A R B S
24 23 ibir A R B S A B x y | x R y S
25 fnopfvb x y z | x R y S φ Fn x y | x R y S A B x y | x R y S x y z | x R y S φ A B = c A B c x y z | x R y S φ
26 18 24 25 syl2an τ A R B S x y z | x R y S φ A B = c A B c x y z | x R y S φ
27 14 26 vtoclg C D τ A R B S x y z | x R y S φ A B = C A B C x y z | x R y S φ
28 27 com12 τ A R B S C D x y z | x R y S φ A B = C A B C x y z | x R y S φ
29 28 exp32 τ A R B S C D x y z | x R y S φ A B = C A B C x y z | x R y S φ
30 29 3imp2 τ A R B S C D x y z | x R y S φ A B = C A B C x y z | x R y S φ
31 20 1 anbi12d x = A x R y S φ A R y S ψ
32 22 2 anbi12d y = B A R y S ψ A R B S χ
33 3 anbi2d z = C A R B S χ A R B S θ
34 31 32 33 eloprabg A R B S C D A B C x y z | x R y S φ A R B S θ
35 34 adantl τ A R B S C D A B C x y z | x R y S φ A R B S θ
36 30 35 bitrd τ A R B S C D x y z | x R y S φ A B = C A R B S θ
37 9 36 syl5bb τ A R B S C D A F B = C A R B S θ
38 biidd A R B S A R B S θ A R B S θ
39 38 bianabs A R B S A R B S θ θ
40 39 3adant3 A R B S C D A R B S θ θ
41 40 adantl τ A R B S C D A R B S θ θ
42 37 41 bitrd τ A R B S C D A F B = C θ