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$
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.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".p ↔ q is to prove p → q (called mp) and q → p (called mpr).X = Y where X and Y are sets, one can use set.ext (a proof of ∀ z : α, z ∈ X ↔ z ∈ Y).∀ 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.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.
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$.
