Theorem: Rank Function of Matroid Satisfies Formulation 1 Rank Axioms

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be the rank function of a matroid on $S$.
Then $\rho$ satisfies formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}

Proof:
Let $\rho$ be the rank function of a matroid $M = \struct{S, \mathscr I}$ on $S$
==== $\rho$ satisfies $(\text R 1)$ ====
$\rho$ satisfies $(\text R 1)$ follows immediately from Rank of Empty Set is Zero.
{{qed|lemma}}
==== $\rho$ satisfies $(\text R 2)$ ====
Let:
:$X \subseteq S$
:$y \in S$
From Rank Function is Increasing:
:$\map \rho X \le \map \rho {X \cup \set y}$
Let $Y$ be a maximal independent subset of $X \cup \set y$.
From Cardinality of Maximal Independent Subset Equals Rank of Set
:$\card Y = \map \rho {X \cup \set y}$
By matroid axiom $(\text I 2)$:
:$Y \setminus \set y \in \mathscr I$
We now consider two cases.
===== Case 1: $y \in Y$ =====
We have:
{{begin-eqn}}
{{eqn | l = \map \rho X
      | o = \ge 
      | r = \card{Y \setminus \set y}
      | c = {{Defof|Rank Function (Matroid)|Rank Function}}
}}
{{eqn | r = \card Y - \card{Y \cap \set y}
      | c = Cardinality of Set Difference
}}
{{eqn | r = \card Y - \card{\set y}
      | c = Singleton of Element is Subset
}}
{{eqn | r = \card Y - 1
      | c = Cardinality of Singleton
}}
{{eqn |ll = \leadsto
      | l = \map \rho X + 1 
      | o = \ge
      | r = \card Y
      | c = Add one to both sides
}}
{{end-eqn}}
{{qed|lemma}}
===== Case 2: $y \notin Y$ =====
We have:
{{begin-eqn}}
{{eqn | l = \map \rho X + 1
      | o = > 
      | r = \map \rho X
}}
{{eqn | o = \ge 
      | r = \card{Y \setminus \set y}
      | c = {{Defof|Rank Function (Matroid)|Rank Function}}
}}
{{eqn | r = \card Y - \card{Y \cap \set y}
      | c = Cardinality of Set Difference
}}
{{eqn | r = \card Y - \O
      | c = Intersection With Singleton is Disjoint if Not Element
}}
{{eqn | r = \card Y - 0
      | c = Cardinality of Empty Set
}}
{{eqn | r = \card Y
}}
{{end-eqn}}
{{qed|lemma}}
In either case:
:$\map \rho X + 1 \ge \card Y = \map \rho {X \cup \set y}$
{{qed|lemma}}
==== $\rho$ satisfies $(\text R 3)$ ====
Let:
:$X \subseteq S$
:$y, z \in S$
===== Case 1: $y, z \notin X$ =====
Let $A = X \cup \set y \cup \set z$.
From Rank Function is Increasing:
:$\map \rho A \ge \map \rho X$
We now prove the contrapositive statement:
:$\map \rho A > \map \rho X \implies$ either $\map \rho {X \cup \set y} > \map \rho X$ or $\map \rho {X \cup \set z} > \map \rho X$
Let $\map \rho A > \map \rho X$.
Let $Y$ be a maximal independent subset of $X$.
Let $Z$ be a maximal independent subset of $A$.
From Cardinality of Maximal Independent Subset Equals Rank of Set:
:$\card Y = \map \rho X < \map \rho A = \card Z$
From Independent Set can be Augmented by Larger Independent Set there exists non-empty set $Z' \subseteq Z \setminus Y$:
:$Y \cup Z' \in \mathscr I$
:$\card{Y \cup Z'} = \card Z$
{{AimForCont}}:
:$y, z \notin Z'$
We have:
{{begin-eqn}}
{{eqn | l = Z'
      | r = Z' \cap Z
}}
{{eqn | o = \subseteq
      | r = Z' \cap A
}}
{{eqn | r = Z' \cap \paren{X \cup \set y \cup \set z}
}}
{{eqn | r = \paren{Z' \cap  X} \cup \paren{Z' \cap \paren{\set y \cup \set z} }
}}
{{eqn | r = \paren{Z' \cap X} \cup \O
}}
{{eqn | r = \paren{Z' \cap X}
}}
{{eqn | o = \subseteq
      | r = X
}}
{{eqn | ll = \leadsto
      | l = Y \cup Z'
      | o = \subseteq
      | r = X
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \card{Y \cup Z'}
      | r = \card Z
}}
{{eqn | r = \map \rho A
}}
{{eqn | o = > 
      | r = \map \rho X
}}
{{eqn | o = \ge 
      | r = \card{Y \cup Z'}
}}
{{end-eqn}}
This is a contradiction.
Hence:
:either $y \in Z'$ or $z \in Z'$
{{WLOG}}, assume $y \in Z'$.
From matroid axiom $(\text I 2)$:
:$Y \cup \set y \in \mathscr I$
We have:
{{begin-eqn}}
{{eqn | l = \map \rho {X \cup \set y}
      | o = \ge
      | r = \card{Y \cup \set y}
      | c = {{Defof|Rank Function (Matroid)}}
}}
{{eqn | r = \card Y + \card{\set y}
      | c = Corollary of Cardinality of Set Union
}}
{{eqn | r = \card Y + 1
      | c = Cardinality of Singleton
}}
{{eqn | o = >
      | r = \card Y
}}
{{eqn | r = \map \rho X
      | c = {{Defof|Rank Function (Matroid)}}
}}
{{end-eqn}}
This proves the contrapositive statement.
{{qed|lemma}}
===== Case 2: Either $y \in X$ or $z \in X$ =====
{{WLOG}}, assume $y \in X$.
Let:
:$\map \rho {X \cup \set y} = \map \rho {X \cup \set z} = \map \rho X$.
We have:
:$X \cup \set y \cup \set z = X \cup \set z$
Hence:
:$\map \rho {X \cup \set y \cup \set z} = \map \rho {X \cup \set z} = \map \rho X$
{{qed|lemma}}
In either case:
:$\map \rho {X \cup \set y} = \map \rho {X \cup \set z} = \map \rho X \implies \map \rho {X \cup \set y \cup \set z} = \map \rho X$