Metamath Proof Explorer

Theorem rdglim

Description: The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)

		Ref	Expression
	Assertion	rdglim	$⊢ (B \in C \land Lim B) \to rec (F, A) (B) = ⋃ rec (F, A) [B]$

Proof

Step	Hyp	Ref	Expression
1		limelon	$⊢ (B \in C \land Lim B) \to B \in On$
2		rdgfnon	$⊢ rec (F, A) Fn On$
3		fndm	$⊢ rec (F, A) Fn On \to dom rec (F, A) = On$
4	2 3	ax-mp	$⊢ dom rec (F, A) = On$
5	1 4	eleqtrrdi	$⊢ (B \in C \land Lim B) \to B \in dom rec (F, A)$
6		rdglimg	$⊢ (B \in dom rec (F, A) \land Lim B) \to rec (F, A) (B) = ⋃ rec (F, A) [B]$
7	5 6	sylancom	$⊢ (B \in C \land Lim B) \to rec (F, A) (B) = ⋃ rec (F, A) [B]$