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	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐼 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐼 ) ‘ ∪ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		onsucuni3	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → 𝐵 = suc ∪ 𝐵 )
2	1	fveq2d	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐼 ) ‘ 𝐵 ) = ( rec ( 𝐹 , 𝐼 ) ‘ suc ∪ 𝐵 ) )
3		onuni	⊢ ( 𝐵 ∈ On → ∪ 𝐵 ∈ On )
4	3	3ad2ant1	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → ∪ 𝐵 ∈ On )
5		rdgsuc	⊢ ( ∪ 𝐵 ∈ On → ( rec ( 𝐹 , 𝐼 ) ‘ suc ∪ 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐼 ) ‘ ∪ 𝐵 ) ) )
6	4 5	syl	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐼 ) ‘ suc ∪ 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐼 ) ‘ ∪ 𝐵 ) ) )
7	2 6	eqtrd	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐼 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐼 ) ‘ ∪ 𝐵 ) ) )