Step |
Hyp |
Ref |
Expression |
0 |
|
cR |
⊢ 𝑅 |
1 |
|
cA |
⊢ 𝐴 |
2 |
|
cF |
⊢ 𝐹 |
3 |
1 0 2
|
cwrecs |
⊢ wrecs ( 𝑅 , 𝐴 , 𝐹 ) |
4 |
|
vf |
⊢ 𝑓 |
5 |
|
vx |
⊢ 𝑥 |
6 |
4
|
cv |
⊢ 𝑓 |
7 |
5
|
cv |
⊢ 𝑥 |
8 |
6 7
|
wfn |
⊢ 𝑓 Fn 𝑥 |
9 |
7 1
|
wss |
⊢ 𝑥 ⊆ 𝐴 |
10 |
|
vy |
⊢ 𝑦 |
11 |
10
|
cv |
⊢ 𝑦 |
12 |
1 0 11
|
cpred |
⊢ Pred ( 𝑅 , 𝐴 , 𝑦 ) |
13 |
12 7
|
wss |
⊢ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 |
14 |
13 10 7
|
wral |
⊢ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 |
15 |
9 14
|
wa |
⊢ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) |
16 |
11 6
|
cfv |
⊢ ( 𝑓 ‘ 𝑦 ) |
17 |
6 12
|
cres |
⊢ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) |
18 |
17 2
|
cfv |
⊢ ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) |
19 |
16 18
|
wceq |
⊢ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) |
20 |
19 10 7
|
wral |
⊢ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) |
21 |
8 15 20
|
w3a |
⊢ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) |
22 |
21 5
|
wex |
⊢ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) |
23 |
22 4
|
cab |
⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } |
24 |
23
|
cuni |
⊢ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } |
25 |
3 24
|
wceq |
⊢ wrecs ( 𝑅 , 𝐴 , 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } |