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