Theorem 2eu5
An alternate definition of double existential uniqueness (see 2eu4 ).
A mistake sometimes made in the literature is to use E! x E! y to
mean "exactly one \( x \) and exactly one \( y \) ". (For example, see
Proposition 7.53 of [TakeutiZaring] p. 53.) It turns out that this is
actually a weaker assertion, as can be seen by expanding out the formal
definitions. This theorem shows that the erroneous definition can be
repaired by conjoining \( \forall x \, \exists^\ast y \, \varphi \) as an additional condition. The
correct definition apparently has never been published. ( E* means
"there exists at most one".) (Contributed by NM, 26-Oct-2003.) Avoid
[ax-13]. (Revised by Wolf Lammen, 2-Oct-2023.)
Conclusion
\( \vdash \exists{!} x \, \exists{!} y \, \varphi \wedge \forall x \, \exists^\ast y \, \varphi \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
Proof
2eu1v
l1
pm5.32ri _
\( \vdash \exists{!} x \, \exists{!} y \, \varphi \wedge \forall x \, \exists^\ast y \, \varphi \leftrightarrow \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \wedge \forall x \, \exists^\ast y \, \varphi \)
l2
eumo
\( \vdash \exists{!} y \, \exists x \, \varphi \rightarrow \exists^\ast y \, \exists x \, \varphi \)
2moexv
\( \vdash \exists^\ast y \, \exists x \, \varphi \rightarrow \forall x \, \exists^\ast y \, \varphi \)
syl l2 _
adantl _
l6
pm4.71i _
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \wedge \forall x \, \exists^\ast y \, \varphi \)
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) \)
3bitr2i l1 l6 _