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	|- ( ( ( B e. On /\ Lim B ) /\ C e. B ) -> ( rec ( F , A ) ` C ) C_ ( rec ( F , A ) ` B ) )

Proof

Step	Hyp	Ref	Expression
1		rdgellim	|- ( ( ( B e. On /\ Lim B ) /\ C e. B ) -> ( x e. ( rec ( F , A ) ` C ) -> x e. ( rec ( F , A ) ` B ) ) )
2	1	ssrdv	|- ( ( ( B e. On /\ Lim B ) /\ C e. B ) -> ( rec ( F , A ) ` C ) C_ ( rec ( F , A ) ` B ) )