Lawvere's Sets for Mathematics defines a separator object $S$ for morphisms $f_1, f_2: X \rightarrow Y$ of the Set category as a logic statement $s$
$s$:
$\forall x \left[ S \xrightarrow{x} X \Rightarrow f_1 \circ x = f_2 \circ x\right] \Rightarrow f_1 = f_2$
Some proof exercises in the book are easier to start with considering morphisms that are not equal $f_1 \neq f_2$. How to invert the above statement $s$ logically?
Is it
$\bar{s}_1$:
$f_1 \neq f_2 \Rightarrow \exists x \left[S \xrightarrow{x} X \Rightarrow f_1 \circ x \neq f_2 \circ x\right]$
?
Somehow I feels it's more "natural" to substitute the "$\Rightarrow$" symbols in the square brackets by "and" or "such that". Do I miss some concepts in logic that might make me feel this way? (My knowledge in logic is whatever I learned from high school maths and remains now.)
EDIT:
$\bar{s}_2$:
$f_1 \neq f_2 \land \exists x \left[S \xrightarrow{x} X \land f_1 \circ x \neq f_2 \circ x\right]$
EDIT 2:
$\bar{s}_3$:
$f_1 \neq f_2 \Rightarrow \exists x \left[S \xrightarrow{x} X \land f_1 \circ x \neq f_2 \circ x\right]$
The denial of $p \Rightarrow q$ is not, as you seem to have it, $p \Rightarrow \lnot q$, but instead it's $p \land (\lnot q).$ So it seems your statement after "Is it" would be correct if you replaced the $\Rightarrow$ in it by a conjunction symbol $\land$.