Can someone verify whether my proof is logically correct? :)

Proof: Assume $A\subseteq B$. Then for every element that belongs in A, such element also belongs in B. Then $A\cap B \subset A$. If $x \in A$, then $x\in B$. Then $A\subset A\cap B$. Then $A\cap B=A$.

Assume $A\cap B=A$. Let $x\in A$. Then $x\in A\cap B$. Then $x\in B$. Since x is any element in A that also belongs in B, by definition of subsets, $A \subseteq B$. $\square$

  • $\begingroup$ Your proof of the second part is spot on. In the first part though, you're basically just skipping from the hypothesis to the conclusion without any intermediate steps. What you should do is suppose $A\subseteq B$. Then take $x\in A\cap B$ and show that it is also in $A$ from the definition of $A\cap B$. Thus $A\cap B\subseteq A$. Then take $x\in A$ and show the reverse inclusion. $\endgroup$ – got it--thanks Jan 8 '18 at 4:38
  • $\begingroup$ Yes, I was honestly lost with the first part and put two different things together and it didn't make much sense to me... I guess I should use the definition of subsets to show containment, right? $\endgroup$ – user482939 Jan 8 '18 at 5:20
  • 1
    $\begingroup$ That's not the only way to do it, but when you're stuck, going back to the definitions is generally not a bad idea. $\endgroup$ – got it--thanks Jan 8 '18 at 16:39

It is important to stick to the definitions (my edits in bold and/or red).

I also edited your connectives to make it easier to read.

Assume $A\subseteq B$. Then, for every element that belongs in A and in B, such element also belongs in B. So $A\cap B \subset A$. Also, If $x \in A$, then $\color{red}{x \in A}$ and $x\in B$, i.e. $A\subset A\cap B$. From $\color{red}{A \cap B \subset A}$ and $\color{red}{A \subset A \cap B}$, we conclude $A\cap B=A$.

Assume $A\cap B=A$. Let $x\in A$. Then $x\in A\cap B$ because $\color{red}{A = A \cap B}$, so $x\in B$. Since any element in A also belongs in B, by definition of subsets we conclude $A \subseteq B$. $\square$

And this is how I would prove it:

For the forward direction, assume $A \subseteq B$, i.e. $x \in A$ implies $x \in B$ for every $x$. Now, $A \cap B \subseteq A$ since every element that is both in $A$ and in $B$ is also in $A$. Also, $A \subseteq A \cap B$ because every element that is in $A$ is in $A$ and also in $B$ because $x \in A$ implies $x \in B$ for every $x$. Therefore, we conclude $A \cap B = A$.

For the backward direction, assume $A \cap B = A$. Now, we need to prove that $A \subseteq B$, i.e. every element in $A$ is also in $B$: Let $x \in A$. Then, since $A = A \cap B$, we have $x \in A \cap B$, which gives us $x \in B$ as required. $\square$

And here is a proof in Lean, a proof assistant similar to coq, using your idea:

example (α : Type u) (A B : set α) : A ⊆ B ↔ A ∩ B = A :=
{ mp  := λ hab, (set.ext $ λ x, ⟨and.left, λ ha, ⟨ha, by exact hab ha⟩⟩),
  mpr := λ hab x ha, by rw ←hab at ha; exact ha.2 }

And here is it expanded for readability:

example (α : Type u) (A B : set α) : A ⊆ B ↔ A ∩ B = A :=
{ mp  := assume hab : A ⊆ B,
           set.ext (assume x : α,
             { mp  := assume h : x ∈ A ∩ B, and.elim_left h,
               mpr := assume ha : x ∈ A,
                 { left  := ha,
                   right := hab ha } } ),
  mpr := assume hab : A ∩ B = A,
         assume x : α,
         assume ha : x ∈ A,
         by rw ←hab at ha; exact and.elim_right ha }

