Metamath Proof Explorer


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