Theorem moexexlem
Factor out the proof skeleton of moexex and moexexvw. (Contributed
by Wolf Lammen, 2-Oct-2023.)
Hypotheses
moexexlem.1
\( \vdash \Finv y \, \varphi \)
moexexlem.2
\( \vdash \Finv y \, \exists^\ast x \, \varphi \)
moexexlem.3
\( \vdash \Finv x \, \exists^\ast y \, \exists x \, (\varphi \wedge \psi) \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \wedge \forall x \, \exists^\ast y \, \psi \rightarrow \exists^\ast y \, \exists x \, (\varphi \wedge \psi) \)
Proof
l0
nfmo1
l1
nfa1
moexexlem.3
l3
nfim l1 _
l4
moexexlem.2
l5
moexexlem.1
mopick
ex _
com23 _
l9
alrimd l4 l5 _
\( \vdash \exists^\ast x \, \varphi \rightarrow \varphi \rightarrow \forall y \, (\exists x \, (\varphi \wedge \psi) \rightarrow \psi) \)
moim
spsd _
\( \vdash \forall y \, (\exists x \, (\varphi \wedge \psi) \rightarrow \psi) \rightarrow \forall x \, \exists^\ast y \, \psi \rightarrow \exists^\ast y \, \exists x \, (\varphi \wedge \psi) \)
syl6 l9 _
l13
exlimd l0 l3 _
\( \vdash \exists^\ast x \, \varphi \rightarrow \exists x \, \varphi \rightarrow \forall x \, \exists^\ast y \, \psi \rightarrow \exists^\ast y \, \exists x \, (\varphi \wedge \psi) \)
moexexlem.1
l15
nfex _
exsimpl
l17
exlimi l15 _
\( \vdash \exists y \, \exists x \, (\varphi \wedge \psi) \rightarrow \exists x \, \varphi \)
nexmo
\( \vdash \neg \exists y \, \exists x \, (\varphi \wedge \psi) \rightarrow \exists^\ast y \, \exists x \, (\varphi \wedge \psi) \)
nsyl5 l17 _
a1d _
\( \vdash \neg \exists x \, \varphi \rightarrow \forall x \, \exists^\ast y \, \psi \rightarrow \exists^\ast y \, \exists x \, (\varphi \wedge \psi) \)
pm2.61d1 l13 _
imp _