Velleman's Proof Designer problem 44 This is an exercise I didn't solve from the group of exercises present on Velleman's site that should be solved using Proof Designer (the little program that comes with the book).
Theorem:
If $\forall \mathcal{F} (\cup \mathcal{F} = A \rightarrow A \in \mathcal{F})$, then $\exists x (A=\{x\})$.
Before addressing my line of reasoning and the tentative proof, just few words on this specific problem. I find it interesting because it shows me that I still have problems figuring (and writing) properly existence results. About this, I would say that no matter what book on proof writing you take, this point is usually quickly considered and the examples are trivial, so not particularly useful for real mathematics. Probably this is related to the fact that existence theorems are in general the "hard ones" to be proven and to be thaught (I guess that they are the most difficult to be grasp by students), but I really don't know and I would like to know the opinions of experts.
Line of Reasoning:
I think the idea is that $x=\emptyset$ and $A=\{\emptyset\})$. In this way, what we have to assume should stand. Indeed, the antecedent should "bind" the nature of the family of sets and the consequence would follow.
Tentative Proof:
Let x be the empty set $\emptyset$. Thus, $\forall \mathcal{F} (\cup \mathcal{F} = \{\emptyset\} \rightarrow \{\emptyset\} \in \mathcal{F})$. Take $\mathcal{F}=\{\emptyset,\{\emptyset\}\}$. Then, we have $\cup \{\emptyset,\{\emptyset\}\} = \{\emptyset\} \rightarrow \{\emptyset\} \in \{\emptyset,\{\emptyset\}\}$, and the result is established.
PS: As I pointed out in another post, in general I try to be more consistent grammatically speaking when I write down proofs, and I avoid the use of logical symbols. I tend to do it when I have doubts about the content of the problem and here... I have no clue at all, so forgive it. Any feedback is more than welcome.
 A: You are still quite far from proving the theorem. The issue seems to be that you misunderstood what the theorem is saying. I will try to explain it with a minimum of logical symbols, as you said you prefer that.

We are given a set $A$. First, let us investigate the premise:
$$\forall \mathcal F: \cup \mathcal F = A \to A \in \mathcal F$$
One could say that this expresses that $A$ is "union-irreducible": when it is the union of any collection of sets $\mathcal F$ (i.e. $\cup\mathcal F = A$), then it must be the case that one of these sets in $\mathcal F$ already is $A$.
It is important that we have the universal quantifier $\forall$ here, because we want to say that $A$ is "irreducible" under all unions, not just some particular ones.
Now let us turn to the conclusion:
$$\exists x: A = \{x\}$$
It does not say anything but: $A$ has precisely one element (formally: "there is an $x$ such that $x$ is the only element of $A$).
Thus, the statement of the theorem becomes: Any union-irreducible set $A$ consists of precisely one element.
In particular, we are not allowed to pick a set $A$, or, equivalently, the element $x \in A$. The theorem has to be proved for all union-irreducible sets.

For completeness, I will indicate a proof of the theorem. Let $A$ be a union-irreducible set.
We have the set $\mathcal F = \{\{x\}:x \in A\}$, comprising a singleton $\{x\}$ for each $x \in A$. It is trivial to see that $\cup\mathcal F = A$.
So now we need the conclusion to hold, i.e. $A \in \mathcal F$. But this means that there must exist an $x\in A$ such that $A = \{x\}$. The theorem follows.
A: Yes, Lord_Farin's elegant proof can be done in Proof Designer.  Start by applying the "Universal Instantiation" command to the hypothesis $\forall \mathcal{F}(\bigcup\mathcal{F} = A \to A \in \mathcal{F})$.  This allows you to plug in whatever you want for $\mathcal{F}$.  You can go ahead and plug in exactly the set suggested by Lord_Farin:  $\{\{x\} \mid x \in A\}$.
A: Your tentative proof is the wrong direction: If $A$ is a singleton (in fact a very specific singleton) then the antecedent holds.
Under the assumption of  $\forall \mathcal{F} (\cup \mathcal{F} = A \rightarrow A \in \mathcal{F}) $, first show $\exists x(x\in A)$. In other words: Show that $A=\emptyset$ implies $\neg\forall \mathcal{F} (\cup \mathcal{F} = A \rightarrow A \in \mathcal{F}) $ or equivalently $\exists \mathcal{F} (\cup \mathcal{F} = A \land A \notin \mathcal{F}) $. You can do this by specifically exhibiting such $\mathcal F$.
Next show $(x\in A\land y\in A)\rightarrow x=y$. Again, exhibit $\mathcal F$ with $\cup \mathcal{F} = A \land A \notin \mathcal{F}$.
You should already know that $x\in A$ and $(x\in A\land y\in A)\rightarrow x=y$ implies $A=\{x\}$.
