Metamath Proof Explorer


Theorem r1funlim

Description: The cumulative hierarchy of sets function is a function on a limit ordinal. (This weak form of r1fnon avoids ax-rep .) (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion r1funlim ( Fun 𝑅1 ∧ Lim dom 𝑅1 )

Proof

Step Hyp Ref Expression
1 rdgfun Fun rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
2 df-r1 𝑅1 = rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
3 2 funeqi ( Fun 𝑅1 ↔ Fun rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) )
4 1 3 mpbir Fun 𝑅1
5 rdgdmlim Lim dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
6 2 dmeqi dom 𝑅1 = dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
7 limeq ( dom 𝑅1 = dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) → ( Lim dom 𝑅1 ↔ Lim dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ) )
8 6 7 ax-mp ( Lim dom 𝑅1 ↔ Lim dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) )
9 5 8 mpbir Lim dom 𝑅1
10 4 9 pm3.2i ( Fun 𝑅1 ∧ Lim dom 𝑅1 )