Metamath Proof Explorer

Theorem rdgellim

Description: Elementhood in a recursive definition at a limit ordinal. (Contributed by ML, 30-Mar-2022)

Ref Expression
Assertion rdgellim ⊢ B ∈ On ∧ Lim ⁡ B ∧ C ∈ B → X ∈ rec ⁡ F A ⁡ C → X ∈ rec ⁡ F A ⁡ B

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ y = C → rec ⁡ F A ⁡ y = rec ⁡ F A ⁡ C
2 1 eleq2d ⊢ y = C → X ∈ rec ⁡ F A ⁡ y ↔ X ∈ rec ⁡ F A ⁡ C
3 2 rspcev ⊢ C ∈ B ∧ X ∈ rec ⁡ F A ⁡ C → ∃ y ∈ B X ∈ rec ⁡ F A ⁡ y
4 3 ex ⊢ C ∈ B → X ∈ rec ⁡ F A ⁡ C → ∃ y ∈ B X ∈ rec ⁡ F A ⁡ y
5 eliun ⊢ X ∈ ⋃ y ∈ B rec ⁡ F A ⁡ y ↔ ∃ y ∈ B X ∈ rec ⁡ F A ⁡ y
6 4 5 imbitrrdi ⊢ C ∈ B → X ∈ rec ⁡ F A ⁡ C → X ∈ ⋃ y ∈ B rec ⁡ F A ⁡ y
7 6 adantl ⊢ B ∈ On ∧ Lim ⁡ B ∧ C ∈ B → X ∈ rec ⁡ F A ⁡ C → X ∈ ⋃ y ∈ B rec ⁡ F A ⁡ y
8 rdglim2a ⊢ B ∈ On ∧ Lim ⁡ B → rec ⁡ F A ⁡ B = ⋃ y ∈ B rec ⁡ F A ⁡ y
9 8 eleq2d ⊢ B ∈ On ∧ Lim ⁡ B → X ∈ rec ⁡ F A ⁡ B ↔ X ∈ ⋃ y ∈ B rec ⁡ F A ⁡ y
10 9 adantr ⊢ B ∈ On ∧ Lim ⁡ B ∧ C ∈ B → X ∈ rec ⁡ F A ⁡ B ↔ X ∈ ⋃ y ∈ B rec ⁡ F A ⁡ y
11 7 10 sylibrd ⊢ B ∈ On ∧ Lim ⁡ B ∧ C ∈ B → X ∈ rec ⁡ F A ⁡ C → X ∈ rec ⁡ F A ⁡ B