Theorem moexexlem 2626

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

Hypotheses

Ref	Expression
moexexlem.1	⊢ Ⅎ𝑦𝜑
moexexlem.2	⊢ Ⅎ𝑦∃*𝑥𝜑
moexexlem.3	⊢ Ⅎ𝑥∃*𝑦∃𝑥(𝜑 ∧ 𝜓)

Assertion

Ref	Expression
moexexlem	⊢ ((∃*𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))

Proof of Theorem moexexlem

Step	Hyp	Ref	Expression
1		nfmo1 2557	. . . 4 ⊢ Ⅎ𝑥∃*𝑥𝜑
2		nfa1 2151	. . . . 5 ⊢ Ⅎ𝑥∀𝑥∃*𝑦𝜓
3		moexexlem.3	. . . . 5 ⊢ Ⅎ𝑥∃*𝑦∃𝑥(𝜑 ∧ 𝜓)
4	2, 3	nfim 1896	. . . 4 ⊢ Ⅎ𝑥(∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
5		moexexlem.2	. . . . . 6 ⊢ Ⅎ𝑦∃*𝑥𝜑
6		moexexlem.1	. . . . . 6 ⊢ Ⅎ𝑦𝜑
7		mopick 2625	. . . . . . . 8 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓))
8	7	ex 412	. . . . . . 7 ⊢ (∃*𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → (𝜑 → 𝜓)))
9	8	com23 86	. . . . . 6 ⊢ (∃*𝑥𝜑 → (𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → 𝜓)))
10	5, 6, 9	alrimd 2215	. . . . 5 ⊢ (∃*𝑥𝜑 → (𝜑 → ∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓)))
11		moim 2544	. . . . . 6 ⊢ (∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
12	11	spsd 2187	. . . . 5 ⊢ (∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
13	10, 12	syl6 35	. . . 4 ⊢ (∃*𝑥𝜑 → (𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))))
14	1, 4, 13	exlimd 2218	. . 3 ⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))))
15	6	nfex 2324	. . . . . 6 ⊢ Ⅎ𝑦∃𝑥𝜑
16		exsimpl 1868	. . . . . 6 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
17	15, 16	exlimi 2217	. . . . 5 ⊢ (∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
18		nexmo 2541	. . . . 5 ⊢ (¬ ∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
19	17, 18	nsyl5 159	. . . 4 ⊢ (¬ ∃𝑥𝜑 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
20	19	a1d 25	. . 3 ⊢ (¬ ∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
21	14, 20	pm2.61d1 180	. 2 ⊢ (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
22	21	imp 406	1 ⊢ ((∃*𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∀wal 1538  ∃wex 1779  Ⅎwnf 1783  ∃*wmo 2538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-mo 2540

This theorem is referenced by:  moexexvw  2628  2moswapv  2629  moexex  2638