Theorem 2eu6
Two equivalent expressions for double existential uniqueness.
(Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro,
17-Oct-2016.) (Proof shortened by Wolf Lammen, 2-Oct-2019.)
Conclusion
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \leftrightarrow x = z \wedge y = w) \)
Proof
l0
2eu4
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
l1
nfia1
l2
nfa1
l3
nfv
simpl
imim2i _
sps _
l7
exlimd l2 l3 _
\( \vdash \forall y \, (\varphi \rightarrow x = z \wedge y = w) \rightarrow \exists y \, \varphi \rightarrow x = z \)
ax12v
\( \vdash x = z \rightarrow \exists y \, \varphi \rightarrow \forall x \, (x = z \rightarrow \exists y \, \varphi) \)
syli l7 _
com12 _
l11
spsd _
\( \vdash \exists y \, \varphi \rightarrow \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \rightarrow \forall x \, (x = z \rightarrow \exists y \, \varphi) \)
l12
nfs1v
simpr
l14
imim2i _
\( \vdash (\varphi \rightarrow x = z \wedge y = w) \rightarrow \varphi \rightarrow y = w \)
sbequ1
\( \vdash y = w \rightarrow \varphi \rightarrow [ w / y ] \, \varphi \)
syli l14 _
sps _
exlimd l2 l12 _
imim2d _
l20
al2imi _
\( \vdash \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \rightarrow \forall x \, (x = z \rightarrow \exists y \, \varphi) \rightarrow \forall x \, (x = z \rightarrow [ w / y ] \, \varphi) \)
l21
sb6
\( \vdash [ z / x ] \, [ w / y ] \, \varphi \leftrightarrow \forall x \, (x = z \rightarrow [ w / y ] \, \varphi) \)
2sb6
\( \vdash [ z / x ] \, [ w / y ] \, \varphi \leftrightarrow \forall x \, \forall y \, (x = z \wedge y = w \rightarrow \varphi) \)
bitr3i l21 _
\( \vdash \forall x \, (x = z \rightarrow [ w / y ] \, \varphi) \leftrightarrow \forall x \, \forall y \, (x = z \wedge y = w \rightarrow \varphi) \)
imbitrdi l20 _
\( \vdash \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \rightarrow \forall x \, (x = z \rightarrow \exists y \, \varphi) \rightarrow \forall x \, \forall y \, (x = z \wedge y = w \rightarrow \varphi) \)
sylcom l11 _
l26
ancld _
\( \vdash \exists y \, \varphi \rightarrow \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \rightarrow \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \wedge \forall x \, \forall y \, (x = z \wedge y = w \rightarrow \varphi) \)
2albiim
\( \vdash \forall x \, \forall y \, (\varphi \leftrightarrow x = z \wedge y = w) \leftrightarrow \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \wedge \forall x \, \forall y \, (x = z \wedge y = w \rightarrow \varphi) \)
imbitrrdi l26 _
exlimi l1 _
2eximdv _
l31
imp _
biimpr
2alimi _
l34
2eximi _
\( \vdash \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \leftrightarrow x = z \wedge y = w) \rightarrow \exists z \, \exists w \, \forall x \, \forall y \, (x = z \wedge y = w \rightarrow \varphi) \)
2exsb
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists z \, \exists w \, \forall x \, \forall y \, (x = z \wedge y = w \rightarrow \varphi) \)
l36
sylibr l34 _
biimp
2alimi _
2eximi _
jca l36 _
impbii l31 _
\( \vdash \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \leftrightarrow \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \leftrightarrow x = z \wedge y = w) \)
bitri l0 _