avewright/proofwiki-math huggingface dataset:
Theorem: Form of Geometric Sequence of Integers

Let $P = \sequence {a_j}_{0 \mathop \le j \mathop \le n}$ be a geometric sequence of length $n + 1$ consisting of integers only.
Then the $j$th term of $P$ is given by:
:$a_j = k p^{n - j} q^j$
where:
: the common ratio of $P$ expressed in canonical form is $\dfrac q p$
: $k$ is an integer.

Proof:
Let $r$ be the common ratio of $P$.
From Common Ratio in Integer Geometric Sequence is Rational, $r$ is a rational number.
Let $r = \dfrac q p$ be in canonical form.
Thus, by definition:
:$p \perp q$
Let $a$ be the first term of $P$.
Then the sequence $P$ is:
:$P = \paren {a, a \dfrac q p, a \dfrac {q^2} {p^2}, \ldots, a \dfrac {q^n} {p^n} }$
All the elements of $P$ are integers, so, in particular:
:$a \dfrac {q^n} {p^n} \in \Z$
We have that: 
:$p \perp q$
From Powers of Coprime Numbers are Coprime:
:$q^n \perp p^n$
and so from Euclid's Lemma:
:$p^n \divides a$
Thus:
:$a = k p^n$
for some $k \in \Z$, and so:
:$P = \paren {k p^n, k q p^{n - 1}, k q^2 p^{n - 2}, \ldots, k q^{n - 1} p, k q^n}$
{{qed}}
Category:Geometric Sequences of Integers
bhfwiu2z97dxzp20i8vusbgjraa7agi
Theorem: Geometric Sequence of Integers with Integer Common Ratio

Let $P = \sequence {a_j}_{1 \mathop \le j \mathop \le n}$ be a geometric sequence of length $n$ consisting entirely of integers.
Let $r$ be the common ratio of $P$.
Then $r$ is an integer {{iff}}:
:$\forall i, j \in \set {1, 2, \ldots, n}, i \le j: a_i \divides a_j$
That is, terms of $P$ divide later terms of $P$ {{iff}} $r$ is an integer.

Proof:
=== Necessary Condition ===
Let $r$ be an integer.
By definition of geometric sequence, the terms of $P$ are in the form:
:$a_k = b r^{k - 1}$
where $b$ and $k$ are integers.
It follows from Integer Multiplication is Closed that $a_k$ is an integer.
{{qed|lemma}}
Theorem: Integers are Coprime iff Powers are Coprime

Let $a, b \in \Z$ be integers.
Then:
:$a \perp b \iff \forall n \in \N: a^n \perp b^n$
That is, two integers are coprime {{iff}} all their positive integer powers are coprime.

Proof:
The forward implication is shown in Powers of Coprime Numbers are Coprime.
The reverse implication is shown by substituting $n = 1$.
{{qed}}
Category:Coprime Integers
8k2ky39jzctjiltp3egexjushvinn3s
Theorem: Successor Mapping of Peano Structure has no Fixed Point

Let $\PP = \struct {P, s, 0}$ be a Peano structure.
Then:
:$\forall n \in P: \map s n \ne n$
That is, the successor mapping has no fixed points.

Proof:
Let $T$ be the set:
:$T = \set {n \in P: \map s n \ne n}$
We will use {{PeanoAxiom|5}} to prove that $T = P$.
Theorem: Integer Addition is Cancellable

The operation of addition on the set of integers $\Z$ is cancellable:
:$\forall x, y, z \in \Z: x + z = y + z \implies x = y$

