fvmptopab

Description: The function value of a mapping M to a restricted binary relation expressed as an ordered-pair class abstraction: The restricted binary relation is a binary relation given as value of a function F restricted by the condition ps . (Contributed by AV, 31-Jan-2021) (Revised by AV, 29-Oct-2021)

	Ref	Expression
Hypotheses	fvmptopab.1	$⊢ (φ \land z = Z) \to (χ \leftrightarrow ψ)$
	fvmptopab.2	$⊢ φ \to \{⟨x, y⟩ \| x F (Z) y\} \in V$
	fvmptopab.3	$⊢ M = (z \in V ⟼ \{⟨x, y⟩ \| (x F (z) y \land χ)\})$
Assertion	fvmptopab	$⊢ φ \to M (Z) = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		fvmptopab.1	$⊢ (φ \land z = Z) \to (χ \leftrightarrow ψ)$
2		fvmptopab.2	$⊢ φ \to \{⟨x, y⟩ \| x F (Z) y\} \in V$
3		fvmptopab.3	$⊢ M = (z \in V ⟼ \{⟨x, y⟩ \| (x F (z) y \land χ)\})$
4		fveq2	$⊢ z = Z \to F (z) = F (Z)$
5	4	breqd	$⊢ z = Z \to (x F (z) y \leftrightarrow x F (Z) y)$
6	5	adantl	$⊢ ((Z \in V \land φ) \land z = Z) \to (x F (z) y \leftrightarrow x F (Z) y)$
7	1	adantll	$⊢ ((Z \in V \land φ) \land z = Z) \to (χ \leftrightarrow ψ)$
8	6 7	anbi12d	$⊢ ((Z \in V \land φ) \land z = Z) \to ((x F (z) y \land χ) \leftrightarrow (x F (Z) y \land ψ))$
9	8	opabbidv	$⊢ ((Z \in V \land φ) \land z = Z) \to \{⟨x, y⟩ \| (x F (z) y \land χ)\} = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\}$
10		simpl	$⊢ (Z \in V \land φ) \to Z \in V$
11		id	$⊢ x F (Z) y \to x F (Z) y$
12	11	gen2	$⊢ \forall x \forall y (x F (Z) y \to x F (Z) y)$
13	2	adantl	$⊢ (Z \in V \land φ) \to \{⟨x, y⟩ \| x F (Z) y\} \in V$
14		opabbrex	$⊢ (\forall x \forall y (x F (Z) y \to x F (Z) y) \land \{⟨x, y⟩ \| x F (Z) y\} \in V) \to \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} \in V$
15	12 13 14	sylancr	$⊢ (Z \in V \land φ) \to \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} \in V$
16	3 9 10 15	fvmptd2	$⊢ (Z \in V \land φ) \to M (Z) = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\}$
17	16	ex	$⊢ Z \in V \to (φ \to M (Z) = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\})$
18		fvprc	$⊢ \neg Z \in V \to M (Z) = \emptyset$
19		br0	$⊢ \neg x \emptyset y$
20		fvprc	$⊢ \neg Z \in V \to F (Z) = \emptyset$
21	20	breqd	$⊢ \neg Z \in V \to (x F (Z) y \leftrightarrow x \emptyset y)$
22	19 21	mtbiri	$⊢ \neg Z \in V \to \neg x F (Z) y$
23	22	intnanrd	$⊢ \neg Z \in V \to \neg (x F (Z) y \land ψ)$
24	23	alrimivv	$⊢ \neg Z \in V \to \forall x \forall y \neg (x F (Z) y \land ψ)$
25		opab0	$⊢ \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} = \emptyset \leftrightarrow \forall x \forall y \neg (x F (Z) y \land ψ)$
26	24 25	sylibr	$⊢ \neg Z \in V \to \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} = \emptyset$
27	18 26	eqtr4d	$⊢ \neg Z \in V \to M (Z) = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\}$
28	27	a1d	$⊢ \neg Z \in V \to (φ \to M (Z) = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\})$
29	17 28	pm2.61i	$⊢ φ \to M (Z) = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\}$

Metamath Proof Explorer

Theorem fvmptopab

Proof