r1dmlim

Description: The domain of the cumulative hierarchy of sets function is a limit ordinal. This weak form of r1fnon avoids ax-rep . (Contributed by Mario Carneiro, 16-Nov-2014) Extract this statement from its conjunction with r1fun . (Revised by BJ, 27-Sep-2026)

		Ref	Expression
	Assertion	r1dmlim	$⊢ Lim dom R_{1}$

Proof

Step	Hyp	Ref	Expression
1		rdgdmlim	$⊢ Lim dom rec ((x \in V ⟼ 𝒫 x), \emptyset)$
2		df-r1	$⊢ R_{1} = rec ((x \in V ⟼ 𝒫 x), \emptyset)$
3	2	dmeqi	$⊢ dom R_{1} = dom rec ((x \in V ⟼ 𝒫 x), \emptyset)$
4		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))$
5	3 4	ax-mp	$⊢ Lim dom R_{1} \leftrightarrow Lim dom rec ((x \in V ⟼ 𝒫 x), \emptyset)$
6	1 5	mpbir	$⊢ Lim dom R_{1}$

Metamath Proof Explorer

Theorem r1dmlim

Proof