Metamath Proof Explorer

Theorem oprabexd

Description: Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by AV, 9-Aug-2024)

		Ref	Expression
	Hypotheses	oprabexd.1	$⊢ φ \to A \in V$
		oprabexd.2	$⊢ φ \to B \in W$
		oprabexd.3	$⊢ (φ \land (x \in A \land y \in B)) \to \exists^{*} z ψ$
		oprabexd.4	$⊢ φ \to F = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\}$
	Assertion	oprabexd	$⊢ φ \to F \in V$

Proof

Step	Hyp	Ref	Expression
1		oprabexd.1	$⊢ φ \to A \in V$
2		oprabexd.2	$⊢ φ \to B \in W$
3		oprabexd.3	$⊢ (φ \land (x \in A \land y \in B)) \to \exists^{*} z ψ$
4		oprabexd.4	$⊢ φ \to F = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\}$
5	3	ex	$⊢ φ \to ((x \in A \land y \in B) \to \exists^{*} z ψ)$
6		moanimv	$⊢ \exists^{} z ((x \in A \land y \in B) \land ψ) \leftrightarrow ((x \in A \land y \in B) \to \exists^{} z ψ)$
7	5 6	sylibr	$⊢ φ \to \exists^{*} z ((x \in A \land y \in B) \land ψ)$
8	7	alrimivv	$⊢ φ \to \forall x \forall y \exists^{*} z ((x \in A \land y \in B) \land ψ)$
9		funoprabg	$⊢ \forall x \forall y \exists^{*} z ((x \in A \land y \in B) \land ψ) \to Fun \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\}$
10	8 9	syl	$⊢ φ \to Fun \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\}$
11		dmoprabss	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\} \subseteq A \times B$
12	1 2	xpexd	$⊢ φ \to A \times B \in V$
13		ssexg	$⊢ (dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\} \subseteq A \times B \land A \times B \in V) \to dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\} \in V$
14	11 12 13	sylancr	$⊢ φ \to dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\} \in V$
15		funex	$⊢ (Fun \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\} \land dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\} \in V) \to \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\} \in V$
16	10 14 15	syl2anc	$⊢ φ \to \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\} \in V$
17	4 16	eqeltrd	$⊢ φ \to F \in V$