Metamath Proof Explorer

Theorem moexexlem

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

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

Proof

Step Hyp Ref Expression
1 moexexlem.1 ⊢ Ⅎ 𝑦 𝜑
2 moexexlem.2 ⊢ Ⅎ 𝑦 ∃* 𝑥 𝜑
3 moexexlem.3 ⊢ Ⅎ 𝑥 ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 )
4 nfmo1 ⊢ Ⅎ 𝑥 ∃* 𝑥 𝜑
5 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∃* 𝑦 𝜓
6 5 3 nfim ⊢ Ⅎ 𝑥 ( ∀ 𝑥 ∃* 𝑦 𝜓 → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
7 mopick ⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 → 𝜓 ) )
8 7 ex ⊢ ( ∃* 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
9 8 com23 ⊢ ( ∃* 𝑥 𝜑 → ( 𝜑 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜓 ) ) )
10 2 1 9 alrimd ⊢ ( ∃* 𝑥 𝜑 → ( 𝜑 → ∀ 𝑦 ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜓 ) ) )
11 moim ⊢ ( ∀ 𝑦 ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜓 ) → ( ∃* 𝑦 𝜓 → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
12 11 spsd ⊢ ( ∀ 𝑦 ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜓 ) → ( ∀ 𝑥 ∃* 𝑦 𝜓 → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
13 10 12 syl6 ⊢ ( ∃* 𝑥 𝜑 → ( 𝜑 → ( ∀ 𝑥 ∃* 𝑦 𝜓 → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) )
14 4 6 13 exlimd ⊢ ( ∃* 𝑥 𝜑 → ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 ∃* 𝑦 𝜓 → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) )
15 1 nfex ⊢ Ⅎ 𝑦 ∃ 𝑥 𝜑
16 exsimpl ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 𝜑 )
17 15 16 exlimi ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 𝜑 )
18 nexmo ⊢ ( ¬ ∃ 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
19 17 18 nsyl5 ⊢ ( ¬ ∃ 𝑥 𝜑 → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
20 19 a1d ⊢ ( ¬ ∃ 𝑥 𝜑 → ( ∀ 𝑥 ∃* 𝑦 𝜓 → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
21 14 20 pm2.61d1 ⊢ ( ∃* 𝑥 𝜑 → ( ∀ 𝑥 ∃* 𝑦 𝜓 → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
22 21 imp ⊢ ( ( ∃* 𝑥 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜓 ) → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )