avewright/proofwiki-math huggingface dataset:
Theorem: Identity Functor is Functor

Let $\mathbf C$ be a metacategory.
Let $\operatorname{id}_{\mathbf C}: \mathbf C \to \mathbf C$ be the identity functor on $\mathbf C$.
Then $\operatorname{id}_{\mathbf C}$ is a functor.

Proof:
Let $f, g$ be morphisms of $\mathbf C$ such that $g \circ f$ is defined.
Then:
{{begin-eqn}}
{{eqn | l = \operatorname{id}_{\mathbf C} \left({g \circ f}\right)
      | r = g \circ f
      | c = {{Defof|Identity Functor}}
}}
{{eqn | r = \operatorname{id}_{\mathbf C} g \circ \operatorname{id}_{\mathbf C} f
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
Also, for any object $C$ of $\mathbf C$:
{{begin-eqn}}
{{eqn | l = \operatorname{id}_{\mathbf C} \operatorname{id}_C
      | r = \operatorname{id}_C
      | c = {{Defof|Identity Functor}}
}}
{{eqn | r = \operatorname{id}_{\operatorname{id}_{\mathbf C} C}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
Hence $\operatorname{id}_{\mathbf C}$ is shown to be a functor.
{{qed}}
Category:Functors
0znnw1ckw87uu1whtqsqxkbz2xyfb0c
Theorem: Category of Categories is Category

Let $\mathbf{Cat}$ be the category of categories.
Then $\mathbf{Cat}$ is a metacategory.

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
For any two functors their composition is again a functor by Composite Functor is Functor.
For any small category $\mathbf C$, we have the identity functor $\operatorname {id}_{\mathbf C}$.
By Identity Functor is Left Identity and Identity Functor is Right Identity this is the identity morphism for $\mathbf C$.
Finally by Composition of Functors is Associative, the associative property is satisfied.
Hence $\mathbf{Cat}$ is a metacategory.
{{qed}}
Category:Category of Categories
123a3t21qyihklh8anw9w92gsbswypt
Theorem: Identity Functor is Left Identity

Let $\mathbf C$ and $\mathbf D$ be metacategories.
Let $F: \mathbf C \to \mathbf D$ be a functor, and let $\operatorname{id}_{\mathbf D}$ be the identity functor on $\mathbf D$.
Then the composite functor $\operatorname{id}_{\mathbf D} F$ satisfies:
:$\operatorname{id}_{\mathbf D} F = F$

Proof:
We have, for all objects $C$ of $\mathbf C$:
:$\operatorname{id}_{\mathbf D} F C = \map {\operatorname{id}_{\mathbf D} } {F C} = F C$
by definition of composition of functors and of identity functor.
Similarly, we have, for a morphism $f$ of $\mathbf C$:
:$\operatorname{id}_{\mathbf D} F f = \map {\operatorname{id}_{\mathbf D} } {F f} = F f$
Hence the result.
{{qed}}
Category:Functors
26e7af4um6p74wwzi40p775bwfmy5of
Theorem: Identity Functor is Right Identity

Let $\mathbf C$ and $\mathbf D$ be metacategories.
Let $F: \mathbf C \to \mathbf D$ be a functor, and let $\operatorname{id}_{\mathbf C}$ be the identity functor on $\mathbf C$.
Then the composite functor $F \operatorname{id}_{\mathbf C}$ satisfies:
:$F \operatorname{id}_{\mathbf C} = F$

Proof:
We have, for all objects $C$ of $\mathbf C$:
:$F \operatorname{id}_{\mathbf C} C = F \left({\operatorname{id}_{\mathbf C} C}\right) = F C$
by definition of composition of functors and of identity functor.
Similarly, we have, for a morphism $f$ of $\mathbf C$:
:$F \operatorname{id}_{\mathbf C} f = F \left({\operatorname{id}_{\mathbf C} f}\right) = F f$
Hence the result.
{{qed}}
Category:Functors
mo0wafs5n5i7na9paje3l98dwvfk2ic
Theorem: Composition of Functors is Associative

Let $\mathbf A$, $\mathbf B$, $\mathbf C$ and $\mathbf D$ be metacategories.
Let $F: \mathbf A \to \mathbf B$, $G: \mathbf B \to \mathbf C$ and $H: \mathbf C \to \mathbf D$ be functors.
Then composition of functors is associative:
:$H \paren {G F} = \paren {H G} F$

Proof:
Let $A$ be an object of $\mathbf A$.
Then, solely by the definition of composite functor:
{{begin-eqn}}
{{eqn | l = H \paren {G F} A
      | r = H \paren {G F A}
}}
{{eqn | r = H \paren {G \paren {F A} }
}}
{{eqn | r = H G \paren {F A}
}}
{{eqn | r = \paren {H G} F A
}}
{{end-eqn}}
Then, {{mutatis}}, the same proof works for a morphism $f$ of $\mathbf A$ as well.
Hence the result.
{{qed}}
Category:Functors
drzbt6p7iuku4hylgdgp5pmiv7ojvs2
Theorem: Abel-Ruffini Theorem

There is no general algebraic solution for determining all the roots of a polynomial of degree $5$ or higher.

Proof:
{{ProofWanted|Galois theory seems the best choice; we probably also want the actual proof by Abel}}
{{tidy}}
{{MissingLinks}}
The general polynomial:
:$\map f x = x^n - s_1 x^{n - 1} + \cdots + \paren {-1}^n s_n$
has Galois group $S_n$.
From Symmetric Group on Greater than 4 Letters is Not Solvable:
:$S_n$ is not solvable for $n \ge 5$.
By Polynomial is Solvable by Radicals iff Galois Group is Solvable, the general polynomial is not solvable by radicals.
{{qed}}
{{Namedfor|Niels Henrik Abel|name2 = Paolo Ruffini|cat = Abel|cat2 = Ruffini}}
Theorem: Cartesian Product is Small

Let $a$ and $b$ be small classes.
Then their Cartesian product $a \times b$ is small:
:$\map {\MM} {a \times b}$

Proof:
By Binary Cartesian Product in Kuratowski Formalization contained in Power Set of Power Set of Union:
:$a \times b \subseteq \powerset {\powerset {a \cup b} }$
By Union of Small Classes is Small, $a \cup b$ is small.
By the Axiom of Powers, $\powerset {\powerset {a \cup b} }$ is small.
By Axiom of Subsets Equivalents, $a \times b$ is small.
{{qed}}
Theorem: Preorder Category is Category

Let $\struct {S, \precsim}$ be a preordered set.
Let $\mathbf S$ be its associated preorder category.
Then $\mathbf S$ is a category.

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
Note that for objects $a, b$ of $\mathbf S$, there is at most ''one'' morphism $a \to b$, by definition of $\mathbf S$.
Suppose that $a \to b$ and $b \to c$ are morphisms of $\mathbf S$.
Then we have $a \precsim b$ and $b \precsim c$, and as $\precsim$ is a preordering:
:$a \precsim c$
which is to say that there is a unique morphism $a \to c$.
By uniqueness, this morphism is the composite of $a \to b$ and $b \to c$.
Also, for any $a \in S$, there is a morphism $a \to a$ by virtue of:
:$a \precsim a$
since $\precsim$ is a preordering.
The uniqueness of the morphisms mentioned above implies directly that $a \to a$ classifies as the identity morphism $\operatorname{id}_a$ for $a$.
The uniqueness of morphisms also immediately implies associativity.
Hence $\mathbf S$ is a metacategory.
Since both $S$ and $\precsim$ are sets, $\mathbf S$ is also a category.
{{qed}}
Category:Preorder Categories
1hnb0owrc0brm4fbepvci2wjlk66sd7
Theorem: Category Induces Preorder

Let $\mathbf S$ be a category with set of objects $S$.
Then the binary relation $\precsim$ defined by:
:$\forall a, b \in S: a \precsim b \iff \exists f: a \to b$
is a preorder on $S$.

Proof:
It suffices to establish $\precsim$ is reflexive and transitive.
Theorem: Preorder Induced by Preorder Category

Let $\struct {S, \precsim}$ be a preordered set.
Let $\mathbf S$ be its associated preorder category.
Let $\precsim'$ be the preorder induced by $\mathbf S$ as on Category Induces Preorder.
Then $\precsim'$ is the same as $\precsim$.

Proof:
Suppose that for some $a, b \in S$, we have:
:$a \precsim' b$
By Category Induces Preorder, this happens {{iff}} there exists an $\mathbf S$-morphism $f: a \to b$.
By definition of $\mathbf S$, this $f: a \to b$ exists {{iff}}:
:$a \precsim b$
Hence the result.
{{qed}}
Category:Preorder Categories
3vb5btihlg5h22v8p3fq6a0emevlzpt
Theorem: Functor between Order Categories

Let $\struct {S, \preceq}$ and $\struct {T, \preceq'}$ be ordered sets.
Let $\mathbf S$ and $\mathbf T$ be their associated order categories, respectively.
Let $F: \mathbf S \to \mathbf T$ be a functor.
Then its object functor $F: S \to T$ is a monotone mapping.

Proof:
Suppose that for some $a, b \in S$, we have:
:$a \preceq b$
Then there is a morphism $a \to b$ in $\mathbf S$.
As $F$ is a functor, it follows that there is a morphism:
:$F a \to F b$
in $\mathbf T$ as well, that is:
:$F a \preceq' F b$
Hence the result.
{{qed}}
Theorem: Discrete Category on Set is Discrete Category

Let $S$ be a set.
Let $\map {\mathbf {Dis} } S$ be the discrete category on $S$.
Then $\map {\mathbf {Dis} } S$ determines a unique (up to isomorphism) discrete category $\map {\mathbf {Dis} } S$ whose objects precisely comprise $S$.
{{explain|What is unique up to isomorphism in this context? This is the definition of $\map {\mathbf {Dis} } S$, isn't it?}}
{{expand|That is, $\mathbf {Dis}: \mathbf {Set} \to \mathbf {Cat}$ is a functor (with left inverse $\mathbf {ob}$) }}

Proof:
{{finish|Trivial.}}
{{qed}}
Theorem: Discrete Category is Order Category

Let $\map {\mathbf{Dis} } S$ be a discrete category.
Then $\map {\mathbf{Dis} } S$ is also an order category.

Proof:
We have, for any morphism $a \to b$ in $\map {\mathbf{Dis} } S$ that $a = b$.
Thus we see that $\map {\mathbf{Dis} } S$ will be an order category {{iff}}:
:$\forall a, b \in S: a \preceq b \iff a = b$
holds for some ordering $\preceq$ on $S$.
The trivial ordering on $S$ accomplishes this.
Hence the result.
{{qed}}
Theorem: Image of Small Class under Mapping is Small

Let $A$ be a mapping.
Let $a$ be a small class.
Then, the image of $a$ under $A$ is small.
{{improve|$A$ being a class variable, I strongly suggest a different letter to denote the mapping}}

Proof:
{{NotZFC}}
Since $A$ is a mapping:
:$\forall y: \exists x: \forall z: \left({ y A z \implies z = x }\right)$
This satisfies the antecedent of the axiom of replacement.  Therefore:
:$\forall w: \exists x: \forall y: \left({ y \in w \implies \forall z: \left({ y A z \implies z \in x }\right) }\right)$
Universal Instantiation yields:
:$\exists x: \forall y: \left({ y \in a \implies \forall z: \left({ y A z \implies z \in x }\right) }\right)$
By applying the definition for the restricted universal quantifier and rearranging quantifiers:
:$\exists x: \forall z: \left({ \exists y \in a: y A z \implies z \in x }\right)$
Applying the definition for image:
:$\exists x: \operatorname{Im} \left({a}\right) \subseteq x$
By Axiom of Subsets Equivalents, the image of $a$ under $A$ must be small.
{{qed}}
Theorem: Inverse of Small Relation is Small

Let $a$ be a small class.
Let $a$ also be a relation.
Then the inverse relation of $a$ is small.

Proof:
Let $A$ equal:
:$\set {\tuple {\tuple {x, y}, \tuple {y, x} } : \tuple {x, y} \in a}$
Then $A$ maps $a$ to its inverse.
{{link wanted|$A$ in general has a name but I can't find it atm}}
Thus, the inverse of $a$ is the image of $a$ under $A$.
By Image of Small Class under Mapping is Small, the inverse of $a$ is small.
{{qed}}
Theorem: Functor between Monoid Categories

Let $\left({S, \circ}\right)$ and $\left({T, *}\right)$ be monoids.
Let $\mathbf S$ and $\mathbf T$ be the associated monoid categories.
Let $F: \mathbf S \to \mathbf T$ be a functor.
Then the morphism functor $F_1$ of $F$ is a monoid homomorphism.

Proof:
By definition of monoid category, we have:
:$\mathbf S_1 = S, \mathbf T_1 = T$
which in particular are sets.
Hence the morphism functor $F_1: \mathbf S_1 \to \mathbf T_1$ is a mapping $F_1: S \to T$.
For $F_1$ to be a monoid homomorphism, it suffices to show that the following hold:
:$F_1 \left({e_S}\right) = e_T$
:$\forall s_1, s_2 \in S: F_1 \left({s_1 \circ s_2}\right) = F_1 \left({s_1}\right) * F_1 \left({s_2}\right)$
Since all $s_1, s_2 \in S$ are composable morphisms of $\mathbf S$, these conditions are exactly equivalent to $F$ being a functor.
Hence the result.
{{qed}}
Theorem: Category of Monoids is Category

Let $\mathbf{Mon}$ be the category of monoids.
Then $\mathbf{Mon}$ is a metacategory.

Proof:
Let us verify the axioms $(C1)$ up to $(C3)$ for a metacategory.
We have Composite of Homomorphisms on Algebraic Structure is Homomorphism, verifying $(C1)$.
We have Identity Mapping is Automorphism providing $\operatorname{id}_S$ for every monoid $\left({S, \circ}\right)$.
Now, $(C2)$ follows from Identity Mapping is Left Identity and Identity Mapping is Right Identity.
Finally, $(C3)$ follows from Composition of Mappings is Associative.
Hence $\mathbf{Mon}$ is a metacategory.
{{qed}}
Category:Category of Monoids
sppgcr1pruam0jkf2euhyvt6y3jpnt0
Theorem: Cayley's Representation Theorem/General Case

Let $\struct {G, \cdot}$ be a group.
Then there exists a permutation group $P$ on some set $S$ such that:
:$G \cong P$
That is, such that $G$ is isomorphic to $P$.

Proof:
Let $G$ be a group and let $a \in G$.
Consider the left regular representation $\lambda_a: G \to G$ defined as:
:$\map {\lambda_a} x = a \cdot x$
From Regular Representations in Group are Permutations we have that $\lambda_a$ is a permutation.
Now let $b \in G$ and consider $\lambda_b: G \to G$ defined as:
:$\map {\lambda_b} x = b \cdot x$
From the Cancellation Laws it follows that $\lambda_a \ne \lambda_b \iff a \ne b$.
Let $H = \set {\lambda_x: x \in G}$.
Consider the mapping $\Phi: G \to H$ defined as:
:$\forall a \in G: \map \Phi a = \lambda_a$
From the above we have that $\Phi$ is a bijection.
Let $a, b \in G$.
From Composition of Regular Representations we have that:
:$\lambda_a \circ \lambda_b = \lambda_{a \cdot b}$
where $\circ$ denotes composition of mappings.
That is, $\Phi$ has the morphism property.
Thus $\Phi$ is seen to be a group isomorphism.
We also have that:
:$\paren {\lambda_a}^{-1} = \lambda_\paren {a^{-1} }$
because:
:$\lambda_a \circ \paren {\lambda_a}^{-1} = \lambda_\paren {a \cdot a^{-1} }$
Hence the set of left regular representations $\set {\lambda_x: x \in G}$ is a group which is isomorphic to $G$.
{{qed}}
Theorem: Cayley's Representation Theorem/General Case

Let $\struct {G, \cdot}$ be a group.
Then there exists a permutation group $P$ on some set $S$ such that:
:$G \cong P$
That is, such that $G$ is isomorphic to $P$.

Proof:
We interpret $\struct {G,\cdot}$ as an group category:
{{DefineCategory
| ob = Only one, say $*$
| mor = $a: * \to *$ for all $a \in G$
| comp =  $a \cdot b: * \to *$
| id = $e: * \to *$
}}
where $e$ is the identity element of $G$.
In particular, $G$ is a small category.
By Cayley's Theorem,  $G$ is isomorphic to a subcategory of $\mathbf{Set}$, say $\mathbf D$.
That is, there are functors:
:$F : G \to \mathbf D$
:$H : \mathbf D \to G$
such that:
:$H F = \operatorname{id}_G$
:$F H = \operatorname{id}_{\mathbf D}$
are identity functors.
Let $S := F \ast$.
Then $P := \set { F_\ast a : a \in G }$ is a permutation group on $S$.
Define a mapping $\phi : G \to P$ by:
:$a \mapsto F_\ast a$
Then $\phi : G \to P$ is a gorup isomorphism.
Indeed, if $\map \phi a = \map \phi b$ then:
:$a = \map {\paren {\operatorname{id}_{\mathbf D} }_\ast} a = \paren {H F}_\ast a = H_{F \ast} \map \phi a = H_{F \ast} \map \phi b = \paren {H F}_\ast b = \map {\paren {\operatorname{id}_{\mathbf D} }_\ast} b = b$
Thus $\phi$ is an injection.
{{finish|Details for the last part}}
Theorem: Permutation of Cosets/Corollary 1

Let $G$ be a group.
Let $H \le G$ such that $\index G H = n$ where $n \in \Z$.
Then:
:$\exists N \lhd G: N \lhd H: n \divides \index G H \divides n!$

Proof:
Apply Permutation of Cosets to $H$ and let $N = \map \ker \theta$.
Then:
:$N \lhd G$ and $N \lhd H$
so from the Correspondence Theorem:
:$H / N \le G / N$
such that:
:$\index {G / N} {H / N} = n$
Thus:
:$n \divides \index G N$
Also by Permutation of Cosets:
:$\exists K \in S_n: G / N \cong K$
Thus:
:$\index G N \divides n!$
as required.
{{Qed}}
Theorem: Cayley's Theorem (Category Theory)

Let $\mathbf C$ be a small category.
Denote with $\mathbf{Set}$ the category of sets.
Then there exists a category $\mathbf D$, subject to:
:$(1): \quad $ The objects of $\mathbf D$ are sets.
:$(2): \quad $ The morphisms of $\mathbf D$ are mappings.
:$(3): \quad \mathbf C \cong \mathbf D$, i.e. $\mathbf C$ and $\mathbf D$ are isomorphic.
That is, $\mathbf C$ is isomorphic to a subcategory of $\mathbf{Set}$.

Proof:
Define a functor $H: \mathbf C \to \mathbf{Set}$ by:
:$H C := \set {f \in \operatorname{mor} \mathbf C: \operatorname{cod} f = C}$
:$H f: H A \to H B, g \mapsto f \circ g$
for $f: A \to B$ a morphism of $\mathbf C$.
It is immediate by the definition of identity morphism that:
:$\map H {\operatorname{id}_A} = \operatorname{id}_{H A}$
For $f: A \to B$ and $g: B \to C$, observe:
{{begin-eqn}}
{{eqn | l = \map {\map H {g \circ f} } h
      | r = \paren {g \circ f} \circ h
      | c = Definition of $\map H {g \circ f}$
}}
{{eqn | r = g \circ \paren {f \circ h}
      | c = Composition of Mappings is Associative
}}
{{eqn | r = g \circ \paren {\map {H f} h}
      | c = Definition of $H f$
}}
{{eqn | r = \map {H g} {\map {H f} h}
      | c = Definition of $H g$
}}
{{eqn | r = \map {\paren {H g \circ H f} } h
      | c = {{Defof|Composition of Mappings|index = 1}}
}}
{{end-eqn}}
Thus by Equality of Mappings:
:$\map H {g \circ f} = H g \circ H f$
It follows that $H$ is a functor.
It is clear that $H$ is injective on objects.
Suppose now that $H$ were not faithful.
Then there would be morphisms $g, h: A \to B$ of $\mathbf C$ such that $H g = H h$.
Since $\operatorname{id}_A \in H A$, this means in particular that:
:$g \circ \operatorname{id}_A = h \circ \operatorname{id}_A$
by Equality of Mappings.
But the definition of identity morphism then reduces this to $g = h$.
Hence, $H$ is faithful.
It follows that $H$ is an embedding.
Thus $\mathbf C$ is isomorphic to a subcategory of $\mathbf{Set}$.
{{qed}}
Theorem: Domain of Small Relation is Small

Let $a$ be a small class.
Let $a$ also be a relation.
Then the domain of $a$ is small.

Proof:
Let $A$ equal:
:$\set {\tuple {\tuple {x, y}, x}: \tuple {x, y} \in a}$
Then, $A$ maps $a$ to its domain.
Thus, the domain of $a$ is the image of $a$ under $A$.
By Image of Small Class under Mapping is Small, the domain of $a$ is small.
{{explain|And exactly why is $A$ small, so that this result applies? Same qn for Range of Small Relation is Small}}
{{qed}}
Theorem: Range of Small Relation is Small

Let $a$ be a small class.
Let $a$ also be a relation.
Then the range of $a$ is small.

Proof:
Let $A$ equal:
:$\set {\tuple {\tuple {x, y}, y}: \tuple {x, y} \in a}$
Then, $A$ maps $a$ to its range.
Thus, the range of $a$ is the image of $A$.
By Image of Small Class under Mapping is Small, the range of $a$ is small.
{{explain|Why is $A$ small, so that Image of Small Class under Mapping is Small of applies?}}
{{qed}}
Theorem: Center of Opposite Group

Let $\struct {G, \circ}$ be a group.
Let $\struct {G, *}$ be the opposite group to $G$.
Let $\map Z {G, \circ}$ and $\map Z {G, *}$ be the centers of $\struct {G, \circ}$ and $\struct {G, *}$, respectively.
Then:
:$\map Z {G, \circ} = \map Z {G, *}$

Proof:
We have, for $g \in G$:
{{begin-eqn}}
{{eqn | l = g \in \map Z {G, \circ}
      | o = \leadstoandfrom
      | r = \forall h \in G: g \circ h = h \circ g
      | c = {{Defof|Center of Group}}
}}
{{eqn | o = \leadstoandfrom
      | r = \forall h \in G: h * g = g * h
      | c = {{Defof|Opposite Group}}
}}
{{eqn | o = \leadstoandfrom
      | r = g \in \map Z {G, *}
      | c = {{Defof|Center of Group}}
}}
{{end-eqn}}
Hence the result, by definition of set equality.
{{qed}}
Category:Opposite Groups
Category:Centers of Groups
plso6ifn0x3uxwi3s1d2porv2x0a12h
Theorem: Opposite Group of Opposite Group

Let $\struct {G, \circ}$ be a group.
Let $\struct {G, *}$ be the opposite group to $\struct {G, \circ}$.
Let $\struct {G, \circ'}$ be the opposite group to $\struct {G, *}$.
Then:
:$\struct {G, \circ} = \struct {G, \circ'}$

Proof:
We have, for all $a, b \in G$:
:$a \circ b = b * a = a \circ' b$
by definition of opposite group.
Hence the result.
{{qed}}
Category:Opposite Groups
hbswvtiqyapehbhxyoz37xhcjs0c5n4
Theorem: Slice Category is Category

Let $\mathbf C$ be a metacategory.
Let $C \in \mathbf C_0$ be a object of $\mathbf C$.
Let $\mathbf C / C$ be the slice category of $\mathbf C$ over $C$.
Then $\mathbf C / C$ is a metacategory.

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
Suppose that $a: f \to g$ and $b: g \to h$ are morphisms in $\mathbf C / C$.
To show that $b \circ a: f \to h$ is a morphism as well, compute:
{{begin-eqn}}
{{eqn|l = \paren {b \circ a} \circ f
     |r = b \circ \paren {a \circ f}
     |c = composition in $\mathbf C$ is associative
}}
{{eqn|r = b \circ g
     |c = $a$ is a morphism
}}
{{eqn|r = h
     |c = $b$ is a morphism
}}
{{end-eqn}}
Hence $b \circ a: f \to h$ is a morphism.
For $(\text C 2)$, observe that for $a: f \to g$, with objects $f: X \to C$ and $g: Y \to C$, we have:
{{begin-eqn}}
{{eqn|l = a \circ \operatorname{id}_f
     |r = a \circ \operatorname{id}_X
     |c = Definition of $\operatorname{id}_f$
}}
{{eqn|r = a
     |c = Since $\mathbf C$ is a metacategory
}}
{{eqn|r = \operatorname{id}_Y \circ a
}}
{{eqn|r = \operatorname{id}_g \circ a
}}
{{end-eqn}}
Hence $(\text C 2)$ is shown to hold.
Since the composition in $\mathbf C / C$ is inherited from $\mathbf C$, satisfaction of the associative property $(\text C 3)$ is also inherited.
Hence $\mathbf C / C$ is a metacategory.
{{qed}}
Category:Slice Categories
ni2sm3rde40hdkrjg7zmzh2ocqntp5k
Theorem: Monoid Category is Category

Let $\struct {S, \circ}$ be a monoid with identity $e_S$.
Let $\mathbf S$ be the associated monoid category.
Then $\mathbf S$ is a category.

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
Suppose that $a, b \in \mathbf S_1$ are morphisms.
From {{MonoidAxiom|0}}, $a \circ b$ is also a morphism.
Axiom $(\text C 2)$ follows directly from {{MonoidAxiom|2}}.
Axiom $(\text C 3)$ follows directly from {{MonoidAxiom|1}}.
Hence $\mathbf S$ is a metacategory.
As $\mathbf S$ has only one object, and $\mathbf S_1 = S$, it follows that $\mathbf S$ is also a category.
{{qed}}
Category:Monoid Categories
ckyllhblc5uuri3vu6stbow7jvczw9q
Theorem: Dual Category is Category

Let $\mathbf C$ be a metacategory.
Let $\mathbf C^{\text{op} }$ be its dual category.
Then $\mathbf C^{\text{op} }$ is also a metacategory.

Proof:
Let us verify the axioms $(C1)$ up to $(C3)$ for a metacategory.
Let $f^{\text{op} }: C^{\text{op} } \to D^{\text{op} }$ and $g^{\text{op} }: D^{\text{op} } \to E^{\text{op} }$ be morphisms in $\mathbf C^{\text{op} }$.
Then $f: D \to C$ and $g: E \to D$ are morphisms in $\mathbf C$, and so is $f \circ g: E \to C$.
Therefore, also $g^{\text{op} } \circ f^{\text{op} }: C^{\text{op} } \to E^{\text{op} }$ is a morphism in $\mathbf C^{\text{op} }$, and $(C1)$ is shown to hold.
For $(C2)$, observe that for $f^{\text{op} }: C^{\text{op} } \to D^{\text{op} }$, we have:
{{begin-eqn}}
{{eqn|l = f^{\text{op} } \circ \operatorname{id}_{C^{\text{op} } }
     |r = f^{\text{op} } \circ \operatorname{id}_C^{\text{op} }
     |c = Definition of $\operatorname{id}_{C^{\text{op} } }$
}}
{{eqn|r = \paren {\operatorname{id}_C \circ f}^{\text{op} }
     |c = {{Defof|Composition of Morphisms}}
}}
{{eqn|r = f^{\text{op} }
     |c = Since $\mathbf C$ is a metacategory
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn|l = \operatorname{id}_{D^{\text{op} } } \circ f^{\text{op} }
     |r = \operatorname{id}_D^{\text{op} } \circ f^{\text{op} }
     |c = Definition of $\operatorname{id}_{D^{\text{op} } }$
}}
{{eqn|r = \paren {f \circ \operatorname{id}_D}^{\text{op} }
     |c = {{Defof|Composition of Morphisms}}
}}
{{eqn|r = f^{\text{op} }
     |c = Since $\mathbf C$ is a metacategory
}}
{{end-eqn}}
Hence $(C2)$ is shown to hold.
To show $(C3)$, reason as follows:
{{begin-eqn}}
{{eqn|l = \paren {f^{\text{op} } \circ g^{\text{op} } } \circ h^{\text{op} }
     |r = \paren {g \circ f}^{\text{op} } \circ h^{\text{op} }
     |c = {{Defof|Composition of Morphisms}}
}}
{{eqn|r = \paren {h \circ \paren {g \circ f} }^{\text{op} }
     |c = {{Defof|Composition of Morphisms}}
}}
{{eqn|r = \paren {\paren {h \circ g} \circ f}^{\text{op} }
     |c = Since $\mathbf C$ is a metacategory
}}
{{eqn|r = f^{\text{op} } \circ \paren {h \circ g}^{\text{op} }
}}
{{eqn|r = f^{\text{op} } \circ \paren {g^{\text{op} } \circ h^{\text{op} } }
}}
{{end-eqn}}
Hence $\mathbf C^{\text{op} }$ is a metacategory.
{{qed}}
Category:Dual Categories
qim8tqtx3c71651xncyrcmmqmryr5o0