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 R_{1} \land Lim dom R_{1})$

Proof

Step	Hyp	Ref	Expression
1		rdgfun	$⊢ Fun rec ((x \in V ⟼ 𝒫 x), \emptyset)$
2		df-r1	$⊢ R_{1} = rec ((x \in V ⟼ 𝒫 x), \emptyset)$
3	2	funeqi	$⊢ Fun R_{1} \leftrightarrow Fun rec ((x \in V ⟼ 𝒫 x), \emptyset)$
4	1 3	mpbir	$⊢ Fun R_{1}$
5		rdgdmlim	$⊢ Lim dom rec ((x \in V ⟼ 𝒫 x), \emptyset)$
6	2	dmeqi	$⊢ dom R_{1} = dom rec ((x \in V ⟼ 𝒫 x), \emptyset)$
7		limeq	$⊢ dom R_{1} = dom rec ((x \in V ⟼ 𝒫 x), \emptyset) \to (Lim dom R_{1} \leftrightarrow Lim dom rec ((x \in V ⟼ 𝒫 x), \emptyset))$
8	6 7	ax-mp	$⊢ Lim dom R_{1} \leftrightarrow Lim dom rec ((x \in V ⟼ 𝒫 x), \emptyset)$
9	5 8	mpbir	$⊢ Lim dom R_{1}$
10	4 9	pm3.2i	$⊢ (Fun R_{1} \land Lim dom R_{1})$