Mathematical Logic, Interpretation, Satisfiable, Consequence relation

[annoymage]

Theorem : let A be a set of formulas, a be a formula

For all A and all a,

Every interpretation which is a model of A is also a model of a iff
not (Sat A) U {~a}

Proof

Every interpretation which is a model of A is also a model of a
iff(1) there is no interpretation which is a model of A but not a model of a
iff(2) there is no interpretation which is model of A U {~a}
iff(3) not (Sat A) U {~a}

i don't understand on the iff(2), it seems to assume that "but" is "union"(U)

this is from ebbinghaus mathematical logic, this is my first time reading mathematical logic books, I've been noticing that much of the proof are using argument(english) rather than formal language. Furthermore like for example iff(1). i can tell how => goes, but rather now i am still trying to accept the <= part. HELP !
Edit: ok i already get the <= part in iff(1), but still don't know what happen on iff(2)
Edit(2):
the statement "Every interpretation which is a model of A is also a model of a"

let B be arbitrary interpretation

is the statement equivalent to "B is a model of A iff B is a model of a"?
or "B is a model of A => B is a model of a"?

 

[Valkarie]

A:The statement "$B$ is a model of $A$ iff $B$ is a model of $a$" is true, and it is what the theorem is asserting.The statement "$B$ is a model of $A$ implies $B$ is a model of $a$" is also true, and is a weaker version of the theorem.The statement "there is no interpretation which is model of $A \cup \{\lnot a\}$" means that for any interpretation $B$, either $B$ is not a model of $A$ or $B$ is not a model of $\lnot a$. This is equivalent to saying that for any interpretation $B$, $B$ is a model of $A$ implies $B$ is a model of $a$.So the equivalence given by the theorem is between "Every interpretation which is a model of $A$ is also a model of $a$" and "not ($\mathrm{Sat}(A) \cup \{\lnot a\}$)".