avewright/proofwiki-math huggingface dataset:
Theorem: Identity Matrix is Permutation Matrix

An identity matrix is an example of a permutation matrix.

Proof:
An identity matrix, by definition, has instances of $1$ on the main diagonal and $0$ elsewhere.
Each diagonal element is by definition on one row and one column of the matrix.
Also by definition, each diagonal element is on a different row and 
column from each other diagonal element.
The result follows by definition of permutation matrix.
{{qed}}
Theorem: Full Rook Matrix is Nonsingular

A full rook matrix is nonsingular.

Proof:
Let $\mathbf A$ be a full rook matrix.
By definition, $\mathbf A$ is an instance of a permutation matrix.
By Determinant of Permutation Matrix, it follows that $\det \mathbf A = \pm 1$.
By Matrix is Nonsingular iff Determinant has Multiplicative Inverse:
:$\mathbf A$ is nonsingular.
{{qed}}
Theorem: Product of Rook Matrices is Rook Matrix

Let $\mathbf A$ and $\mathbf B$ be rook matrices.
Their product $\mathbf {A B}$ is also a rook matrix.

Proof:
An element $a b_{ij}$ of $\mathbf {A B}$ is formed by multiplying each element of row $i$ of $\mathbf A$ by its corresponding element of column $j$ of $\mathbf B$.
No more than $1$ element of row $i$ equals $1$, and the rest equal $0$.
No more than $1$ column $k$ of $\mathbf B$ contains $1$ in its $i$th element, and the rest contain $0$.
So of all the elements of row $i$ of $\mathbf {A B}$, only $a b_{ik}$ is $1$, and the rest are $0$.
By the same argument, each row of $\mathbf {A B}$ contains no more than one $1$, and all the rest of the elements are $0$.
In $\mathbf B$, each column $j$ has no more than one element equal to $1$, and all are in a different row $k$.
Thus each row contains its $1$, if it has one, in a different column from all the other rows.
So there is no more than one $1$ in each column of $\mathbf {A B}$.
Hence the result by definition of rook matrix.
{{qed}}
Theorem: Topology Defined by Basis

Let $S$ be a set.
Let $\BB$ be a set of subsets of $S$.
Suppose that
:$(\text B1): \quad \forall A_1, A_2 \in \BB: \forall x \in A_1 \cap A_2: \exists A \in \BB: x \in A \subseteq A_1 \cap A_2$
:$(\text B2): \quad \forall x \in X: \exists A \in \BB: x \in A$
::$\tau = \set {\bigcup \GG: \GG \subseteq \BB}$
Then:
:$T = \struct {S, \tau}$ is a topological space
:$\BB$ is a basis of $T$.

Proof:
We have to prove Open Set Axioms:
Theorem: Equivalence of Definitions of Singular Matrix

{{TFAE|def = Singular Matrix}}
Let $\struct {R, +, \circ}$ be a ring with unity.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $\mathbf A$ be an element of the ring of square matrices $\struct {\map {\MM_R} n, +, \times}$.

Proof:
Follows directly from Matrix is Nonsingular iff Determinant has Multiplicative Inverse.
{{qed}}
Category:Singular Matrices
avq5fidzrgypqx4rm6rl12cyoniwy22
Theorem: Matrix is Singular iff Product with Non-Zero Vector is Zero

Let $\mathbb F$ be a field.
Let $\mathbf A$ be a square matrix of order $n$ over $\mathbb F$.
Then $\mathbf A$ is singular {{iff}} there exists a vector $\mathbf v \in \mathbb F^n$:
:$\mathbf v \ne \mathbf 0$
:$\mathbf A \mathbf v = \mathbf 0$
where $\mathbf 0$ is the zero vector.