Proof:
Let $x = \eqclass {a, b} {}$, $y = \eqclass {c, d} {}$ and $z = \eqclass {e, f} {}$ for some $x, y, z\in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = x + z
      | r = y + z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a, b} {} + \eqclass {e, f} {}
      | r = \eqclass {c, d} {} + \eqclass {e, f} {}
      | c =
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a + e, b + f} {}
      | r = \eqclass {c + e, d + f} {}
      | c = {{Defof|Integer Addition}}
}}
{{eqn | ll= \leadsto
      | l = a + e
      | r = c + e
      | c = {{Defof|Integer}}
}}
{{eqn | lo= \land
      | l = b + f
      | r = d + f
      | c = {{Defof|Integer}}
}}
{{eqn | ll= \leadsto
      | l = a
      | r = c
      | c = Natural Number Addition is Cancellable
}}
{{eqn | lo= \land
      | l = b
      | r = d
      | c = Natural Number Addition is Cancellable
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a, b} {}
      | r = \eqclass {c, d} {}
      | c = {{Defof|Integer}}
}}
{{end-eqn}}
{{qed}}
Theorem: Open Real Interval is Subset of Closed Real Interval

Let $a, b \in \R$ be real numbers.
Then:
:$\openint a b \subseteq \closedint a b$
where:
:$\openint a b$ is the open interval between $a$ and $b$
:$\closedint a b$ is the closed interval between $a$ and $b$.

Proof:
Let $x \in \openint a b$.
Then by definition of open interval:
:$a < x < b$
Thus:
:$a \le x \le b$
and so by definition of closed interval:
:$x \in \closedint a b$
{{qed}}
Theorem: Complement Relative to Subset is Subset of Complement Relative to Superset

Let $A, B, C$ be sets such that $A \subseteq B \subseteq C$.
Then:
:$\relcomp B A \subseteq \relcomp C A$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \relcomp B A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = B
      | c = {{Defof|Relative Complement}}
}}
{{eqn | lo= \land
      | l = x
      | o = \notin
      | r = A
      | c = {{Defof|Relative Complement}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = C
      | c = {{Defof|Subset}}: $B \subseteq C$
}}
{{eqn | lo= \land
      | l = x
      | o = \notin
      | r = A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \relcomp C A
      | c = {{Defof|Relative Complement}}
}}
{{eqn | ll= \leadsto
      | l = \relcomp B A
      | o = \subseteq
      | r = \relcomp C A
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complement of Relative Complement is Union with Complement

Let $A, B, C$ be sets such that $A \subseteq B \subseteq C$.
Then:
:$\relcomp C {\relcomp B A} = A \cup \relcomp C B$

Proof:
{{begin-eqn}}
{{eqn | l = \relcomp C {\relcomp B A}
      | r = C \setminus \paren {B \setminus A}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = \paren {C \setminus B} \cup \paren {C \cap A}
      | c = Set Difference with Set Difference is Union of Set Difference with Intersection
}}
{{eqn | r = \paren {C \setminus B} \cup A
      | c = Intersection with Subset is Subset
}}
{{eqn | r = A \cup \paren {C \setminus B}
      | c = Union is Commutative
}}
{{eqn | r = A \cup \relcomp C B
      | c = {{Defof|Relative Complement}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set Union Preserves Subsets/Families of Sets

Let $I$ be an indexing set.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ and $\family {B_\alpha}_{\alpha \mathop \in I}$ be indexed families of subsets of a set $S$.
Let:
:$\forall \beta \in I: A_\beta \subseteq B_\beta$
Then:
:$\ds \bigcup_{\alpha \mathop \in I} A_\alpha \subseteq \bigcup_{\alpha \mathop \in I} B_\alpha$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} A_\alpha
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadsto
      | q = \exists \alpha \in I
      | l = x
      | o = \in
      | r = B_\alpha
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} B_\alpha
      | c = {{Defof|Union of Family}}
}}
{{end-eqn}}
By definition of subset:
:$\ds \bigcup_{\alpha \mathop \in I} A_\alpha \subseteq \bigcup_{\alpha \mathop \in I} B_\alpha$
{{qed}}
Theorem: Set Union Preserves Subsets/General Result

Let $\mathbb S, \mathbb T$ be sets of sets.
Suppose that for each $S \in \mathbb S$ there exists a $T \in \mathbb T$ such that $S \subseteq T$.
Then $\bigcup \mathbb S \subseteq \bigcup \mathbb T$.

Proof:
Let $x \in \bigcup \mathbb S$.
By the definition of union, there exists an $S \in \mathbb S$ such that $x \in S$.
By the premise, there exists a $T \in \mathbb T$ such that $S \subseteq T$.
By the definition of Subset:
:$x \in T$
Thus by the definition of union:
:$x \in \bigcup \mathbb T$
{{qed}}
Category:Set Union Preserves Subsets
p76bex02v5vodwdiwzu81ezytmoz9dx
Theorem: Intersection of Family is Subset of Intersection of Subset of Family

Let $I$ be an indexing set.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ be an indexed family of subsets of a set $S$.
Let $J \subseteq I$.
Then:
:$\ds \bigcap_{\alpha \mathop \in I} A_\alpha \subseteq \bigcap_{\alpha \mathop \in J} A_\alpha$
where $\ds \bigcap_{\alpha \mathop \in I} A_\alpha$ denotes the intersection of $\family {A_\alpha}_{\alpha \mathop \in I}$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcap_{\alpha \mathop \in I} A_\alpha
      | c =
}}
{{eqn | ll= \leadsto
      | q = \forall \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha
      | c = Intersection is Subset
}}
{{eqn | ll= \leadsto
      | q = \forall \alpha \in J
      | l = x
      | o = \in
      | r = A_\alpha
      | c = {{Defof|Subset}}: $J \subseteq I$
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcap_{\alpha \mathop \in J} A_\alpha
      | c = {{Defof|Intersection of Family}}
}}
{{end-eqn}}
{{qed}}
Theorem: Union of Subset of Family is Subset of Union of Family

