Metamath Proof Explorer

Theorem rdgsucuni

Description: If an ordinal number has a predecessor, the value of the recursive definition generator at that number in terms of its predecessor. (Contributed by ML, 17-Oct-2020)

		Ref	Expression
	Assertion	rdgsucuni	$⊢ (B \in On \land B \neq \emptyset \land \neg Lim B) \to rec (F, I) (B) = F (rec (F, I) (⋃ B))$

Proof

Step	Hyp	Ref	Expression
1		onsucuni3	$⊢ (B \in On \land B \neq \emptyset \land \neg Lim B) \to B = suc ⋃ B$
2	1	fveq2d	$⊢ (B \in On \land B \neq \emptyset \land \neg Lim B) \to rec (F, I) (B) = rec (F, I) (suc ⋃ B)$
3		onuni	$⊢ B \in On \to ⋃ B \in On$
4	3	3ad2ant1	$⊢ (B \in On \land B \neq \emptyset \land \neg Lim B) \to ⋃ B \in On$
5		rdgsuc	$⊢ ⋃ B \in On \to rec (F, I) (suc ⋃ B) = F (rec (F, I) (⋃ B))$
6	4 5	syl	$⊢ (B \in On \land B \neq \emptyset \land \neg Lim B) \to rec (F, I) (suc ⋃ B) = F (rec (F, I) (⋃ B))$
7	2 6	eqtrd	$⊢ (B \in On \land B \neq \emptyset \land \neg Lim B) \to rec (F, I) (B) = F (rec (F, I) (⋃ B))$