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 
|- F/ y ph
moexexlem.2 
|- F/ y E* x ph
moexexlem.3 
|- F/ x E* y E. x ( ph /\ ps )
Assertion moexexlem 
|- ( ( E* x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 moexexlem.1 
 |-  F/ y ph
2 moexexlem.2 
 |-  F/ y E* x ph
3 moexexlem.3 
 |-  F/ x E* y E. x ( ph /\ ps )
4 nfmo1 
 |-  F/ x E* x ph
5 nfa1 
 |-  F/ x A. x E* y ps
6 5 3 nfim 
 |-  F/ x ( A. x E* y ps -> E* y E. x ( ph /\ ps ) )
7 mopick 
 |-  ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )
8 7 ex 
 |-  ( E* x ph -> ( E. x ( ph /\ ps ) -> ( ph -> ps ) ) )
9 8 com23 
 |-  ( E* x ph -> ( ph -> ( E. x ( ph /\ ps ) -> ps ) ) )
10 2 1 9 alrimd 
 |-  ( E* x ph -> ( ph -> A. y ( E. x ( ph /\ ps ) -> ps ) ) )
11 moim 
 |-  ( A. y ( E. x ( ph /\ ps ) -> ps ) -> ( E* y ps -> E* y E. x ( ph /\ ps ) ) )
12 11 spsd 
 |-  ( A. y ( E. x ( ph /\ ps ) -> ps ) -> ( A. x E* y ps -> E* y E. x ( ph /\ ps ) ) )
13 10 12 syl6 
 |-  ( E* x ph -> ( ph -> ( A. x E* y ps -> E* y E. x ( ph /\ ps ) ) ) )
14 4 6 13 exlimd 
 |-  ( E* x ph -> ( E. x ph -> ( A. x E* y ps -> E* y E. x ( ph /\ ps ) ) ) )
15 1 nfex 
 |-  F/ y E. x ph
16 exsimpl 
 |-  ( E. x ( ph /\ ps ) -> E. x ph )
17 15 16 exlimi 
 |-  ( E. y E. x ( ph /\ ps ) -> E. x ph )
18 nexmo 
 |-  ( -. E. y E. x ( ph /\ ps ) -> E* y E. x ( ph /\ ps ) )
19 17 18 nsyl5 
 |-  ( -. E. x ph -> E* y E. x ( ph /\ ps ) )
20 19 a1d 
 |-  ( -. E. x ph -> ( A. x E* y ps -> E* y E. x ( ph /\ ps ) ) )
21 14 20 pm2.61d1 
 |-  ( E* x ph -> ( A. x E* y ps -> E* y E. x ( ph /\ ps ) ) )
22 21 imp 
 |-  ( ( E* x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) )