This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑥 𝐹
nfrdg.2 ⊢ Ⅎ 𝑥 𝐴
Assertion nfrdg Ⅎ 𝑥 rec ( 𝐹 , 𝐴 )

Proof

Step Hyp Ref Expression
1 nfrdg.1 ⊢ Ⅎ 𝑥 𝐹
2 nfrdg.2 ⊢ Ⅎ 𝑥 𝐴
3 df-rdg ⊢ rec ( 𝐹 , 𝐴 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
4 nfcv ⊢ Ⅎ 𝑥 V
5 nfv ⊢ Ⅎ 𝑥 𝑔 = ∅
6 nfv ⊢ Ⅎ 𝑥 Lim dom 𝑔
7 nfcv ⊢ Ⅎ 𝑥 ∪ ran 𝑔
8 nfcv ⊢ Ⅎ 𝑥 ( 𝑔 ‘ ∪ dom 𝑔 )
9 1 8 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) )
10 6 7 9 nfif ⊢ Ⅎ 𝑥 if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) )
11 5 2 10 nfif ⊢ Ⅎ 𝑥 if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) )
12 4 11 nfmpt ⊢ Ⅎ 𝑥 ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) )
13 12 nfrecs ⊢ Ⅎ 𝑥 recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
14 3 13 nfcxfr ⊢ Ⅎ 𝑥 rec ( 𝐹 , 𝐴 )