This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ y φ
moexexlem.2 ⊢ Ⅎ y ∃* x φ
moexexlem.3 ⊢ Ⅎ x ∃* y ∃ x φ ∧ ψ
Assertion moexexlem ⊢ ∃* x φ ∧ ∀ x ∃* y ψ → ∃* y ∃ x φ ∧ ψ

Proof

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