Proof of Counting through Bijections, Injections and Surjections

If $f$ is surjective, then $f(A)=B$: the image lies in $B$ by Membership in Inverse Relations, Preimages and Images of Classes, and Enlarging the Codomain of a Map (iv), and every $b\in B$ is $f(a)$ for some $a\in A$, hence lies in $f(A)$ by The Image and the Preimage of a Class under a Class (i).

Surjections. Let $f$ be surjective and $A$ finite. Then $B=f(A)$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (vi), and

$$\#B=\#f(A)\le\#A$$

by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products (iii). This proves (iii).

Bijections. Let $f$ be bijective and $A$ finite. Since $f$ is surjective, $B=f(A)$ is finite as above, and since $f$ is injective, Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products (iii) gives the equality $\#B=\#f(A)=\#A$. This proves (i).

Injections. Let $f$ be injective and $B$ finite. The image $f(A)$ is a subset of $B$, so it is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iv) and $\#f(A)\le\#B$ by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products (iv). Since $f$ is injective, its range is $\operatorname{ran}f=f(A)$ and its inverse is a bijective map $f^{-1}:f(A)\to A$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (v). Applying (i) to $f^{-1}$ and the finite set $f(A)$ shows that $A$ is finite and $\#A=\#f(A)$. Hence

$$\#A=\#f(A)\le\#B,$$

which proves (ii).