avewright/proofwiki-math huggingface dataset:
Theorem: Infimum of Infima

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $\mathbb T$ be a collection of subsets of $S$.
Suppose all $T \in \mathbb T$ admit an infimum $\inf T$ in $S$.
Then:
:$\inf \bigcup \mathbb T = \inf \left\{{\inf T: T \in \mathbb T}\right\}$
as soon as one of these two quantities exists.

Proof:
Suppose that $s = \inf \bigcup \mathbb T \in S$.
By Set is Subset of Union, $T \subseteq \bigcup \mathbb T$ for all $T \in \mathbb T$.
Hence by Infimum of Subset:
:$\forall T \in \mathbb T: s \preceq \inf T$
Suppose now that $a \in S$ satisfies:
:$\forall T \in \mathbb T: a \preceq \inf T$
Then by transitivity of $\preceq$:
:$\forall t \in T: a \preceq t$
Since this holds for any $T \in \mathbb T$, also:
:$\forall t \in \bigcup \mathbb T: a \preceq t$
Hence $a \preceq s$, by definition of infimum.
That is, $s = \inf \left\{{\inf T: T \in \mathbb T}\right\}$.
{{qed|lemma}}
Suppose now that $r = \inf \left\{{\inf T: T \in \mathbb T}\right\} \in S$.
By definition of infimum, for all $T \in \mathbb T$ and $t \in T$:
:$\inf T \preceq t$
By transitivity of $\preceq$:
:$\forall T \in \mathbb T: \forall t \in T: r \preceq t$
Hence for all $t \in \bigcup \mathbb T$:
:$r \preceq t$
Suppose that $a \in S$ satisfies:
:$\forall t \in \bigcup \mathbb T: a \preceq t$
In particular, for any $T \in \mathbb T$, since $T \subseteq \bigcup \mathbb T$:
:$a \preceq \inf T$
and therefore by definition of infimum, also:
:$a \preceq r$
That is, $r = \inf \bigcup \mathbb T$.
{{qed}}
Category:Order Theory
fq5xoc97v99rszpr7xohflxeoe0z8e5
Theorem: Join Semilattice is Ordered Structure

Let $\struct {S, \vee, \preceq}$ be a join semilattice.
Then $\struct {S, \vee, \preceq}$ is an ordered structure.
That is, $\preceq$ is compatible with $\vee$.

Proof:
For $\struct {S, \vee, \preceq}$ to be an ordered structure is equivalent to, for all $a, b, c \in S$:
:$a \preceq b \implies a \vee c \preceq b \vee c$
:$a \preceq b \implies c \vee a \preceq c \vee b$
Since Join is Commutative, it suffices to prove the first of these implications.
By definition of join:
:$a \vee c = \sup \set {a, c}$
where $\sup$ denotes supremum.
By Join Succeeds Operands:
:$b \preceq b \vee c$
:$c \preceq b \vee c$
Now also $a \preceq b$, and by transitivity of $\preceq$ we find that:
:$a \preceq b \vee c$
Thus $b \vee c$ is an upper bound for $\set {a, c}$.
Hence:
:$a \vee c \preceq b \vee c$
by definition of supremum.
{{qed}}
Theorem: Join Semilattice is Ordered Structure

Let $\struct {S, \vee, \preceq}$ be a join semilattice.
Then $\struct {S, \vee, \preceq}$ is an ordered structure.
That is, $\preceq$ is compatible with $\vee$.

Proof:
Let $a, b, c \in S$.
Let $a \preceq b$.
By the definition of join semilattice:
:$a \vee b = b$
Thus:
:$\paren {a \vee b} \vee c = b \vee c$
Since $\vee$ is associative, commutative, and idempotent:
:$\paren {a \vee c} \vee \paren {b \vee c} = b \vee c$
Therefore, $a \vee c \preceq b \vee c$.
From Join is Commutative, we conclude that:
:$c \vee a \preceq c \vee b$
{{qed}}
Theorem: Meet Semilattice is Ordered Structure