Proof:
=== Sufficient Case ===
Aiming for a Proof by Contraposition, suppose that
:$\neg \exists \mathbf v \in \mathbb F^n : \mathbf v \neq \mathbf 0 \wedge \mathbf A \mathbf v = \mathbf 0$
Then, for any two vectors $\mathbf p, \mathbf q \in \mathbb F^n$,
{{begin-eqn}}
{{eqn | l = \mathbf A \mathbf p
      | r = \mathbf A \mathbf q
}}
{{eqn | ll= \leadsto
      | l = \mathbf A \mathbf p - \mathbf A \mathbf q
      | r = \mathbf 0
}}
{{eqn | ll= \leadsto
      | l = \mathbf A \paren {\mathbf p - \mathbf q}
      | r = \mathbf 0
      | c = Matrix Multiplication Distributes over Matrix Addition
}}
{{eqn | ll= \leadsto
      | l = \mathbf p - \mathbf q
      | r = \mathbf 0
}}
{{eqn | ll= \leadsto
      | l = \mathbf p
      | r = \mathbf q
}}
{{end-eqn}}
Thus, multiplying by $\mathbf A$ is injective.
Using block multiplication, the product $\mathbf A \mathbf v$ can be written as
{{begin-eqn}}
{{eqn | l = \mathbf A \mathbf v
      | r = \begin{bmatrix} \mathbf A_1 & \mathbf A_2 & \cdots & \mathbf A_n \end{bmatrix} \begin{bmatrix} v_1 \\ v_2 \\ \vdots \\ v_n \end{bmatrix}
      | c = $\mathbf A_k$ is the $k$th column of $\mathbf A$, $v_k$ is the $k$th component of $\mathbf v$
}}
{{eqn | r = \sum_{k \mathop = 1}^n \mathbf A_k v_k
}}
{{end-eqn}}
Since the only way this vector sum can equal $\mathbf 0$ is if $\mathbf v = \mathbf 0$, which entails that $\forall k \in \closedint 1 n : v_k = 0$, the vectors $\set {\mathbf A_k}$ must be linearly independent.
By Sufficient Conditions for Basis of Finite Dimensional Vector Space, a set of $n$ linearly independent vectors in $\mathbb F^n$ is a basis for $\mathbb F^n$.
Therefore,
:$\forall \mathbf y \in \mathbb F^n : \exists \mathbf x \in \mathbb F^n : \mathbf A \mathbf x = y$
Therefore, multiplication by $\mathbf A$ is surjective.
Since multiplication by $\mathbf A$ is both injective and surjective, it is bijective.
By the definition of bijective, $\mathbf A$ has an inverse.
Therefore, $\mathbf A$ is nonsingular.
Now, we have that
:$\neg \exists \mathbf v \in \mathbb F^n : \mathbf v \neq \mathbf 0 \wedge \mathbf A \mathbf v = \mathbf 0 \implies \mathbf A$ is nonsingular.
By the Rule of Transposition,
:$\mathbf A$ is singular $\implies \exists \mathbf v \in \mathbb F^n : \mathbf v \neq \mathbf 0 \wedge \mathbf A \mathbf v = \mathbf 0$
{{qed|lemma}}
Theorem: Equivalence of Definitions of Integer Congruence

Let $m \in \Z_{> 0}$.
{{TFAE|def = Congruence Modulo Integer|view = congruence modulo $m$}}

