avewright/proofwiki-math huggingface dataset:
Theorem: Convergence in Sigma-Finite Measure

Let $\struct {X, \Sigma, \mu}$ be a $\sigma$-finite measure space.
Let $\sequence {f_n}_{n \mathop \in \N}: f_n: X \to \R$ be a sequence of measurable functions.
Also, let $f, g: X \to \R$ be measurable functions.
Suppose that $f_n$ converges in measure to both $f$ and $g$ (in $\mu$).
Then $f$ and $g$ are equal $\mu$-almost everywhere.

Proof:
As $\mu$ is $\sigma$-finite, there is an exhausting sequence $\sequence {E_m}_m$ in $\Sigma$ such that:
:$\forall m : \map \mu {E_m} < \infty$
By triangle inequality:
:$\forall x \in X :\quad \cmod {\map f x - \map g x} \le  \cmod {\map f x - \map {f_n} x}  +  \cmod {\map {f_n} x - \map g x}$
For all $m, k \in \N_{>0}$, since:
:$\ds \forall n \in \N :\quad \set {\cmod {f - g} > \frac 1 k } \subseteq \set {\cmod {f - f_n} > \frac 1 {2 k} } \cup \set {\cmod {f_n - g} > \frac 1 {2 k} }$
we have:
{{begin-eqn}}
{{eqn | l = \map \mu {\set {\cmod {f - g} > \frac 1 k} \cap E_m }
      | o = \le
      | r = \map \mu {\paren {\set {\cmod {f - f_n} > \frac 1 {2 k} } \cup \set {\cmod {f_n - g} > \frac 1 {2 k} } } \cap E_m }
}}
{{eqn | r = \map \mu { \paren {\set {\cmod {f - f_n} > \frac 1 {2 k} } \cap E_m } \cup \paren {\set {\cmod {f_n - g} > \frac 1 {2 k} } \cap E_m } }
      | c = Intersection Distributes over Union
}}
{{eqn | o = \le
      | r = \map \mu {\set {\cmod {f - f_n} > \frac 1 {2 k} } \cap E_m } + \map \mu {\set {\cmod {f_n - g} > \frac 1 {2 k} } \cap E_m }
      | c = Measure is Subadditive
}}
{{eqn | o = \to
      | r = 0
      | c = as $n \to \infty$ {{hypothesis}}
}}
{{end-eqn}}
Thus:
:$\ds \forall m, k \in \N_{>0} : \map \mu {\set {\cmod {f - g} > \frac 1 k} \cap E_m} = 0$
By Monotone Convergence Theorem:
:$\ds \forall k \in \N_{>0} : \map \mu {\set {\cmod {f - g} > \frac 1 k} } = \lim_{m \mathop \to \infty} \map \mu {\set {\cmod {f - g} > \frac 1 k} \cap E_m} = 0$
Now, observe:
:$\ds \set {\cmod {f - g} > 0} = \bigcup_{k \mathop = 1}^\infty \set {\cmod {f - g} > \frac 1 k}$
Therefore:
{{begin-eqn}}
{{eqn | l = \map \mu {\set {\cmod {f - g} > 0} }
      | r = \map \mu {\bigcup_{k\mathop = 1}^\infty \set {\cmod {f - g} > \frac 1 k} }
}}
{{eqn | o = \le
      | r = \sum_{k\mathop = 1}^\infty \map \mu {\set {\cmod {f - g} > \frac 1 k} }
      | c = Measure is Subadditive
}}
{{eqn | r = 0}}
{{end-eqn}}
{{qed}}
Theorem: Vitali's Theorem

