Theorem nfwrecs

Description: Bound-variable hypothesis builder for the well-founded 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 ( 𝑅 , 𝐴 , 𝐹 )