Theorem rdglimss

Description: A recursive definition at a limit ordinal is a superset of itself at any smaller ordinal. (Contributed by ML, 30-Mar-2022)

	Ref	Expression
Assertion	rdglimss	⊢ ( ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rdgellim	⊢ ( ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝑥 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) → 𝑥 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )
2	1	ssrdv	⊢ ( ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) )