Metamath Proof Explorer

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∈On∧Lim⁡B∧C∈B→rec⁡FA⁡C⊆rec⁡FA⁡B

Proof

Step Hyp Ref Expression
1 rdgellim ⊢B∈On∧Lim⁡B∧C∈B→x∈rec⁡FA⁡C→x∈rec⁡FA⁡B
2 1 ssrdv ⊢B∈On∧Lim⁡B∧C∈B→rec⁡FA⁡C⊆rec⁡FA⁡B