Let $\struct {S, \wedge, \preceq}$ be a meet semilattice.
Then $\struct {S, \wedge, \preceq}$ is an ordered structure.

Proof:
For $\struct {S, \wedge, \preceq}$ to be an ordered structure is equivalent to, for all $a,b,c \in S$:
:$a \preceq b \implies a \wedge c \preceq b \wedge c$
:$a \preceq b \implies c \wedge a \preceq c \wedge b$
Since Meet is Commutative, it suffices to prove the first of these implications.
By definition of meet:
:$b \wedge c = \inf \set {b, c}$
where $\inf$ denotes infimum.
By Meet Precedes Operands:
:$a \wedge c \preceq a$
:$a \wedge c \preceq c$
Now also $a \preceq b$, and by transitivity of $\preceq$ we find that:
:$a \wedge c \preceq b$
Thus $a \wedge c$ is a lower bound for $\set {b, c}$.
Hence:
:$a \wedge c \preceq b \wedge c$
by definition of infimum.
{{qed}}
Theorem: Join Semilattice is Semilattice

Let $\struct {S, \vee, \preceq}$ be a join semilattice.
Then $\struct {S, \vee}$ is a semilattice.

Proof:
Recall the definition of join semilattice:
{{:Definition:Join Semilattice}}
By definition of join semilattice, $\vee$ is closed.
The other three defining properties for a semilattice follow respectively from:
:Join is Commutative
:Join is Associative
:Join is Idempotent
Hence $\struct {S, \vee}$ is a semilattice.
{{qed}}
Theorem: Meet Semilattice is Semilattice

Let $\struct {S, \wedge, \preceq}$ be a meet semilattice.
Then $\struct {S, \wedge}$ is a semilattice.

Proof:
By definition of meet semilattice, $\wedge$ is closed.
The other three defining properties for a semilattice follow respectively from:
:Meet is Commutative
:Meet is Associative
:Meet is Idempotent
Hence $\struct {S, \wedge}$ is a semilattice.
{{qed}}
Theorem: Semilattice Induces Ordering

Let $\struct {S, \circ}$ be a semilattice.
Let $\RR$ be the relation on $S$ defined by, for all $a, b \in S$:
:$a \mathrel \RR b$ {{iff}} $a \circ b = b$
Then $\RR$ is an ordering.

Proof:
Let us verify that $\RR$ satisfies the three conditions for an ordering.
Theorem: Elementary Row Operations Associate with Matrix Multiplication

Let $\struct {R, +, \circ}$ be a commutative ring.
Let $\mathbf A = \sqbrk a_{m n}$ be an $m \times n$ matrix over $R$.
Let $\mathbf B = \sqbrk b_{n p}$ be an $n \times p$ matrix over $R$.
Let $\hat o_1, \ldots, \hat o_{\hat n}$ be a finite sequence of elementary row operations that can be performed on a matrix over $R$ with $m$ rows.
Let $\mathbf A'$ denote the $m \times n$-matrix that results from using $\hat o_1, \ldots, \hat o_{\hat n}$ on $\mathbf A$.
Let $\mathbf C = \mathbf A \mathbf B$ be the matrix product of $\mathbf A$ and $\mathbf B$.
Let $\mathbf C'$ denote the $m \times p$-matrix that results from using $\hat o_1, \ldots, \hat o_{\hat n}$ on $\mathbf C$.
Then:
:$\mathbf C' = \mathbf A' \mathbf B$

Proof:
Proof by induction over $\hat n \in \N$, the number of elementary row operations.
Theorem: Union of Relations Compatible with Operation is Compatible

Let $\struct {S, \circ}$ be a closed algebraic structure.
Let $\FF$ be a family of relations on $S$.
Let each element of $\FF$ be compatible with $\circ$.
Let $\QQ = \bigcup \FF$.
Then $Q$ is a relation compatible with $\circ$.

