This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )