Theorem ovmpodxf 7505

Description: Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)

Hypotheses

Ref	Expression
ovmpodx.1	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))
ovmpodx.2	⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)
ovmpodx.3	⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿)
ovmpodx.4	⊢ (𝜑 → 𝐴 ∈ 𝐶)
ovmpodx.5	⊢ (𝜑 → 𝐵 ∈ 𝐿)
ovmpodx.6	⊢ (𝜑 → 𝑆 ∈ 𝑋)
ovmpodxf.px	⊢ Ⅎ𝑥𝜑
ovmpodxf.py	⊢ Ⅎ𝑦𝜑
ovmpodxf.ay	⊢ Ⅎ𝑦𝐴
ovmpodxf.bx	⊢ Ⅎ𝑥𝐵
ovmpodxf.sx	⊢ Ⅎ𝑥𝑆
ovmpodxf.sy	⊢ Ⅎ𝑦𝑆

Assertion

Ref	Expression
ovmpodxf	⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)

Distinct variable groups:   𝑥,𝑦   𝑥,𝐴   𝑦,𝐵

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑦)   𝐵(𝑥)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝑆(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐿(𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem ovmpodxf

Step	Hyp	Ref	Expression
1		ovmpodx.1	. . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))
2	1	oveqd 7374	. 2 ⊢ (𝜑 → (𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵))
3		ovmpodx.4	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4		ovmpodxf.px	. . . . 5 ⊢ Ⅎ𝑥𝜑
5		ovmpodx.5	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝐿)
6		ovmpodxf.py	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
7		eqid 2736	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
8	7	ovmpt4g 7502	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅)
9	8	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅))
10	6, 9	alrimi 2206	. . . . . 6 ⊢ (𝜑 → ∀𝑦((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅))
11	5, 10	spsbcd 3753	. . . . 5 ⊢ (𝜑 → [𝐵 / 𝑦]((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅))
12	4, 11	alrimi 2206	. . . 4 ⊢ (𝜑 → ∀𝑥[𝐵 / 𝑦]((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅))
13	3, 12	spsbcd 3753	. . 3 ⊢ (𝜑 → [𝐴 / 𝑥][𝐵 / 𝑦]((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅))
14	5	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐿)
15		simplr 767	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑥 = 𝐴)
16	3	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝐴 ∈ 𝐶)
17	15, 16	eqeltrd 2838	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑥 ∈ 𝐶)
18	5	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝐵 ∈ 𝐿)
19		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵)
20		ovmpodx.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿)
21	20	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝐷 = 𝐿)
22	18, 19, 21	3eltr4d 2853	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑦 ∈ 𝐷)
23		ovmpodx.2	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)
24	23	anassrs 468	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
25		ovmpodx.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ 𝑋)
26	25	elexd 3465	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ V)
27	26	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑆 ∈ V)
28	24, 27	eqeltrd 2838	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑅 ∈ V)
29		biimt 360	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → ((𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅 ↔ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅)))
30	17, 22, 28, 29	syl3anc 1371	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → ((𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅 ↔ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅)))
31	15, 19	oveq12d 7375	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵))
32	31, 24	eqeq12d 2752	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → ((𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅 ↔ (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆))
33	30, 32	bitr3d 280	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) ↔ (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆))
34		ovmpodxf.ay	. . . . . . 7 ⊢ Ⅎ𝑦𝐴
35	34	nfeq2 2924	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 = 𝐴
36	6, 35	nfan 1902	. . . . 5 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 = 𝐴)
37		nfmpo2 7438	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
38		nfcv 2907	. . . . . . . 8 ⊢ Ⅎ𝑦𝐵
39	34, 37, 38	nfov 7387	. . . . . . 7 ⊢ Ⅎ𝑦(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵)
40		ovmpodxf.sy	. . . . . . 7 ⊢ Ⅎ𝑦𝑆
41	39, 40	nfeq 2920	. . . . . 6 ⊢ Ⅎ𝑦(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆
42	41	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → Ⅎ𝑦(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆)
43	14, 33, 36, 42	sbciedf 3783	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ([𝐵 / 𝑦]((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) ↔ (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆))
44		nfcv 2907	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
45		nfmpo1 7437	. . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
46		ovmpodxf.bx	. . . . . . 7 ⊢ Ⅎ𝑥𝐵
47	44, 45, 46	nfov 7387	. . . . . 6 ⊢ Ⅎ𝑥(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵)
48		ovmpodxf.sx	. . . . . 6 ⊢ Ⅎ𝑥𝑆
49	47, 48	nfeq 2920	. . . . 5 ⊢ Ⅎ𝑥(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆
50	49	a1i 11	. . . 4 ⊢ (𝜑 → Ⅎ𝑥(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆)
51	3, 43, 4, 50	sbciedf 3783	. . 3 ⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) ↔ (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆))
52	13, 51	mpbid 231	. 2 ⊢ (𝜑 → (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆)
53	2, 52	eqtrd 2776	1 ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  Ⅎwnf 1785   ∈ wcel 2106  Ⅎwnfc 2887  Vcvv 3445  [wsbc 3739  (class class class)co 7357   ∈ cmpo 7359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-iota 6448  df-fun 6498  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362

This theorem is referenced by:  ovmpodx  7506  elovmporab  7599  elovmporab1w  7600  elovmporab1  7601  ovmpt3rab1  7611  mpoxopoveq  8150  fvmpocurryd  8202  mdetralt2  21958  mdetunilem2  21962  gsummatr01lem4  22007