Theorem moexexlem 2623

Description: Factor out the proof skeleton of moexex 2635 and moexexvw 2625. (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 2552	. . . 4 ⊢ Ⅎ𝑥∃*𝑥𝜑
2		nfa1 2149	. . . . 5 ⊢ Ⅎ𝑥∀𝑥∃*𝑦𝜓
3		moexexlem.3	. . . . 5 ⊢ Ⅎ𝑥∃*𝑦∃𝑥(𝜑 ∧ 𝜓)
4	2, 3	nfim 1900	. . . 4 ⊢ Ⅎ𝑥(∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
5		moexexlem.2	. . . . . 6 ⊢ Ⅎ𝑦∃*𝑥𝜑
6		moexexlem.1	. . . . . 6 ⊢ Ⅎ𝑦𝜑
7		mopick 2622	. . . . . . . 8 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓))
8	7	ex 414	. . . . . . 7 ⊢ (∃*𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → (𝜑 → 𝜓)))
9	8	com23 86	. . . . . 6 ⊢ (∃*𝑥𝜑 → (𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → 𝜓)))
10	5, 6, 9	alrimd 2209	. . . . 5 ⊢ (∃*𝑥𝜑 → (𝜑 → ∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓)))
11		moim 2539	. . . . . 6 ⊢ (∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
12	11	spsd 2181	. . . . 5 ⊢ (∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
13	10, 12	syl6 35	. . . 4 ⊢ (∃*𝑥𝜑 → (𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))))
14	1, 4, 13	exlimd 2212	. . 3 ⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))))
15	6	nfex 2318	. . . . . 6 ⊢ Ⅎ𝑦∃𝑥𝜑
16		exsimpl 1872	. . . . . 6 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
17	15, 16	exlimi 2211	. . . . 5 ⊢ (∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
18		nexmo 2536	. . . . 5 ⊢ (¬ ∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
19	17, 18	nsyl5 159	. . . 4 ⊢ (¬ ∃𝑥𝜑 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
20	19	a1d 25	. . 3 ⊢ (¬ ∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
21	14, 20	pm2.61d1 180	. 2 ⊢ (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
22	21	imp 408	1 ⊢ ((∃*𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397  ∀wal 1540  ∃wex 1782  Ⅎwnf 1786  ∃*wmo 2533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-11 2155  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-mo 2535

This theorem is referenced by:  moexexvw  2625  2moswapv  2626  moexex  2635