Theorem rankfn

Description: The rank function is a function on the universe. (Contributed by BTernaryTau, 23-Jun-2026)

	Ref	Expression
Assertion	rankfn	$$⊢\mathrm{rank}Fn\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		rankfo	$$⊢\mathrm{rank}:\mathrm{V}\underset{onto}{⟶}\mathrm{On}$$
2		fofn	$$⊢\mathrm{rank}:\mathrm{V}\underset{onto}{⟶}\mathrm{On}\to \mathrm{rank}Fn\mathrm{V}$$
3	1 2	ax-mp	$$⊢\mathrm{rank}Fn\mathrm{V}$$