Detailed syntax breakdown of Definition df-frecs
Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class 𝐴 |
2 | | cR |
. . 3
class 𝑅 |
3 | | cF |
. . 3
class 𝐹 |
4 | 1, 2, 3 | cfrecs 33440 |
. 2
class
frecs(𝑅, 𝐴, 𝐹) |
5 | | vf |
. . . . . . . 8
setvar 𝑓 |
6 | 5 | cv 1541 |
. . . . . . 7
class 𝑓 |
7 | | vx |
. . . . . . . 8
setvar 𝑥 |
8 | 7 | cv 1541 |
. . . . . . 7
class 𝑥 |
9 | 6, 8 | wfn 6335 |
. . . . . 6
wff 𝑓 Fn 𝑥 |
10 | 8, 1 | wss 3844 |
. . . . . . 7
wff 𝑥 ⊆ 𝐴 |
11 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
12 | 11 | cv 1541 |
. . . . . . . . . 10
class 𝑦 |
13 | 1, 2, 12 | cpred 6129 |
. . . . . . . . 9
class
Pred(𝑅, 𝐴, 𝑦) |
14 | 13, 8 | wss 3844 |
. . . . . . . 8
wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 |
15 | 14, 11, 8 | wral 3054 |
. . . . . . 7
wff
∀𝑦 ∈
𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 |
16 | 10, 15 | wa 399 |
. . . . . 6
wff (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) |
17 | 12, 6 | cfv 6340 |
. . . . . . . 8
class (𝑓‘𝑦) |
18 | 6, 13 | cres 5528 |
. . . . . . . . 9
class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)) |
19 | 12, 18, 3 | co 7173 |
. . . . . . . 8
class (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) |
20 | 17, 19 | wceq 1542 |
. . . . . . 7
wff (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) |
21 | 20, 11, 8 | wral 3054 |
. . . . . 6
wff
∀𝑦 ∈
𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) |
22 | 9, 16, 21 | w3a 1088 |
. . . . 5
wff (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) |
23 | 22, 7 | wex 1786 |
. . . 4
wff
∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) |
24 | 23, 5 | cab 2717 |
. . 3
class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} |
25 | 24 | cuni 4797 |
. 2
class ∪ {𝑓
∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} |
26 | 4, 25 | wceq 1542 |
1
wff frecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} |