What is the logical structure of this proof about closed sets and convergent sequences. $\require{enclose}$
The proof below is from Introduction to Real Analysis by Rosenlicht,

Let $S$ be a subset of a metric space $E$. Then $S$ is closed if and
only if, whenever $p_1$,$p_2$,$p_3$,$\dots$ is a sequence of points of
S that is convergent in $E$, we have $\lim\limits_{n \to \infty} p_n$
$\in$ $S$.
Suppose that $S$ is closed and that $p_1$,$p_2$,$p_3$,$\dots$ is a
sequence of points of $S$ that converges to a point $p$ of $E$.  We
must show that $p$ $\in$ $S$.  If this is not so, we have $p$ $\in$
$\mathscr C S$.  Since $\mathscr C S$ is open, there is some
$\epsilon$>0 such that $\mathscr C S$ contains the entire open ball of
center $p$ and radius $\epsilon$.  Thus if $N$ is a positive integer
such that d($p$, $p_n$) < $\epsilon$ whenever $n$ > $N$, we have $p_n$
$\in$ $\mathscr C S$ whenever $n$ > $N$, a contradiction.  This shows
that $p$ $\in$ $S$ and proves the "only if" part of the theorem.
To prove the "if" part, suppose $S$ $\subset$ $E$ is not closed.  Then
$\mathscr C S$ is not open, and there exists a point $p$ in $\mathscr C S$
such that any open ball of center $p$ contains points of $S$.
Hence for each positive integer $n$ we can choose $p_n$ $\in$ $S$ such
that d($p$, $p_n$) < $1/n$.  Then $\lim\limits_{n \to \infty} p_n$ =
$p$, with each $\enclose{horizontalstrike}{p_n \in \mathscr C S\,and\,p \in S}$ $p_n\in S\,and\,p \notin S$  .
This shows that if the hypothesis on convergent sequences holds, then
$S$ must be closed, completing the proof of the "if" part, and hence
of the whole theorem.

I understand that to prove a statement of the form $P \iff Q$ it's necessary to show $P \implies Q$ and $Q \implies P$.  In the above theorem, let's call the statements:
$$X := S\,is\,closed.$$
$$ Y := p_1,p_2,p_3,\dots\,is\,a\,sequence\,of\,points\,of\,S\,that\,converges\,to\,a\,point\,p\,of\,E.$$
$$Z := \lim\limits_{n \to \infty} p_n
\in S. $$
In terms of those, the theorem is $X \iff Y \land Z$ so it's necessary to show $X \implies Y \land Z$ and $Y \land Z \implies X$.
The "only if" part of the theorem is $Y \land Z \implies X$ and the proof is of the form:
$$ Assume\, X \land Y \\  \lnot Z \implies Y \land \lnot Y\\ \therefore\,Z$$
The "if" part of the theorem is $X \iff Y \land Z$ and the proof is of the form:
$$ \lnot X \implies \lnot Y \land Z $$
I don't understand how this proof is valid. My questions are:

*

*The "only if" part seems to be by contradiction.  In a proof by contradiction, you're supposed to assume that the antecedant is false, in this case $Y \land Z$.  But here only $Z$ is assumed false.  Is that OK because a false $Z$ makes $Y \land Z$ false as well?



*The "if" part of the proof seems to be by contrapositive?  In a proof by contrapositive, you're supposed to assume the consequent is false and derive that the antecedent is false, in this case $\lnot X \implies \lnot(Y \land Z)$. But here only $\lnot Y \land Z$ is shown to be false.


*I doubt I got the logical forms of the theorem or proofs right.  What are their logical forms?
 A: 
$X$ := $S$ is closed $Y$ := $p_1,p_2,p_3,\dots$ is a sequence of points in $S$  that converges to a point in $E$ $Z$ := $\lim\limits_{n \to \infty} p_n \in S$

Let $S$ be a subset of a metric space $E$. Then $S$ is closed if and
only if, whenever $p_1$,$p_2$,$p_3$,$\dots$ is a sequence of points of
S that is convergent in $E$, we have $\lim\limits_{n \to \infty} p_n$
$\in$ $S$.


As pointed out by Karl, the above theorem translates as $$X\leftrightarrow\forall \vec p \:\big(Y(\vec p)\to Z(\vec p)\big).$$ This is actually logically equivalent to the conjunction of $$\forall \vec p \:\big(X\land Y(\vec p)\to Z(\vec p)\big)\tag1$$ and $$\lnot X\to  \exists \vec p \:\big(Y(\vec p)\land\lnot Z(\vec p)\big).\tag2$$


Suppose that $S$ is closed and that $p_1$,$p_2$,$p_3$,$\dots$ is a
sequence of points of $S$ that converges to a point $p$ of $E$.  We
must show that $p$ $\in$ $S$.


proves the "only if" part of the theorem


This is statement $(1)$ from above: $$\forall \vec p \:\big(X\land Y(\vec p)\to Z(\vec p)\big).\tag1$$


To prove the "if" part, suppose $S$ $\subset$ $E$ is not closed. Then


there exists


$\lim\limits_{n \to \infty} p_n = p$, with each $p_n \in S$ and $p\not\in S.$


completing the proof of the "if" part


This is statement $(2)$ from above: $$\lnot X\to  \exists \vec p \:\big(Y(\vec p)\land\lnot Z(\vec p)\big).\tag2$$

Referring to the original text screen-captured below, note that you have mistranscribed


Then $\lim\limits_{n \to \infty} p_n = p,$ with each $p_n\in \boldsymbol S$ and $p\boldsymbol{\not\in S}$


as


Then $\lim\limits_{n \to \infty} p_n = p,$ with each $p_n \in \boldsymbol{\mathscr C S}$ and $p \boldsymbol{\in S}$


and that the excerpt I used above is actually the corrected one.

