[proofplan]
Define $\mathcal I:=\{I\subseteq E: e\notin \operatorname{cl}(I\setminus\{e\}) \text{ for every } e\in I\}$. We verify the independent-set axioms for a matroid for the family $\mathcal I$, using the stated closure axioms for $\operatorname{cl}$. The empty set is immediate, and hereditary closure follows from monotonicity of $\operatorname{cl}$. The main point is augmentation: assuming independent sets $I,J$ with $|I|<|J|$, we first prove a closure-exchange replacement lemma, then use it to replace elements of $I\setminus J$ by elements of $J\setminus I$ without changing closure. This reduces the contradiction argument to the case where an independent set of size $|I|$ lies inside $J$, forcing some element of $J\setminus I$ to lie outside $\operatorname{cl}(I)$; the same exchange lemma then shows that this element augments $I$ independently.
[/proofplan]
custom_env
admin
[step:Derive the two-element closure replacement lemma]Let $A \subseteq E$ and let $a,b \in E$. Suppose that
\begin{align*}
b \notin \operatorname{cl}(A)
\end{align*}
and
\begin{align*}
b \in \operatorname{cl}(A \cup \{a\}).
\end{align*}
By the exchange axiom applied with $e=a$ and $f=b$, we obtain
\begin{align*}
a \in \operatorname{cl}(A \cup \{b\}).
\end{align*}
We claim that
\begin{align*}
\operatorname{cl}(A \cup \{a\})=\operatorname{cl}(A \cup \{b\}).
\end{align*}
Indeed, extensivity gives $A \subseteq \operatorname{cl}(A \cup \{b\})$, and the previous paragraph gives $a \in \operatorname{cl}(A \cup \{b\})$. Hence
\begin{align*}
A \cup \{a\} \subseteq \operatorname{cl}(A \cup \{b\}).
\end{align*}
By monotonicity and idempotence,
\begin{align*}
\operatorname{cl}(A \cup \{a\}) \subseteq \operatorname{cl}(\operatorname{cl}(A \cup \{b\}))=\operatorname{cl}(A \cup \{b\}).
\end{align*}
Conversely, extensivity gives $A \subseteq \operatorname{cl}(A \cup \{a\})$, and the hypothesis gives $b \in \operatorname{cl}(A \cup \{a\})$. Thus
\begin{align*}
A \cup \{b\} \subseteq \operatorname{cl}(A \cup \{a\}),
\end{align*}
so monotonicity and idempotence give
\begin{align*}
\operatorname{cl}(A \cup \{b\}) \subseteq \operatorname{cl}(\operatorname{cl}(A \cup \{a\}))=\operatorname{cl}(A \cup \{a\}).
\end{align*}
The two inclusions prove the equality.[/step]
custom_env
admin
[guided]Let $A \subseteq E$ and let $a,b \in E$ satisfy
\begin{align*}
b \notin \operatorname{cl}(A)
\end{align*}
and
\begin{align*}
b \in \operatorname{cl}(A \cup \{a\}).
\end{align*}
We prove that
\begin{align*}
\operatorname{cl}(A \cup \{a\})=\operatorname{cl}(A \cup \{b\}).
\end{align*}
The exchange axiom says that if $b$ first becomes forced after adding $a$ to $A$, then $a$ becomes forced after adding $b$ to $A$. Formally, the two displayed hypotheses give
\begin{align*}
b \in \operatorname{cl}(A \cup \{a\}) \setminus \operatorname{cl}(A),
\end{align*}
so the exchange axiom applies with $e=a$ and $f=b$. Therefore
\begin{align*}
a \in \operatorname{cl}(A \cup \{b\}).
\end{align*}
Why does this imply equality of closures? We prove both inclusions. Since $A \subseteq A \cup \{b\}$, extensivity gives
\begin{align*}
A \subseteq \operatorname{cl}(A \cup \{b\}).
\end{align*}
Together with $a \in \operatorname{cl}(A \cup \{b\})$, this gives
\begin{align*}
A \cup \{a\} \subseteq \operatorname{cl}(A \cup \{b\}).
\end{align*}
Applying monotonicity to this inclusion gives
\begin{align*}
\operatorname{cl}(A \cup \{a\}) \subseteq \operatorname{cl}(\operatorname{cl}(A \cup \{b\})).
\end{align*}
Idempotence then reduces the right-hand side:
\begin{align*}
\operatorname{cl}(\operatorname{cl}(A \cup \{b\}))=\operatorname{cl}(A \cup \{b\}).
\end{align*}
Hence
\begin{align*}
\operatorname{cl}(A \cup \{a\}) \subseteq \operatorname{cl}(A \cup \{b\}).
\end{align*}
For the reverse inclusion, the hypothesis $b \in \operatorname{cl}(A \cup \{a\})$ plays the same role as the conclusion $a \in \operatorname{cl}(A \cup \{b\})$. Extensivity gives
\begin{align*}
A \subseteq \operatorname{cl}(A \cup \{a\}),
\end{align*}
and therefore
\begin{align*}
A \cup \{b\} \subseteq \operatorname{cl}(A \cup \{a\}).
\end{align*}
By monotonicity and idempotence,
\begin{align*}
\operatorname{cl}(A \cup \{b\}) \subseteq \operatorname{cl}(\operatorname{cl}(A \cup \{a\}))=\operatorname{cl}(A \cup \{a\}).
\end{align*}
Combining the two inclusions gives
\begin{align*}
\operatorname{cl}(A \cup \{a\})=\operatorname{cl}(A \cup \{b\}).
\end{align*}[/guided]
custom_env
admin
[step:Verify the empty set and hereditary axioms]
The empty set belongs to $\mathcal I$ because the condition defining independence is vacuous when $I=\varnothing$.
Let $I \in \mathcal I$, and let $H \subseteq I$. We prove that $H \in \mathcal I$. Fix $h \in H$. Since
\begin{align*}
H \setminus \{h\} \subseteq I \setminus \{h\},
\end{align*}
monotonicity gives
\begin{align*}
\operatorname{cl}(H \setminus \{h\}) \subseteq \operatorname{cl}(I \setminus \{h\}).
\end{align*}
Because $I$ is independent, $h \notin \operatorname{cl}(I \setminus \{h\})$. Hence
\begin{align*}
h \notin \operatorname{cl}(H \setminus \{h\}).
\end{align*}
Since $h \in H$ was arbitrary, $H \in \mathcal I$.
[/step]
custom_env
admin
[step:Prove independent sets cannot be contained in the closure of smaller sets]We prove the following cardinality lemma. If $X \in \mathcal I$ and $Y \subseteq E$ satisfy
\begin{align*}
X \subseteq \operatorname{cl}(Y),
\end{align*}
then
\begin{align*}
|X| \leq |Y|.
\end{align*}
We induct on the nonnegative integer $m:=|Y\setminus X|$. If $m=0$, then $Y\subseteq X$. If $Y\neq X$, choose $x\in X\setminus Y$. Then $Y\subseteq X\setminus\{x\}$, so monotonicity gives
\begin{align*}
\operatorname{cl}(Y)\subseteq \operatorname{cl}(X\setminus\{x\}).
\end{align*}
Because $x\in X\subseteq \operatorname{cl}(Y)$, this implies $x\in \operatorname{cl}(X\setminus\{x\})$, contradicting $X\in\mathcal I$. Hence $Y=X$, and $|X|=|Y|$.
Assume $m>0$ and choose $y\in Y\setminus X$. If
\begin{align*}
X \subseteq \operatorname{cl}(Y\setminus\{y\}),
\end{align*}
then the induction hypothesis applied to $Y\setminus\{y\}$ gives $|X|\leq |Y|-1<|Y|$, as required. Otherwise choose
\begin{align*}
x\in X\setminus \operatorname{cl}(Y\setminus\{y\}).
\end{align*}
Since $x\in X\subseteq \operatorname{cl}(Y)=\operatorname{cl}((Y\setminus\{y\})\cup\{y\})$, the closure replacement lemma with $A=Y\setminus\{y\}$, $a=y$, and $b=x$ gives
\begin{align*}
\operatorname{cl}(Y)=\operatorname{cl}((Y\setminus\{y\})\cup\{x\}).
\end{align*}
Define
\begin{align*}
Y' := (Y\setminus\{y\})\cup\{x\}.
\end{align*}
Extensivity gives $Y\setminus\{y\}\subseteq \operatorname{cl}(Y\setminus\{y\})$, so the choice $x\notin \operatorname{cl}(Y\setminus\{y\})$ implies $x\notin Y\setminus\{y\}$. Also $x\in X$ and $y\notin X$. Therefore replacing $y$ by $x$ preserves cardinality and reduces the number of elements outside $X$ by one: $|Y'|=|Y|$ and $|Y'\setminus X|=m-1$. Since $X\subseteq \operatorname{cl}(Y')$, the induction hypothesis applied to $Y'$ gives $|X|\leq |Y'|=|Y|$.[/step]
custom_env
admin
[guided]The purpose of this lemma is to convert closure containment into a size bound. The statement is: whenever an independent set $X$ is contained in the closure of a set $Y$, the set $Y$ must have at least as many elements as $X$.
We use induction on $m:=|Y\setminus X|$, the number of elements of $Y$ that are not already in $X$. If $m=0$, then $Y\subseteq X$. Suppose $Y\neq X$ and choose $x\in X\setminus Y$. Since $Y\subseteq X\setminus\{x\}$, monotonicity gives
\begin{align*}
\operatorname{cl}(Y)\subseteq \operatorname{cl}(X\setminus\{x\}).
\end{align*}
But $x\in X\subseteq\operatorname{cl}(Y)$, so $x\in\operatorname{cl}(X\setminus\{x\})$. This contradicts the defining independence condition for $X$. Therefore $Y=X$, and the desired inequality is equality.
Now assume $m>0$ and choose $y\in Y\setminus X$. There are two cases. If $X\subseteq\operatorname{cl}(Y\setminus\{y\})$, then we can delete $y$ and apply the induction hypothesis to the smaller set $Y\setminus\{y\}$. This gives
\begin{align*}
|X|\leq |Y\setminus\{y\}|=|Y|-1,
\end{align*}
which is stronger than needed.
In the remaining case, some element of $X$ is not in the closure after deleting $y$. Choose
\begin{align*}
x\in X\setminus\operatorname{cl}(Y\setminus\{y\}).
\end{align*}
Since $X\subseteq\operatorname{cl}(Y)$, this same $x$ belongs to
\begin{align*}
\operatorname{cl}(Y)=\operatorname{cl}((Y\setminus\{y\})\cup\{y\}).
\end{align*}
Thus $x$ is forced by adding $y$ to $Y\setminus\{y\}$ but was not forced before. The closure replacement lemma applies with $A=Y\setminus\{y\}$, $a=y$, and $b=x$, and gives
\begin{align*}
\operatorname{cl}(Y)=\operatorname{cl}((Y\setminus\{y\})\cup\{x\}).
\end{align*}
Set
\begin{align*}
Y':=(Y\setminus\{y\})\cup\{x\}.
\end{align*}
We check the counting carefully. Extensivity gives $Y\setminus\{y\}\subseteq \operatorname{cl}(Y\setminus\{y\})$, so $x\notin \operatorname{cl}(Y\setminus\{y\})$ forces $x\notin Y\setminus\{y\}$. Also $x\in X$ by construction, while $y\notin X$ because $y\in Y\setminus X$. Thus the replacement removes one element outside $X$ and inserts one element inside $X$, while preserving the total size of the set. Therefore $|Y'|=|Y|$ and $|Y'\setminus X|=m-1$. The closure equality also preserves the containment $X\subseteq\operatorname{cl}(Y')$, so the induction hypothesis gives
\begin{align*}
|X|\leq |Y'|=|Y|.
\end{align*}[/guided]
custom_env
admin
[step:Force an augmenting element outside $\operatorname{cl}(I)$]
Let $I,J\in\mathcal I$ satisfy $|I|<|J|$. We prove that there exists an element
\begin{align*}
e\in J\setminus I
\end{align*}
such that
\begin{align*}
e\notin \operatorname{cl}(I).
\end{align*}
Assume for contradiction that $J\setminus I\subseteq\operatorname{cl}(I)$. Since $I\subseteq\operatorname{cl}(I)$ by extensivity, we get
\begin{align*}
J\subseteq I\cup(J\setminus I)\subseteq \operatorname{cl}(I).
\end{align*}
Applying the cardinality lemma with $X=J$ and $Y=I$ gives $|J|\leq |I|$, contradicting $|I|<|J|$. Therefore some $e\in J\setminus I$ satisfies $e\notin\operatorname{cl}(I)$.
[/step]
custom_env
admin
[step:Show the element outside $\operatorname{cl}(I)$ augments $I$]
Let $e \in J\setminus I$ satisfy $e \notin \operatorname{cl}(I)$. We prove that
\begin{align*}
I\cup\{e\}\in \mathcal I.
\end{align*}
First,
\begin{align*}
e \notin \operatorname{cl}(I)=\operatorname{cl}((I\cup\{e\})\setminus\{e\}).
\end{align*}
Now fix $x \in I$. Suppose, for contradiction, that
\begin{align*}
x \in \operatorname{cl}((I\setminus\{x\})\cup\{e\}).
\end{align*}
Because $I$ is independent,
\begin{align*}
x \notin \operatorname{cl}(I\setminus\{x\}).
\end{align*}
Applying the exchange axiom with $A=I\setminus\{x\}$, $f=x$, and $e=e$, we obtain
\begin{align*}
e \in \operatorname{cl}((I\setminus\{x\})\cup\{x\})=\operatorname{cl}(I),
\end{align*}
contradicting the choice of $e$. Thus
\begin{align*}
x \notin \operatorname{cl}((I\cup\{e\})\setminus\{x\})
\end{align*}
for every $x \in I$, and the same condition has already been checked for $e$. Therefore $I\cup\{e\}\in \mathcal I$.
We have verified that $\varnothing \in \mathcal I$, that $\mathcal I$ is closed under subsets, and that whenever $I,J\in\mathcal I$ with $|I|<|J|$, there exists $e\in J\setminus I$ such that $I\cup\{e\}\in\mathcal I$. These are precisely the independent-set axioms for a matroid on the finite ground set $E$. Hence $\mathcal I$ is the collection of independent sets of a matroid on $E$.
[/step]