Theorem fnoprabg

Description: Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007)

	Ref	Expression
Assertion	fnoprabg	$$⊢\forall x\forall y\left(\phi \to \exists !z\psi \right)\to \left\{⟨⟨x,y⟩,z⟩|\left(\phi \wedge \psi \right)\right\}Fn\left\{⟨x,y⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		eumo	$$⊢\exists !z\psi \to {\exists }^{*}z\psi$$
2	1	imim2i	$$⊢\left(\phi \to \exists !z\psi \right)\to \left(\phi \to {\exists }^{*}z\psi \right)$$
3		moanimv	$$⊢{\exists }^{*}z\left(\phi \wedge \psi \right)\leftrightarrow \left(\phi \to {\exists }^{*}z\psi \right)$$
4	2 3	sylibr	$$⊢\left(\phi \to \exists !z\psi \right)\to {\exists }^{*}z\left(\phi \wedge \psi \right)$$
5	4	2alimi	$$⊢\forall x\forall y\left(\phi \to \exists !z\psi \right)\to \forall x\forall y{\exists }^{*}z\left(\phi \wedge \psi \right)$$
6		funoprabg	$$⊢\forall x\forall y{\exists }^{*}z\left(\phi \wedge \psi \right)\to \mathrm{Fun}\left\{⟨⟨x,y⟩,z⟩|\left(\phi \wedge \psi \right)\right\}$$
7	5 6	syl	$$⊢\forall x\forall y\left(\phi \to \exists !z\psi \right)\to \mathrm{Fun}\left\{⟨⟨x,y⟩,z⟩|\left(\phi \wedge \psi \right)\right\}$$
8		dmoprab	$$⊢\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\left(\phi \wedge \psi \right)\right\}=\left\{⟨x,y⟩|\exists z\left(\phi \wedge \psi \right)\right\}$$
9		nfa1	$$⊢Ⅎx\forall x\forall y\left(\phi \to \exists !z\psi \right)$$
10		nfa2	$$⊢Ⅎy\forall x\forall y\left(\phi \to \exists !z\psi \right)$$
11		simpl	$$⊢\left(\phi \wedge \psi \right)\to \phi$$
12	11	exlimiv	$$⊢\exists z\left(\phi \wedge \psi \right)\to \phi$$
13		euex	$$⊢\exists !z\psi \to \exists z\psi$$
14	13	imim2i	$$⊢\left(\phi \to \exists !z\psi \right)\to \left(\phi \to \exists z\psi \right)$$
15	14	ancld	$$⊢\left(\phi \to \exists !z\psi \right)\to \left(\phi \to \left(\phi \wedge \exists z\psi \right)\right)$$
16		19.42v	$$⊢\exists z\left(\phi \wedge \psi \right)\leftrightarrow \left(\phi \wedge \exists z\psi \right)$$
17	15 16	imbitrrdi	$$⊢\left(\phi \to \exists !z\psi \right)\to \left(\phi \to \exists z\left(\phi \wedge \psi \right)\right)$$
18	12 17	impbid2	$$⊢\left(\phi \to \exists !z\psi \right)\to \left(\exists z\left(\phi \wedge \psi \right)\leftrightarrow \phi \right)$$
19	18	sps	$$⊢\forall y\left(\phi \to \exists !z\psi \right)\to \left(\exists z\left(\phi \wedge \psi \right)\leftrightarrow \phi \right)$$
20	19	sps	$$⊢\forall x\forall y\left(\phi \to \exists !z\psi \right)\to \left(\exists z\left(\phi \wedge \psi \right)\leftrightarrow \phi \right)$$
21	9 10 20	opabbid	$$⊢\forall x\forall y\left(\phi \to \exists !z\psi \right)\to \left\{⟨x,y⟩|\exists z\left(\phi \wedge \psi \right)\right\}=\left\{⟨x,y⟩|\phi \right\}$$
22	8 21	eqtrid	$$⊢\forall x\forall y\left(\phi \to \exists !z\psi \right)\to \mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\left(\phi \wedge \psi \right)\right\}=\left\{⟨x,y⟩|\phi \right\}$$
23		df-fn	$$⊢\left\{⟨⟨x,y⟩,z⟩|\left(\phi \wedge \psi \right)\right\}Fn\left\{⟨x,y⟩|\phi \right\}\leftrightarrow \left(\mathrm{Fun}\left\{⟨⟨x,y⟩,z⟩|\left(\phi \wedge \psi \right)\right\}\wedge \mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\left(\phi \wedge \psi \right)\right\}=\left\{⟨x,y⟩|\phi \right\}\right)$$
24	7 22 23	sylanbrc	$$⊢\forall x\forall y\left(\phi \to \exists !z\psi \right)\to \left\{⟨⟨x,y⟩,z⟩|\left(\phi \wedge \psi \right)\right\}Fn\left\{⟨x,y⟩|\phi \right\}$$