Metamath Proof Explorer

Theorem rdgseg

Description: The initial segments of the recursive definition generator are sets. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion rdgseg ⊢ B ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ↾ B ∈ V

Proof

Step Hyp Ref Expression
1 df-rdg ⊢ rec ⁡ F A = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
2 1 reseq1i ⊢ rec ⁡ F A ↾ B = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ↾ B
3 rdglem1 ⊢ w | ∃ y ∈ On w Fn y ∧ ∀ v ∈ y w ⁡ v = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ w ↾ v = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ f ↾ y
4 3 tfrlem9a ⊢ B ∈ dom ⁡ recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g → recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ↾ B ∈ V
5 1 dmeqi ⊢ dom ⁡ rec ⁡ F A = dom ⁡ recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
6 4 5 eleq2s ⊢ B ∈ dom ⁡ rec ⁡ F A → recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ↾ B ∈ V
7 2 6 eqeltrid ⊢ B ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ↾ B ∈ V