Theorem wl-mo3t

Description: Closed form of mo3 . (Contributed by Wolf Lammen, 18-Aug-2019)

	Ref	Expression
Assertion	wl-mo3t	$$⊢\forall xℲy\phi \to \left({\exists }^{*}x\phi \leftrightarrow \forall x\forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfa1	$$⊢Ⅎx\forall xℲy\phi$$
2		nfmo1	$$⊢Ⅎx{\exists }^{*}x\phi$$
3		nfnf1	$$⊢ℲyℲy\phi$$
4	3	nfal	$$⊢Ⅎy\forall xℲy\phi$$
5		sp	$$⊢\forall xℲy\phi \to Ⅎy\phi$$
6	1 5	nfmod	$$⊢\forall xℲy\phi \to Ⅎy{\exists }^{*}x\phi$$
7	4 6	nfan1	$$⊢Ⅎy\left(\forall xℲy\phi \wedge {\exists }^{*}x\phi \right)$$
8		df-mo	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists u\forall x\left(\phi \to x=u\right)$$
9		sp	$$⊢\forall x\left(\phi \to x=u\right)\to \left(\phi \to x=u\right)$$
10		spsbim	$$⊢\forall x\left(\phi \to x=u\right)\to \left(\left[y/x\right]\phi \to \left[y/x\right]x=u\right)$$
11		equsb3	$$⊢\left[y/x\right]x=u\leftrightarrow y=u$$
12	10 11	imbitrdi	$$⊢\forall x\left(\phi \to x=u\right)\to \left(\left[y/x\right]\phi \to y=u\right)$$
13	9 12	anim12d	$$⊢\forall x\left(\phi \to x=u\right)\to \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to \left(x=u\wedge y=u\right)\right)$$
14		equtr2	$$⊢\left(x=u\wedge y=u\right)\to x=y$$
15	13 14	syl6	$$⊢\forall x\left(\phi \to x=u\right)\to \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
16	15	exlimiv	$$⊢\exists u\forall x\left(\phi \to x=u\right)\to \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
17	8 16	sylbi	$$⊢{\exists }^{*}x\phi \to \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
18	17	adantl	$$⊢\left(\forall xℲy\phi \wedge {\exists }^{*}x\phi \right)\to \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
19	7 18	alrimi	$$⊢\left(\forall xℲy\phi \wedge {\exists }^{*}x\phi \right)\to \forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
20	19	ex	$$⊢\forall xℲy\phi \to \left({\exists }^{*}x\phi \to \forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$
21	1 2 20	alrimd	$$⊢\forall xℲy\phi \to \left({\exists }^{*}x\phi \to \forall x\forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$
22		nfa1	$$⊢Ⅎx\forall x\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
23		nfs1v	$$⊢Ⅎx\left[y/x\right]\phi$$
24		pm3.3	$$⊢\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\to \left(\phi \to \left(\left[y/x\right]\phi \to x=y\right)\right)$$
25	24	com23	$$⊢\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\to \left(\left[y/x\right]\phi \to \left(\phi \to x=y\right)\right)$$
26	25	sps	$$⊢\forall x\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\to \left(\left[y/x\right]\phi \to \left(\phi \to x=y\right)\right)$$
27	22 23 26	alrimd	$$⊢\forall x\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\to \left(\left[y/x\right]\phi \to \forall x\left(\phi \to x=y\right)\right)$$
28	27	aleximi	$$⊢\forall y\forall x\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\to \left(\exists y\left[y/x\right]\phi \to \exists y\forall x\left(\phi \to x=y\right)\right)$$
29	28	alcoms	$$⊢\forall x\forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\to \left(\exists y\left[y/x\right]\phi \to \exists y\forall x\left(\phi \to x=y\right)\right)$$
30		moabs	$$⊢{\exists }^{*}x\phi \leftrightarrow \left(\exists x\phi \to {\exists }^{*}x\phi \right)$$
31		wl-sb8et	$$⊢\forall xℲy\phi \to \left(\exists x\phi \leftrightarrow \exists y\left[y/x\right]\phi \right)$$
32		wl-mo2t	$$⊢\forall xℲy\phi \to \left({\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)\right)$$
33	31 32	imbi12d	$$⊢\forall xℲy\phi \to \left(\left(\exists x\phi \to {\exists }^{*}x\phi \right)\leftrightarrow \left(\exists y\left[y/x\right]\phi \to \exists y\forall x\left(\phi \to x=y\right)\right)\right)$$
34	30 33	bitrid	$$⊢\forall xℲy\phi \to \left({\exists }^{*}x\phi \leftrightarrow \left(\exists y\left[y/x\right]\phi \to \exists y\forall x\left(\phi \to x=y\right)\right)\right)$$
35	29 34	imbitrrid	$$⊢\forall xℲy\phi \to \left(\forall x\forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\to {\exists }^{*}x\phi \right)$$
36	21 35	impbid	$$⊢\forall xℲy\phi \to \left({\exists }^{*}x\phi \leftrightarrow \forall x\forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$