Theorem sn-axprlem3

Description: axprlem3 using only Tarski's FOL axiom schemes and ax-rep . (Contributed by SN, 22-Sep-2023)

	Ref	Expression
Assertion	sn-axprlem3	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \exists w\in xif-\left(\phi ,z=a,z=b\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		axrep6	$$⊢\forall w{\exists }^{*}zif-\left(\phi ,z=a,z=b\right)\to \exists y\forall z\left(z\in y\leftrightarrow \exists w\in xif-\left(\phi ,z=a,z=b\right)\right)$$
2		ax6evr	$$⊢\exists ya=y$$
3		ifptru	$$⊢\phi \to \left(if-\left(\phi ,z=a,z=b\right)\leftrightarrow z=a\right)$$
4	3	biimpd	$$⊢\phi \to \left(if-\left(\phi ,z=a,z=b\right)\to z=a\right)$$
5		equtrr	$$⊢a=y\to \left(z=a\to z=y\right)$$
6	4 5	sylan9r	$$⊢\left(a=y\wedge \phi \right)\to \left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)$$
7	6	alrimiv	$$⊢\left(a=y\wedge \phi \right)\to \forall z\left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)$$
8	7	expcom	$$⊢\phi \to \left(a=y\to \forall z\left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)\right)$$
9	8	eximdv	$$⊢\phi \to \left(\exists ya=y\to \exists y\forall z\left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)\right)$$
10	2 9	mpi	$$⊢\phi \to \exists y\forall z\left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)$$
11		ax6evr	$$⊢\exists yb=y$$
12		ifpfal	$$⊢\neg \phi \to \left(if-\left(\phi ,z=a,z=b\right)\leftrightarrow z=b\right)$$
13	12	biimpd	$$⊢\neg \phi \to \left(if-\left(\phi ,z=a,z=b\right)\to z=b\right)$$
14		equtrr	$$⊢b=y\to \left(z=b\to z=y\right)$$
15	13 14	sylan9r	$$⊢\left(b=y\wedge \neg \phi \right)\to \left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)$$
16	15	alrimiv	$$⊢\left(b=y\wedge \neg \phi \right)\to \forall z\left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)$$
17	16	expcom	$$⊢\neg \phi \to \left(b=y\to \forall z\left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)\right)$$
18	17	eximdv	$$⊢\neg \phi \to \left(\exists yb=y\to \exists y\forall z\left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)\right)$$
19	11 18	mpi	$$⊢\neg \phi \to \exists y\forall z\left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)$$
20	10 19	pm2.61i	$$⊢\exists y\forall z\left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)$$
21		df-mo	$$⊢{\exists }^{*}zif-\left(\phi ,z=a,z=b\right)\leftrightarrow \exists y\forall z\left(if-\left(\phi ,z=a,z=b\right)\to z=y\right)$$
22	20 21	mpbir	$$⊢{\exists }^{*}zif-\left(\phi ,z=a,z=b\right)$$
23	1 22	mpg	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \exists w\in xif-\left(\phi ,z=a,z=b\right)\right)$$