r1funlimOLD

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) (Proof modification is discouraged.) Use r1fun or r1dmlim instead. (New usage is discouraged.)

		Ref	Expression
	Assertion	r1funlimOLD	$⊢ (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})$

Metamath Proof Explorer

Theorem r1funlimOLD

Proof