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.