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 ⁡ F A ⁡ C ⊆ rec ⁡ F A ⁡ B

Proof

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