Theorem nffrecs

Description: Bound-variable hypothesis builder for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021)

	Ref	Expression
Hypotheses	nffrecs.1	⊢ Ⅎ 𝑥 𝑅
	nffrecs.2	⊢ Ⅎ 𝑥 𝐴
	nffrecs.3	⊢ Ⅎ 𝑥 𝐹
Assertion	nffrecs	⊢ Ⅎ 𝑥 frecs ( 𝑅 , 𝐴 , 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		nffrecs.1	⊢ Ⅎ 𝑥 𝑅
2		nffrecs.2	⊢ Ⅎ 𝑥 𝐴
3		nffrecs.3	⊢ Ⅎ 𝑥 𝐹
4		df-frecs	⊢ frecs ( 𝑅 , 𝐴 , 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑦 ( 𝑓 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	8 3 14	nfov	⊢ Ⅎ 𝑥 ( 𝑧 𝐹 ( 𝑓 ↾ 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	⊢ Ⅎ 𝑥 frecs ( 𝑅 , 𝐴 , 𝐹 )