Theorem moexexlem

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

	Ref	Expression
Hypotheses	moexexlem.1	|- F/ y ph
	moexexlem.2	|- F/ y E* x ph
	moexexlem.3	|- F/ x E* y E. x ( ph /\ ps )
Assertion	moexexlem	|- ( ( E* x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		moexexlem.1	|- F/ y ph
2		moexexlem.2	|- F/ y E* x ph
3		moexexlem.3	|- F/ x E* y E. x ( ph /\ ps )
4		nfmo1	|- F/ x E* x ph
5		nfa1	|- F/ x A. x E* y ps
6	5 3	nfim	|- F/ x ( A. x E* y ps -> E* y E. x ( ph /\ ps ) )
7		mopick	|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )
8	7	ex	|- ( E* x ph -> ( E. x ( ph /\ ps ) -> ( ph -> ps ) ) )
9	8	com23	|- ( E* x ph -> ( ph -> ( E. x ( ph /\ ps ) -> ps ) ) )
10	2 1 9	alrimd	|- ( E* x ph -> ( ph -> A. y ( E. x ( ph /\ ps ) -> ps ) ) )
11		moim	|- ( A. y ( E. x ( ph /\ ps ) -> ps ) -> ( E* y ps -> E* y E. x ( ph /\ ps ) ) )
12	11	spsd	|- ( A. y ( E. x ( ph /\ ps ) -> ps ) -> ( A. x E* y ps -> E* y E. x ( ph /\ ps ) ) )
13	10 12	syl6	|- ( E* x ph -> ( ph -> ( A. x E* y ps -> E* y E. x ( ph /\ ps ) ) ) )
14	4 6 13	exlimd	|- ( E* x ph -> ( E. x ph -> ( A. x E* y ps -> E* y E. x ( ph /\ ps ) ) ) )
15	1	nfex	|- F/ y E. x ph
16		exsimpl	|- ( E. x ( ph /\ ps ) -> E. x ph )
17	15 16	exlimi	|- ( E. y E. x ( ph /\ ps ) -> E. x ph )
18		nexmo	|- ( -. E. y E. x ( ph /\ ps ) -> E* y E. x ( ph /\ ps ) )
19	17 18	nsyl5	|- ( -. E. x ph -> E* y E. x ( ph /\ ps ) )
20	19	a1d	|- ( -. E. x ph -> ( A. x E* y ps -> E* y E. x ( ph /\ ps ) ) )
21	14 20	pm2.61d1	|- ( E* x ph -> ( A. x E* y ps -> E* y E. x ( ph /\ ps ) ) )
22	21	imp	|- ( ( E* x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) )