Theorem moexexlem 2643

Description: Factor out the proof skeleton of moexex 2655 and moexexvw 2645. (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 2574	. . . 4 ⊢ Ⅎ𝑥∃*𝑥𝜑
2		nfa1 2175	. . . . 5 ⊢ Ⅎ𝑥∀𝑥∃*𝑦𝜓
3		moexexlem.3	. . . . 5 ⊢ Ⅎ𝑥∃*𝑦∃𝑥(𝜑 ∧ 𝜓)
4	2, 3	nfim 1906	. . . 4 ⊢ Ⅎ𝑥(∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
5		moexexlem.2	. . . . . 6 ⊢ Ⅎ𝑦∃*𝑥𝜑
6		moexexlem.1	. . . . . 6 ⊢ Ⅎ𝑦𝜑
7		mopick 2642	. . . . . . . 8 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓))
8	7	ex 415	. . . . . . 7 ⊢ (∃*𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → (𝜑 → 𝜓)))
9	8	com23 86	. . . . . 6 ⊢ (∃*𝑥𝜑 → (𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → 𝜓)))
10	5, 6, 9	alrimd 2240	. . . . 5 ⊢ (∃*𝑥𝜑 → (𝜑 → ∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓)))
11		moim 2561	. . . . . 6 ⊢ (∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
12	11	spsd 2212	. . . . 5 ⊢ (∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
13	10, 12	syl6 35	. . . 4 ⊢ (∃*𝑥𝜑 → (𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))))
14	1, 4, 13	exlimd 2243	. . 3 ⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))))
15	6	nfex 2346	. . . . . 6 ⊢ Ⅎ𝑦∃𝑥𝜑
16		exsimpl 1878	. . . . . 6 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
17	15, 16	exlimi 2242	. . . . 5 ⊢ (∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
18		nexmo 2558	. . . . 5 ⊢ (¬ ∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
19	17, 18	nsyl5 159	. . . 4 ⊢ (¬ ∃𝑥𝜑 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
20	19	a1d 25	. . 3 ⊢ (¬ ∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
21	14, 20	pm2.61d1 181	. 2 ⊢ (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
22	21	imp 409	1 ⊢ ((∃*𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398  ∀wal 1548  ∃wex 1789  Ⅎwnf 1793  ∃*wmo 2554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-10 2165  ax-11 2181  ax-12 2202

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1790  df-nf 1794  df-mo 2556

This theorem is referenced by:  moexexvw  2645  2moswapv  2646  moexex  2655