Theorem 2mo
Two ways of expressing "there exists at most one ordered pair
<. x , y >. such that ph ( x , y ) holds. See also 2mo2.
(Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro,
17-Oct-2016.) (Proof shortened by Wolf Lammen, 2-Nov-2019.)
Conclusion
\( \vdash \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \leftrightarrow \forall x \, \forall y \, \forall z \, \forall w \, (\varphi \wedge [ z / x ] \, [ w / y ] \, \varphi \rightarrow x = z \wedge y = w) \)
Proof
l0
2mo2
\( \vdash \exists^\ast x \, \exists y \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi \leftrightarrow \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
l1
nfmo1
nfe1
nfmov _
l4
nfan l1 _
nfe1
l6
nfmov _
nfmo1
l8
nfan l6 _
l9
19.8a
\( \vdash \varphi \rightarrow \exists y \, \varphi \)
spsbe
l11
sbimi _
\( \vdash [ z / x ] \, [ w / y ] \, \varphi \rightarrow [ z / x ] \, \exists y \, \varphi \)
nfv
mo3 _
biimpi _
\( \vdash \exists^\ast x \, \exists y \, \varphi \rightarrow \forall x \, \forall z \, (\exists y \, \varphi \wedge [ z / x ] \, \exists y \, \varphi \rightarrow x = z) \)
19.21bbi _
\( \vdash \exists^\ast x \, \exists y \, \varphi \rightarrow \exists y \, \varphi \wedge [ z / x ] \, \exists y \, \varphi \rightarrow x = z \)
l16
syl2ani l9 l11 _
l17
19.8a
\( \vdash \varphi \rightarrow \exists x \, \varphi \)
l18
sbcom2
\( \vdash [ z / x ] \, [ w / y ] \, \varphi \leftrightarrow [ w / y ] \, [ z / x ] \, \varphi \)
spsbe
sbimi _
\( \vdash [ w / y ] \, [ z / x ] \, \varphi \rightarrow [ w / y ] \, \exists x \, \varphi \)
l21
sylbi l18 _
\( \vdash [ z / x ] \, [ w / y ] \, \varphi \rightarrow [ w / y ] \, \exists x \, \varphi \)
nfv
mo3 _
biimpi _
\( \vdash \exists^\ast y \, \exists x \, \varphi \rightarrow \forall y \, \forall w \, (\exists x \, \varphi \wedge [ w / y ] \, \exists x \, \varphi \rightarrow y = w) \)
19.21bbi _
\( \vdash \exists^\ast y \, \exists x \, \varphi \rightarrow \exists x \, \varphi \wedge [ w / y ] \, \exists x \, \varphi \rightarrow y = w \)
syl2ani l17 l21 _
anim12ii l16 _
alrimi l8 _
alrimi l4 _
alrimivv _
\( \vdash \exists^\ast x \, \exists y \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi \rightarrow \forall z \, \forall w \, \forall x \, \forall y \, (\varphi \wedge [ z / x ] \, [ w / y ] \, \varphi \rightarrow x = z \wedge y = w) \)
l31
sylbir l0 _
l32
nfs1v
nfs1v
l34
nfsbv _
pm3.21
imim1d _
alimd l34 _
alimd l32 _
com12 _
aleximi _
l41
aleximi _
\( \vdash \forall z \, \forall w \, \forall x \, \forall y \, (\varphi \wedge [ z / x ] \, [ w / y ] \, \varphi \rightarrow x = z \wedge y = w) \rightarrow \exists z \, \exists w \, [ z / x ] \, [ w / y ] \, \varphi \rightarrow \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
l42
2nexaln
\( \vdash \neg \exists x \, \exists y \, \varphi \leftrightarrow \forall x \, \forall y \, \neg \varphi \)
l43
nfv
nfv
2sb8ef l43 _
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists z \, \exists w \, [ z / x ] \, [ w / y ] \, \varphi \)
l46
xchnxbi l42 _
\( \vdash \neg \exists z \, \exists w \, [ z / x ] \, [ w / y ] \, \varphi \leftrightarrow \forall x \, \forall y \, \neg \varphi \)
pm2.21
2alimi _
2eximi _
\( \vdash \exists z \, \exists w \, \forall x \, \forall y \, \neg \varphi \rightarrow \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
19.23bi _
\( \vdash \exists w \, \forall x \, \forall y \, \neg \varphi \rightarrow \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
19.23bi _
\( \vdash \forall x \, \forall y \, \neg \varphi \rightarrow \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
sylbi l46 _
\( \vdash \neg \exists z \, \exists w \, [ z / x ] \, [ w / y ] \, \varphi \rightarrow \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
pm2.61d1 l41 _
l54
impbii l31 _
\( \vdash \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \leftrightarrow \forall z \, \forall w \, \forall x \, \forall y \, (\varphi \wedge [ z / x ] \, [ w / y ] \, \varphi \rightarrow x = z \wedge y = w) \)
alrot4
\( \vdash \forall z \, \forall w \, \forall x \, \forall y \, (\varphi \wedge [ z / x ] \, [ w / y ] \, \varphi \rightarrow x = z \wedge y = w) \leftrightarrow \forall x \, \forall y \, \forall z \, \forall w \, (\varphi \wedge [ z / x ] \, [ w / y ] \, \varphi \rightarrow x = z \wedge y = w) \)
bitri l54 _