Is the following Proof Correct ? In particular can the argument below be shortened and made more concise.?
NOTE: The argument below makes use of the following notation and theorems.
$I_n = \{i\in\mathbf{Z^+}|i\leq n\}$
$A\thicksim B\Leftrightarrow$ There is a bijection from A to B
A is finite $\Leftrightarrow\exists n\in\mathbf{N}(A\thicksim I_n)$
$4.6.6$ Suppose A is a set and $\mathcal{F}$ is a partition of $A$. Then there is an equivalence relation R on A such that $A\backslash R$ = $\mathcal{F}$.
(8) If $n\in \mathbf{N}$ and $A\subseteq I_n$, then $A$ is finite and $|A| ≤ n$.
- (19) Given that $n$ is a positive integer and for each $i\in I_n$, $A_i$ is a finite set and $\forall i\in I_n\forall j\in I_n(i\neq j \implies A_i\cap A_j = \varnothing)$, $\cup_{i\in I_n}A_i$ is finite and $$|\cup_{i\in I_n}A_i| = \sum_{i=1}^{n}|A_i|$$
Theorem. Given that $A$ is finite and $R$ is an equivalence relation on $A$ such that $\forall x\in A(|[x]_R| = n)$, then $A\backslash R$ is finite and $|A\backslash R| = \frac{|A|}{n}$.
Proof. Since $A$ is finite it follows that for some $n\in\mathbf{Z^+}$ there exists a bijection $f:I_n\to A$. Consider now the function $\phi:A\backslash R\to I_n$ defined as follows. $$\phi(X) = \operatorname{min}\left(f^{-1}(X)\right)\ \operatorname{where}\ f^{-1}(X) = \{a\in I_n|f(a)\in X\}$$ The above definition makes sense since given any $Y = [y]_R\in A\backslash R$ the surjectivity of $f$ implies that for some $\alpha\in I_n$, $f(\alpha) = y,$ this together with the reflexivity of $R$ implies $f(\alpha)\in Y$, consequently $\alpha\in f^{-1}(Y)$ so $f^{-1}(Y)\neq\varnothing$, furthermore the Well-Ordering-Principle guarantees the existence of the minimum element.
Assume now that for some $X_1,X_2\in A\backslash R$ such that $\phi(X_1) = \phi(X_2)$. Since $\phi(X_1) = \phi(X_2)$ it follows that $X_1\cap X_2\neq\varnothing$ from theorem $\textbf{4.6.6}$ we know that $\mathcal{F} = A\backslash R$ is a partition on $A$ and is therefore pair-wise dijoint implying that $X_1=X_2$ thus $\phi$ is injective and consequently $A\backslash R \thicksim \operatorname{range}(\phi)$ but $\operatorname{range}(\phi)\subseteq I_n$ thus by appealing to (8) it follows that $A\backslash R$ is finite.
Now having established that $A\backslash R$ is finite , we may invoke the existence of the bijection $h:I_{|A\backslash R|}\to A\backslash R$ and then by appealing to theorem $4.6.6$ in conjunction with 19 we have $$|A| = |\cup_{x\in A}[x]_R| = |\cup_{j\in I_{A\backslash R}}h(j)| = \sum_{j=1}^{|A\backslash R|}|h(j)| = \sum_{x\in A}[x]_R| = |A\backslash R|\cdot n$$ consequently $|A\backslash R| = \frac{|A|}{n}$.
I couldn't follow the whole length of your proof.
I suppose the main reason is poor phrase construction, and for that you have some of my sympathy.
Anyway, you mention, for example the Well-Ordering principle where you're trying to produce a proof about finite sets: there is no need for that and it is clear an overkill.
Below, I present a more concise proof instead.
Given that all equivalence classes have the same number of elements, you have $$A/R = \{ A_1, \ldots, A_k \},$$ where $|A_i| = n$, for $1 \leq i \leq n$ (that is, I'm naming the equivalence classes of $R$ as $A_1, \ldots, A_k$).
It follows that $|A/R| = k$ (the number of equivalence classes) and $$A = \bigcup_{i=1}^k A_i.$$ Since the equivalence classes are pair-wise disjoint, $$|A| = \sum_{i=1}^k |A_i| = \sum_{i=1}^k n = kn,$$ whence $$|A/R| = k = \frac{|A|}{n}.$$