Proof:
Let $x, y, z \in S$.
Let $x \mathrel \QQ y$.
Then for some $\RR \in \FF$:
:$x \mathrel \RR y$.
Since $\RR$ is a relation compatible with $\circ$:
:$\tuple {x \circ z} \mathrel \RR \tuple {y \circ z}$
Since $\RR \in \FF$:
:$\RR \subseteq \bigcup \FF = \QQ$
Thus 
:$\tuple {x \circ z} \mathrel \QQ \tuple {y \circ z}$
We have shown that:
:$\forall x, y, z \in S: x \mathrel \QQ y \implies \tuple {x \circ z} \mathrel \QQ \tuple {y \circ z}$
A similar argument shows that:
:$\forall x, y, z \in S: x \mathrel \QQ y \implies \tuple {z \circ x} \mathrel \QQ \tuple {z \circ y}$
So $Q$ is a relation compatible with $\circ$.
{{qed}}
Category:Compatible Relations
nyywugl78am4cwx9shqjs418r9rifbr
Theorem: Complement of Relation Compatible with Group is Compatible

Let $\struct {G, \circ}$ be a group.
Let $\RR$ be a relation on $G$.
Let $\RR$ be compatible with $\circ$.
Let $\QQ = \complement_{G \times G} \RR$, so that:
:$\forall a, b \in G: a \mathrel \QQ b \iff \neg \paren {a \mathrel \RR b}$
Then $\QQ$ is a relation compatible with $\circ$.

Proof:
Let $x, y, z \in G$.
Suppose that $\neg \paren {\paren {x \circ z} \mathrel \QQ \paren {y \circ z} }$.
Then by the definition of $\QQ$:
:$\paren {x \circ z} \mathrel \RR \paren {y \circ z}$
Because $\RR$ is compatible with $\circ$:
:$\paren {x \circ z} \circ z^{-1} \mathrel \RR \paren {y \circ z} \circ z^{-1}$
By {{Group-axiom|1}} and {{Group-axiom|3}}:
:$x \mathrel \RR y$
so by the definition of $\QQ$:
:$\neg \paren {x \mathrel \QQ y}$
By the Rule of Transposition:
:$\forall x, y, z \in G: x \mathrel \QQ y \implies \paren {x \circ z} \mathrel \QQ \paren {y \circ z}$
A similar argument shows that:
:$\forall x, y, z \in G: x \mathrel \QQ y \implies \paren {z \circ x} \mathrel \QQ \paren {z \circ y}$
Thus, by definition, $\QQ$ is a relation compatible with $\circ$.
{{qed}}
Category:Compatible Relations
Category:Group Theory
t1042u3hj54o94oxlal22oavv5us3fa
Theorem: Relation Compatible with Group Operation is Strongly Compatible

$\RR$ is strongly compatible with $\circ$:
:$\forall x, y, z \in G:$
::$x \mathrel \RR y \iff x \circ z \mathrel \RR y \circ z$
::$x \mathrel \RR y \iff z \circ x \mathrel \RR z \circ y$

Proof:
Since $\RR$ is compatible with $\circ$:
:$\forall a, b, c \in G: a \mathrel \RR b \implies a \circ c \mathrel \RR b \circ c$
In particular, letting $a = x$, $b = y$, and $c = z$, we see that:
:$x \mathrel \RR y \implies x \circ z \mathrel \RR y \circ z$
On the other hand, letting $a = x \circ z$, $b = y \circ z$, and $c = z^{-1}$, we see that:
:$x \circ z \mathrel \RR y \circ z \implies \paren {x \circ z} \circ z^{-1} \mathrel \RR \paren {y \circ z} \circ z^{-1}$
By the associativity of $\circ$ and the definition of inverse, this reduces to:
:$x \circ z \mathrel \RR y \circ z \implies x \mathrel \RR y$
We have thus shown that:
:$x \mathrel \RR y \iff x \circ z \mathrel \RR y \circ z$
A similar argument shows that:
:$x \mathrel \RR y \iff z \circ x \mathrel \RR z \circ y$
so $\RR$ is strongly compatible with $\circ$.
{{qed}}
Category:Relations Compatible with Group Operation
3fidc2c4nd2ztukpuogksye0qgwatd3
Theorem: Intersection of Relations Compatible with Operation is Compatible

