Metamath Proof Explorer

Theorem fwfffun

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

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

Proof

Step	Hyp	Ref	Expression
1		fwfffun.1	$⊢ Ⅎ y ψ$
2		fwfffun.2	$⊢ φ \to \forall x \in A \exists y \forall z \in A (ψ \to z = y)$
3		fwfffun.3	$⊢ F = \{⟨x, z⟩ \| (x \in A \land z \in A \land ψ)\}$
4	3	eleq2i	$⊢ ⟨x, z⟩ \in F \leftrightarrow ⟨x, z⟩ \in \{⟨x, z⟩ \| (x \in A \land z \in A \land ψ)\}$
5		opabidw	$⊢ ⟨x, z⟩ \in \{⟨x, z⟩ \| (x \in A \land z \in A \land ψ)\} \leftrightarrow (x \in A \land z \in A \land ψ)$
6	4 5	bitri	$⊢ ⟨x, z⟩ \in F \leftrightarrow (x \in A \land z \in A \land ψ)$
7	1	rmo2	$⊢ \exists^{*} z \in A ψ \leftrightarrow \exists y \forall z \in A (ψ \to z = y)$
8	7	ralbii	$⊢ \forall x \in A \exists^{*} z \in A ψ \leftrightarrow \forall x \in A \exists y \forall z \in A (ψ \to z = y)$
9	2 8	sylibr	$⊢ φ \to \forall x \in A \exists^{*} z \in A ψ$
10		funopab	$⊢ Fun \{⟨x, z⟩ \| (x \in A \land z \in A \land ψ)\} \leftrightarrow \forall x \exists^{*} z (x \in A \land z \in A \land ψ)$
11	3	funeqi	$⊢ Fun F \leftrightarrow Fun \{⟨x, z⟩ \| (x \in A \land z \in A \land ψ)\}$
12		2reu5lem2	$⊢ \forall x \in A \exists^{} z \in A ψ \leftrightarrow \forall x \exists^{} z (x \in A \land z \in A \land ψ)$
13	10 11 12	3bitr4i	$⊢ Fun F \leftrightarrow \forall x \in A \exists^{*} z \in A ψ$
14	9 13	sylibr	$⊢ φ \to Fun F$
15		df-br	$⊢ x F z \leftrightarrow ⟨x, z⟩ \in F$
16		funbrfv2b	$⊢ Fun F \to (x F z \leftrightarrow (x \in dom F \land F (x) = z))$
17	15 16	bitr3id	$⊢ Fun F \to (⟨x, z⟩ \in F \leftrightarrow (x \in dom F \land F (x) = z))$
18	14 17	syl	$⊢ φ \to (⟨x, z⟩ \in F \leftrightarrow (x \in dom F \land F (x) = z))$
19	6 18	bitr3id	$⊢ φ \to ((x \in A \land z \in A \land ψ) \leftrightarrow (x \in dom F \land F (x) = z))$