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 \in V, e \in V ⟼ \{⟨x, y⟩ \| (x (v R e) y \land χ)\})$
		sprmpod.2	$⊢ (φ \land v = V \land e = E) \to (χ \leftrightarrow ψ)$
		sprmpod.3	$⊢ φ \to (V \in V \land E \in V)$
		sprmpod.4	$⊢ φ \to \forall x \forall y (x (V R E) y \to θ)$
		sprmpod.5	$⊢ φ \to \{⟨x, y⟩ \| θ\} \in V$
	Assertion	sprmpod	$⊢ φ \to V M E = \{⟨x, y⟩ \| (x (V R E) y \land ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		sprmpod.1	$⊢ M = (v \in V, e \in V ⟼ \{⟨x, y⟩ \| (x (v R e) y \land χ)\})$
2		sprmpod.2	$⊢ (φ \land v = V \land e = E) \to (χ \leftrightarrow ψ)$
3		sprmpod.3	$⊢ φ \to (V \in V \land E \in V)$
4		sprmpod.4	$⊢ φ \to \forall x \forall y (x (V R E) y \to θ)$
5		sprmpod.5	$⊢ φ \to \{⟨x, y⟩ \| θ\} \in V$
6	1	a1i	$⊢ φ \to M = (v \in V, e \in V ⟼ \{⟨x, y⟩ \| (x (v R e) y \land χ)\})$
7		oveq12	$⊢ (v = V \land e = E) \to v R e = V R E$
8	7	breqd	$⊢ (v = V \land e = E) \to (x (v R e) y \leftrightarrow x (V R E) y)$
9	8	adantl	$⊢ (φ \land (v = V \land e = E)) \to (x (v R e) y \leftrightarrow x (V R E) y)$
10	2	3expb	$⊢ (φ \land (v = V \land e = E)) \to (χ \leftrightarrow ψ)$
11	9 10	anbi12d	$⊢ (φ \land (v = V \land e = E)) \to ((x (v R e) y \land χ) \leftrightarrow (x (V R E) y \land ψ))$
12	11	opabbidv	$⊢ (φ \land (v = V \land e = E)) \to \{⟨x, y⟩ \| (x (v R e) y \land χ)\} = \{⟨x, y⟩ \| (x (V R E) y \land ψ)\}$
13	3	simpld	$⊢ φ \to V \in V$
14	3	simprd	$⊢ φ \to E \in V$
15		opabbrex	$⊢ (\forall x \forall y (x (V R E) y \to θ) \land \{⟨x, y⟩ \| θ\} \in V) \to \{⟨x, y⟩ \| (x (V R E) y \land ψ)\} \in V$
16	4 5 15	syl2anc	$⊢ φ \to \{⟨x, y⟩ \| (x (V R E) y \land ψ)\} \in V$
17	6 12 13 14 16	ovmpod	$⊢ φ \to V M E = \{⟨x, y⟩ \| (x (V R E) y \land ψ)\}$