Theorem rankfo

Description: The rank function maps the universe onto the ordinals. (Contributed by BTernaryTau, 23-Jun-2026)

	Ref	Expression
Assertion	rankfo	|- rank : _V -onto-> On

Proof

Step	Hyp	Ref	Expression
1		rankf	|- rank : U. ( R1 " On ) --> On
2		unir1	|- U. ( R1 " On ) = _V
3	2	feq2i	|- ( rank : U. ( R1 " On ) --> On <-> rank : _V --> On )
4	1 3	mpbi	|- rank : _V --> On
5		vex	|- y e. _V
6		rankonid	|- ( y e. dom R1 <-> ( rank ` y ) = y )
7	6	biimpi	|- ( y e. dom R1 -> ( rank ` y ) = y )
8		r1fnon	|- R1 Fn On
9	8	fndmi	|- dom R1 = On
10	9	eqcomi	|- On = dom R1
11	7 10	eleq2s	|- ( y e. On -> ( rank ` y ) = y )
12	11	eqcomd	|- ( y e. On -> y = ( rank ` y ) )
13		fveq2	|- ( x = y -> ( rank ` x ) = ( rank ` y ) )
14	13	rspceeqv	|- ( ( y e. _V /\ y = ( rank ` y ) ) -> E. x e. _V y = ( rank ` x ) )
15	5 12 14	sylancr	|- ( y e. On -> E. x e. _V y = ( rank ` x ) )
16	15	rgen	|- A. y e. On E. x e. _V y = ( rank ` x )
17		dffo3	|- ( rank : _V -onto-> On <-> ( rank : _V --> On /\ A. y e. On E. x e. _V y = ( rank ` x ) ) )
18	4 16 17	mpbir2an	|- rank : _V -onto-> On