Theorem isarep2

Description: Part of a study of the Axiom of Replacement used by the Isabelle prover. In Isabelle, the sethood of PrimReplace is apparently postulated implicitly by its type signature " [ i, [ i, i ] => o ] => i", which automatically asserts that it is a set without using any axioms. To prove that it is a set in Metamath, we need the hypotheses of Isabelle's "Axiom of Replacement" as well as the Axiom of Replacement in the form funimaex . (Contributed by NM, 26-Oct-2006)

	Ref	Expression
Hypotheses	isarep2.1	$$⊢A\in \mathrm{V}$$
	isarep2.2	$$⊢\forall x\in A\forall y\forall z\left(\left(\phi \wedge \left[z/y\right]\phi \right)\to y=z\right)$$
Assertion	isarep2	$$⊢\exists ww=\left\{⟨x,y⟩|\phi \right\}\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		isarep2.1	$$⊢A\in \mathrm{V}$$
2		isarep2.2	$$⊢\forall x\in A\forall y\forall z\left(\left(\phi \wedge \left[z/y\right]\phi \right)\to y=z\right)$$
3		resima	$$⊢\left({\left\{⟨x,y⟩|\phi \right\}\upharpoonright }_A\right)\left[A\right]=\left\{⟨x,y⟩|\phi \right\}\left[A\right]$$
4		resopab	$$⊢{\left\{⟨x,y⟩|\phi \right\}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
5	4	imaeq1i	$$⊢\left({\left\{⟨x,y⟩|\phi \right\}\upharpoonright }_A\right)\left[A\right]=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\left[A\right]$$
6	3 5	eqtr3i	$$⊢\left\{⟨x,y⟩|\phi \right\}\left[A\right]=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\left[A\right]$$
7		funopab	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\leftrightarrow \forall x{\exists }^{*}y\left(x\in A\wedge \phi \right)$$
8	2	rspec	$$⊢x\in A\to \forall y\forall z\left(\left(\phi \wedge \left[z/y\right]\phi \right)\to y=z\right)$$
9		nfv	$$⊢Ⅎz\phi$$
10	9	mo3	$$⊢{\exists }^{*}y\phi \leftrightarrow \forall y\forall z\left(\left(\phi \wedge \left[z/y\right]\phi \right)\to y=z\right)$$
11	8 10	sylibr	$$⊢x\in A\to {\exists }^{*}y\phi$$
12		moanimv	$$⊢{\exists }^{*}y\left(x\in A\wedge \phi \right)\leftrightarrow \left(x\in A\to {\exists }^{*}y\phi \right)$$
13	11 12	mpbir	$$⊢{\exists }^{*}y\left(x\in A\wedge \phi \right)$$
14	7 13	mpgbir	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
15	1	funimaex	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\to \left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\left[A\right]\in \mathrm{V}$$
16	14 15	ax-mp	$$⊢\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\left[A\right]\in \mathrm{V}$$
17	6 16	eqeltri	$$⊢\left\{⟨x,y⟩|\phi \right\}\left[A\right]\in \mathrm{V}$$
18	17	isseti	$$⊢\exists ww=\left\{⟨x,y⟩|\phi \right\}\left[A\right]$$