Metamath Proof Explorer


Theorem ov2gf

Description: The value of an operation class abstraction. A version of ovmpog using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006) (Revised by Mario Carneiro, 19-Dec-2013)

Ref Expression
Hypotheses ov2gf.a
|- F/_ x A
ov2gf.c
|- F/_ y A
ov2gf.d
|- F/_ y B
ov2gf.1
|- F/_ x G
ov2gf.2
|- F/_ y S
ov2gf.3
|- ( x = A -> R = G )
ov2gf.4
|- ( y = B -> G = S )
ov2gf.5
|- F = ( x e. C , y e. D |-> R )
Assertion ov2gf
|- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )

Proof

Step Hyp Ref Expression
1 ov2gf.a
 |-  F/_ x A
2 ov2gf.c
 |-  F/_ y A
3 ov2gf.d
 |-  F/_ y B
4 ov2gf.1
 |-  F/_ x G
5 ov2gf.2
 |-  F/_ y S
6 ov2gf.3
 |-  ( x = A -> R = G )
7 ov2gf.4
 |-  ( y = B -> G = S )
8 ov2gf.5
 |-  F = ( x e. C , y e. D |-> R )
9 elex
 |-  ( S e. H -> S e. _V )
10 4 nfel1
 |-  F/ x G e. _V
11 nfmpo1
 |-  F/_ x ( x e. C , y e. D |-> R )
12 8 11 nfcxfr
 |-  F/_ x F
13 nfcv
 |-  F/_ x y
14 1 12 13 nfov
 |-  F/_ x ( A F y )
15 14 4 nfeq
 |-  F/ x ( A F y ) = G
16 10 15 nfim
 |-  F/ x ( G e. _V -> ( A F y ) = G )
17 5 nfel1
 |-  F/ y S e. _V
18 nfmpo2
 |-  F/_ y ( x e. C , y e. D |-> R )
19 8 18 nfcxfr
 |-  F/_ y F
20 2 19 3 nfov
 |-  F/_ y ( A F B )
21 20 5 nfeq
 |-  F/ y ( A F B ) = S
22 17 21 nfim
 |-  F/ y ( S e. _V -> ( A F B ) = S )
23 6 eleq1d
 |-  ( x = A -> ( R e. _V <-> G e. _V ) )
24 oveq1
 |-  ( x = A -> ( x F y ) = ( A F y ) )
25 24 6 eqeq12d
 |-  ( x = A -> ( ( x F y ) = R <-> ( A F y ) = G ) )
26 23 25 imbi12d
 |-  ( x = A -> ( ( R e. _V -> ( x F y ) = R ) <-> ( G e. _V -> ( A F y ) = G ) ) )
27 7 eleq1d
 |-  ( y = B -> ( G e. _V <-> S e. _V ) )
28 oveq2
 |-  ( y = B -> ( A F y ) = ( A F B ) )
29 28 7 eqeq12d
 |-  ( y = B -> ( ( A F y ) = G <-> ( A F B ) = S ) )
30 27 29 imbi12d
 |-  ( y = B -> ( ( G e. _V -> ( A F y ) = G ) <-> ( S e. _V -> ( A F B ) = S ) ) )
31 8 ovmpt4g
 |-  ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x F y ) = R )
32 31 3expia
 |-  ( ( x e. C /\ y e. D ) -> ( R e. _V -> ( x F y ) = R ) )
33 1 2 3 16 22 26 30 32 vtocl2gaf
 |-  ( ( A e. C /\ B e. D ) -> ( S e. _V -> ( A F B ) = S ) )
34 9 33 syl5
 |-  ( ( A e. C /\ B e. D ) -> ( S e. H -> ( A F B ) = S ) )
35 34 3impia
 |-  ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )