Theorem moexexlem

Description: Factor out the proof skeleton of moexex and moexexvw . (Contributed by Wolf Lammen, 2-Oct-2023)

	Ref	Expression
Hypotheses	moexexlem.1	$$⊢Ⅎy\phi$$
	moexexlem.2	$$⊢Ⅎy{\exists }^{*}x\phi$$
	moexexlem.3	$$⊢Ⅎx{\exists }^{*}y\exists x\left(\phi \wedge \psi \right)$$
Assertion	moexexlem	$$⊢\left({\exists }^{*}x\phi \wedge \forall x{\exists }^{*}y\psi \right)\to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		moexexlem.1	$$⊢Ⅎy\phi$$
2		moexexlem.2	$$⊢Ⅎy{\exists }^{*}x\phi$$
3		moexexlem.3	$$⊢Ⅎx{\exists }^{*}y\exists x\left(\phi \wedge \psi \right)$$
4		nfmo1	$$⊢Ⅎx{\exists }^{*}x\phi$$
5		nfa1	$$⊢Ⅎx\forall x{\exists }^{*}y\psi$$
6	5 3	nfim	$$⊢Ⅎx\left(\forall x{\exists }^{*}y\psi \to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)\right)$$
7		mopick	$$⊢\left({\exists }^{*}x\phi \wedge \exists x\left(\phi \wedge \psi \right)\right)\to \left(\phi \to \psi \right)$$
8	7	ex	$$⊢{\exists }^{*}x\phi \to \left(\exists x\left(\phi \wedge \psi \right)\to \left(\phi \to \psi \right)\right)$$
9	8	com23	$$⊢{\exists }^{*}x\phi \to \left(\phi \to \left(\exists x\left(\phi \wedge \psi \right)\to \psi \right)\right)$$
10	2 1 9	alrimd	$$⊢{\exists }^{*}x\phi \to \left(\phi \to \forall y\left(\exists x\left(\phi \wedge \psi \right)\to \psi \right)\right)$$
11		moim	$$⊢\forall y\left(\exists x\left(\phi \wedge \psi \right)\to \psi \right)\to \left({\exists }^{*}y\psi \to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)\right)$$
12	11	spsd	$$⊢\forall y\left(\exists x\left(\phi \wedge \psi \right)\to \psi \right)\to \left(\forall x{\exists }^{*}y\psi \to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)\right)$$
13	10 12	syl6	$$⊢{\exists }^{*}x\phi \to \left(\phi \to \left(\forall x{\exists }^{*}y\psi \to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)\right)\right)$$
14	4 6 13	exlimd	$$⊢{\exists }^{*}x\phi \to \left(\exists x\phi \to \left(\forall x{\exists }^{*}y\psi \to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)\right)\right)$$
15	1	nfex	$$⊢Ⅎy\exists x\phi$$
16		exsimpl	$$⊢\exists x\left(\phi \wedge \psi \right)\to \exists x\phi$$
17	15 16	exlimi	$$⊢\exists y\exists x\left(\phi \wedge \psi \right)\to \exists x\phi$$
18		nexmo	$$⊢\neg \exists y\exists x\left(\phi \wedge \psi \right)\to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)$$
19	17 18	nsyl5	$$⊢\neg \exists x\phi \to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)$$
20	19	a1d	$$⊢\neg \exists x\phi \to \left(\forall x{\exists }^{*}y\psi \to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)\right)$$
21	14 20	pm2.61d1	$$⊢{\exists }^{*}x\phi \to \left(\forall x{\exists }^{*}y\psi \to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)\right)$$
22	21	imp	$$⊢\left({\exists }^{*}x\phi \wedge \forall x{\exists }^{*}y\psi \right)\to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)$$