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 |
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 |