fwfffunres

Description: If ps is function-like over A , then F matches its behavior over x . (Contributed by BTernaryTau, 28-Sep-2026)

	Ref	Expression
Hypotheses	fwfffunres.1	$⊢ Ⅎ y ψ$
	fwfffunres.2	$⊢ φ \to \forall w \in A \exists y \forall z \in A (ψ \to z = y)$
	fwfffunres.3	$⊢ F = {\{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} ↾}_{x}$
Assertion	fwfffunres	$⊢ φ \to ((z \in A \land (w \in A \land w \in x \land ψ)) \leftrightarrow (w \in dom F \land F (w) = z))$

Proof

Step	Hyp	Ref	Expression
1		fwfffunres.1	$⊢ Ⅎ y ψ$
2		fwfffunres.2	$⊢ φ \to \forall w \in A \exists y \forall z \in A (ψ \to z = y)$
3		fwfffunres.3	$⊢ F = {\{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} ↾}_{x}$
4		eqid	$⊢ \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} = \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\}$
5	1 2 4	fwfffun	$⊢ φ \to ((w \in A \land z \in A \land ψ) \leftrightarrow (w \in dom \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} \land \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} (w) = z))$
6	5	adantr	$⊢ (φ \land w \in x) \to ((w \in A \land z \in A \land ψ) \leftrightarrow (w \in dom \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} \land \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} (w) = z))$
7	3	dmeqi	$⊢ dom F = dom ({\{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} ↾}_{x})$
8		dmres	$⊢ dom ({\{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} ↾}_{x}) = x \cap dom \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\}$
9	7 8	eqtri	$⊢ dom F = x \cap dom \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\}$
10	9	elin2	$⊢ w \in dom F \leftrightarrow (w \in x \land w \in dom \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\})$
11	10	baib	$⊢ w \in x \to (w \in dom F \leftrightarrow w \in dom \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\})$
12	3	fveq1i	$⊢ F (w) = ({\{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} ↾}_{x}) (w)$
13		fvres	$⊢ w \in x \to ({\{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} ↾}_{x}) (w) = \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} (w)$
14	12 13	eqtrid	$⊢ w \in x \to F (w) = \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} (w)$
15	14	eqeq1d	$⊢ w \in x \to (F (w) = z \leftrightarrow \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} (w) = z)$
16	11 15	anbi12d	$⊢ w \in x \to ((w \in dom F \land F (w) = z) \leftrightarrow (w \in dom \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} \land \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} (w) = z))$
17	16	adantl	$⊢ (φ \land w \in x) \to ((w \in dom F \land F (w) = z) \leftrightarrow (w \in dom \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} \land \{⟨w, z⟩ \| (w \in A \land z \in A \land ψ)\} (w) = z))$
18	6 17	bitr4d	$⊢ (φ \land w \in x) \to ((w \in A \land z \in A \land ψ) \leftrightarrow (w \in dom F \land F (w) = z))$
19	18	pm5.32da	$⊢ φ \to ((w \in x \land (w \in A \land z \in A \land ψ)) \leftrightarrow (w \in x \land (w \in dom F \land F (w) = z)))$
20		an4	$⊢ ((z \in A \land w \in A) \land (w \in x \land ψ)) \leftrightarrow ((z \in A \land w \in x) \land (w \in A \land ψ))$
21		ancom	$⊢ (z \in A \land w \in x) \leftrightarrow (w \in x \land z \in A)$
22	21	anbi1i	$⊢ ((z \in A \land w \in x) \land (w \in A \land ψ)) \leftrightarrow ((w \in x \land z \in A) \land (w \in A \land ψ))$
23		an4	$⊢ ((w \in x \land z \in A) \land (w \in A \land ψ)) \leftrightarrow ((w \in x \land w \in A) \land (z \in A \land ψ))$
24	20 22 23	3bitri	$⊢ ((z \in A \land w \in A) \land (w \in x \land ψ)) \leftrightarrow ((w \in x \land w \in A) \land (z \in A \land ψ))$
25		13an22anass	$⊢ (z \in A \land (w \in A \land w \in x \land ψ)) \leftrightarrow ((z \in A \land w \in A) \land (w \in x \land ψ))$
26		13an22anass	$⊢ (w \in x \land (w \in A \land z \in A \land ψ)) \leftrightarrow ((w \in x \land w \in A) \land (z \in A \land ψ))$
27	24 25 26	3bitr4i	$⊢ (z \in A \land (w \in A \land w \in x \land ψ)) \leftrightarrow (w \in x \land (w \in A \land z \in A \land ψ))$
28	10	simplbi	$⊢ w \in dom F \to w \in x$
29	28	adantr	$⊢ (w \in dom F \land F (w) = z) \to w \in x$
30	29	pm4.71ri	$⊢ (w \in dom F \land F (w) = z) \leftrightarrow (w \in x \land (w \in dom F \land F (w) = z))$
31	19 27 30	3bitr4g	$⊢ φ \to ((z \in A \land (w \in A \land w \in x \land ψ)) \leftrightarrow (w \in dom F \land F (w) = z))$

Metamath Proof Explorer

Theorem fwfffunres

Proof