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

Metamath Proof Explorer

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 ( 𝑅 , 𝐴 , 𝐹 )