Metamath Proof Explorer

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