Let $\struct {S, \circ}$ be a closed algebraic structure.
Let $\mathscr F$ be a indexed family of relations on $S$.
Suppose that each element of $\mathscr F$ is compatible with $\circ$.
Let $\QQ = \bigcap \mathscr F$ be the intersection of $\mathscr F$.
Then $\QQ$ is a relation compatible with $\circ$.

Proof:
Let $x, y, z \in S$.
Suppose that $x \mathrel \QQ y$.
Then for each $\RR \in \mathscr F$:
:$x \mathrel \RR y$
Then since $\RR$ is a relation compatible with $\circ$:
:$\paren {x \circ z} \mathrel \RR \paren {y \circ z}$
Since this holds for each $\RR \in \mathscr F$:
:$\paren {x \circ z} \mathrel \QQ \paren {y \circ z}$
We have shown that:
:$\forall x, y, z \in S: x \mathrel \QQ y \implies \paren {x \circ z} \mathrel \QQ \paren {y \circ z}$
A similar argument shows that:
:$\forall x, y, z \in S: x \mathrel \QQ y \implies \paren {z \circ x} \mathrel \QQ \paren {z \circ y}$
so $Q$ is a relation compatible with $\circ$.
{{qed}}
Category:Compatible Relations
6ahue29b035401wxcwed9oazy028n3m
Theorem: Inverse of Relation Compatible with Operation is Compatible

Let $\struct {S, \circ}$ be a closed algebraic structure.
Let $\RR$ be a relation on $S$ which is compatible with $\circ$.
Let $\QQ$ be the inverse relation of $\RR$.
Then $\QQ$ is compatible with $\circ$.

Proof:
Let $x, y, z \in S$.
Suppose that $x \mathrel \QQ y$.
Then by the definition of $\QQ$:
:$y \mathrel \RR x$.
Since $\RR$ is compatible with $\circ$:
:$\paren {y \circ z} \mathrel \RR \paren {x \circ z}$
and
:$\paren {z \circ y} \mathrel \RR \paren {z \circ x}$
Thus by the definition of $\QQ$:
:$\paren {x \circ z} \mathrel \QQ \paren {y \circ z}$
and
:$\paren {z \circ x} \mathrel \RR \paren {z \circ y}$
Thus $\QQ$ is compatible with $\circ$.
{{qed}}
Category:Compatible Relations
0u3weabzc3s18lsaglvdwpa9na99e0e
Theorem: Ordering Compatible with Group Operation is Strongly Compatible

{{begin-eqn}}
{{eqn | q = \forall x, y, z \in G
      | l = x \preccurlyeq y
      | o = \iff
      | r = x \circ z \preccurlyeq y \circ z
}}
{{eqn | l = x \preccurlyeq y
      | o = \iff
      | r = z \circ x \preccurlyeq z \circ y
}}
{{eqn | l = x \prec y
      | o = \iff
      | r = x \circ z \prec y \circ z
}}
{{eqn | l = x \preceq y
      | o = \iff
      | r = z \circ x \prec z \circ y
}}
{{end-eqn}}

