description/proof of that for map from product of \(2\) sets into set, subset of 2nd set, and subset of 3rd set, complement of subset of 1st s.t. image of product of point and subset of 2nd is contained in subset of 3rd is projection of intersection of preimage of complement of subset of 3rd and product of 1st and subset of 2nd
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of product set.
- The reader knows a definition of projection from product set onto subproduct set.
- The reader knows a definition of map preimage of subset of codomain.
Target Context
- The reader will have a description and a proof of the proposition that for any map from the product of any \(2\) sets into any set, any subset of the 2nd set, and any subset of the 3rd set, the complement of the subset of the 1st set such that the image of the product of each point and the subset of the 2nd set is contained in the subset of the 3rd set is the projection of the intersection of the preimage of the complement of the subset of the 3rd set and the product of the 1st set and the subset of the 2nd set.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(S_1\): \(\in \{\text{ the sets }\}\)
\(S_2\): \(\in \{\text{ the sets }\}\)
\(S_3\): \(\in \{\text{ the sets }\}\)
\(f\): \(: S_1 \times S_2 \to S_3\)
\({S_2}^`\): \(\subseteq S_2\)
\({S_3}^`\): \(\subseteq S_3\)
\(\pi_1\): \(: S_1 \times S_2 \to S_1, (s_1, s_2) \mapsto s_1\)
//
Statements:
\(S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\} = \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\)
//
2: Proof
Whole Strategy: Step 1: see that for each \(s_1 \in S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\), \(s_1 \in \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\); Step 2: see that for each \(s_1 \in \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\), \(s_1 \in S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\); Step 3: conclude the proposition.
Step 1:
Let \(s_1 \in S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\) be any.
\(s_1 \notin \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\), which means that \(f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\) does not hold.
That means that there is an \({s_2}^` \in {S_2}^`\) such that \(f ((s_1, {s_2}^`)) \notin {S_3}^`\).
\(f ((s_1, {s_2}^`)) \in S_3 \setminus {S_3}^`\), so, \((s_1, {s_2}^`) \in f^{-1} (S_3 \setminus {S_3}^`)\).
Also \((s_1, {s_2}^`) \in S_1 \times {S_2}^`\), so, \((s_1, {s_2}^`) \in f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`)\).
So, \(s_1 = \pi_1 ((s_1, {s_2}^`)) \in \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\).
So, \(S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\} \subseteq \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\).
Step 2:
Let \(s_1 \in \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\) be any.
There is an \(s_2 \in S_2\) such that \((s_1, s_2) \in f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`)\).
\(f ((s_1, s_2)) \in S_3 \setminus {S_3}^`\) and \(s_2 \in {S_2}^`\).
\(f ((s_1, s_2)) \notin {S_3}^`\).
So, \(f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\) does not hold.
So, \(s_1 \notin \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\).
So, \(s_1 \in S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\).
So, \(\pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`)) \subseteq S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\).
Step 3:
So, \(S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\} = \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\).
