Description: Value of an operation given by a maps-to rule. Deduction form of ovmpoga . (Contributed by SN, 14-Mar-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ovmpogad.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) | |
ovmpogad.s | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑅 = 𝑆 ) | ||
ovmpogad.1 | ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 ) | ||
ovmpogad.2 | ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 ) | ||
ovmpogad.v | ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 ) | ||
Assertion | ovmpogad | ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = 𝑆 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovmpogad.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) | |
2 | ovmpogad.s | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑅 = 𝑆 ) | |
3 | ovmpogad.1 | ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 ) | |
4 | ovmpogad.2 | ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 ) | |
5 | ovmpogad.v | ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 ) | |
6 | 1 | a1i | ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) ) |
7 | 2 | adantl | ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 ) |
8 | 6 7 3 4 5 | ovmpod | ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = 𝑆 ) |