Proof:
By definition of ordered group, $\preccurlyeq$ is a relation compatible with $\circ$.
Thus by Relation Compatible with Group Operation is Strongly Compatible:
{{begin-eqn}}
{{eqn | l = x \preccurlyeq y
      | o = \iff
      | r = x \circ z \preccurlyeq y \circ z
}}
{{eqn | l = x \preccurlyeq y
      | o = \iff
      | r = z \circ x \preccurlyeq z \circ y
}}
{{end-eqn}}
By Reflexive Reduction of Relation Compatible with Group Operation is Compatible, $\prec$ is compatible with $\circ$.
Thus again by Relation Compatible with Group Operation is Strongly Compatible:
{{begin-eqn}}
{{eqn | l = x \prec y
      | o = \iff
      | r = x \circ z \prec y \circ z
}}
{{eqn | l = x \preceq y
      | o = \iff
      | r = z \circ x \prec z \circ y
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Ordering Compatible with Group Operation is Strongly Compatible

{{begin-eqn}}
{{eqn | q = \forall x, y, z \in G
      | l = x \preccurlyeq y
      | o = \iff
      | r = x \circ z \preccurlyeq y \circ z
}}
{{eqn | l = x \preccurlyeq y
      | o = \iff
      | r = z \circ x \preccurlyeq z \circ y
}}
{{eqn | l = x \prec y
      | o = \iff
      | r = x \circ z \prec y \circ z
}}
{{eqn | l = x \preceq y
      | o = \iff
      | r = z \circ x \prec z \circ y
}}
{{end-eqn}}

Proof:
By the definition of an ordered group, $\preccurlyeq$ is a relation compatible with $\circ$.
Thus by {{Corollary|Relation Compatible with Group Operation is Strongly Compatible}}, we obtain the first four results.
By Reflexive Reduction of Relation Compatible with Group Operation is Compatible, $\prec$ is compatible with $\circ$.
Again by {{Corollary|Relation Compatible with Group Operation is Strongly Compatible}}, we obtain the remaining results.
{{qed}}
Theorem: Ordering Compatible with Group Operation is Strongly Compatible

{{begin-eqn}}
{{eqn | q = \forall x, y, z \in G
      | l = x \preccurlyeq y
      | o = \iff
      | r = x \circ z \preccurlyeq y \circ z
}}
{{eqn | l = x \preccurlyeq y
      | o = \iff
      | r = z \circ x \preccurlyeq z \circ y
}}
{{eqn | l = x \prec y
      | o = \iff
      | r = x \circ z \prec y \circ z
}}
{{eqn | l = x \preceq y
      | o = \iff
      | r = z \circ x \prec z \circ y
}}
{{end-eqn}}

Proof:
Each result follows from Ordering Compatible with Group Operation is Strongly Compatible.
For example, by Ordering Compatible with Group Operation is Strongly Compatible:
:$x \preccurlyeq y \iff x \circ x^{-1} \preccurlyeq y \circ x^{-1}$
Since $x \circ x^{-1} = e$:
:$x \preccurlyeq y \iff e \preccurlyeq y \circ x^{-1}$
{{qed}}
Theorem: Relations Compatible with Operation Form Complete Distributive Lattice

Let $\struct {S, \circ}$ be an algebraic structure.
Let $C$ be the set of relations on $S$ compatible with $\circ$.
Then $\struct {C, \cap, \cup, \subseteq}$ is a complete distributive lattice.

Proof:
{{ProofWanted}}
Category:Compatible Relations
Category:Complete Lattices
Category:Distributive Lattices
poocmfwwi4z2mb95eaedgnbgag5sxt3
Theorem: Relations Compatible with Group Form Complete Boolean Algebra

Let $\struct {S, \circ}$ be a group.
Let $C$ be the set of relations on $S$ which are compatible with $\circ$.
Then $\struct {C, \cap, \cup, \subseteq}$ is a complete Boolean lattice.

Proof:
{{ProofWanted}}
Category:Compatible Relations
Category:Complete Lattices
Category:Boolean Lattices
tbnnoumtcegy19fm00qmai3k9d785za
Theorem: Hypothetical Syllogism/Formulation 3

:$\vdash \paren {\paren {p \implies q} \land \paren {q \implies r} } \implies \paren {p \implies r}$

Proof:
Let us use the following abbreviations:
{{begin-eqn}}
{{eqn | l = \phi
      | o = \text{ for }
      | r = p \implies q
      | c = 
}}
{{eqn | l = \psi
      | o = \text{ for }
      | r = q \implies r
      | c = 
}}
{{eqn | l = \chi
      | o = \text{ for }
      | r = p \implies r
      | c = 
}}
{{end-eqn}}
{{BeginTableau|\vdash \paren {\phi \land \psi} \implies \chi}}
{{Assumption|1|\phi \land \psi}}
{{Simplification|2|1|\phi|1|1}}
{{Simplification|3|1|\psi|1|2}}
{{SequentIntro|4|1|\chi|2, 3|{{Formulation|Hypothetical Syllogism|1}}}}
{{Implication|5||\paren {\phi \land \psi} \implies \chi|1|4}}
{{EndTableau}}
Expanding the abbreviations leads us back to:
:$\paren {\paren {p \implies q} \land \paren {q \implies r} } \implies \paren {p \implies r}$
{{qed}}
Theorem: Hypothetical Syllogism/Formulation 3

:$\vdash \paren {\paren {p \implies q} \land \paren {q \implies r} } \implies \paren {p \implies r}$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccccc|c|ccc|} \hline
((p & \implies & q) & \land & (q & \implies & r)) & \implies & (p & \implies & r) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \F & \T & \T & \T & \F & \T & \T \\
\F & \T & \T & \T & \T & \F & \F & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \T & \F & \F \\
\T & \F & \F & \T & \F & \T & \T & \T & \T & \T & \T \\
\T & \T & \T & \F & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Hypothetical Syllogism/Formulation 4

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

Proof:
Let us use the following abbreviations
{{begin-eqn}}
{{eqn | l = \phi
      | o = \text{ for }
      | r = p \implies q
}}
{{eqn | l = \psi
      | o = \text{ for }
      | r = q \implies r
}}
{{eqn | l = \chi
      | o = \text{ for }
      | r = p \implies r
}}
{{end-eqn}}
{{BeginTableau|\paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} } }}
{{TheoremIntro|1|\paren {\phi \land \psi} \implies \chi|Hypothetical Syllogism: Formulation 3}}
{{SequentIntro|2||\phi \implies \paren {\psi \implies \chi}|1|Rule of Exportation}}
{{EndTableau}}
Expanding the abbreviations leads us back to:
:$\vdash \paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} }$
{{qed}}
Theorem: Hypothetical Syllogism/Formulation 4

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

