Theorem rankfn

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

	Ref	Expression
Assertion	rankfn	⊢ rank Fn V

Proof

Step	Hyp	Ref	Expression
1		rankfo	⊢ rank : V –onto→ On
2		fofn	⊢ ( rank : V –onto→ On → rank Fn V )
3	1 2	ax-mp	⊢ rank Fn V