Metamath Proof Explorer

Theorem ovmpordxf

Description: Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf . (Contributed by AV, 30-Mar-2019)

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

Proof

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