Theorem r1fnon

Description: The cumulative hierarchy of sets function is a function on the class of ordinal numbers. (Contributed by NM, 5-Oct-2003) (Revised by Mario Carneiro, 10-Sep-2013)

	Ref	Expression
Assertion	r1fnon	⊢ 𝑅1 Fn On

Proof

Step	Hyp	Ref	Expression
1		rdgfnon	⊢ rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) Fn On
2		df-r1	⊢ 𝑅1 = rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
3	2	fneq1i	⊢ ( 𝑅1 Fn On ↔ rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) Fn On )
4	1 3	mpbir	⊢ 𝑅1 Fn On