Let $I$ be an indexing set.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ be an indexed family of subsets of a set $S$.
Let $J \subseteq I$
Then:
:$\ds \bigcup_{\alpha \mathop \in J} A_\alpha \subseteq \bigcup_{\alpha \mathop \in I} A_\alpha$
where $\ds \bigcup_{\alpha \mathop \in I} A_\alpha$ denotes the union of $\family {A_\alpha}_{\alpha \mathop \in I}$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in J} A_\alpha
      | c =
}}
{{eqn | ll= \leadsto
      | q = \exists \alpha \in J
      | l = x
      | o = \in
      | r = A_\alpha
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadsto
      | q = \exists \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha
      | c = {{Defof|Subset}}: $J \subseteq I$
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} A_\alpha
      | c = Set is Subset of Union of Family
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection of Open Intervals of Positive Reals is Empty

Let $\R_{>0}$ be the set of strictly positive real numbers.
For all $x \in \R_{>0}$, let $A_x$ be the open real interval $\openint 0 x$.
Then:
:$\ds \bigcap_{x \mathop \in \R_{>0} } A_x = \O$

Proof:
Let $\ds A = \bigcap_{x \mathop \in \R_{>0} } A_x$.
{{AimForCont}} $A \ne \O$.
Then:
:$\exists y \in \R_{>0}: y \in A$
By definition of open interval:
:$y \notin \openint 0 y = A_y$
and so by definition of intersection of family:
:$y \notin A$
From this contradiction it follows that $A$ has no elements.
That is:
:$\ds \bigcap_{x \mathop \in \R_{>0} } A_x = \O$
{{qed}}
Theorem: Union of Open Intervals of Positive Reals is Set of Strictly Positive Reals

Let $\R_{>0}$ be the set of strictly positive real numbers.
For all $x \in \R_{>0}$, let $A_x$ be the open real interval $\openint 0 x$.
Then:
:$\ds \bigcup_{x \mathop \in \R_{>0} } A_x = \R_{>0}$

Proof:
Let $\ds A = \bigcup_{x \mathop \in \R_{>0} } A_x$.
Let $y \in A$.
Then by definition of union of family:
:$\exists x \in \R_{>0}: y \in A_x$
As $A_x \subseteq \R_{>0}$ it follows by definition of subset that:
:$y \in \R_{>0}$
So:
:$\ds \bigcup_{x \mathop \in \R_{>0} } A_x \subseteq \R_{>0}$
{{qed|lemma}}
Let $y \in \R_{>0}$.
By the Axiom of Archimedes: 
:$\exists z \in \N: z > y$
and so:
:$y \in A_z$
That is by definition of union of family:
:$y \in \ds \bigcup_{x \mathop \in \R_{>0} } A_x$
So by definition of subset:
:$\ds \R_{>0} \subseteq \bigcup_{x \mathop \in \R_{>0} } A_x$
{{qed|lemma}}
By definition of set equality:
:$\ds \bigcup_{x \mathop \in \R_{>0} } A_x = \R_{>0}$
{{qed}}
Theorem: Intersection of Closed Intervals of Positive Reals is Zero

Let $\R_{> 0}$ be the set of strictly positive real numbers.
For all $x \in \R_{> 0}$, let $B_x$ be the closed real interval $\closedint 0 x$.
Then:
:$\ds \bigcap_{x \mathop \in \R_{> 0} } B_x = \set 0$

Proof:
Let $\ds B = \bigcap_{x \mathop \in \R_{> 0} } B_x$.
We have that:
:$\forall x \in \R_{> 0}: 0 \in \closedint 0 x$
So by definition of intersection:
:$0 \in B$
and so by Singleton of Element is Subset:
:$\ds \set 0 \subseteq \bigcap_{x \mathop \in \R_{> 0} } B_x$
{{AimForCont}} $\exists y \in \R_{> 0}: y \in B$.
By definition of $B_x$:
:$y \notin \closedint 0 {\dfrac y 2} = B_{y/2}$
and so by definition of intersection of family:
:$y \notin B$
From this contradiction it follows that there can be no elements in $B$ apart from $0$.
That is:
:$\ds \bigcap_{x \mathop \in \R_{> 0} } A_x \subseteq \set 0$
By definition of set equality:
:$\ds \bigcap_{x \mathop \in \R_{> 0} } B_x = \set 0$
{{qed}}
Theorem: Union of Closed Intervals of Positive Reals is Set of Positive Reals

Let $\R_{>0}$ be the set of strictly positive real numbers.
For all $x \in \R_{> 0}$, let $B_x$ be the closed real interval $\closedint 0 x$.
Then:
:$\ds \bigcup_{x \mathop \in \R_{>0} } B_x = \R_{\ge 0}$

Proof:
Let $\ds B = \bigcap_{x \mathop \in \R_{>0} } B_x$.
Let $y \in B$.
Then by definition of union of family:
:$\exists x \in \R_{>0}: y \in B_x$
As $B_x \subseteq \R_{>0}$ it follows by definition of subset that:
:$y = 0$
or
:$y \in \R_{>0}$
In either case, $y \in \R_{\ge 0}$
So:
:$\ds \bigcap_{x \mathop \in \R_{>0} } B_x \subseteq \R_{\ge 0}$
{{qed|lemma}}
Let $y \in \R_{\ge 0}$.
If $y = 0$ then $y \in \R_{\ge 0}$ by definition.
Otherwise, by the Axiom of Archimedes: 
:$\exists z \in \N: z > y$
and so:
:$y \in B_z$
That is by definition of union of family:
:$\ds y \in \bigcap_{x \mathop \in \R_{\ge 0} } B_x$
So by definition of subset:
:$\ds \R_{\ge 0} \subseteq \bigcap_{x \mathop \in \R_{>0} } B_x$
{{qed|lemma}}
By definition of set equality:
:$\ds \bigcup_{x \mathop \in \R_{>0} } B_x = \R_{\ge 0}$
{{qed}}
Theorem: Relative Complement of Cartesian Product

Let $A$ and $B$ be sets.
Let $X \subseteq A$ and $Y \subseteq B$.
Then:
:$\relcomp {A \mathop \times B} {X \times Y} = \paren {A \times \relcomp B Y} \cup \paren {\relcomp A X \times B}$

Proof:
From Set with Relative Complement forms Partition:
:$A = \set {X \mid \relcomp A X}$
:$B = \set {Y \mid \relcomp B Y}$
and so by definition of partition:
:$A = X \cup \relcomp A X$
:$B = Y \cup \relcomp B Y$
By Cartesian Product of Unions:
:$A \times B = \paren {X \times Y} \cup \paren {\relcomp A X \times \relcomp B Y} \cup \paren {X \times \relcomp B Y} \cup \paren {\relcomp A X \times Y}$
and so:
{{begin-eqn}}
{{eqn | l = \paren {A \times B} \setminus \paren {X \times Y}
      | r = \paren {\relcomp A X \times \relcomp B Y} \cup \paren {X \times \relcomp B Y} \cup \paren {\relcomp A X \times Y}
      | c = 
}}
{{eqn | r = \paren {X \times \relcomp B Y} \cup \paren {\relcomp A X \times \relcomp B Y} \cup \paren {\relcomp A X \times Y} \cup \paren {\relcomp A X \times \relcomp B Y}
      | c = 
}}
{{eqn | r = \paren {\paren {X \cup \relcomp A X} \times \relcomp B Y} \cup \paren {\relcomp A X \times \paren {Y \cup \relcomp B Y} }
      | c = 
}}
{{eqn | r = \paren {A \times \relcomp B Y} \cup \paren {\relcomp A X \times B}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Relative Complement of Cartesian Product

Let $A$ and $B$ be sets.
Let $X \subseteq A$ and $Y \subseteq B$.
Then:
:$\relcomp {A \mathop \times B} {X \times Y} = \paren {A \times \relcomp B Y} \cup \paren {\relcomp A X \times B}$

Proof:
{{begin-eqn}}
{{eqn | o =
      | r = \relcomp {A \mathop \times B} {X \times Y}
}}
{{eqn | ll= \leadstoandfrom
      | o =
      | r = A \times B \setminus X \times Y
      | c = {{Defof|Relative Complement}}
}}
{{eqn | ll= \leadstoandfrom
      | o =
      | r = \set {\tuple {x, y}: x \in A \land y \in B \land \neg \paren {x \in X \land y \in Y} }
      | c =  {{Defof|Cartesian Product}}
}}
{{eqn | ll= \leadstoandfrom
      | o =
      | r = \set {\tuple {x, y}: x \in A \land y \in B \land \paren {x \notin X \lor y \notin Y} }
      | c = De Morgan's Laws: Disjunction of Negations
}}
{{eqn | ll= \leadstoandfrom
      | o =
      | r = \paren {A \times \relcomp B Y} \cup \paren {\relcomp A X \times B}
      | c = {{Defof|Cartesian Product}}
}}
{{end-eqn}}
and so by definition of set equality:
:$\relcomp {A \mathop \times B} {X \times Y} = \paren {A \times \relcomp B Y} \cup \paren {\relcomp A X \times B}$
{{qed}}
Theorem: Subset of Cartesian Product not necessarily Cartesian Product of Subsets

Let $A$ and $B$ be sets.
Let $A$ and $B$ both have at least two distinct elements.
Then there exists $W \subseteq A \times B$ such that $W$ is not the cartesian product of a subset of $A$ and a subset of $B$.

Proof:
Let $a \in A, b \in A, c \in B, d \in B$ be arbitrary elements of $A$ and $B$.
Let:
:$W = \set {\tuple {a, c}, \tuple {a, d}, \tuple {b, d} }$
Then $W \subseteq A \times B$.
Suppose $W = X \times Y$ such that $X \subseteq A, Y \subseteq B$.
Then $a, b \in X$ and $c, d \in Y$.
But $X \times Y$ also contains $\tuple {b, c}$ which is not in $W$.
Hence the result.
{{qed}}
Theorem: Subset equals Preimage of Image implies Injection

Let $f: S \to T$ be a mapping.
Let $f^\to: \powerset S \to \powerset T$ be the direct image mapping of $f$.
Similarly, let $f^\gets: \powerset T \to \powerset S$ be the inverse image mapping of $f$.
Let:
:$\forall A \in \powerset S: A = \map {\paren {f^\gets \circ f^\to} } A$
Then $f$ is an injection.

Proof:
Let $f$ be such that:
:$\forall A \in \powerset S: A = \map {\paren {f^\gets \circ f^\to} } A$
In particular, it holds for all subsets of $A$ which are singletons.
Now, consider any $x, y \in A$.
We have:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \map f y
      | c =
}}
{{eqn | ll= \leadsto
      | l = \set {\map f x}
      | r = \set {\map f y}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {f^\to} {\set x}
      | r = \map {f^\to} {\set y}
      | c = {{Defof|Direct Image Mapping of Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \set x
      | r = \map {f^\gets} {\map {f^\to} {\set x} }
      | c = by hypothesis: $A = \map {\paren {f^\gets \circ f^\to} } A$
}}
{{eqn | r = \map {f^\gets} {\map {f^\to} {\set y} }
      | c = 
}}
{{eqn | r = \set y
      | c = by hypothesis: $A = \map {\paren {f^\gets \circ f^\to} } A$
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = 
}}
{{end-eqn}}
So $f$ is an injection.
{{qed}}
Theorem: Subset equals Preimage of Image implies Injection

Let $f: S \to T$ be a mapping.
Let $f^\to: \powerset S \to \powerset T$ be the direct image mapping of $f$.
Similarly, let $f^\gets: \powerset T \to \powerset S$ be the inverse image mapping of $f$.
Let:
:$\forall A \in \powerset S: A = \map {\paren {f^\gets \circ f^\to} } A$
Then $f$ is an injection.

Proof:
Suppose that $f$ is not an injection.
Then two elements of $S$ map to the same one element of $T$.
That is:
:$\exists a_1, a_2 \in S, b \in T: \map f {a_1} = \map f {a_2} = b$
Let $A = \set {a_1}$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f^\to} A
      | r = \set b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {f^\gets} {\map {f^\to} A}
      | o = \supseteq
      | r = \set {a_1, a_2}
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \map {f^\gets} {\map {f^\to} A}
      | o = \supsetneqq
      | r = A
      | c = as $A = \set {a_1}$
}}
{{end-eqn}}
So by the Rule of Transposition:
:$\forall A \in \powerset S: A = \map {\paren {f^\gets \circ f^\to} } A$
implies that $f$ is an injection.
{{qed}}
Theorem: Preimage of Image of Subset under Injection equals Subset

