Metamath Proof Explorer

Theorem fvmpopr2d

Description: Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024)

Ref Expression
Hypotheses fvmpopr2d.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) )
fvmpopr2d.2 ⊢ ( 𝜑 → 𝑃 = ⟨ 𝑎 , 𝑏 ⟩ )
fvmpopr2d.3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
Assertion fvmpopr2d ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑃 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 fvmpopr2d.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) )
2 fvmpopr2d.2 ⊢ ( 𝜑 → 𝑃 = ⟨ 𝑎 , 𝑏 ⟩ )
3 fvmpopr2d.3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
4 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝐹 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) )
5 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝑃 = ⟨ 𝑎 , 𝑏 ⟩ )
6 4 5 fveq12d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑃 ) = ( ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
7 df-ov ⊢ ( 𝑎 ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) = ( ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) ‘ ⟨ 𝑎 , 𝑏 ⟩ )
8 6 7 syl6reqr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) = ( 𝐹 ‘ 𝑃 ) )
9 nfcv ⊢ Ⅎ 𝑐 𝐶
10 nfcv ⊢ Ⅎ 𝑑 𝐶
11 nfcv ⊢ Ⅎ 𝑎 𝑑
12 nfcsb1v ⊢ Ⅎ 𝑎 ⦋ 𝑐 / 𝑎 ⦌ 𝐶
13 11 12 nfcsbw ⊢ Ⅎ 𝑎 ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶
14 nfcsb1v ⊢ Ⅎ 𝑏 ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶
15 csbeq1a ⊢ ( 𝑎 = 𝑐 → 𝐶 = ⦋ 𝑐 / 𝑎 ⦌ 𝐶 )
16 csbeq1a ⊢ ( 𝑏 = 𝑑 → ⦋ 𝑐 / 𝑎 ⦌ 𝐶 = ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶 )
17 15 16 sylan9eq ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → 𝐶 = ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶 )
18 9 10 13 14 17 cbvmpo ⊢ ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑐 ∈ 𝐴 , 𝑑 ∈ 𝐵 ↦ ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶 )
19 18 oveqi ⊢ ( 𝑎 ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) = ( 𝑎 ( 𝑐 ∈ 𝐴 , 𝑑 ∈ 𝐵 ↦ ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶 ) 𝑏 )
20 eqidd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑐 ∈ 𝐴 , 𝑑 ∈ 𝐵 ↦ ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶 ) = ( 𝑐 ∈ 𝐴 , 𝑑 ∈ 𝐵 ↦ ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶 ) )
21 equcom ⊢ ( 𝑎 = 𝑐 ↔ 𝑐 = 𝑎 )
22 equcom ⊢ ( 𝑏 = 𝑑 ↔ 𝑑 = 𝑏 )
23 21 22 anbi12i ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ↔ ( 𝑐 = 𝑎 ∧ 𝑑 = 𝑏 ) )
24 23 17 sylbir ⊢ ( ( 𝑐 = 𝑎 ∧ 𝑑 = 𝑏 ) → 𝐶 = ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶 )
25 24 eqcomd ⊢ ( ( 𝑐 = 𝑎 ∧ 𝑑 = 𝑏 ) → ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶 = 𝐶 )
26 25 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 = 𝑎 ∧ 𝑑 = 𝑏 ) ) → ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶 = 𝐶 )
27 simp2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ 𝐴 )
28 simp3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
29 20 26 27 28 3 ovmpod ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( 𝑐 ∈ 𝐴 , 𝑑 ∈ 𝐵 ↦ ⦋ 𝑑 / 𝑏 ⦌ ⦋ 𝑐 / 𝑎 ⦌ 𝐶 ) 𝑏 ) = 𝐶 )
30 19 29 syl5eq ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) = 𝐶 )
31 8 30 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑃 ) = 𝐶 )