Proof:
Let $x_1, x_2, z \in \Z$.
Let $x_1 \equiv x_2 \pmod z$ as defined by the equal remainder after division:
:$\RR_z = \set {\tuple {x, y} \in \Z \times \Z: \exists k \in \Z: x = y + k z}$
Let $\tuple {x_1, x_2} \in \RR_z$.
Then by definition:
:$\exists k \in \Z: x_1 = x_2 + k z$
So, by definition of the modulo operation:
{{begin-eqn}}
{{eqn | l = x_1 \mod z
      | r = \paren {x_2 + k z} - z \floor {\frac {x_2 + k z} z}
      | c = 
}}
{{eqn | r = \paren {x_2 + k z} - z \floor {\frac {x_2} z + k}
      | c = 
}}
{{eqn | r = \paren {x_2 + k z} - z \floor {\frac {x_2} z} + k z
      | c = 
}}
{{eqn | r = x_2 - z \floor {\frac {x_2} z}
      | c = 
}}
{{eqn | r = x_2 \mod z
      | c = 
}}
{{end-eqn}}
So:
:$x_1 \equiv x_2 \pmod z$
in the sense of definition by modulo operation.
{{qed|lemma}}
Now let $x_1 \equiv x_2 \pmod z$ in the sense of definition by modulo operation.
That is:
:$x_1 \equiv x_2 \pmod z \iff x_1 \mod z = x_2 \mod z$
Let $z = 0$.
Then by definition, $x_1 \mod 0 = x_1$ and $x_2 \mod 0 = x_2$.
So as $x_1 \mod 0 = x_2 \mod 0$ we have that $x_1 = x_2$.
So:
:$x_1 - x_2 = 0 = 0.z$
and so $x_1 \equiv x_2 \pmod z$ in the sense of definition by integer multiple.
Now suppose $z \ne 0$.
Then from definition of the modulo operation:
:$x_1 \mod z = x_1 - z \floor {\dfrac {x_1} z}$
:$x_2 \mod z = x_2 - z \floor {\dfrac {x_2} z}$
Thus:
:$x_1 - z \floor {\dfrac {x_1} z} = x_2 - z \floor {\dfrac {x_2} z}$
and so:
:$x_1 - x_2 = z \paren {\floor {\dfrac {x_1} z} - \floor {\dfrac {x_2} z} }$
From the definition of the floor function, we see that both $\floor {\dfrac {x_1} z}$ and $\floor {\dfrac {x_2} z}$ are integers.
Therefore, so is $\floor {\dfrac {x_1} z} - \floor {\dfrac {x_2} z}$ an integer.
So $\exists k \in \Z: x_1 - x_2 = k z$.
Thus $x_1 - x_2 = k z$ and:
:$x_1 \equiv x_2 \pmod z$
in the sense of definition by integer multiple.
{{qed|lemma}}
Now let $x_1 \equiv x_2 \pmod z$ in the sense of definition by integer multiple.
That is, $\exists k \in \Z: x_1 - x_2 = k z$.
Then $x_1 = x_2 + k z$ and so $\tuple {x_1, x_2} \in \RR_z$ where:
:$\RR_z = \set {\tuple {x, y} \in \R \times \R: \exists k \in \Z: x = y + k z}$
and so
:$x_1 \equiv x_2 \pmod z$
in the sense of definition by equivalence relation.
{{qed|lemma}}
So all three definitions are equivalent: $(1) \implies (2) \implies (3) \implies (1)$.
{{qed}}
Theorem: Occurrence in Prefix Notation has Unique Scope

Let $\FF$ be a formal language in prefix notation.
Let $\mathbf A$ be a well-formed formula of $\FF$.
Let $a$ be an occurrence in $\mathbf A$.
Then $a$ has a unique scope.

Proof:
From the formal definition of prefix notation, it follows that $a$ must be introduced by the rule of formation:
:$a \mathbf A_1 \cdots \mathbf A_n$
for some well-formed formulas $\mathbf A_1, \ldots, \mathbf A_n$.
By Unique Readability for Prefix Notation, the $\mathbf A_i$ are uniquely determined.
Then $\mathbf A' = a \mathbf A_1 \cdots \mathbf A_n$ is a well-formed part of $\mathbf A$.
Moreover, any well-formed part of $\mathbf A$ containing $a$ must contain $\mathbf A'$.
Hence $\mathbf A'$ is the scope of $a$.
{{qed}}
Theorem: Krull's Theorem

Let $R$ be a non-null ring with unity.
Then $R$ has a maximal ideal.

Proof:
Let $\struct {P, \subseteq}$ be the ordered set consisting of all proper ideals of $R$, ordered by inclusion.
The theorem is proved by applying Zorn's Lemma to $P$.
First, we check that the conditions for Zorn's Lemma are met: $P$ must be non-empty, and every non-empty chain in $P$ must have an upper bound.
Theorem: Exclusive Or as Conjunction of Disjunctions

:$p \oplus q \dashv \vdash \paren {p \lor q} \land \paren {\neg p \lor \neg q}$

Proof:
{{begin-eqn}}
{{eqn | l = p \oplus q
      | o = \dashv \vdash
      | r = \paren {p \lor q} \land \neg \paren {p \land q}
      | c = {{Defof|Exclusive Or}}
}}
{{eqn | o = \dashv \vdash
      | r = \paren {p \lor q} \land \paren {\neg p \lor \neg q}
      | c = De Morgan's Laws: Disjunction of Negations
}}
{{end-eqn}}
{{qed}}
Theorem: Exclusive Or as Conjunction of Disjunctions

