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) Add disjoint variable condition on F , x , y to remove a sethood hypothesis. (Revised by SN, 13-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		fvmptopab.1	$⊢ z = Z \to (φ \leftrightarrow ψ)$
2		fvmptopab.m	$⊢ M = (z \in V ⟼ \{⟨x, y⟩ \| (x F (z) y \land φ)\})$
3		fveq2	$⊢ z = Z \to F (z) = F (Z)$
4	3	breqd	$⊢ z = Z \to (x F (z) y \leftrightarrow x F (Z) y)$
5	4 1	anbi12d	$⊢ z = Z \to ((x F (z) y \land φ) \leftrightarrow (x F (Z) y \land ψ))$
6	5	opabbidv	$⊢ z = Z \to \{⟨x, y⟩ \| (x F (z) y \land φ)\} = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\}$
7		opabresex2	$⊢ \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} \in V$
8	6 2 7	fvmpt	$⊢ Z \in V \to M (Z) = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\}$
9		fvprc	$⊢ \neg Z \in V \to M (Z) = \emptyset$
10		elopabran	$⊢ z \in \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} \to z \in F (Z)$
11	10	ssriv	$⊢ \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} \subseteq F (Z)$
12		fvprc	$⊢ \neg Z \in V \to F (Z) = \emptyset$
13	11 12	sseqtrid	$⊢ \neg Z \in V \to \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} \subseteq \emptyset$
14		ss0	$⊢ \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} \subseteq \emptyset \to \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} = \emptyset$
15	13 14	syl	$⊢ \neg Z \in V \to \{⟨x, y⟩ \| (x F (Z) y \land ψ)\} = \emptyset$
16	9 15	eqtr4d	$⊢ \neg Z \in V \to M (Z) = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\}$
17	8 16	pm2.61i	$⊢ M (Z) = \{⟨x, y⟩ \| (x F (Z) y \land ψ)\}$

Metamath Proof Explorer

Theorem fvmptopab

Proof