Theorem mo3
Alternate definition of the at-most-one quantifier. Definition of
[BellMachover] p. 460, except that definition has the side condition
that \( y \) not occur in \( \varphi \) in place of our hypothesis. (Contributed
by NM, 8-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Aug-2019.)
Remove dependency on [ax-13]. (Revised by BJ and WL, 29-Jan-2023.)
Hypothesis
mo3.nf
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \forall x \, \forall y \, (\varphi \wedge [ y / x ] \, \varphi \rightarrow x = y) \)
Proof
l0
nfmo1
mo3.nf
l2
nfmov _
l3
dfmo
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
l4
sp
l5
spsbim
\( \vdash \forall x \, (\varphi \rightarrow x = z) \rightarrow [ y / x ] \, \varphi \rightarrow [ y / x ] \, x = z \)
equsb3
\( \vdash [ y / x ] \, x = z \leftrightarrow y = z \)
imbitrdi l5 _
l8
anim12d l4 _
\( \vdash \forall x \, (\varphi \rightarrow x = z) \rightarrow \varphi \wedge [ y / x ] \, \varphi \rightarrow x = z \wedge y = z \)
equtr2
\( \vdash x = z \wedge y = z \rightarrow x = y \)
syl6 l8 _
exlimiv _
\( \vdash \exists z \, \forall x \, (\varphi \rightarrow x = z) \rightarrow \varphi \wedge [ y / x ] \, \varphi \rightarrow x = y \)
sylbi l3 _
alrimi l2 _
l14
alrimi l0 _
l15
nfs1v
pm3.21
imim1d _
alimd l15 _
com12 _
l20
aleximi _
\( \vdash \forall y \, \forall x \, (\varphi \wedge [ y / x ] \, \varphi \rightarrow x = y) \rightarrow \exists y \, [ y / x ] \, \varphi \rightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
mo3.nf
l22
sb8ef _
\( \vdash \exists x \, \varphi \leftrightarrow \exists y \, [ y / x ] \, \varphi \)
mo3.nf
mof _
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
l25
3imtr4g l20 l22 _
\( \vdash \forall y \, \forall x \, (\varphi \wedge [ y / x ] \, \varphi \rightarrow x = y) \rightarrow \exists x \, \varphi \rightarrow \exists^\ast x \, \varphi \)
moabs
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \exists^\ast x \, \varphi \)
sylibr l25 _
alcoms _
impbii l14 _