Let $f: S \to T$ be an injection.
Then:
:$\forall A \subseteq S: A = \paren {f^{-1} \circ f} \sqbrk A$
where:
:$f \sqbrk A$ denotes the image of $A$ under $f$
:$f^{-1}$ denotes the inverse of $f$
:$f^{-1} \circ f$ denotes composition of $f^{-1}$ and $f$.

Proof:
Let $f$ be an injection.
From Subset of Domain is Subset of Preimage of Image, we have that:
:$\forall A \subseteq S: A \subseteq \paren {f^{-1} \circ f} \sqbrk A$
by dint of $f$ being a relation.
So what we need to do is show that:
:$\forall A \subseteq S: \paren {f^{-1} \circ f} \sqbrk A \subseteq A$
Take any $A \subseteq S$.
Let $x \in A$.
We have:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \paren {f^{-1} \circ f} \sqbrk A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = f^{-1} \sqbrk {f \sqbrk A}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | ll= \leadsto
      | l = \map f x
      | o = \in
      | r = f \sqbrk A
      | c = {{Defof|Inverse of Mapping}}
}}
{{eqn | ll= \leadsto
      | q = \exists y \in A
      | l = \map f x
      | r = \map f y
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = {{Defof|Injection}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A
      | c = as $y \in A$
}}
{{end-eqn}}
Thus we see that:
:$\paren {f^{-1} \circ f} \sqbrk A \subseteq A$
and hence the result:
:$\forall A \subseteq S: A = \paren {f^{-1} \circ f} \sqbrk A$
{{qed}}
Theorem: Subset equals Image of Preimage implies Surjection

Let $f: S \to T$ be a mapping.
Let:
:$\forall B \subseteq T: B = \paren {f \circ f^{-1} } \sqbrk B$
where $f \sqbrk B$ denotes the image of $B$ under $f$.
Then $f$ is a surjection.

Proof:
Let $f$ be such that:
:$\forall B \subseteq T: B = \paren {f \circ f^{-1} } \sqbrk B$
In particular, it holds for $T$ itself.
Hence:
{{begin-eqn}}
{{eqn | l = T
      | r = \paren {f \circ f^{-1} } \sqbrk T
      | c = 
}}
{{eqn | l = T
      | r = f \sqbrk {f^{-1} \sqbrk T}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | o = \subseteq
      | r = f \sqbrk S
      | c = Image of Subset under Mapping is Subset of Image
}}
{{eqn | r = \Img f
      | c = {{Defof|Image of Mapping}}
}}
{{eqn | o = \subseteq
      | r = T
      | c = {{Corollary|Image is Subset of Codomain|1}}
}}
{{end-eqn}}
So:
:$T \subseteq \Img f \subseteq T$
and so by definition of set equality:
:$\Img f = T$
So, by definition, $f$ is a surjection.
{{qed}}
Theorem: Subset equals Image of Preimage implies Surjection

Let $f: S \to T$ be a mapping.
Let:
:$\forall B \subseteq T: B = \paren {f \circ f^{-1} } \sqbrk B$
where $f \sqbrk B$ denotes the image of $B$ under $f$.
Then $f$ is a surjection.

Proof:
Suppose $f$ is not a surjection.
$T$ must have at least two elements for this to be the case.
Let one of these two elements not be the image of any element of $S$.
That is, let $b_1, b_2 \in T$ such that:
:$\exists a \in S: f \paren a = b_1$
:$\nexists x \in S: f \paren x = b_2$
Let $B = \set {b_1, b_2}$.
Then:
{{begin-eqn}}
{{eqn | l = f^{-1} \sqbrk B
      | r = A
      | c = for some $A \subseteq S$
}}
{{eqn | ll= \leadsto
      | l = f \sqbrk {f^{-1} \sqbrk B}
      | r = \set {b_1}
      | c = as $b_2$ has no preimage
}}
{{eqn | ll= \leadsto
      | l = f \sqbrk {f^{-1} \sqbrk B}
      | o = \ne
      | r = B
      | c = as $B = \set {b_1, b_2}$
}}
{{end-eqn}}
So by the Rule of Transposition:
:$\forall B \subseteq S: B = \paren {f \circ f^{-1} } \sqbrk B$
implies that $f$ is an surjection.
{{qed}}
Theorem: Image of Preimage of Subset under Surjection equals Subset

Let $f: S \to T$ be a surjection.
Then:
:$\forall B \subseteq T: B = \paren {f \circ f^{-1} } \sqbrk B$
where:
:$f \sqbrk B$ denotes the image of $B$ under $f$
:$f^{-1}$ denotes the inverse of $f$
:$f \circ f^{-1}$ denotes composition of $f$ and $f^{-1}$.

Proof:
Let $g$ be a surjection.
Let $B \subseteq T$.
Let $b \in B$.
Then:
{{begin-eqn}}
{{eqn | q = \exists a \in S
      | l = b
      | r = \map f a
      | c = {{Defof|Surjection}}
}}
{{eqn | ll= \leadsto
      | l = a 
      | o = \in
      | r = f^{-1} \sqbrk B
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{eqn | ll= \leadsto
      | l = b
      | o = \in
      | r = f \sqbrk {f^{-1} \sqbrk B}
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | ll= \leadsto
      | l = B
      | o = \subseteq
      | r = f \sqbrk {f^{-1} \sqbrk B}
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = B
      | o = \subseteq
      | r = \paren {f \circ f^{-1} } \sqbrk B
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
From Subset of Codomain is Superset of Image of Preimage, we already have that:
:$\paren {f \circ f^{-1} } \sqbrk B \subseteq B$
So:
:$B \subseteq \paren {f \circ f^{-1} } \sqbrk B \subseteq B$
and by definition of set equality:
:$B = \paren {f \circ f^{-1} } \sqbrk B$
{{qed}}