Metamath Proof Explorer


Theorem nfwrecs

Description: Bound-variable hypothesis builder for the well-ordered recursive function generator. (Contributed by Scott Fenton, 9-Jun-2018)

Ref Expression
Hypotheses nfwrecs.1 𝑥 𝑅
nfwrecs.2 𝑥 𝐴
nfwrecs.3 𝑥 𝐹
Assertion nfwrecs 𝑥 wrecs ( 𝑅 , 𝐴 , 𝐹 )

Proof

Step Hyp Ref Expression
1 nfwrecs.1 𝑥 𝑅
2 nfwrecs.2 𝑥 𝐴
3 nfwrecs.3 𝑥 𝐹
4 df-wrecs wrecs ( 𝑅 , 𝐴 , 𝐹 ) = { 𝑓 ∣ ∃ 𝑦 ( 𝑓 Fn 𝑦 ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝑦 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑦 ) ∧ ∀ 𝑧𝑦 ( 𝑓𝑧 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) }
5 nfv 𝑥 𝑓 Fn 𝑦
6 nfcv 𝑥 𝑦
7 6 2 nfss 𝑥 𝑦𝐴
8 nfcv 𝑥 𝑧
9 1 2 8 nfpred 𝑥 Pred ( 𝑅 , 𝐴 , 𝑧 )
10 9 6 nfss 𝑥 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑦
11 6 10 nfralw 𝑥𝑧𝑦 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑦
12 7 11 nfan 𝑥 ( 𝑦𝐴 ∧ ∀ 𝑧𝑦 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑦 )
13 nfcv 𝑥 𝑓
14 13 9 nfres 𝑥 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
15 3 14 nffv 𝑥 ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
16 15 nfeq2 𝑥 ( 𝑓𝑧 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
17 6 16 nfralw 𝑥𝑧𝑦 ( 𝑓𝑧 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
18 5 12 17 nf3an 𝑥 ( 𝑓 Fn 𝑦 ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝑦 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑦 ) ∧ ∀ 𝑧𝑦 ( 𝑓𝑧 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
19 18 nfex 𝑥𝑦 ( 𝑓 Fn 𝑦 ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝑦 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑦 ) ∧ ∀ 𝑧𝑦 ( 𝑓𝑧 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
20 19 nfab 𝑥 { 𝑓 ∣ ∃ 𝑦 ( 𝑓 Fn 𝑦 ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝑦 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑦 ) ∧ ∀ 𝑧𝑦 ( 𝑓𝑧 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) }
21 20 nfuni 𝑥 { 𝑓 ∣ ∃ 𝑦 ( 𝑓 Fn 𝑦 ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝑦 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑦 ) ∧ ∀ 𝑧𝑦 ( 𝑓𝑧 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) }
22 4 21 nfcxfr 𝑥 wrecs ( 𝑅 , 𝐴 , 𝐹 )