Metamath Proof Explorer

Theorem sprmpod

Description: The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 20-Jun-2019)

Ref Expression
Hypotheses sprmpod.1 ⊢ M = v ∈ V , e ∈ V ⟼ x y | x v R e y ∧ χ
sprmpod.2 ⊢ φ ∧ v = V ∧ e = E → χ ↔ ψ
sprmpod.3 ⊢ φ → V ∈ V ∧ E ∈ V
sprmpod.4 ⊢ φ → ∀ x ∀ y x V R E y → θ
sprmpod.5 ⊢ φ → x y | θ ∈ V
Assertion sprmpod ⊢ φ → V M E = x y | x V R E y ∧ ψ

Proof

Step Hyp Ref Expression
1 sprmpod.1 ⊢ M = v ∈ V , e ∈ V ⟼ x y | x v R e y ∧ χ
2 sprmpod.2 ⊢ φ ∧ v = V ∧ e = E → χ ↔ ψ
3 sprmpod.3 ⊢ φ → V ∈ V ∧ E ∈ V
4 sprmpod.4 ⊢ φ → ∀ x ∀ y x V R E y → θ
5 sprmpod.5 ⊢ φ → x y | θ ∈ V
6 1 a1i ⊢ φ → M = v ∈ V , e ∈ V ⟼ x y | x v R e y ∧ χ
7 oveq12 ⊢ v = V ∧ e = E → v R e = V R E
8 7 breqd ⊢ v = V ∧ e = E → x v R e y ↔ x V R E y
9 8 adantl ⊢ φ ∧ v = V ∧ e = E → x v R e y ↔ x V R E y
10 2 3expb ⊢ φ ∧ v = V ∧ e = E → χ ↔ ψ
11 9 10 anbi12d ⊢ φ ∧ v = V ∧ e = E → x v R e y ∧ χ ↔ x V R E y ∧ ψ
12 11 opabbidv ⊢ φ ∧ v = V ∧ e = E → x y | x v R e y ∧ χ = x y | x V R E y ∧ ψ
13 3 simpld ⊢ φ → V ∈ V
14 3 simprd ⊢ φ → E ∈ V
15 opabbrex ⊢ ∀ x ∀ y x V R E y → θ ∧ x y | θ ∈ V → x y | x V R E y ∧ ψ ∈ V
16 4 5 15 syl2anc ⊢ φ → x y | x V R E y ∧ ψ ∈ V
17 6 12 13 14 16 ovmpod ⊢ φ → V M E = x y | x V R E y ∧ ψ