avewright/proofwiki-math huggingface dataset:
Theorem: Set Difference is Right Distributive over Set Intersection

:$\paren {A \cap B} \setminus C = \paren {A \setminus C} \cap \paren {B \setminus C}$

Proof:
Consider $A, B, C \subseteq \mathbb U$, where $\mathbb U$ is considered as the universal set.
{{begin-eqn}}
{{eqn | l = \paren {A \cap B} \setminus C
      | r = \paren {A \cap B} \cap \map \complement C
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {A \cap B} \cap \paren {\map \complement C \cap \map \complement C}
      | c = Set Intersection is Idempotent
}}
{{eqn | r = \paren {A \cap \map \complement C} \cap \paren {B \cap \map \complement C}
      | c = Intersection is Associative and Intersection is Commutative
}}
{{eqn | r = \paren {A \setminus C} \cap \paren {B \setminus C}
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference is Right Distributive over Set Intersection

:$\paren {A \cap B} \setminus C = \paren {A \setminus C} \cap \paren {B \setminus C}$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \paren {A \cap B} \setminus C
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in 
      | r = A \land x \in B
      | c = {{Defof|Set Intersection}}
}}
{{eqn | lo= \land
      | l = x
      | o = \notin 
      | r = C
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = A \land x \in B
      | c = Rule of Idempotence
}}
{{eqn | lo= \land
      | l = x
      | o = \notin
      | r = C \land x \notin C
      | c = Rule of Idempotence
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = A
      | c = Rule of Association
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = x \in B \land x \notin C
      | c = 
}}
{{eqn | lo= \land
      | l = x
      | o = \notin
      | r = C
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = A
      | c = 
}}
{{eqn | lo= \land
      | l = x
      | o = \notin
      | r = C \land x \in B
      | c = Rule of Commutation
}}
{{eqn | lo= \land
      | l = x
      | o = \notin
      | r = C
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = A \land x \notin C
      | c = Rule of Association
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = B \land x \notin C
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \paren {A \setminus C}
      | c = {{Defof|Set Difference}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = \paren {B \setminus C}
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \paren {A \setminus C} \cap \paren {B \setminus C}
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set Intersection Distributes over Set Difference

:$\paren {R \setminus S} \cap T = \paren {R \cap T} \setminus \paren {S \cap T}$
:$R \cap \paren {S \setminus T} = \paren {R \cap S} \setminus \paren {R \cap T}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {R \cap T} \setminus \paren {S \cap T}
      | r = \paren {\paren {R \cap T} \setminus S} \cup \paren {\paren {R \cap T} \setminus T}
      | c = De Morgan's Laws: Difference with Intersection
}}
{{eqn | r = \paren {\paren {R \cap T} \setminus S} \cup \O
      | c = Set Difference of Intersection with Set is Empty Set
}}
{{eqn | r = \paren {R \cap T} \setminus S
      | c = Union with Empty Set
}}
{{eqn | r = \paren {R \setminus S} \cap T
      | c = Intersection with Set Difference is Set Difference with Intersection
}}
{{end-eqn}}
{{qed|lemma}}
Then:
{{begin-eqn}}
{{eqn | l = R \cap \paren {S \setminus T}
      | r = \paren {S \setminus T} \cap R
      | c = Intersection is Commutative
}}
{{eqn | r = \paren {S \cap R} \setminus \paren {T \cap R}
      | c = from above
}}
{{eqn | r = \paren {R \cap S} \setminus \paren {R \cap T}
      | c = Intersection is Commutative
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference with Intersection is Difference

:$S \setminus \paren {S \cap T} = S \setminus T$

Proof:
{{begin-eqn}}
{{eqn | l = S \setminus \paren {S \cap T}
      | r = \paren {S \setminus S} \cup \paren {S \setminus T}
      | c = De Morgan's Laws: Difference with Intersection
}}
{{eqn | r = \O \cup \paren {S \setminus T}
      | c = Set Difference with Self is Empty Set
}}
{{eqn | r = S \setminus T
      | c = Union with Empty Set
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference of Intersection with Set is Empty Set

:$\paren {S \cap T} \setminus S = \O$
:$\paren {S \cap T} \setminus T = \O$

Proof:
From Set Difference is Right Distributive over Set Intersection:
: $\paren {R \cap S} \setminus T = \paren {R \setminus T} \cap \paren {S \setminus T}$
Hence:
{{begin-eqn}}
{{eqn | l=\paren {S \cap T} \setminus S
      | r=\paren {S \setminus S} \cap \paren {T \setminus S}
      | c=Set Difference is Right Distributive over Set Intersection
}}
{{eqn | r=\O \cap \paren {T \setminus S}
      | c=Set Difference with Self is Empty Set
}}
{{eqn | r=\O
      | c=Intersection with Empty Set
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l=\paren {S \cap T} \setminus T
      | r=\paren {T \cap S} \setminus T
      | c=Intersection is Commutative
}}
{{eqn | r=\O
      | c=from above
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Set Intersection
Category:Empty Set
ifxfcnhmb3dfz8rns71h6wp0c57axva
Theorem: Set Difference Intersection with First Set is Set Difference

:$\paren {S \setminus T} \cap S = S \setminus T$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {S \setminus T}
      | o = \subseteq
      | r = S
      | c = Set Difference is Subset
}}
{{eqn | ll= \leadsto
      | l = \paren {S \setminus T} \cap S
      | r = S \setminus T
      | c = Intersection with Subset is Subset
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference Intersection with First Set is Set Difference

:$\paren {S \setminus T} \cap S = S \setminus T$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {S \setminus T} \cap S
      | r = \paren {S \cap S} \setminus T
      | c = Intersection with Set Difference is Set Difference with Intersection
}}
{{eqn | r = S \setminus T
      | c = Set Intersection is Idempotent
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference Intersection with Second Set is Empty Set

:$\paren {S \setminus T} \cap T = \O$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {S \setminus T} \cap T
      | r = \paren {S \cap T} \setminus \paren {T \cap T}
      | c = Set Intersection Distributes over Set Difference
}}
{{eqn | r = \paren {S \cap T} \setminus T
      | c = Set Intersection is Idempotent
}}
{{eqn | r = \O
      | c = Set Difference of Intersection with Set is Empty Set
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference Intersection with Second Set is Empty Set

:$\paren {S \setminus T} \cap T = \O$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {S \setminus T} \cap T
      | r = \paren {S \cap T} \setminus T
      | c = Intersection with Set Difference is Set Difference with Intersection
}}
{{eqn | r = \O
      | c = Set Difference of Intersection with Set is Empty Set
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference with Union is Set Difference

:$\paren {S \cup T} \setminus T = S \setminus T$

Proof:
Consider $S, T \subseteq \mathbb U$, where $\mathbb U$ is considered as the universal set.
{{begin-eqn}}
{{eqn | l = \paren {S \cup T} \setminus T
      | r = \paren {S \cup T} \cap \overline T
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {S \cap \overline T} \cup \paren {T \cap \overline T}
      | c = Intersection Distributes over Union
}}
{{eqn | r = \paren {S \setminus T} \cup \paren {T \setminus T}
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {S \setminus T} \cup \O
      | c = Set Difference with Self is Empty Set
}}
{{eqn | r = S \setminus T
      | c = Union with Empty Set
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Set Union
1eu95ymw9tq9dq3kuga3pni45lnkv42
Theorem: Set Difference Union First Set is First Set

:$\paren {S \setminus T} \cup S = S$

Proof:
Consider $S, T \subseteq \mathbb U$, where $\mathbb U$ is considered as the universal set.
{{begin-eqn}}
{{eqn | l = \paren {S \setminus T} \cup S
      | r = \paren {S \cap \map \complement T} \cup S
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = S
      | c = Union Absorbs Intersection
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Set Union
burbrgy5pwhe1leojwhbimbzu5hlmym
Theorem: Set Difference Union Second Set is Union

:$\paren {S \setminus T} \cup T = S \cup T$

Proof:
Consider $S, T \subseteq \mathbb U$, where $\mathbb U$ is considered as the universal set.
{{begin-eqn}}
{{eqn | l = \paren {S \setminus T} \cup T
      | r = \paren {S \cap \map \complement T} \cup T
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {S \cup T} \cap \paren {\map \complement T \cup T}
      | c = Union Distributes over Intersection
}}
{{eqn | r = \paren {S \cup T} \cap \mathbb U
      | c = Union with Complement
}}
{{eqn | r = S \cup T
      | c = Intersection with Universal Set
}}
{{end-eqn}}
{{qed}}
{{LEM|Union with Complement}}
Theorem: Set Difference with Union

:$R \setminus \paren {S \cup T} = \paren {R \cup T} \setminus \paren {S \cup T} = \paren {R \setminus S} \setminus T = \paren {R \setminus T} \setminus S$

Proof:
Consider $R, S, T \subseteq \mathbb U$, where $\mathbb U$ is considered as the universal set.
{{begin-eqn}}
{{eqn | l = \paren {R \cup T} \setminus \paren {S \cup T}
      | r = \paren {R \cup T} \cap \overline {\paren {S \cup T} }
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {R \cup T} \cap \paren {\overline S \cap \overline T}
      | c = De Morgan's Laws: Complement of Union
}}
{{eqn | r = \paren {\paren {R \cup T} \cap \overline T} \cap \overline S
      | c = Intersection is Associative and Intersection is Commutative
}}
{{eqn | r = \paren {\paren {R \cup T} \setminus T} \setminus S
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {R \setminus T} \setminus S
      | c = Set Difference with Union is Set Difference
}}
{{end-eqn}}
{{qed|lemma}}
Then:
{{begin-eqn}}
{{eqn | l = R \setminus \paren {S \cup T}
      | r = R \cap \overline {\paren {S \cup T} }
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = R \cap \paren {\overline S \cap \overline T}
      | c = De Morgan's Laws: Complement of Union
}}
{{eqn | r = \paren {R \cap \overline S} \cap \overline T
      | c = Intersection is Associative
}}
{{eqn | r = \paren {R \setminus S} \setminus  T
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed|lemma}}
Then:
{{begin-eqn}}
{{eqn | l = R \setminus \paren {S \cup T}
      | r = R \setminus \paren {T \cup S}
      | c = Union is Commutative
}}
{{eqn | r = \paren {R \setminus T} \setminus S
      | c = from above
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference is Right Distributive over Union

:$\paren {R \cup S} \setminus T = \paren {R \setminus T} \cup \paren {S \setminus T}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {R \cup S} \setminus T
      | r = \paren {R \cup S} \cap \overline T
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {R \cap \overline T} \cup \paren {S \cap \overline T}
      | c = Intersection Distributes over Union
}}
{{eqn | r = \paren {R \setminus T} \cup \paren {S \setminus T}
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Set Union
Category:Examples of Distributive Operations
fdto6uhmqtr7sig533aca78c0q688bz
Theorem: Set Difference with Set Difference is Union of Set Difference with Intersection

:$R \setminus \paren {S \setminus T} = \paren {R \setminus S} \cup \paren {R \cap T}$

Proof:
Consider $R, S, T \subseteq \mathbb U$, where $\mathbb U$ is considered as the universal set.
{{begin-eqn}}
{{eqn | l = R \setminus \paren {S \setminus T}
      | r = R \cap \overline {\paren {S \cap \overline T} }
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = R \cap \paren {\overline S \cup \overline {\paren {\overline T} } }
      | c = De Morgan's Laws
}}
{{eqn | r = R \cap \paren {\overline S \cup T}
      | c = Complement of Complement
}}
{{eqn | r = \paren {R \cap \overline S} \cup \paren {R \cap T}
      | c = Intersection Distributes over Union
}}
{{eqn | r = \paren {R \setminus S} \cup \paren {R \cap T}
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference is Subset of Union of Differences

:$R \setminus S \subseteq \paren {R \setminus T} \cup \paren {T \setminus S}$

Proof:
Consider $R, S, T \subseteq \mathbb U$, where $\mathbb U$ is considered as the universal set.
{{begin-eqn}}
{{eqn | l = R \setminus S
      | r = R \cap \overline S
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {R \cap \overline S} \cap \mathbb U
      | c = Intersection with Universal Set
}}
{{eqn | r = \paren {R \cap \overline S} \cap \paren {\overline T \cup T}
      | c = Union with Complement
}}
{{eqn | r = \paren {R \cap \overline S \cap \overline T} \cup \paren {T \cap R \cap \overline S}
      | c = Intersection Distributes over Union
}}
{{eqn | o = \subseteq
      | r = \paren {R \cap \overline T} \cup \paren {T \cap \overline S}
      | c = Union of Intersections
}}
{{eqn | r = \paren {R \setminus T} \cup \paren {T \setminus S}
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Set Union
5f4q0rqulug1vjzstamchdizvic35xy
Theorem: Ordered Sum of Tosets is Totally Ordered Set

Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be tosets.
Let $S + T = \struct {S \cup T, \preceq}$ be the ordered sum of $S$ and $T$.
Then $\struct {S \cup T, \preceq}$ is itself a toset.

Proof:
By definition of ordered sum, we have that:
* If $a, b \in S$, then $a \preceq b \iff a \preceq_1 b$.
* Otherwise, if $a, b \in T$, then $a \preceq b \iff a \preceq_2 b$.
* If neither of these is the case, then $a \in S, b \in T \iff a \preceq b$.
First we show that $\preceq$ is connected.
We note that as $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ are both tosets, then $\preceq_1$ and $\preceq_2$ are both connected.
Let $a, b \in S \cup T$.
There are three cases:
: $(1): \quad a, b \in S$, in which case $a \preceq_1 b$ or $b \preceq_1 a$
: $(2): \quad a, b \notin S$, in which case $a \preceq_2 b$ or $b \preceq_2 a$
: $(3): \quad$ Otherwise, in which case either $a \in S, b \notin S$ or $a \notin S, b \in S$.
:::By definition of $\preceq$ it follows that $a \preceq b$ or $b \preceq a$, but clearly not both.
So in all cases $a \preceq b$ or $b \preceq a$, and $\preceq$ is connected.
Now we check in turn each of the criteria for an ordering:
Theorem: Antilexicographic Product of Totally Ordered Sets is Totally Ordered

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be totally ordered sets.
Let $S_1 \otimes^a S_2 = \struct {S_1 \times S_2, \preccurlyeq_a}$ be the antilexicographic product of $S_1$ and $S_2$.
Then $\struct {S_1 \times S_2, \preccurlyeq_a}$ is itself a totally ordered set.

Proof:
From Antilexicographic Order is Ordering, we have that $\preccurlyeq_a$ is an ordering.
It remains to be shown that $\preccurlyeq_a$ is connected.
By definition of antilexicographic product, we have that:
::$\tuple {a, b} \preccurlyeq_a \tuple {c, d} \iff \tuple {c \prec_2 d} \lor \paren {c = d \land a \preccurlyeq_1 b}$
We note that as $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ are both totally ordered sets, then $\preccurlyeq_1$ and $\preccurlyeq_2$ are both connected.
Hence either:
:$c \prec_2 d$ or $d \prec_2 c$ or $c = d$
and also either 
:$a \preccurlyeq_2 b$ or $b \preccurlyeq_2 a$
If $c \prec_2 d$ or $d \prec_2 c$, it follows directly that:
:$\tuple {a, b} \preccurlyeq_a \tuple {c, d}$ or $\tuple {c, d} \preccurlyeq_a \tuple {a, b}$
Suppose $c = d$.
We have that either:
:$a \preccurlyeq_2 b$ or $b \preccurlyeq_2 a$
and so it follows that:
:$\tuple {a, b} \preccurlyeq_a \tuple {c, d}$ or $\tuple {c, d} \preccurlyeq_a \tuple {a, b}$
Hence, by definition, $\preccurlyeq_a$ is connected.
So we have shown that:
:$\preccurlyeq_a$ is connected
:$\preccurlyeq_a$ is reflexive, transitive and antisymmetric.
Thus by definition, $\preccurlyeq_a$ is a total ordering and so $\struct {S_1 \times S_2, \preccurlyeq_a}$ is a totally ordered set.
{{qed}}
Theorem: Restriction of Mapping is Mapping

Let $f: S \to T$ be a mapping.
Let $X \subseteq S$.
Let $f \restriction_X$ be the restriction of $f$ to $X$.
Then $f \restriction_X: X \to T$ is a mapping:
: whose domain is $X$
: whose preimage is $X$.

Proof:
As $f: S \to T$ is a mapping, we have that:
:$\forall x \in S: \tuple {x, y_1} \in f \land \tuple {x, y_2} \in f \implies y_1 = y_2$
From the definition of a subset, $x \in X \implies x \in S$, and so:
:$\forall x \in X: \tuple {x, y_1} \in f \restriction_X \land \tuple {x, y_2} \in f \restriction_X \implies y_1 = y_2$
Also from the definition of a mapping:
:$\forall x \in S: \exists y \in T: \tuple {x, y} \in f$
Again from the definition of a subset, $x \in X \implies x \in S$, and so:
:$\forall x \in X: \exists y \in T: \tuple {x, y} \in f \restriction_X$
So $f \restriction_X: X \to T$ is a mapping.
The fact that the domain of $f \restriction_X$ is $X$ follows from the definition of domain.
The fact that the preimage of $f \restriction_X$ is also $X$ follows from Preimage of Mapping equals Domain.
{{qed}}
Theorem: Image of Subset is Image of Restriction

Let $f: S \to T$ be a mapping.
Let $X \subseteq S$.
Let $f {\restriction_X}$ be the restriction of $f$ to $X$.
Then:
:$f \sqbrk X = \Img {f {\restriction_X} }$
where $\Img f$ denotes the image of $f$, defined as:
:$\Img f = \set {t \in T: \exists s \in S: t = \map f s}$

Proof:
Let $y \in f \sqbrk X$.
Then by definition of the image of a subset:
:$\exists x \in X: \map f x = y$
or equivalently:
:$\exists x \in X: \tuple {x, y} \in f$
But then by definition of restriction of $f$ to $X$:
:$f {\restriction_X} = \set {\tuple {x, y} \in f: x \in X}$
Thus by definition of the image set of $f {\restriction_X}$:
:$\Img {f {\restriction_X} } = f {\restriction_X} \sqbrk X = \set {y \in T: \exists x \in X: \tuple {x, y} \in f {\restriction_X} }$
Hence it can be seen that:
:$y \in \Img {f {\restriction_X} }$
So:
:$f \sqbrk X \subseteq \Img {f {\restriction_X} }$
{{qed|lemma}}
Now suppose that $y \in \Img {f {\restriction_X} }$.
Then by definition of the image set of $f {\restriction_X}$:
:$\exists x \in S: \tuple {x, y} \in f {\restriction_X}$
By definition of restriction of $f$ to $X$:
:$x \in X$
Thus by definition of image of a subset:
:$y \in f \sqbrk X$
So:
:$\Img {f {\restriction_X} } \subseteq f \sqbrk X$
{{qed|lemma}}
We have:
:$f \sqbrk X \subseteq \Img {f {\restriction_X} }$
:$\Img {f {\restriction_X} } \subseteq f \sqbrk X$
The result follows by definition of set equality.
{{qed}}
Theorem: Probability Mass Function of Binomial Distribution

The probability mass function (pmf) of a binomially distributed random variable $X$ is equal to:
:$\map \Pr {X = x} = \dbinom n x p^x \paren {1 - p}^{n - x}$
where $n$ is the number of trials and $p$ is the probability of success.

Proof:
Let $B_i: i = 1, 2, \ldots, \dbinom n x$ be events such that:
:$(1): \quad B_i$ is the $i$th possible way to see $x$ successes in $n$ Bernoulli trials
:$(2): \quad \forall i \ne j: B_i \cap B_j = \O$
We can see that:
:$\forall i: \map \Pr {B_i} = p^x \paren {1 - p}^{n - x}$
This is true since there will be $x$ successes, each with probability $p$ of occurring, and $n - x$ failures each with probability $1 - p$ of occurring.
Furthermore we can assume independent trials and thus the result follows.
See Binomial Experiment has Binomial Distribution for further analysis of this.
Now our task becomes finding:
:$\ds \map \Pr {X = x} = \map \Pr {\bigcup_{i \mathop = 1}^{\binom n x} B_i}$
which is the probability of one of the $\dbinom n x$ outcomes occurring.
Then by the Inclusion-Exclusion Principle considered as an extension of the Addition Law of Probability we have that for any countable union of events:
:$\ds \map \Pr {\bigcup_{i \mathop = 1}^n A_i} = \sum_{i \mathop = 1}^n \map \Pr {A_i} - \sum_{i \mathop \ne j: i, j \mathop = 1}^n \map \Pr {A_i \cap A_j} - \map \Pr {\bigcap_{i \mathop = 1}^n A_i}$
Fortunately in this case the above reduces to:
:$\ds \map \Pr {\bigcup_{i \mathop = 1}^n A_i} = \sum_{i \mathop = 1}^n \map \Pr {A_i}$
since the events are pairwise disjoint and $\map \Pr \O = 0$.
Thus:
{{begin-eqn}}
{{eqn | l = \map \Pr {X = x}
      | r = \map \Pr {\bigcup_{i \mathop = 1}^{\binom n x} B_i}
      | c = 
}}
{{eqn | r = \sum_{i \mathop = 1}^{\binom n x} \map \Pr {B_i}
      | c = 
}}
{{eqn | r = \sum_{i \mathop = 1}^{\binom n x} p^x \paren {1 - p}^{n - x}
      | c = 
}}
{{eqn | r = \binom n x p^x \paren {1 - p}^{n - x}
      | c = 
}}
{{end-eqn}}
{{Qed}}
<!--
Our last task is to show that the PMF sums to unity.
{{begin-eqn}}
{{eqn | l = \sum_{x \mathop = 0}^n \map \Pr {X = x}
      | r = \sum_{x \mathop = 0}^n \binom n x p^x \paren {1 - p}^{n - x}
      | c = 
}}
{{eqn | r = \paren {p + \paren {1 - p} }^n
      | c = 
}}
{{eqn | r = 1^n = 1
      | c = 
}}
{{end-eqn}}
-->
Theorem: Semantic Consequence Union Negation

Let $U$ be a set of propositional formulas.
Let $P$ be a propositional formula.
Let $U \models P$ denote that $U$ is a semantic consequence $P$.
Then:
:$U \models P$
iff:
:$U \cup \set {\neg P}$ has no models.

Proof:
=== Sufficient Condition ===
{{AimForCont}} $U \models P$.
Let $\MM$ be a model such that:
:$\MM \models U \cup \set {\neg P}$
Then by definition of $\MM$ being a model, we have that:
:$\MM \models U$
and by definition of semantic consequence:
:$\MM \models P$
So we have that $\MM \models P$ and $\MM \models \neg P$
By definition of contradiction, it follows that there can be no such model.
So $U \models P$ is a sufficient condition for $U \cup \set {\neg P}$ to have no models.
{{qed|lemma}}
Theorem: Union of Singleton

Consider the set of sets $A$ such that $A$ consists of just one set $x$:
:$A = \set x$
Then the union of $A$ is $x$:
:$\bigcup A = x$

Proof:
Let $A = \set x$.
From the definition of set union:
:$\bigcup \set x = \set {y: \exists z \in \set x: y \in z}$
from which it follows directly that:
:$\bigcup \set x = \set {y: y \in x}$
as $x$ is the only set in $\set x$.
That is:
:$\bigcup A = x$
{{qed}}
Theorem: Intersection of Singleton

Consider the set of sets $A$ such that $A$ consists of just one set $x$:
:$A = \set x$
Then the intersection of $A$ is $x$:
:$\bigcap A = x$

Proof:
Let $A = \set x$.
Then from the definition:
:$\bigcap \set x = \set {y: \forall z \in \set x: y \in z}$
from which it follows directly:
:$\bigcap \set x = \set {y: y \in x}$
as $x$ is the only set in $\set x$.
That is:
:$\bigcap A = x$
{{qed}}
Theorem: Union of Empty Set

Consider the set of sets $\mathbb S$ such that $\mathbb S$ is the empty set $\O$.
Then the union of $\mathbb S$ is $\O$:
:$\mathbb S = \O \implies \bigcup \mathbb S = \O$

Proof:
Let $\mathbb S = \O$.
Then from the definition:
:$\bigcup \mathbb S = \set {x: \exists X \in \mathbb S: x \in X}$
from which it follows directly:
:$\bigcup \mathbb S = \O$
as there are no sets in $\mathbb S$.
{{qed}}
Theorem: Intersection of Empty Set

Consider the set of sets $\mathbb S$ such that $\mathbb S$ is the empty set $\O$.
Then the intersection of $\mathbb S$ is $\mathbb U$:
:$\mathbb S = \O \implies \bigcap \mathbb S = \mathbb U$
where $\mathbb U$ is the universal set.
A paradoxical result.

Proof:
Let $\mathbb S = \O$.
Then from the definition:
:$ \bigcap \mathbb S = \set {x: \forall X \in \mathbb S: x \in X}$
Consider any $x \in \mathbb U$.
Then as $\mathbb S = \O$, it follows that:
:$\forall X \in \mathbb S: x \in X$
from the definition of vacuous truth.
It follows directly that:
:$\bigcap \mathbb S = \set {x: x \in \mathbb U}$
That is:
:$\bigcap \mathbb S = \mathbb U$
{{qed}}