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	⊢ Ⅎ 𝑥 𝐴
	ov2gf.c	⊢ Ⅎ 𝑦 𝐴
	ov2gf.d	⊢ Ⅎ 𝑦 𝐵
	ov2gf.1	⊢ Ⅎ 𝑥 𝐺
	ov2gf.2	⊢ Ⅎ 𝑦 𝑆
	ov2gf.3	⊢ ( 𝑥 = 𝐴 → 𝑅 = 𝐺 )
	ov2gf.4	⊢ ( 𝑦 = 𝐵 → 𝐺 = 𝑆 )
	ov2gf.5	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
Assertion	ov2gf	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ov2gf.a	⊢ Ⅎ 𝑥 𝐴
2		ov2gf.c	⊢ Ⅎ 𝑦 𝐴
3		ov2gf.d	⊢ Ⅎ 𝑦 𝐵
4		ov2gf.1	⊢ Ⅎ 𝑥 𝐺
5		ov2gf.2	⊢ Ⅎ 𝑦 𝑆
6		ov2gf.3	⊢ ( 𝑥 = 𝐴 → 𝑅 = 𝐺 )
7		ov2gf.4	⊢ ( 𝑦 = 𝐵 → 𝐺 = 𝑆 )
8		ov2gf.5	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
9		elex	⊢ ( 𝑆 ∈ 𝐻 → 𝑆 ∈ V )
10	4	nfel1	⊢ Ⅎ 𝑥 𝐺 ∈ V
11		nfmpo1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
12	8 11	nfcxfr	⊢ Ⅎ 𝑥 𝐹
13		nfcv	⊢ Ⅎ 𝑥 𝑦
14	1 12 13	nfov	⊢ Ⅎ 𝑥 ( 𝐴 𝐹 𝑦 )
15	14 4	nfeq	⊢ Ⅎ 𝑥 ( 𝐴 𝐹 𝑦 ) = 𝐺
16	10 15	nfim	⊢ Ⅎ 𝑥 ( 𝐺 ∈ V → ( 𝐴 𝐹 𝑦 ) = 𝐺 )
17	5	nfel1	⊢ Ⅎ 𝑦 𝑆 ∈ V
18		nfmpo2	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
19	8 18	nfcxfr	⊢ Ⅎ 𝑦 𝐹
20	2 19 3	nfov	⊢ Ⅎ 𝑦 ( 𝐴 𝐹 𝐵 )
21	20 5	nfeq	⊢ Ⅎ 𝑦 ( 𝐴 𝐹 𝐵 ) = 𝑆
22	17 21	nfim	⊢ Ⅎ 𝑦 ( 𝑆 ∈ V → ( 𝐴 𝐹 𝐵 ) = 𝑆 )
23	6	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝑅 ∈ V ↔ 𝐺 ∈ V ) )
24		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ) = ( 𝐴 𝐹 𝑦 ) )
25	24 6	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐹 𝑦 ) = 𝑅 ↔ ( 𝐴 𝐹 𝑦 ) = 𝐺 ) )
26	23 25	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑅 ∈ V → ( 𝑥 𝐹 𝑦 ) = 𝑅 ) ↔ ( 𝐺 ∈ V → ( 𝐴 𝐹 𝑦 ) = 𝐺 ) ) )
27	7	eleq1d	⊢ ( 𝑦 = 𝐵 → ( 𝐺 ∈ V ↔ 𝑆 ∈ V ) )
28		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐹 𝑦 ) = ( 𝐴 𝐹 𝐵 ) )
29	28 7	eqeq12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐹 𝑦 ) = 𝐺 ↔ ( 𝐴 𝐹 𝐵 ) = 𝑆 ) )
30	27 29	imbi12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐺 ∈ V → ( 𝐴 𝐹 𝑦 ) = 𝐺 ) ↔ ( 𝑆 ∈ V → ( 𝐴 𝐹 𝐵 ) = 𝑆 ) ) )
31	8	ovmpt4g	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V ) → ( 𝑥 𝐹 𝑦 ) = 𝑅 )
32	31	3expia	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 ∈ V → ( 𝑥 𝐹 𝑦 ) = 𝑅 ) )
33	1 2 3 16 22 26 30 32	vtocl2gaf	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝑆 ∈ V → ( 𝐴 𝐹 𝐵 ) = 𝑆 ) )
34	9 33	syl5	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝑆 ∈ 𝐻 → ( 𝐴 𝐹 𝐵 ) = 𝑆 ) )
35	34	3impia	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )