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

Metamath Proof Explorer

Theorem r1lim

Description: Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of TakeutiZaring p. 76. (Contributed by NM, 4-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	r1lim	$⊢ (A \in B \land Lim A) \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$

Proof

Step	Hyp	Ref	Expression
1		limelon	$⊢ (A \in B \land Lim A) \to A \in On$
2		r1fnon	$⊢ R_{1} Fn On$
3		fndm	$⊢ R_{1} Fn On \to dom R_{1} = On$
4	2 3	ax-mp	$⊢ dom R_{1} = On$
5	1 4	eleqtrrdi	$⊢ (A \in B \land Lim A) \to A \in dom R_{1}$
6		r1limg	$⊢ (A \in dom R_{1} \land Lim A) \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$
7	5 6	sylancom	$⊢ (A \in B \land Lim A) \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$