Let $\struct {X, \Sigma, \mu}$ be a $\sigma$-finite measure space, and let $p \in \R, p \ge 1$.
Let $\sequence {f_n}_{n \mathop \in \N}: f_n: X \to \R$ be a sequence of $p$-integrable functions.
Also, let $f: X \to \R$ be a measurable function.
Suppose that $\ds \operatorname*{\mu-\!\lim\,} \limits_{n \mathop \to \infty} f_n = f$, that is $f_n$ converges in measure to $f$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\ds \lim_{n \mathop \to \infty} \norm {f_n - f}_p {{=}} 0$, where $\norm {\,\cdot\,}_p$ is the $p$-seminorm (that is $\ds \operatorname*{\LL^{\textit p}-\!\lim\,} \limits_{n \mathop \to \infty} f_n {{=}} f$)}}
{{item|(2):|$\sequence {\size {f_n}^p}_{n \mathop \in \N}$ is a uniformly integrable collection}}
{{item|(3):|$\lim_{n \mathop \to \infty} \int \size {f_n}^p \rd \mu {{=}} \int \size f^p \rd \mu$}}
{{end-itemize}}
If $\struct {X, \Sigma, \mu}$ is not $\sigma$-finite, $(1)$ and $(3)$ must be replaced by, respectively:
{{begin-itemize}}
{{item|(1'):|$\sequence {f_n}_{n \mathop \in \N}$ converges in $\LL^p$}}
{{item|(3'):|$\ds \lim_{n \mathop \to \infty} \int \size {f_n}^p \rd \mu$ exists in $\R$}}
{{end-itemize}}
{{ExtractTheorem|The last part should be a corollary}}

Proof:
{{ProofWanted}}
{{Namedfor|Giuseppe Vitali|cat = Vitali}}
Theorem: Element Commutes with Product of Commuting Elements/General Theorem

Let $\struct {S, \circ}$ be a semigroup.
Let $\sequence {a_k}_{1 \mathop \le k \mathop \le n}$ be a sequence of terms of $S$.
Let $b \in S$ such that $b$ commutes with $a_k$ for each $k \in \closedint 1 n$.
Then $b$ commutes with $a_1 \circ \cdots \circ a_n$.

Proof:
The proof proceeds by induction on $n$, the length of $\sequence {a_k}_{1 \mathop \le k \mathop \le n}$.
Theorem: Trivial Subgroup is Subgroup

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Then the trivial subgroup $\struct {\set e, \circ}$ is indeed a subgroup of $\struct {G, \circ}$.

Proof:
Using the One-Step Subgroup Test:
: $(1): \quad e \in \set e \leadsto \set e \ne \O$
: $(2): \quad e \in \set e \leadsto e \circ e^{-1} = e \in \set e$
{{qed}}
Theorem: Trivial Subgroup is Normal

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Then the trivial subgroup $\struct {\set e, \circ}$ of $G$ is a normal subgroup in $G$.

Proof:
First, by Trivial Subgroup is Subgroup, $\struct {\set e, \circ}$ is a subgroup of $G$.
To show $\struct {\set e, \circ}$ is normal in $G$:
:$\forall a \in G: a \circ e \circ a^{-1} = a \circ a^{-1} = e$
Hence the result.
{{qed}}
Theorem: Group is Normal in Itself

Let $\struct {G, \circ}$ be a group.
Then $\struct {G, \circ}$ is a normal subgroup of itself.

Proof:
First, by Group is Subgroup of Itself, $\struct {G, \circ}$ is a subgroup of itself.
To show $\struct {G, \circ}$ is normal in $G$:
:$\forall a, g \in G: a \circ g \circ a^{-1} \in G$
as $G$ is closed by definition.
Hence the result.
{{qed}}
Theorem: Relativisation is Standard Model

Let $P$ be a well-formed formula.
Let $A$ be a finite set such that $x \in A$ {{iff}} $x$ is a free variable in $P$.
Then:
:$A \subseteq B \implies \paren {B \models P \iff P^B}$
{{explain|Definition of $P^B$}}

Proof:
The proof proceeds by Induction on Well-Formed Formulas of $P$.
$P$ must be of the form:
:$x \in y$
:$\paren {Q \land R}$
:$\neg Q$
or:
:$\forall x: Q$
for some propositions $Q$ and $R$.
Theorem: Induction on Well-Formed Formulas

Let $\FF$ be a formal language with a bottom-up grammar.
Let $\Phi$ be a proposition about the well-formed formulas of $\FF$.
Suppose that $\Phi$ is true for all letters of $\FF$.
Suppose further that every rule of formation preserves $\Phi$, i.e. when fed well-formed formulas satisfying $\Phi$, it yields new well-formed formulas satisfying $\Phi$.
Then all well-formed formulas of $\FF$ satisfy $\Phi$.

Proof:
By definition of bottom-up grammar, the well-formed formulas of $\FF$ comprise:
:letters of $\FF$;
:expressions resulting from rules of formation.
Either case is dealt with by the assumptions on $\Phi$.
Hence the result, from Proof by Cases.
{{qed}}
Category:Formal Languages
dtt1zuemgcw8nkikkml6zac4n15jrf7
Theorem: Substitution of Elements

Let $a$, $b$, and $x$ be sets.
:$a = b \implies \paren {a \in x \iff b \in x}$

Proof:
By the {{Axiom-link|Extension|Sets}}:
:$a = b \implies \paren {a \in x \implies b \in x}$
Equality is Symmetric, so also by the {{Axiom-link|Extension|Sets}}:
:$a = b \implies \paren {b \in x \implies a \in x}$
{{qed}}
Theorem: Limit Ordinals Preserved Under Ordinal Multiplication

Let $x$ and $y$ be ordinals.
Let $x$ be non-empty.
Let $y$ be a limit ordinal.
It follows that the ordinal product $\left({x \times y}\right)$ is a limit ordinal.

Proof:
$y$ is a limit ordinal and thus is nonzero, by definition.
$x$ and $y$ are both nonzero.
So by Ordinals have No Zero Divisors:
:$x \times y \ne 0$
So by definition of limit ordinal:
:$x \times y \in K_{II} \lor \exists z \in \On: x \times y = z^+$
{{AimForCont}} $x \times y = z^+$ for some ordinal $z$.
{{begin-eqn}}
{{eqn | l = x \times y
      | r = \bigcup_{w \mathop \in y} \paren {x \times w}
      | c = {{Defof|Ordinal Multiplication}}
}}
{{end-eqn}}
It follows that:
{{begin-eqn}}
{{eqn | l = z
      | o = \in
      | r = \bigcup_{w \mathop \in y} \tuple {x \times w}
}}
{{eqn | ll= \leadsto
      | q = \exists w \in y
      | l = z
      | o = \in
      | r = x \times w
      | c = {{Defof|Set Union|Set Union}}
}}
{{eqn | ll= \leadsto
      | q = \exists w \in y
      | l = z^+
      | o = \in
      | r = \paren {x \times w}^+
      | c = Successor is Less than Successor
}}
{{eqn | l = \paren {x \times w}^+
      | r = \paren {x \times w} + 1
      | c = Ordinal Addition by One
}}
{{eqn | ll= \leadsto
      | q = \exists w \in y
      | l = z^+
      | o = \in
      | r = \paren {x \times w} + 1
      | c = 
}}
{{end-eqn}}
But by Subset is Right Compatible with Ordinal Addition:
:$\paren {x \times w} + 1 \subseteq \paren {x \times w} + x$
Therefore:
{{begin-eqn}}
{{eqn | q = \exists w \in y
      | l = z^+ 
      | o = \in
      | r = \paren {x \times w} + x
      | c = 
}}
{{eqn | r = \paren {x \times w^+}
      | c = {{Defof|Ordinal Multiplication}}
}}
{{end-eqn}}
But by Successor of Ordinal Smaller than Limit Ordinal is also Smaller:
:$w^+ \in y$
Therefore:
:$z^+ \in x \times y$
contradicting the fact that $z^+ = x \times y$.
Thus:
:$z^+ \ne x \times y$
and:
:$x \times y \in K_{II}$
{{qed}}
Theorem: Ordinal is Less than Ordinal times Limit

Let $y$ be a limit ordinal.
Let $x$ and $z$ be ordinals.
Then:
:$z < x \times y \iff \exists w \in y: z < x \times w$

Proof:
{{begin-eqn}}
{{eqn | l = z
      | o = <
      | r = x \times y
}}
{{eqn | ll= \leadstoandfrom
      | l = z
      | o = <
      | r = \bigcup_{w \mathop \in y} \paren {x \times w}
      | c = {{Defof|Ordinal Multiplication}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists w \in y
      | l = z
      | o = <
      | r = x \times w
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
{{qed}}
Theorem: Class Equality is Reflexive

Let $A$ be a class.
Then:
:$A = A$
where $=$ denotes class equality.

Proof:
{{NotZFC}}
:$\forall x: \left({ x \in A \iff x \in A }\right)$
{{explain|More explanation is needed as to why this constitutes a proof.}}
{{qed}}
Theorem: Class Equality is Symmetric

Let $A$ and $B$ be classes.
Let $=$ denote class equality.
Then:
:$A = B \implies B = A$

Proof:
{{NotZFC}}
From Biconditional is Commutative:
:$\forall x: \left({ x \in A \iff x \in B }\right) \implies \forall x: \left({ x \in B \iff x \in A }\right)$
Hence the result by definition of class equality.
Theorem: Class Equality is Transitive

Let $A$, $B$, and $C$ be classes.
Let $=$ denote class equality.
Then
:$\left({ A = B \land B = C }\right) \implies B = A$

Proof:
{{NotZFC}}
By Universal Generalisation and Biconditional is Transitive:
:$\forall x: \left({ \left({ x \in A \iff x \in B }\right) \land \left({ x \in B \iff x \in C }\right) }\right) \implies \forall x: \left({ x \in A \iff x \in C }\right)$ by Universal Generalisation and Biconditional is Transitive
{{explain|Further explanation needs to be added here to explain why this constitutes a proof.}}
{{qed}}
Theorem: Substitutivity of Class Equality

Let $A$ and $B$ be classes.
Let $\map P A$ be a well-formed formula of the language of set theory.
Let $\map P B$ be the same proposition $\map P A$ with all instances of $A$ replaced with instances of $B$.
Let $=$ denote class equality.
:$A = B \implies \paren {\map P A \iff \map P B}$

Proof:
By induction on the well-formed parts of $\map P A$.
The proof shall use $\implies$ and $\neg$ as the primitive connectives.
Theorem: Class is Extensional

Let $A$ be a class.
Then:
:$A = \set {x : x \in A}$
That is, $A$ is extensional.

Proof:
We have:
:$x \in \set {x : x \in A} \iff x \in A$
by Characterization of Class Membership (applied to $\set {x : x \in A}$).
By Universal Generalisation, it follows that:
:$\forall x: \paren {x \in A \iff x \in \set {x : x \in A} }$
Hence the result, by definition of class equality.
{{qed}}
Theorem: Set is Small Class

Let $x$ be a set.
Then $x$ is a small class.

Proof:
:$x = x$
Therefore by Existential Generalisation:
:$\exists y: x = y$
{{qed}}
{{explain|Add the appropriate words to link the above statements to the fact being proved, e.g. "Therefore by definition of ..." etc.}}
Theorem: Class Member of Class Builder

Let $A$ be a class.
Let $x$ be a set.
Let $\map P x$ be a well-formed formula in the language of set theory.
Let $\map P A$ denote the formula $\map P x$ with all free instances of $x$ replaced with instances of $A$.
Let $\set {x: \map P x}$ be a class specified using class builder notation.
Then:
:$A \in \set {x: \map P x} \iff \paren {\exists x: x = A \land \map P A}$

Proof:
{{begin-eqn}}
{{eqn | l = A
      | o = \in
      | m = \leftset x
      | mo= :
      | r = \rightset {\map P x}
}}
{{eqn | ll= \leadsto
      | q = \exists x \in \set {x: \map P x}
      | l = A
      | m = x
      | c = {{Defof|Class (Zermelo-Fraenkel)}}
}}
{{eqn | ll= \leadsto
      | q = \exists x
      | l = x
      | m = A
      | mo= \land
      | r = \map P x
      | c = {{Defof|Bounded Existential Quantifier}}
}}
{{eqn | ll= \leadsto
      | q = \exists x
      | l = x
      | m = A
      | mo= \land
      | r = \map P A
      | c = Substitutivity of Class Equality
}}
{{end-eqn}}
{{qed}}
Theorem: Class Equality Extension of Set Equality

Let $=_s$ denote set equality.
Let $=_c$ denote class equality.
Let $x$ and $y$ be sets.
Then $x =_s y$ {{iff}} $x =_c y$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = =_s
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall z
      | l = \leftparen {z \in x}
      | o = \iff
      | r = \rightparen {z \in y}
      | c = {{Defof|Set Equality}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = =_c
      | r = y
      | c = {{Defof|Class Equality}}, Class Membership is Extension of Set Membership
}}
{{end-eqn}}
{{qed}}
{{questionable|This has been put in the category :Category:Zermelo-Fraenkel Class Theory. Should it really be that specific? Does it not also apply to Definition:NBG for example? Or others? Complete review of the applicability of this is of high importance, because I believe that upon this depends the applicability of identifying a small class with a set.}}
Category:Zermelo-Fraenkel Class Theory
lcx1dzzaxbmqysh91qb6ny81lirlklv
Theorem: B-Algebra Induced by Group Induced by B-Algebra

Let $\struct {S, *}$ be a $B$-algebra.
Let $\struct {S, \circ}$ be the group described on $B$-Algebra Induces Group.
Let $\struct {S, *'}$ be the $B$-algebra described on Group Induces $B$-Algebra.
Then $\struct {S, *'} = \struct {S, *}$.

Proof:
Let $a, b \in S$.
It is required to show that:
:$a *' b = a * b$
To achieve this, recall that $*'$ is defined on Group Induces $B$-Algebra to satisfy:
:$a *' b = a \circ b^{-1}$
which, by the definition of $\circ$ on $B$-Algebra Induces Group comes down to:
{{begin-eqn}}
{{eqn | l = a *' b
      | r = a * \paren {0 * b^{-1} }
}}
{{eqn | r = a * \paren {0 * \paren {0 * b} }
      | c = $B$-Algebra Induces Group
}}
{{eqn | r = a * b
      | c = Identity: $0 * \paren {0 * x} = x$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Group Induced by B-Algebra Induced by Group

Let $\struct {S, \circ}$ be a group.
Let $\struct {S, *}$ be the $B$-algebra described on Group Induces $B$-Algebra.
Let $\struct {S, \circ'}$ be the group described on $B$-Algebra Induces Group.
Then $\struct {S, \circ'} = \struct {S, \circ}$.

Proof:
Let $a, b \in S$.
It is required to show that:
:$a \circ' b = a \circ b$
To achieve this, recall that $\circ'$ is defined on $B$-Algebra Induces Group to satisfy:
:$a \circ' b = a * \paren {e * b}$
which, by the definition of $*$ on Group Induces $B$-Algebra comes down to:
{{begin-eqn}}
{{eqn | l = a \circ' b
      | r = a \circ \paren {e \circ b^{-1} }^{-1}
}}
{{eqn | r = a \circ \paren {b^{-1} }^{-1}
      | c = {{Group-axiom|2}}
}}
{{eqn | r = a \circ b
      | c = Inverse of Group Inverse
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Union of Doubleton

Let $x$ and $y$ be sets.
Let $\set {x, y}$ be a doubleton.
Then $\bigcup \set {x, y}$ is a set such that:
:$\bigcup \set {x, y} = x \cup y$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = z \in \bigcup \set {x, y}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \exists w \in \set {x, y}: z \in w
      | c = {{Defof|Union of Class}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \exists w: \paren {\paren {w = x \lor w = y} \land z \in w}
      | c = {{Defof|Doubleton Class}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {z \in x \lor z \in y}
      | c = Equality implies Substitution
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = z \in \paren {x \cup y}
      | c = {{Defof|Class Union}}
}}
{{end-eqn}}
Then, from Axiom of Unions, it follows that $x \cup y$ is a set.
{{qed}}
Theorem: Union of Small Classes is Small

Let $x$ and $y$ be small classes.
Then $x \cup y$ is also small.

Proof:
Let $\map {\mathscr M} A$ denote that $A$ is small.
{{begin-eqn}}
{{eqn | l = \map {\mathscr M} x \land \map {\mathscr M} y
      | o = \leadsto
      | r = \map {\mathscr M} {\set {x, y} }
      | c = {{Axiom-link|Pairing|Class Theory}}
}}
{{eqn | o = \leadsto
      | r = \map {\mathscr M} {\bigcup \set {x, y} }
      | c = {{Axiom-link|Unions|Set Theory}}
}}
{{eqn | o = \leadsto
      | r = \map {\mathscr M} {x \cup y}
      | c = Union of Doubleton
}}
{{end-eqn}}
{{qed}}
Theorem: Category of Finite Sets is Category

Let $\mathbf{Set}$ be the category of finite sets.
Then $\mathbf{Set}$ is a metacategory.

Proof:
{{mutatis}} the same as that of Category of Sets is Category.
{{qed}}
Category:Category of Finite Sets
r9us00xl8llon0j528uau6br64jkgnt
Theorem: Category of Ordered Sets is Category

Let $\mathbf{OrdSet}$ be the category of ordered sets.
Then $\mathbf{OrdSet}$ is a metacategory.

Proof:
Let us verify the axioms $(C1)$ up to $(C3)$ for a metacategory.
For any two increasing mappings their composition (in the usual set theoretic sense) is again increasing by Composite of Increasing Mappings is Increasing.
For any set $X$, we have the identity mapping $\operatorname{id}_X$.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity that this is the identity morphism for $X$.
That it is increasing follows from Identity Mapping is Increasing.
Finally by Composition of Mappings is Associative, the associative property is satisfied.
Hence $\mathbf{OrdSet}$ is a metacategory.
{{qed}}
Theorem: Set Difference is Set

Let $x$ be a small class.
Let $A$ be a class.
Let $\map \MM B$ denote that $B$ is small.
Then: 
:$\map \MM {x \setminus A}$

Proof:
Consider $R, S, T \subseteq \mathbb U$, where $\mathbb U$ is considered as the universe.
Then:
{{begin-eqn}}
{{eqn | l = \paren {R \setminus S} \cap T
      | r = \paren {R \cap \map \complement S} \cap T
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {R \cap T} \cap \map \complement S
      | c = Intersection is Commutative and Intersection is Associative
}}
{{eqn | r = \paren {R \cap T} \setminus S
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference is Set

Let $x$ be a small class.
Let $A$ be a class.
Let $\map \MM B$ denote that $B$ is small.
Then: 
:$\map \MM {x \setminus A}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \paren {R \setminus S} \cap T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in R \land x \notin S} \land x \in T
      | c = {{Defof|Set Intersection}} and {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in R \land x \in T} \land x \notin S
      | c = Rule of Commutation and Rule of Association
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = x \in \paren {R \cap T} \setminus S
      | c = {{Defof|Set Intersection}} and {{Defof|Set Difference}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference is Set

Let $x$ be a small class.
Let $A$ be a class.
Let $\map \MM B$ denote that $B$ is small.
Then: 
:$\map \MM {x \setminus A}$

Proof:
{{NotZFC}}
By Set Difference as Intersection with Relative Complement:
:$\paren {x \setminus A} = \paren {x \cap \map \complement A}$
{{wtd|This rule must be proven for classes}}
Next, by Axiom of Subsets Equivalents, $\paren {x \cap \map \complement A}$ is small.
Therefore:
:$\map \MM {x \setminus A}$
{{qed}}
Theorem: Nonempty Class has Members

Let $A$ be a class.
Then:
:$A \ne \O \iff \exists x: x \in A$

Proof:
{{NotZFC}}
{{begin-eqn}}
{{eqn | l = A \ne \O
      | o = \leadstoandfrom
      | r = \neg \forall x: \paren {x \in A \iff x \in \O}
      | c = {{Defof|Class Equality}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \forall x: \neg x \in A
      | c = {{Defof|Empty Set}}
}}
{{eqn | o = \leadstoandfrom
      | r = \exists x: x \in A
      | c = De Morgan's Laws (Predicate Logic)
}}
{{end-eqn}}
{{qed}}
Theorem: Class is Not Element of Itself

Let $A$ be a class.
Then $A$ is not an element of itself:
:$A \notin A$

Proof:
$A \in A$ would create a relational loop for the class membership sign.
By No Membership Loops, this is a contradiction.
{{qed}}
Theorem: Category of Relations is Category

Let $\mathbf{Rel}$ be the category of relations.
Then $\mathbf{Rel}$ is a metacategory.

Proof:
Let us verify the axioms $(C1)$ up to $(C3)$ for a metacategory.
We have already defined the composition of morphisms.
For any set $X$, we have the diagonal relation $\operatorname{id}_X$.
By Diagonal Relation is Left Identity and Diagonal Relation is Right Identity it follows that this is the identity morphism for $X$.
Finally by Composition of Relations is Associative, the associative property is satisfied.
Hence $\mathbf{Rel}$ is a metacategory.
{{qed}}
Theorem: Universal Class is Proper

Let $V$ denote the universal class.
Then $V$ is a proper class.

Proof:
{{AimForCont}} $V$ is small.
We have that:
:$\operatorname {Ru} \subseteq V$
where $\operatorname {Ru}$ denotes the Russell class.
By Axiom of Subsets Equivalents, $\operatorname {Ru}$ is also small.
This contradicts Russell's Paradox.
{{qed}}
Theorem: Universal Class is Proper

Let $V$ denote the universal class.
Then $V$ is a proper class.

Proof:
{{NotZFC}}
Let $I_V$ be the identity mapping on $V$.
By Identity Mapping is Bijection it follows that $I_V$ is a bijection.
Therefore, by the Axiom of Limitation of Size, $V$ is proper.
{{qed}}
Theorem: Universal Class is Proper

Let $V$ denote the universal class.
Then $V$ is a proper class.

Proof:
{{AimForCont}} $V$ is small.
By Cantor's Theorem, there is no surjection from $V$ to $\powerset V$.
By definition of universal class:
:$\powerset V \subseteq V$
By Injection from Subset to Superset, there exists an injection from $\powerset V$ to $V$.
By Injection has Surjective Left Inverse Mapping, there is a surjection from $V$ to $\powerset V$.
But this contradicts Cantor's Theorem.
Therefore $V$ is proper. 
{{qed}}
Theorem: Composite Functor is Functor

Let $\mathbf C, \mathbf D$ and $\mathbf E$ be metacategories.
Let $F: \mathbf C \to \mathbf D$ and $G: \mathbf D \to \mathbf E$ be covariant functors.
Let $GF: \mathbf C \to \mathbf E$ be the composition of $G$ with $F$.
Then $G F$ is also a covariant functor.

Proof:
Let $f, g$ be morphisms of $\mathbf C$ such that $g \circ f$ is defined.
Then:
{{begin-eqn}}
{{eqn | l = \map {G F} {g \circ f}
      | r = \map G {\map F {g \circ f} }
      | c = {{Defof|Composition of Functors}}
}}
{{eqn | r = \map G {F g \circ F f}
      | c = $F$ is a Covariant Functor
}}
{{eqn | r = \map G {F g} \circ \map G {F f}
      | c = $G$ is a functor
}}
{{eqn | r = G F g \circ G F f
      | c = {{Defof|Composition of Functors}}
}}
{{end-eqn}}
Also, for any object $C$ of $\mathbf C$:
{{begin-eqn}}
{{eqn | l = G F I_C
      | r = \map G {F I_C}
      | c = {{Defof|Composition of Functors}}
}}
{{eqn | r = G I_{F C}
      | c = $F$ is a Covariant Functor
}}
{{eqn | r = I_{\map G {F C} }
      | c = $G$ is a Covariant Functor
}}
{{eqn | r = I_{G F C}
      | c = {{Defof|Composition of Functors}}
}}
{{end-eqn}}
Hence $G F$ is shown to be a covariant functor.
{{qed}}
Category:Functors
olpzsc4iskdw8pb98sj7tn6iiah0oeo