avewright/proofwiki-math huggingface dataset:
Theorem: Set Difference of Cartesian Products

:$\paren {S_1 \times S_2} \setminus \paren {T_1 \times T_2} = \paren {S_1 \times \paren {S_2 \setminus T_2} } \cup \paren {\paren {S_1 \setminus T_1} \times S_2}$

Proof:
Let $\tuple {x, y} \in \paren {S_1 \times S_2} \setminus \paren {T_1 \times T_2}$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {x, y} \in S_1 \times S_2
      | o = \land
      | r = \tuple {x, y} \notin T_1 \times T_2
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \in S_1 \land y \in S_2
      | o = \land
      | r = \neg \paren {x \in T_1 \land y \in T_2}
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \in S_1 \land y \in S_2
      | o = \land
      | r = \paren {x \notin T_1 \lor y \notin T_2}
      | c = De Morgan's Laws: Disjunction of Negations
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x \in S_1 \land y \in S_2 \land x \notin T_1}
      | o = \lor
      | r = \paren {x \in S_1 \land y \in S_2 \land y \notin T_2}
      | c = Rule of Distribution
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x \in S_1 \setminus T_1 \land y \in S_2}
      | o = \lor
      | r = \paren {x \in S_1 \land y \in S_2 \setminus T_2}
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {\tuple {x, y} \in \paren {S_1 \setminus T_1} \times S_2}
      | o = \lor
      | r = \paren {\tuple {x, y} \in S_1 \times \paren {S_2 \setminus T_2} }
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {x, y}
      | o = \in
      | r = \paren {S_1 \times \paren {S_2 \setminus T_2} } \cup \paren {\paren {S_1 \setminus T_1} \times S_2}
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
The result follows from the definition of subset and set equality.
{{qed}}
Theorem: Inverse of Inverse Relation

The inverse of an inverse relation is the relation itself:
:$\paren {\RR^{-1} }^{-1} = \RR$

