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 ⊢ Ⅎ _ x A
ov2gf.c ⊢ Ⅎ _ y A
ov2gf.d ⊢ Ⅎ _ y B
ov2gf.1 ⊢ Ⅎ _ x G
ov2gf.2 ⊢ Ⅎ _ y S
ov2gf.3 ⊢ x = A → R = G
ov2gf.4 ⊢ y = B → G = S
ov2gf.5 ⊢ F = x ∈ C , y ∈ D ⟼ R
Assertion ov2gf ⊢ A ∈ C ∧ B ∈ D ∧ S ∈ H → A F B = S

Proof

Step Hyp Ref Expression
1 ov2gf.a ⊢ Ⅎ _ x A
2 ov2gf.c ⊢ Ⅎ _ y A
3 ov2gf.d ⊢ Ⅎ _ y B
4 ov2gf.1 ⊢ Ⅎ _ x G
5 ov2gf.2 ⊢ Ⅎ _ y S
6 ov2gf.3 ⊢ x = A → R = G
7 ov2gf.4 ⊢ y = B → G = S
8 ov2gf.5 ⊢ F = x ∈ C , y ∈ D ⟼ R
9 elex ⊢ S ∈ H → S ∈ V
10 4 nfel1 ⊢ Ⅎ x G ∈ V
11 nfmpo1 ⊢ Ⅎ _ x x ∈ C , y ∈ D ⟼ R
12 8 11 nfcxfr ⊢ Ⅎ _ x F
13 nfcv ⊢ Ⅎ _ x y
14 1 12 13 nfov ⊢ Ⅎ _ x A F y
15 14 4 nfeq ⊢ Ⅎ x A F y = G
16 10 15 nfim ⊢ Ⅎ x G ∈ V → A F y = G
17 5 nfel1 ⊢ Ⅎ y S ∈ V
18 nfmpo2 ⊢ Ⅎ _ y x ∈ C , y ∈ D ⟼ R
19 8 18 nfcxfr ⊢ Ⅎ _ y F
20 2 19 3 nfov ⊢ Ⅎ _ y A F B
21 20 5 nfeq ⊢ Ⅎ y A F B = S
22 17 21 nfim ⊢ Ⅎ y S ∈ V → A F B = S
23 6 eleq1d ⊢ x = A → R ∈ V ↔ G ∈ 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 ∈ V → x F y = R ↔ G ∈ V → A F y = G
27 7 eleq1d ⊢ y = B → G ∈ V ↔ S ∈ 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 ∈ V → A F y = G ↔ S ∈ V → A F B = S
31 8 ovmpt4g ⊢ x ∈ C ∧ y ∈ D ∧ R ∈ V → x F y = R
32 31 3expia ⊢ x ∈ C ∧ y ∈ D → R ∈ V → x F y = R
33 1 2 3 16 22 26 30 32 vtocl2gaf ⊢ A ∈ C ∧ B ∈ D → S ∈ V → A F B = S
34 9 33 syl5 ⊢ A ∈ C ∧ B ∈ D → S ∈ H → A F B = S
35 34 3impia ⊢ A ∈ C ∧ B ∈ D ∧ S ∈ H → A F B = S