:$p \oplus q \dashv \vdash \paren {p \lor q} \land \paren {\neg p \lor \neg q}$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc||ccccccccc|} \hline
p & \oplus & q & (p & \lor & q) & \land & (\neg & p & \lor & \neg & q) \\
\hline
\F & \F & \F & \F & \F & \F & \F & \T & \F & \T & \T & \F \\
\F & \T & \T & \F & \T & \T & \T & \T & \F & \T & \F & \T \\
\T & \T & \F & \T & \T & \F & \T & \F & \T & \T & \T & \F \\
\T & \F & \T & \T & \T & \T & \F & \F & \T & \F & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: NAND as Disjunction of Negations

:$p \uparrow q \dashv \vdash \neg p \lor \neg q$

Proof:
{{begin-eqn}}
{{eqn | l = p \uparrow q
      | o = \dashv \vdash
      | r = \map \neg {p \land q}
      | c = {{Defof|Logical NAND}}
}}
{{eqn | o = \dashv \vdash
      | r = \neg p \lor \neg q
      | c = De Morgan's Laws: Disjunction of Negations
}}
{{end-eqn}}
{{qed}}
Theorem: NAND as Disjunction of Negations

:$p \uparrow q \dashv \vdash \neg p \lor \neg q$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccc||ccccc|} \hline
p & \uparrow & q & \neg & p & \lor & \neg & q \\
\hline
\F & \T & \F & \T & \F & \T & \T & \F \\
\F & \T & \T & \T & \F & \T & \F & \T  \\
\T & \T & \F & \F & \T & \T & \T & \F  \\
\T & \F & \T & \F & \T & \F & \F & \T  \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Idempotence/Disjunction/Formulation 2/Forward Implication

: $\vdash p \implies \paren {p \lor p}$

Proof:
{{BeginTableau|p \implies \paren {p \lor p} }}
{{Assumption|1|p}}
{{Addition|2|1|p \lor p|1|1}}
{{Implication|3||p \implies \paren {p \lor p}|1|2}}
{{EndTableau}}
{{qed}}
Category:Rule of Idempotence
9466a8vtv1pw8m79feaeim5qqcdowfs
Theorem: Rule of Idempotence/Disjunction/Formulation 2/Reverse Implication

: $\vdash \left({p \lor p}\right) \implies p$