Proof:
{{begin-eqn}}
{{eqn | l = \tuple {s, t}
      | o = \in
      | r = \RR
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {t, s}
      | o = \in
      | r = \RR^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {s, t}
      | o = \in
      | r = \paren {\RR^{-1} }^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Diagonal Relation is Equivalence

The diagonal relation $\Delta_S$ on a set $S$ is always an equivalence in $S$.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Trivial Relation is Equivalence

The trivial relation on $S$:
:$\RR = S \times S$
is always an equivalence in $S$.

Proof:
Let us verify the conditions for an equivalence in turn.
Theorem: Equality of Relations

Let $\RR_1$ and $\RR_2$ be relations on $S_1 \times T_1$ and $S_2 \times T_2$ respectively.
Then $\RR_1$ and $\RR_2$ are '''equal''' {{iff}}:
:$S_1 = S_2$
:$T_1 = T_2$
:$\tuple {s, t} \in \RR_1 \iff \tuple {s, t} \in \RR_2$
It is worth labouring the point that for two relations to be '''equal''', not only must their domains be equal, but so must their codomains.

Proof:
This follows from set equality and Equality of Ordered Pairs.
A '''relation''' on $S \times T$ is an ordered triple, thus:
{{begin-eqn}}
{{eqn | l = \RR_1
      | r = \tuple {S_1, T_1, R_1}
      | c = where $R_1 \subseteq S_1 \times T_1$
}}
{{eqn | l = \RR_2
      | r = \tuple {S_2, T_2, R_2}
      | c = where $R_2 \subseteq S_2 \times T_2$
}}
{{end-eqn}}
From Equality of Ordered Tuples, $\RR_1 = \RR_1$ {{iff}}:
{{begin-eqn}}
{{eqn | l = S_1
      | r = S_2
}}
{{eqn | l = T_1
      | r = T_2
}}
{{eqn | l = R_1
      | r = R_2
}}
{{end-eqn}}
Then we have that $R_1$ and $R_2$ are sets of ordered pairs.
Thus by definition of set equality:
:$R_1 = R_2 \iff \paren {\forall \tuple {x, y} \in \S_1 \times T_2: \tuple {x, y} \in R_1 \iff \tuple {x, y} \in R_2}$
Hence the result.
{{Qed}}
Theorem: Image of Singleton under Relation

Let $\RR \subseteq S \times T$ be a relation.
Then the image of an element of $S$ is equal to the image of a singleton containing that element, the singleton being a subset of $S$:
:$\forall s \in S: \map \RR s = \RR \sqbrk {\set s}$

Proof:
We have the definitions:
{{begin-eqn}}
{{eqn | l = \map \RR s
      | r = \set {t \in T: \tuple {s, t} \in \RR}
      | c = {{Defof|Image of Element under Relation}}
}}
{{eqn | l = \RR \sqbrk {\set s}
      | r = \set {t \in T: \exists s \in \set s: \tuple {s, t} \in \RR}
      | c = {{Defof|Image of Subset under Relation}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = t  
      | o = \in
      | r = \map \RR s
}}
{{eqn | ll= \leadsto
      | l = \tuple {s, t}
      | o = \in
      | r = \RR
}}
{{eqn | ll= \leadsto
      | q = \exists s \in \set s
      | l = \tuple {s, t}
      | o = \in
      | r = \RR
      | c = {{Defof|Singleton}}
}}
{{eqn | ll= \leadsto
      | l = t
      | o = \in
      | r = \RR \sqbrk {\set s}
}}
{{eqn | ll= \leadsto
      | l = \map \RR s
      | o = \subseteq
      | r = \RR \sqbrk {\set s}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = t
      | o = \in
      | r = \RR \sqbrk {\set s}
}}
{{eqn | ll= \leadsto
      | q = \exists s \in \set s
      | l = \tuple {s, t}
      | o = \in
      | r = \RR
}}
{{eqn | ll= \leadsto
      | l = \tuple {s, t}
      | o = \in
      | r = \RR
      | c = as $r \in \set s \implies r = s$ by Singleton Equality
}}
{{eqn | ll= \leadsto
      | l = t
      | o = \in
      | r = \map \RR s
}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk {\set s}
      | o = \subseteq
      | r = \map \RR s
}}
{{end-eqn}}
Finally:
:$\map \RR s = \RR \sqbrk {\set s}$
by definition of set equality.
{{Qed}}
Category:Relation Theory
Category:Singletons
th8xh97568mahbktw62z5jw9wag3j88
Theorem: Image of Subset under Relation is Subset of Image

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation from $S$ to $T$.
Let $A, B \subseteq S$ such that $A \subseteq B$.
Then the image of $A$ is a subset of the image of $B$:
:$A \subseteq B \implies \RR \sqbrk A \subseteq \RR \sqbrk B$
In the notation of direct image mappings, this can be written:
:$A \subseteq B \implies \map {\RR^\to} A \subseteq \map {\RR^\to} B$

Proof:
Suppose $\RR \sqbrk A \nsubseteq \RR \sqbrk B$.
{{begin-eqn}}
{{eqn | l = \RR \sqbrk A
      | o = \nsubseteq
      | r = \RR \sqbrk B
}}
{{eqn | ll= \leadsto
      | q = \exists t \in \RR \sqbrk A: \exists \tuple {s, t} \in \RR
      | l = s
      | o = \notin
      | r = B
      | c = {{Defof|Image of Subset under Relation}}
}}
{{eqn | ll= \leadsto
      | q = \exists s \notin B
      | l = s
      | o = \in
      | r = A
      | c = {{Defof|Ordered Pair}}
}}
{{eqn | ll= \leadsto
      | l = A
      | o = \nsubseteq
      | r = B
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
The result follows by the Rule of Transposition.
{{qed}}
Theorem: Image of Element is Subset

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $A \subseteq S$.
Then:
:$s \in A \implies \map \RR s \subseteq \RR \sqbrk A$

Proof:
From Image of Singleton under Relation:
:$\map \RR s = \RR \sqbrk {\set s}$
From Singleton of Element is Subset:
:$s \in A \implies \set s \subseteq A$
The result follows from Image of Subset is Subset of Image.
{{qed}}
Category:Relation Theory
81ns2wlo73dzga5xv99qsw98k988h3w
Theorem: Image is Subset of Codomain

Let $\RR = S \times T$ be a relation.
For all subsets $A$ of the domain of $\RR$, the image of $A$ is a subset of the codomain of $\RR$:
:$\forall A \subseteq \Dom \RR: \RR \sqbrk A \subseteq T$
In the notation of direct image mappings, this can be written as:
:$\forall A \in \powerset S: \map {\RR^\to} A \in \powerset T$

Proof:
{{begin-eqn}}
{{eqn | l = A
      | o = \subseteq
      | r = \Dom \RR
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk A
      | o = \subseteq
      | r = \Img \RR
      | c = Image of Subset is Subset of Image
}}
{{eqn | o = \subseteq
      | r = T
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Relation Theory
hy4x25yvdjd9rj1cqotvh3g8hhde5km
Theorem: Image of Empty Set is Empty Set

Let $\RR \subseteq S \times T$ be a relation.
The image of the empty set is the empty set:
:$\RR \sqbrk \O = \O$

Proof:
{{begin-eqn}}
{{eqn | l = \RR \sqbrk \O
      | r = \set {t \in \Rng \RR: \exists s \in \O: \tuple {s, t} \in \RR}
      | c = {{Defof|Image of Subset under Relation}}
}}
{{eqn | l = \neg \exists s
      | o = \in
      | r = \O
      | c = {{Defof|Empty Set}}
}}
{{eqn | ll= \leadsto
      | l = \neg \exists t
      | o = \in
      | r = \set {t \in \Rng \RR: \exists s \in \O: \tuple {s, t} \in \RR}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk \O
      | r = \O
      | c = {{Defof|Empty Set}}
}}
{{end-eqn}}
{{qed}}
Category:Image of Empty Set is Empty Set
Category:Empty Set
Category:Images
Category:Relation Theory
mlvagi3tkp7kr284qsjxbhli6ndm7h9
Theorem: Domain of Composite Relation

Let $\RR_2 \circ \RR_1$ be a composite relation.
Then the domain of $\RR_2 \circ \RR_1$ is the domain of $\RR_1$:
{{Mistake|All that can be said is that the domain of the composition is a subset of the domain of the first relation}}
:$\Dom {\RR_2 \circ \RR_1} = \Dom {\RR_1}$

Proof:
Let $\RR_1 \subseteq S_1 \times S_2$ and $\RR_2 \subseteq S_2 \times S_3$.
The domain of $\RR_1$ is $S_1$.
The composite of $\RR_1$ and $\RR_2$ is defined as:
:$\RR_2 \circ \RR_1 = \set {\tuple {x, z}: x \in S_1, z \in S_3: \exists y \in S_2: \tuple {x, y} \in \RR_1 \land \tuple {y, z} \in \RR_2}$
From this definition:
:$\RR_2 \circ \RR_1 \subseteq S_1 \times S_3$.
Thus the domain of $\RR_2 \circ \RR_1$ is $S_1$.
Thus:
:$\Dom {\RR_2 \circ \RR_1} = S_1 = \Dom {\RR_1}$
{{qed}}
Category:Composite Relations
j6vkyb0twgvwmz8hcfqbarg1p7uy9zq
Theorem: Codomain of Composite Relation

Let $\RR_2 \circ \RR_1$ be a composite relation.
Then the codomain of $\RR_2 \circ \RR_1$ is the codomain of $\RR_2$:
:$\Cdm {\RR_2 \circ \RR_1} = \Cdm {\RR_2}$

Proof:
Let $\RR_1 \subseteq S_1 \times S_2$ and $\RR_2 \subseteq S_2 \times S_3$.
The codomain of $\RR_2$ is $S_3$.
The composite of $\RR_1$ and $\RR_2$ is defined as:
:$\RR_2 \circ \RR_1 = \set {\tuple {x, z}: x \in S_1, z \in S_3: \exists y \in S_2: \tuple {x, y} \in \RR_1 \land \tuple {y, z} \in \RR_2}$
From this definition:
:$\RR_2 \circ \RR_1 \subseteq S_1 \times S_3$
Thus the codomain of $\RR_2 \circ \RR_1$ is $S_3$.
Thus:
:$\Cdm {\RR_2 \circ \RR_1} = S_3 = \Cdm {\RR_2}$
{{qed}}
Category:Composite Relations
1ud451rt4knvb7jiqbis137ljeuaqx9
Theorem: Preimage of Mapping equals Domain

The preimage of a mapping is the same set as its domain:
:$\Preimg f = \Dom f$

Proof:
Let $f \subseteq S \times T$ be a mapping.
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = \forall x \in S: \exists y \in T: \tuple {x, y} \in f
      | c = {{Defof|Mapping}}
}}
{{eqn | o = \leadsto
      | r = \forall x \in S: x \in \Preimg f
      | c = {{Defof|Preimage of Mapping}}
}}
{{eqn | o = \leadsto
      | r = S \subseteq \Preimg f
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
From Preimage of Relation is Subset of Domain, we have that $\Preimg f \subseteq S$.
The result follows from the definition of set equality.
{{qed}}
Category:Preimages under Mappings
Category:Domains of Mappings
62wk8qbb9tf9lqnn18jrcx5eu5z50a4
Theorem: Preimage of Relation is Subset of Domain

Let $\RR \subseteq S \times T$ be a relation.
Then the preimage of $\RR$ is a subset of its domain:
:$\Preimg \RR \subseteq S$

Proof:
The preimage of $\RR$ is defined as:
:$\Preimg \RR = \set {s \in \Dom \RR: \exists t \in \Rng \RR: \tuple {s, t} \in \RR}$
Hence:
{{begin-eqn}}
{{eqn | l = s
      | o = \in
      | r = \Preimg \RR
}}
{{eqn | ll= \leadsto
      | l = s
      | o = \in
      | r = \Dom \RR
      | c = {{Defof|Preimage of Relation}}
}}
{{eqn | ll= \leadsto
      | l = \Preimg \RR
      | o = \subseteq
      | r = \Dom \RR
      | c = Subset of Set with Propositional Function
}}
{{end-eqn}}
{{qed}}
Category:Relation Theory
eqytitn4gsyklkuqcgder77er7i40q3
Theorem: Preimage of Image under Left-Total Relation is Superset

Let $\RR \subseteq S \times T$ be a left-total relation.
Then:
:$A \subseteq S \implies A \subseteq \paren {\RR^{-1} \circ \RR} \sqbrk A$
where:
:$\RR \sqbrk A$ denotes the image of $A$ under $\RR$
:$\RR^{-1} \sqbrk A$ denotes the preimage of $A$ under $\RR$
:$\RR^{-1} \circ \RR$ denotes composition of $\RR^{-1}$ and $\RR$.
This can be expressed in the language and notation of direct image mappings and inverse image mappings as:
:$\forall A \in \powerset S: A \subseteq \map {\paren {\RR^\gets \circ \RR^\to} } A$

Proof:
Suppose $A \subseteq S$.
We have:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = A
}}
{{eqn | ll= \leadsto
      | l = \set x
      | o = \subseteq
      | r = A
      | c = Singleton of Element is Subset
}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk {\set x}
      | o = \subseteq
      | r = \RR \sqbrk A
      | c = Image of Subset under Relation is Subset of Image
}}
{{eqn | ll= \leadsto
      | l = \RR^{-1} \sqbrk {\RR \sqbrk {\set x} }
      | o = \subseteq
      | r = \RR^{-1} \sqbrk {\RR \sqbrk A}
      | c = {{Corollary|Image of Subset under Relation is Subset of Image|1}}
}}
{{end-eqn}}
Then we have that $\RR$ is a left-total relation.
Thus:
:$\exists t \in T: \tuple {x, t} \in \RR$
Hence by definition of inverse relation:
:$\exists t \in T: \tuple {t, x} \in \RR^{-1}$
Hence:
{{begin-eqn}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \RR^{-1} \sqbrk {\RR \sqbrk A}
      | c = {{Defof|Relation}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \paren {\RR^{-1} \circ \RR} \sqbrk A
      | c = {{Defof|Composition of Relations}}
}}
{{end-eqn}}
So by definition of subset:
:$A \subseteq S \implies A \subseteq \paren {\RR^{-1} \circ \RR} \sqbrk A$
{{qed}}
Theorem: Inverse of Composite Relation

Let $\RR_2 \circ \RR_1 \subseteq S_1 \times S_3$ be the composite of the two relations $\RR_1 \subseteq S_1 \times S_2$ and $\RR_2 \subseteq S_2 \times S_3$.
Then:
:$\paren {\RR_2 \circ \RR_1}^{-1} = \RR_1^{-1} \circ \RR_2^{-1}$

Proof:
Let $\RR_1 \subseteq S_1 \times S_2$ and $\RR_2 \subseteq S_2 \times S_3$ be relations.
We assume that:
:$\Dom {\RR_2} = \Cdm {\RR_1}$
where $\Dom \RR$ denotes domain and $\Cdm \RR$ denotes codomain of a relation $\RR$.
This is necessary for $\RR_2 \circ \RR_1$ to exist.
From the definition of an inverse relation, we have:
:$\Dom {\RR_2} = \Cdm {\RR_2^{-1} }$
:$\Cdm {\RR_1} = \Dom {\RR_1^{-1} }$
So we confirm that $\RR_1^{-1} \circ \RR_2^{-1}$ is defined.
{{begin-eqn}}
{{eqn | l = \RR_2 \circ \RR_1
      | r = \set {\tuple {x, z}: x \in S_1, z \in S_3: \exists y \in S_2: \tuple {x, y} \in \RR_1 \land \tuple {y, z} \in \RR_2}
      | c = {{Defof|Composition of Relations}}
}}
{{eqn | ll= \leadsto
      | l = \paren {\RR_2 \circ \RR_1}^{-1}
      | r = \set {\tuple {z, x}: \tuple {x, z} \in \RR_2 \circ \RR_1}
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | r = \set {\tuple {z, x}: x \in S_1, z \in S_3: \exists y \in S_2: \tuple {x, y} \in \RR_1 \land \tuple {y, z} \in \RR_2}
      | c = {{Defof|Composition of Relations}}
}}
{{eqn | r = \set {\tuple {z, x}: z \in S_3, x \in S_1: \exists y \in S_2: \tuple {z, y} \in \RR_2^{-1} \land \tuple {y, x} \in \RR_1^{-1} }
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | r = \RR_1^{-1} \circ \RR_2^{-1}
      | c = {{Defof|Composition of Relations}}
}}
{{end-eqn}}
{{qed}}
Theorem: Image of Union under Relation

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $S_1$ and $S_2$ be subsets of $S$.
Then:
:$\RR \sqbrk {S_1 \cup S_2} = \RR \sqbrk {S_1} \cup \RR \sqbrk {S_2}$
That is, the image of the union of subsets of $S$ is equal to the union of their images.

Proof:
{{begin-eqn}}
{{eqn | l = t
      | o = \in
      | r = \RR \sqbrk {S_1 \cup S_2}
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists s \in S_1 \cup S_2
      | l = t
      | o = \in
      | r = \RR \sqbrk s
      | c = {{Defof|Image of Subset under Relation}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists s: s \in S_1 \lor s \in S_2
      | l = t
      | o = \in
      | r = \RR \sqbrk s
      | c = {{Defof|Set Union}}
}}
{{eqn | ll= \leadstoandfrom
      | l = t
      | o = \in
      | r = \RR \sqbrk {S_1}
      | c = {{Defof|Image of Subset under Relation}}
}}
{{eqn | lo= \lor
      | l = t
      | o = \in
      | r = \RR \sqbrk {S_2}
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = t
      | o = \in
      | r = \RR \sqbrk {S_1} \cup \RR \sqbrk {S_2}
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Image of Intersection under Relation

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $S_1$ and $S_2$ be subsets of $S$.
Then:
:$\RR \sqbrk {S_1 \cap S_2} \subseteq \RR \sqbrk {S_1} \cap \RR \sqbrk {S_2}$
That is, the image of the intersection of subsets of $S$ is a subset of the intersection of their images.

Proof:
{{begin-eqn}}
{{eqn | l = S_1 \cap S_2
      | o = \subseteq
      | r = S_1
      | c = Intersection is Subset
}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk {S_1 \cap S_2}
      | o = \subseteq
      | r = \RR \sqbrk {S_1}
      | c = Image of Subset is Subset of Image
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = S_1 \cap S_2
      | o = \subseteq
      | r = S_2
      | c = Intersection is Subset
}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk {S_1 \cap S_2}
      | o = \subseteq
      | r = \RR \sqbrk {S_2}
      | c = Image of Subset is Subset of Image
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk {S_1 \cap S_2}
      | o = \subseteq
      | r = \RR \sqbrk {S_1} \cap \RR \sqbrk {S_2}
      | c = Intersection is Largest Subset
}}
{{end-eqn}}
{{qed}}
Theorem: Image of Set Difference under Relation

Let $\RR \subseteq S \times T$ be a relation.
Let $A$ and $B$ be subsets of $S$.
Then:
:$\RR \sqbrk A \setminus \RR \sqbrk B \subseteq \RR \sqbrk {A \setminus B}$
where:
:$\setminus$ denotes set difference
:$\RR \sqbrk A$ denotes image of $A$ under $\RR$.

Proof:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \RR \sqbrk A \setminus \RR \sqbrk B
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists x \in A: x \notin B
      | l = \tuple {x, y}
      | o = \in
      | r = \RR
      | c = {{Defof|Image of Subset under Relation}}
}}
{{eqn | ll= \leadsto
      | q = \exists x \in A \setminus B
      | l = \tuple {x, y}
      | o = \in
      | r = \RR
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = \RR \sqbrk {A \setminus B}
      | c = {{Defof|Image of Subset under Relation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Preimage of Union under Relation

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $T_1$ and $T_2$ be subsets of $T$.
Then:
:$\RR^{-1} \sqbrk {T_1 \cup T_2} = \RR^{-1} \sqbrk {T_1} \cup \RR^{-1} \sqbrk {T_2}$

Proof:
We have that $\RR^{-1}$ is a relation.
The result follows from Image of Union under Relation.
{{qed}}
Theorem: Preimage of Intersection under Relation

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $C$ and $D$ be subsets of $T$.
Then:
:$\RR^{-1} \sqbrk {C \cap D} \subseteq \RR^{-1} \sqbrk C \cap \RR^{-1} \sqbrk D$

Proof:
This follows from Image of Intersection under Relation, and the fact that $\RR^{-1}$ is itself a relation, and therefore obeys the same rules.
{{qed}}
Category:Relation Theory
Category:Set Intersection
osjfreff1fjhbf3bsq2mmphacmym5ec
Theorem: Preimage of Set Difference under Relation

Let $\RR \subseteq S \times T$ be a relation.
Let $C$ and $D$ be subsets of $T$.
Then:
:$\RR^{-1} \sqbrk C \setminus \RR^{-1} \sqbrk D \subseteq \RR^{-1} \sqbrk {C \setminus D}$
where:
:$\setminus$ denotes set difference
:$\RR^{-1} \sqbrk C$ denotes the preimage of $C$ under $\RR$.

Proof:
We have that $\RR^{-1}$ is itself a relation
The result then follows from Image of Set Difference under Relation.
{{qed}}
Category:Preimages under Relations
Category:Set Difference
jg0wummvseuge8ns642yx293yqmwlw0
Theorem: Restriction is Subset of Relation

Let $\RR \subseteq S \times T$ be a relation.
Let $X \subseteq S$.
Then the restriction of $\RR$ to $X$ is a subset of $\RR$.

Proof:
From the definition of restriction:
:$\forall x \in X: \map {\RR \restriction_X} x = \map \RR x$
Thus:
:$\forall x \in X: \exists t \in T: \tuple {x, t} \in \RR \restriction_X$
But $\tuple {x, t}$ is also (by definition) in $\RR$.
It follows that:
:$\RR \restriction_X \subseteq \RR$
{{qed}}
Category:Restrictions
73kf7ly09mrcy0dydmw3rvzamcx1391
Theorem: Null Relation is Antireflexive, Symmetric and Transitive

Let $S$ be a set which is non-empty.
Let $\RR \subseteq S \times S$ be the null relation.
Then $\RR$ is antireflexive, symmetric and transitive.
If $S = \O$ then Relation on Empty Set is Equivalence applies.

Proof:
From the definition of null relation:
:$\RR = \O$
Theorem: Symmetry of Relations is Symmetric

Let $\RR$ be a relation on $S$ which is symmetric. Then:
:$\tuple {x, y} \in \RR \iff \tuple {y, x} \in \RR$.

Proof:
Let $\RR$ be symmetric.
{{begin-eqn}}
{{eqn | l = \tuple {x, y} \in \RR
      | o = \implies
      | r = \tuple {y, x} \in \RR
      | c = {{Defof|Symmetric Relation}}
}}
{{eqn | l = \tuple {y, x} \in \RR
      | o = \implies
      | r = \tuple {x, y} \in \RR
      | c = {{Defof|Symmetric Relation}}
}}
{{eqn | ll= \leadsto
      | l = \leftparen {\tuple {x, y} \in \RR}
      | o = \iff
      | r = \rightparen {\tuple {y, x} \in \RR}
      | c = {{Defof|Biconditional}}
}}
{{end-eqn}}
{{qed}}
Category:Symmetric Relations
7me9t24od6hj85ztjyzpotupraoj3rz
Theorem: Relation is Symmetric and Antisymmetric iff Coreflexive

Let $S$ be a set.
Let $\RR \subseteq S \times S$ be a relation in $S$.
Then:
:$\RR$ is both symmetric and antisymmetric
{{iff}}:
:$\RR$ is coreflexive.

Proof:
=== Necessary Condition ===
Let $\RR$ be both symmetric and antisymmetric
Suppose $\RR \nsubseteq \Delta_S$.
Then:
:$\exists \tuple {x, y} \in \RR: x \ne y$
But then as $\RR$ is symmetric:
:$\tuple {y, x} \in \RR$
So we have:
:$\tuple {x, y} \in \RR$
and:
:$\tuple {y, x} \in \RR$
where $x \ne y$.
Thus $\RR$ is not antisymmetric, contrary to hypothesis.
So our assumption that $\RR \nsubseteq \Delta_S$ is false.
That is:
:$\RR \subseteq \Delta_S$
The result follows by definition of coreflexive.
{{qed|lemma}}
Theorem: Relation both Symmetric and Asymmetric is Null

Let $\RR$ be a relation in $S$ which is both symmetric and asymmetric.
Then:
:$\RR = \O$

Proof:
Let $\RR \ne \O$.
Then:
:$\exists \tuple {x, y} \in \RR$
Now, either $\tuple {y, x} \in \RR$ or $\tuple {y, x} \notin \RR$.
If $\tuple {y, x} \in \RR$, then $\RR$ is not asymmetric.
If $\tuple {y, x} \notin \RR$, then $\RR$ is not symmetric.
Therefore, if $\RR \ne \O$, $\RR$ cannot be both symmetric and asymmetric.
{{qed|lemma}}
Let $\RR = \O$.
Then:
:$\forall x, y \in S: \tuple {x, y} \notin \RR \land \tuple {y, x} \notin \RR$
From Biconditional as Disjunction of Conjunctions:
:$\tuple {p \land q} \lor \tuple {\neg p \land \neg q} \vdash p \iff q$
Thus:
:$\forall x, y \in S: \tuple {x, y} \in \RR \iff \tuple {y, x} \in \RR$
So the condition for symmetry is fulfilled, and $\RR = \O$ is symmetric.
As $\RR = \O$:
:$\forall x, y \in S: \tuple {x, y} \notin \RR$
From False Statement implies Every Statement $\neg p \vdash p \implies q$, we can deduce:
:$\forall x, y \in S: \tuple {x, y} \notin \RR$
therefore:
:$\forall x, y \in S: \tuple {x, y} \in \RR \implies \forall x, y \in S: \tuple {y, x} \notin \RR$
This is the definition of asymmetric.
Thus the only relation $\RR$ to be both symmetric and asymmetric is $\RR = \O$.
{{qed}}