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 )