Proof:
{{BeginTableau|\paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} } }}
{{Assumption|1|p \implies q}}
{{Assumption|2|p}}
{{Assumption|3|q \implies r}}
{{ModusPonens|4|1,2|q|1|2}}
{{ModusPonens|5|1,2,3|r|3|4}}
{{Implication|6|1,3|p \implies r|2|5}}
{{Implication|7|1|\paren {q \implies r} \implies \paren {p \implies r}|3|6}}
{{Implication|8||\paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} }|1|7}}
{{EndTableau|qed}}
Theorem: Hypothetical Syllogism/Formulation 4

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

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} }|instance 1 of a Hilbert proof system}}
{{Assumption|1|p}}
{{Assumption|2|p \implies q}}
{{ModusPonens|3|1, 2|q|1|2}}
{{Assumption|4|q \implies r}}
{{ModusPonens|5|1, 2, 4|r|3|4}}
{{TableauLine|n = 6
  | pool = 2, 4
  | f = p \implies r
  | rlnk = Deduction Theorem
  | rtxt = Deduction Theorem
  | dep  = 1, 5
  | c = Assumption $1$ has been discharged
}}
{{TableauLine|n = 7
  | pool = 2
  | f = \paren {q \implies r} \implies \paren {p \implies r}
  | rlnk = Deduction Theorem
  | rtxt = Deduction Theorem
  | dep  = 4, 6
  | c = Assumption $4$ has been discharged
}}
{{TableauLine|n = 8
  | f = \paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} }
  | rlnk = Deduction Theorem
  | rtxt = Deduction Theorem
  | dep  = 2, 7
  | c = Assumption $2$ has been discharged
}}
{{EndTableau|qed}}
Theorem: Hypothetical Syllogism/Formulation 5

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

Proof:
Let us use the following abbreviations
{{begin-eqn}}
{{eqn | l = \phi
      | o = \text{ for }
      | r = p \implies q
      | c = 
}}
{{eqn | l = \psi
      | o = \text{ for }
      | r = q \implies r
      | c = 
}}
{{eqn | l = \chi
      | o = \text{ for }
      | r = p \implies r
      | c = 
}}
{{end-eqn}}
From Hypothetical Syllogism: Formulation 3 we have:
:$(1): \quad \vdash \paren {\paren {p \implies q} \land \paren {q \implies r} } \implies \paren {p \implies r}$
{{BeginTableau|\paren {q \implies r} \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} } }}
{{Assumption|1|\psi \land \phi}}
{{Commutation|2|1|\phi \land \psi|1|Conjunction}}
{{SequentIntro|3|1|\chi|2|Hypothetical Syllogism: Formulation 3 (see $(1)$ above)}}
{{Implication|4||\paren {\psi \land \phi} \implies \chi|1|3}}
{{SequentIntro|5||\psi \implies \paren {\phi \implies \chi}|4|Rule of Exportation}}
{{EndTableau}}
Expanding the abbreviations leads us back to:
:$\vdash \paren {q \implies r} \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }$
{{qed}}
Theorem: Hypothetical Syllogism/Formulation 5

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

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

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

Proof:
{{BeginTableau|\vdash \paren {q \implies r} \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} } }}
{{Assumption|1|q \implies r}}
{{Assumption|2|p \implies q}}
{{Assumption|3|p}}
{{ModusPonens|4|2,3|q|2|3}}
{{ModusPonens|5|1,2,3|r|1|4}}
{{Implication|6|1,2|p \implies r|3|5}}
{{Implication|7|1|\paren {p \implies q} \implies \paren {p \implies r}|2|6}}
{{Implication|8||\paren {q \implies r} \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }|1|7}}
{{EndTableau|qed}}
Theorem: Duality Principle (Order Theory)/Global Duality

The following are equivalent:
:$(1): \quad \Sigma$ is true for all ordered sets
:$(2): \quad \Sigma^*$ is true for all ordered sets

Proof:
=== $(1)$ implies $(2)$ ===
Let $\struct {S, \preceq}$ be an ordered set.
Let $\struct {S, \succeq}$ be its dual.
By assumption, $\Sigma$ is true for $\struct {S, \succeq}$.
By Local Duality, this implies $\Sigma^*$ is true for $\struct {S, \preceq}$.
Since $\struct {S, \preceq}$ was arbitrary, the result follows.
{{qed}}
Theorem: Duality Principle (Order Theory)/Local Duality

Let $\struct {S, \preceq}$ be an ordered set, and let $\struct {S, \succeq}$ be its dual.
Then the following are equivalent:
:$(1): \quad \Sigma$ is true for $\struct {S, \preceq}$
:$(2): \quad \Sigma^*$ is true for $\struct {S, \succeq}$

Proof:
=== $(1)$ implies $(2)$ ===
By assumption, $\Sigma$ is true for $\struct {S, \preceq}$.
By Dual of Dual Ordering, the dual statement $\Sigma^*$ applied to $\struct {S, \succeq}$ is the same as $\Sigma$ applied to $\struct {S, \preceq}$.
Hence $\Sigma^*$ is true for $\struct {S, \succeq}$.
{{qed|lemma}}
Theorem: Diagonal Complement Relation Compatible with Group Operation

Let $\left({G, \circ}\right)$ be a group.
Let $\Delta_G$ be the diagonal relation on $G$.
Then $\Delta_G^c = \complement_{G \times G} \Delta_G$ is a relation compatible with $\circ$.
{{explain|Find another way to write the above, it's ugly}}
In other words, $\ne$ is a relation compatible with $\circ$.

Proof:
By Diagonal Relation is Universally Compatible, $\Delta_G$ is compatible with $\circ$.
By Complement of Relation Compatible with Group is Compatible , $\Delta_G^c$ is also compatible with $\circ$.
{{qed}}
Category:Compatible Relations
n07d4bm10j5n1oe24z8vocmgjasgc45