This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oprabex3

Description: Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004)

		Ref	Expression
	Hypotheses	oprabex3.1	$⊢ H \in V$
		oprabex3.2	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in (H \times H) \land y \in (H \times H)) \land \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R))\}$
	Assertion	oprabex3	$⊢ F \in V$

Proof

Step	Hyp	Ref	Expression
1		oprabex3.1	$⊢ H \in V$
2		oprabex3.2	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in (H \times H) \land y \in (H \times H)) \land \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R))\}$
3	1 1	xpex	$⊢ H \times H \in V$
4		moeq	$⊢ \exists^{*} z z = R$
5	4	mosubop	$⊢ \exists^{*} z \exists u \exists f (y = ⟨u, f⟩ \land z = R)$
6	5	mosubop	$⊢ \exists^{*} z \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = R))$
7		anass	$⊢ ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = R))$
8	7	2exbii	$⊢ \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow \exists u \exists f (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = R))$
9		19.42vv	$⊢ \exists u \exists f (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = R)) \leftrightarrow (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = R))$
10	8 9	bitri	$⊢ \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = R))$
11	10	2exbii	$⊢ \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = R))$
12	11	mobii	$⊢ \exists^{} z \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow \exists^{} z \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = R))$
13	6 12	mpbir	$⊢ \exists^{*} z \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R)$
14	13	a1i	$⊢ (x \in (H \times H) \land y \in (H \times H)) \to \exists^{*} z \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R)$
15	3 3 14 2	oprabex	$⊢ F \in V$