Metamath Proof Explorer

Theorem ovmpodxf

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

Ref Expression
Hypotheses 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 ovmpodxf ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = 𝑆 )

Proof

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