Theorem rankfo

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

	Ref	Expression
Assertion	rankfo	$$⊢\mathrm{rank}:\mathrm{V}\underset{onto}{⟶}\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		rankf	$$⊢\mathrm{rank}:\bigcup R_1\left[\mathrm{On}\right]⟶\mathrm{On}$$
2		unir1	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$
3	2	feq2i	$$⊢\mathrm{rank}:\bigcup R_1\left[\mathrm{On}\right]⟶\mathrm{On}\leftrightarrow \mathrm{rank}:\mathrm{V}⟶\mathrm{On}$$
4	1 3	mpbi	$$⊢\mathrm{rank}:\mathrm{V}⟶\mathrm{On}$$
5		vex	$$⊢y\in \mathrm{V}$$
6		rankonid	$$⊢y\in \mathrm{dom}{R}_1\leftrightarrow \mathrm{rank}\left(y\right)=y$$
7	6	biimpi	$$⊢y\in \mathrm{dom}{R}_1\to \mathrm{rank}\left(y\right)=y$$
8		r1fnon	$$⊢R_{1}Fn\mathrm{On}$$
9	8	fndmi	$$⊢\mathrm{dom}{R}_1=\mathrm{On}$$
10	9	eqcomi	$$⊢\mathrm{On}=\mathrm{dom}{R}_1$$
11	7 10	eleq2s	$$⊢y\in \mathrm{On}\to \mathrm{rank}\left(y\right)=y$$
12	11	eqcomd	$$⊢y\in \mathrm{On}\to y=\mathrm{rank}\left(y\right)$$
13		fveq2	$$⊢x=y\to \mathrm{rank}\left(x\right)=\mathrm{rank}\left(y\right)$$
14	13	rspceeqv	$$⊢\left(y\in \mathrm{V}\wedge y=\mathrm{rank}\left(y\right)\right)\to \exists x\in \mathrm{V}y=\mathrm{rank}\left(x\right)$$
15	5 12 14	sylancr	$$⊢y\in \mathrm{On}\to \exists x\in \mathrm{V}y=\mathrm{rank}\left(x\right)$$
16	15	rgen	$$⊢\forall y\in \mathrm{On}\exists x\in \mathrm{V}y=\mathrm{rank}\left(x\right)$$
17		dffo3	$$⊢\mathrm{rank}:\mathrm{V}\underset{onto}{⟶}\mathrm{On}\leftrightarrow \left(\mathrm{rank}:\mathrm{V}⟶\mathrm{On}\wedge \forall y\in \mathrm{On}\exists x\in \mathrm{V}y=\mathrm{rank}\left(x\right)\right)$$
18	4 16 17	mpbir2an	$$⊢\mathrm{rank}:\mathrm{V}\underset{onto}{⟶}\mathrm{On}$$