Some explanations:

  • X : Y is type notation, it means that X is an object of type Y. Lean uses type theory as the foundation insetad of set theory.
  • A proof of a proposition is an object of the proposition, so a proposition is also a type. For example, assume hab : A ⊆ B is to introduce an object of the type A ⊆ B, i.e. to introduce a proof of A ⊆ B. So in effect, it is saying, "given a proof of A ⊆ B, to produce a proof of A ∩ B = A".
  • To prove p ↔ q is to prove p → q (called mp) and q → p (called mpr).
  • To prove X = Y where X and Y are sets, one can use set.ext (a proof of ∀ z : α, z ∈ X ↔ z ∈ Y).
  • To prove ∀ z : α, (some proposition), introduce an object of type α and then proof (some proposition).
  • x ∈ A ∩ B is by definition x ∈ A ∧ x ∈ B where is logical and.
  • To prove p ∧ q is to prove p (called left) and q (called right).
  • rw (equality) at (something) is to modify (something) by replacing terms as stipulated by (equality).

This serves to further confirm your proof.

Here is my long proof in Lean translated:

To prove A ⊆ B ↔ A ∩ B = A, I will now prove A ⊆ B → A ∩ B = A as well as A ∩ B = A → A ⊆ B:

To prove A ⊆ B → A ∩ B = A: assume A ⊆ B, and now I prove A ∩ B = A: by set extensionality, I need to prove ∀ x : α, x ∈ A ∩ B ↔ x ∈ A: assume x, now to prove x ∈ A ∩ B ↔ x ∈ A: to prove x ∈ A ∩ B → x ∈ A and to prove x ∈ A → x ∈ A ∩ B. The first part: assume x ∈ A ∩ B, i.e. x ∈ A and x ∈ B. The left hand side is what we need. The second part: assume x ∈ A, to prove x ∈ A ∩ B: to prove x ∈ A and x ∈ B: the first part is the assumption; the second part follows from the initial assumption A ⊆ B.

To prove A ∩ B = A → A ⊆ B: assume A ∩ B = A, and to prove A ⊆ B: let x ∈ A, to prove x ∈ B: rewrite our assumption x ∈ A according to the reverse of the initial assumption A ∩ B = A, and it becomes x ∈ A ∩ B; this means x ∈ A and x ∈ B, and the right hand side is what we need.

  • $\begingroup$ Your answer went beyond my expectation! You really took the time to care, and I really appreciate it. Thank you for your multiple insights, I now understand the first part of the proof better :) $\endgroup$ – user482939 Jan 8 '18 at 5:22
  • 1
    $\begingroup$ @numericalorange added a translation $\endgroup$ – Kenny Lau Jan 8 '18 at 5:28

I think this is a valid proof except from a slight notation mistake in the first part. You say if $A\cap B \subset A$ and $A\subset A\cap B$ then $A\cap B=A$. But notice that what you used is proper subset ($\subset$) and not subset or equal ($\subseteq$). If they are proper, the argument above does not imply $A\cap B=A$ but a contradiction; because if $A\cap B \subset A$ then $A\cap B \ne A$.

  • 1
    $\begingroup$ $\subset$ is not strict subset. $\endgroup$ – Kenny Lau Jan 8 '18 at 4:42
  • 1
    $\begingroup$ Thank you for the correction, I didn't know that $\subset$ is called proper subset. I edited in the answer. $\endgroup$ – ArsenBerk Jan 8 '18 at 4:45
  • 1
    $\begingroup$ That isn't what I mean. $\subset$ is an ambiguous notation that can mean both $\subseteq$ and $\subsetneq$. I personally do not prefer using this symbol, but it still does not need to exclude equality. $\endgroup$ – Kenny Lau Jan 8 '18 at 4:46
  • 1
    $\begingroup$ You may be right about the ambiguity of notations, I just found a definition in here: mathworld.wolfram.com/ProperSubset.html and I haven't seen someone who used $\subset$ for equality instead of $\subseteq$, that's why I commented but you are right, in some concepts these kind of notations are ambiguous. And I haven't seen someone used it this way doesn't mean that it cannot be used in this way. $\endgroup$ – ArsenBerk Jan 8 '18 at 4:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy