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 : ∪ ( 𝑅1 “ On ) ⟶ On
2		unir1	⊢ ∪ ( 𝑅1 “ On ) = V
3	2	feq2i	⊢ ( rank : ∪ ( 𝑅1 “ On ) ⟶ On ↔ rank : V ⟶ On )
4	1 3	mpbi	⊢ rank : V ⟶ On
5		vex	⊢ 𝑦 ∈ V
6		rankonid	⊢ ( 𝑦 ∈ dom 𝑅1 ↔ ( rank ‘ 𝑦 ) = 𝑦 )
7	6	biimpi	⊢ ( 𝑦 ∈ dom 𝑅1 → ( rank ‘ 𝑦 ) = 𝑦 )
8		r1fnon	⊢ 𝑅1 Fn On
9	8	fndmi	⊢ dom 𝑅1 = On
10	9	eqcomi	⊢ On = dom 𝑅1
11	7 10	eleq2s	⊢ ( 𝑦 ∈ On → ( rank ‘ 𝑦 ) = 𝑦 )
12	11	eqcomd	⊢ ( 𝑦 ∈ On → 𝑦 = ( rank ‘ 𝑦 ) )
13		fveq2	⊢ ( 𝑥 = 𝑦 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) )
14	13	rspceeqv	⊢ ( ( 𝑦 ∈ V ∧ 𝑦 = ( rank ‘ 𝑦 ) ) → ∃ 𝑥 ∈ V 𝑦 = ( rank ‘ 𝑥 ) )
15	5 12 14	sylancr	⊢ ( 𝑦 ∈ On → ∃ 𝑥 ∈ V 𝑦 = ( rank ‘ 𝑥 ) )
16	15	rgen	⊢ ∀ 𝑦 ∈ On ∃ 𝑥 ∈ V 𝑦 = ( rank ‘ 𝑥 )
17		dffo3	⊢ ( rank : V –onto→ On ↔ ( rank : V ⟶ On ∧ ∀ 𝑦 ∈ On ∃ 𝑥 ∈ V 𝑦 = ( rank ‘ 𝑥 ) ) )
18	4 16 17	mpbir2an	⊢ rank : V –onto→ On