Theorem moexexlem 2657

Description: Factor out the proof skeleton of moexex 2669 and moexexvw 2659. (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 2588	. . . 4 ⊢ Ⅎ𝑥∃*𝑥𝜑
2		nfa1 2189	. . . . 5 ⊢ Ⅎ𝑥∀𝑥∃*𝑦𝜓
3		moexexlem.3	. . . . 5 ⊢ Ⅎ𝑥∃*𝑦∃𝑥(𝜑 ∧ 𝜓)
4	2, 3	nfim 1929	. . . 4 ⊢ Ⅎ𝑥(∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
5		moexexlem.2	. . . . . 6 ⊢ Ⅎ𝑦∃*𝑥𝜑
6		moexexlem.1	. . . . . 6 ⊢ Ⅎ𝑦𝜑
7		mopick 2656	. . . . . . . 8 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓))
8	7	ex 418	. . . . . . 7 ⊢ (∃*𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → (𝜑 → 𝜓)))
9	8	com23 87	. . . . . 6 ⊢ (∃*𝑥𝜑 → (𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → 𝜓)))
10	5, 6, 9	alrimd 2254	. . . . 5 ⊢ (∃*𝑥𝜑 → (𝜑 → ∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓)))
11		moim 2575	. . . . . 6 ⊢ (∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
12	11	spsd 2226	. . . . 5 ⊢ (∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
13	10, 12	syl6 36	. . . 4 ⊢ (∃*𝑥𝜑 → (𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))))
14	1, 4, 13	exlimd 2257	. . 3 ⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))))
15	6	nfex 2360	. . . . . 6 ⊢ Ⅎ𝑦∃𝑥𝜑
16		exsimpl 1901	. . . . . 6 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
17	15, 16	exlimi 2256	. . . . 5 ⊢ (∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
18		nexmo 2572	. . . . 5 ⊢ (¬ ∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
19	17, 18	nsyl5 160	. . . 4 ⊢ (¬ ∃𝑥𝜑 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
20	19	a1d 26	. . 3 ⊢ (¬ ∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
21	14, 20	pm2.61d1 182	. 2 ⊢ (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
22	21	imp 412	1 ⊢ ((∃*𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816  ∃*wmo 2568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2179  ax-11 2195  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-mo 2570

This theorem is used by:  moexexvw  2659  2moswapv  2660  moexex  2669