Metamath Proof Explorer

Theorem nfrdg

Description: Bound-variable hypothesis builder for the recursive definition generator. (Contributed by NM, 14-Sep-2003) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Hypotheses nfrdg.1 ⊢ Ⅎ _ x F
nfrdg.2 ⊢ Ⅎ _ x A
Assertion nfrdg ⊢ Ⅎ _ x rec ⁡ F A

Proof

Step Hyp Ref Expression
1 nfrdg.1 ⊢ Ⅎ _ x F
2 nfrdg.2 ⊢ Ⅎ _ x A
3 df-rdg ⊢ rec ⁡ F A = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
4 nfcv ⊢ Ⅎ _ x V
5 nfv ⊢ Ⅎ x g = ∅
6 nfv ⊢ Ⅎ x Lim ⁡ dom ⁡ g
7 nfcv ⊢ Ⅎ _ x ⋃ ran ⁡ g
8 nfcv ⊢ Ⅎ _ x g ⁡ ⋃ dom ⁡ g
9 1 8 nffv ⊢ Ⅎ _ x F ⁡ g ⁡ ⋃ dom ⁡ g
10 6 7 9 nfif ⊢ Ⅎ _ x if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
11 5 2 10 nfif ⊢ Ⅎ _ x if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
12 4 11 nfmpt ⊢ Ⅎ _ x g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
13 12 nfrecs ⊢ Ⅎ _ x recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
14 3 13 nfcxfr ⊢ Ⅎ _ x rec ⁡ F A