Proof:
{{BeginTableau|\left({p \lor p}\right) \implies p}}
{{Premise|1|p \lor p}}
{{Assumption|2|p}}
{{ProofByCases|3|1|p|1|2|2|2|2}}
{{Implication|4||\left({p \lor p}\right) \implies p|1|3}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Addition/Sequent Form/Formulation 2/Form 1

:$\vdash p \implies \paren {p \lor q}$

Proof:
{{BeginTableau|p \implies \paren {p \lor q} }}
{{Premise|1|p}}
{{Addition|2|1|p \lor q|1|1}}
{{Implication|3||p \implies \paren {p \lor q}|1|3}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Addition/Sequent Form/Formulation 2/Form 1

:$\vdash p \implies \paren {p \lor q}$

Proof:
{{BeginTableau|p \implies \paren {p \lor q}|Instance 2 of the Hilbert-style systems}}
{{TableauLine
 | n = 1
 | f = q \implies \paren {p \lor q}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 2$
}}
{{TableauLine
 | n = 2
 | f = p \implies \paren {q \lor p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep  = 1
 | c    = $p \,/\, q, q \,/\, p$
}}
{{TableauLine
 | n = 3
 | f = \paren {p \lor q} \implies \paren {q \lor p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 3$
}}
{{TableauLine
 | n = 4
 | f = \paren {q \lor p} \implies \paren {p \lor q}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep  = 3
 | c    = $p \,/\, q, q \,/\, p$
}}
{{TableauLine
 | n = 5
 | f = p \implies \paren {p \lor q}
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 2, 4
}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Addition/Sequent Form/Formulation 2/Form 2

:$\vdash q \implies \left({p \lor q}\right)$

Proof:
{{BeginTableau|q \implies \paren {p \lor q} }}
{{Premise|1|q}}
{{Addition|2|1|p \lor q|1|2}}
{{Implication|3||q \implies \paren {p \lor q}|1|3}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Addition/Sequent Form/Formulation 2

{{begin-eqn}}
{{eqn | n = 1
      | l = \vdash p
      | o = \implies
      | r = \paren {p \lor q}
}}
{{eqn | n = 2
      | l = \vdash q
      | o = \implies
      | r = \paren {p \lor q}
}}
{{end-eqn}}

Proof:
{{BeginTableau|p \implies \paren {p \lor q} }}
{{Premise|1|p}}
{{Addition|2|1|p \lor q|1|1}}
{{Implication|3||p \implies \paren {p \lor q}|1|3}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Addition/Sequent Form/Formulation 2

{{begin-eqn}}
{{eqn | n = 1
      | l = \vdash p
      | o = \implies
      | r = \paren {p \lor q}
}}
{{eqn | n = 2
      | l = \vdash q
      | o = \implies
      | r = \paren {p \lor q}
}}
{{end-eqn}}

Proof:
{{BeginTableau|p \implies \paren {p \lor q}|Instance 2 of the Hilbert-style systems}}
{{TableauLine
 | n = 1
 | f = q \implies \paren {p \lor q}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 2$
}}
{{TableauLine
 | n = 2
 | f = p \implies \paren {q \lor p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep  = 1
 | c    = $p \,/\, q, q \,/\, p$
}}
{{TableauLine
 | n = 3
 | f = \paren {p \lor q} \implies \paren {q \lor p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 3$
}}
{{TableauLine
 | n = 4
 | f = \paren {q \lor p} \implies \paren {p \lor q}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep  = 3
 | c    = $p \,/\, q, q \,/\, p$
}}
{{TableauLine
 | n = 5
 | f = p \implies \paren {p \lor q}
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 2, 4
}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Addition/Sequent Form/Formulation 2

{{begin-eqn}}
{{eqn | n = 1
      | l = \vdash p
      | o = \implies
      | r = \paren {p \lor q}
}}
{{eqn | n = 2
      | l = \vdash q
      | o = \implies
      | r = \paren {p \lor q}
}}
{{end-eqn}}

Proof:
{{BeginTableau|q \implies \paren {p \lor q} }}
{{Premise|1|q}}
{{Addition|2|1|p \lor q|1|2}}
{{Implication|3||q \implies \paren {p \lor q}|1|3}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Addition/Sequent Form/Formulation 2

{{begin-eqn}}
{{eqn | n = 1
      | l = \vdash p
      | o = \implies
      | r = \paren {p \lor q}
}}
{{eqn | n = 2
      | l = \vdash q
      | o = \implies
      | r = \paren {p \lor q}
}}
{{end-eqn}}

Proof:
=== Form 1 ===
{{:Rule of Addition/Sequent Form/Formulation 2/Proof 1/Form 1}}
=== Form 2 ===
{{:Rule of Addition/Sequent Form/Formulation 2/Proof 1/Form 2}}
Theorem: Rule of Addition/Sequent Form/Formulation 2

{{begin-eqn}}
{{eqn | n = 1
      | l = \vdash p
      | o = \implies
      | r = \paren {p \lor q}
}}
{{eqn | n = 2
      | l = \vdash q
      | o = \implies
      | r = \paren {p \lor q}
}}
{{end-eqn}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives are $T$ for all boolean interpretations.
:<nowiki>$\begin{array}{|c|c|ccccc|ccccc|} \hline
p & q & p & \implies & (p & \lor & q) & q & \implies & (p & \lor & q) \\
\hline
\F & \F & \F & \T & \F & \F & \F & \F & \T & \F & \F & \F \\
\F & \T & \F & \T & \F & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Hilbert Proof System Instance 2 is Consistent

Instance 2 of the Hilbert proof systems $\mathscr H_2$ is consistent.

Proof:
Consider Instance 1 of a constructed semantics, denoted $\mathscr C_1$.
Note that $\neg p$ is not a tautology for $\mathscr C_1$.
We will establish that every $\mathscr H_2$-theorem is a $\mathscr C_1$-tautology.
That is, that $\mathscr H_2$ is sound for $\mathscr C_1$.
Starting with the axioms:
{{begin-axiom}}
{{axiom|n = A1
       |lc = Rule of Idempotence
       |m = (p \lor p) \implies p
       |rc = Proof of Tautology
}}
{{axiom|n = A2
       |lc = Rule of Addition
       |m = q \implies (p \lor q)
       |rc = Proof of Tautology
}}
{{axiom|n = A3
       |lc = Rule of Commutation
       |m = (p \lor q) \implies (q \lor p)
       |rc = Proof of Tautology
}}
{{axiom|n = A4
       |lc = Factor Principle
       |m = (q \implies r) \implies \left({ (p \lor q) \implies (p \lor r)}\right)
       |rc = Proof of Tautology
}}
{{end-axiom}}
Next it needs to be shown that the rules of inference of $\mathscr H_2$ preserve $\mathscr C_1$-tautologies.
Theorem: Set of Local Minimum is Countable

Let $X$ be a subset of $\R$.
The set:
:$\leftset {x \in X: x}$ is local minimum in $\rightset X$
is countable.

Proof:
Define:
:$Y := \leftset {x \in X: x}$ is local minimum in $\rightset X$
By definition of $Y$ and definition of local minimum in set:
:$\forall x \in Y: \exists y \in \R: y < x \land \openint y x \cap X = \O$
By the Axiom of Choice, define a mapping $f: Y \to \powerset \R$ as:
:$\forall x \in Y: \exists y \in \R: \map f x = \openint y x \land y < x \land \map f x \cap X = \O$
We will prove that $f$ is an injection by definition:
Let $x_1, x_2 \in Y$ such that
:$\map f {x_1} = \map f {x_2}$
By definition of $f$:
:$\exists y_1 \in \R: \map f {x_1} = \openint {y_1} {x_1} \land y_1 < x_1 \land \map f {x_1} \cap X = \O$
and:
:$\exists y_2 \in \R: \map f {x_2} = \openint {y_2} {x_2} \land y_2 < x_2 \land \map f {x_2} \cap X = \O$
Then:
:$\openint {y_1} {x_1} = \openint {y_2} {x_2}$
Thus $x_1 = x_2$.
This ends the proof of injection.
By Cardinality of Image of Injection:
:$(1): \quad \card Y = \card {\map {f^\to} Y} = \card {\Img f}$
where
:$\card Y$ denotes the cardinality of $Y$,
:$\map {f^\to} Y$ denotes the image of $Y$ under $f$,
:$\Img f$ denotes the image of $f$.
We will prove that $\Img f$ is pairwise disjoint by definition.
Let $A, B \in \Img f$ such that
:$A \ne B$.
Then by definition of image:
:$\exists x_1 \in Y: \map f {x_1} = A$
and
:$\exists x_2 \in Y: \map f {x_2} = B$.
By difference of $A$ and $B$:
:$x_1 \ne x_2$
By definition of $f$:
:$\exists y_1 \in \R: \map f {x_1} = \openint {y_1} {x_1} \land y_1 < x_1 \land \map f {x_1} \cap X = \O$
and:
:$\exists y_2 \in \R: \map f {x_2} = \openint {y_2} {x_2} \land y_2 < x_2 \land \map f {x_2} \cap X = \O$
Aiming at contradiction suppose that
:$A \cap B \ne \O$.
$x_1 < x_2$ or $x_1 > x_2$.
In case when $x_1 < x_2$, $x_1 \in \map f {x_2}$ what contradicts with $\map f {x_2} \cap X = \O$.
In case when $x_1 > x_2$, analogically.
This ends the proof that $\Img f$ is pairwise disjoint.
By Set of Pairwise Disjoint Intervals is Countable:
:$\Img f$ is countable.
Thus by $(1)$ and Set is Countable if Cardinality equals Cardinality of Countable Set the result:
:$Y$ is countable.
{{qed}}
Theorem: Set of Pairwise Disjoint Intervals is Countable

Let $X$ be a subset of $\powerset \R$ such that:
:$(1): \quad X$ is pairwise disjoint:
::::$\forall A, B \in X: A \ne B \implies A \cap B = \O$.
:$(2): \quad$ every element of $X$ contains an open interval:
::::$\forall A \in X: \exists x, y \in \R: x < y \land \openint x y \subseteq A$.
Then $X$ is countable.

Proof:
By Between two Real Numbers exists Rational Number:
:$\forall A \in X: \exists x, y \in \R, q \in \Q: x < y \land q \in \openint x y \subseteq A$
By the Axiom of Choice define a mapping $f: X \to \Q$:
:$\forall A \in X: \map f A \in A$
First it needs to be shown that $f$ is an injection by definition.
Let $A, B \in X$ such that:
:$\map f A = \map f B$
By definition of $f$:
:$\map f A \in A$ and $\map f B \in B$
By definition of intersection:
:$\map f A \in A \cap B$
Then by definition of empty set:
:$A \cap B \ne \O$
Thus by definition of pairwise disjoint:
:$A = B$
Hence $f$ is an injection.
By Set is Subset of Itself, $X$ is a subset of $X$.
Thus by Cardinality of Image of Injection:
:$\card X = \card {f^\to \sqbrk X}$
By definition of image:
:$f^\to \sqbrk X \subseteq \Q$
By Rational Numbers are Countably Infinite:
:$\Q$ is countable.
Hence by Subset of Countable Set is Countable:
:$f^\to \sqbrk X$ is countable.
Thus by Set is Countable if Cardinality equals Cardinality of Countable Set the result:
:$X$ is countable.
{{qed}}
Theorem: Set is Countable if Cardinality equals Cardinality of Countable Set

Let $X, Y$ be sets.
Let:
:$\card X = \card Y$
where $\card X$ denotes the cardinality of $X$.
If $X$ is countable then $Y$ is countable.

Proof:
Assume that $X$ is countable.
By definition of countable set there exists an injection:L
:$f: X \to \N$
By definition of cardinality the sets $Y$ and $X$ are equivalent:
:$Y \sim X$
Then by definition of set equivalence there exists a bijection:
:$g: Y \to X$
By definition of bijection:
:$g$ is an injection.
Hence by Composite of Injections is Injection:
:$f \circ g: Y \to \N$ is an injection.
Thus by definition:
:$Y$ is countable.
{{qed}}
Category:Countable Sets
0n5frtcd7pgu3rhpse9dctnmsr3lk2i
Theorem: Double Negation/Double Negation Introduction/Sequent Form

{{:Double Negation/Double Negation Introduction/Sequent Form/Formulation 1}}

Proof:
{{BeginTableau|p \vdash \neg \neg p}}
{{Premise|1|p}}
{{Assumption|2|\neg p}}
{{NonContradiction|3|1, 2|1|2}}
{{Contradiction|4|1|\neg \neg p|2|3}}
{{EndTableau|qed}}
Theorem: Principle of Non-Contradiction/Sequent Form

{{:Principle of Non-Contradiction/Sequent Form/Formulation 1}}

Proof:
{{BeginTableau|p, \neg p \vdash \bot}}
{{Premise|1|p}}
{{Premise|2|\neg p}}
{{NonContradiction|3|1, 2|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Principle of Non-Contradiction/Sequent Form

{{:Principle of Non-Contradiction/Sequent Form/Formulation 1}}

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin {array} {|cccc||c|} \hline
p & \land & \neg & p & \bot \\
\hline
\F & \F & \T & \F & \F \\
\T & \F & \F & \T & \F \\
\hline
\end {array}$</nowiki>
As can be seen by inspection, the truth value of the main connective, that is $\land$, is $F$ for each boolean interpretation for $p$.
{{qed}}
Theorem: Principle of Non-Contradiction/Sequent Form

{{:Principle of Non-Contradiction/Sequent Form/Formulation 1}}

Proof:
{{BeginTableau|\vdash \neg \left({p \land \neg p}\right)}}
{{Assumption|1|p \land \neg p}}
{{Simplification|2|1|p|1|1}}
{{Simplification|3|1|\neg p|1|2}}
{{NonContradiction|4|1|2|3}}
{{Contradiction|5||\neg \left({p \land \neg p}\right)|1|4}}
{{EndTableau|qed}}
Theorem: Principle of Non-Contradiction/Sequent Form

{{:Principle of Non-Contradiction/Sequent Form/Formulation 1}}

Proof:
We apply the Method of Truth Tables to the proposition $\neg \paren {p \land \neg p}$.
As can be seen by inspection, the truth value of the main connective, that is $\neg$, is $T$ for each boolean interpretation for $p$.
:<nowiki>$\begin {array} {|ccccc|} \hline
\neg & (p & \land & \neg & p)\\
\hline
\T & \F & \F & \T & \F \\
\T & \T & \F & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}