Detailed syntax breakdown of Definition df-fcls
Step | Hyp | Ref
| Expression |
1 | | cfcls 23087 |
. 2
class
fClus |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | ctop 22042 |
. . 3
class
Top |
5 | | cfil 22996 |
. . . . 5
class
Fil |
6 | 5 | crn 5590 |
. . . 4
class ran
Fil |
7 | 6 | cuni 4839 |
. . 3
class ∪ ran Fil |
8 | 2 | cv 1538 |
. . . . . 6
class 𝑗 |
9 | 8 | cuni 4839 |
. . . . 5
class ∪ 𝑗 |
10 | 3 | cv 1538 |
. . . . . 6
class 𝑓 |
11 | 10 | cuni 4839 |
. . . . 5
class ∪ 𝑓 |
12 | 9, 11 | wceq 1539 |
. . . 4
wff ∪ 𝑗 =
∪ 𝑓 |
13 | | vx |
. . . . 5
setvar 𝑥 |
14 | 13 | cv 1538 |
. . . . . 6
class 𝑥 |
15 | | ccl 22169 |
. . . . . . 7
class
cls |
16 | 8, 15 | cfv 6433 |
. . . . . 6
class
(cls‘𝑗) |
17 | 14, 16 | cfv 6433 |
. . . . 5
class
((cls‘𝑗)‘𝑥) |
18 | 13, 10, 17 | ciin 4925 |
. . . 4
class ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥) |
19 | | c0 4256 |
. . . 4
class
∅ |
20 | 12, 18, 19 | cif 4459 |
. . 3
class if(∪ 𝑗 =
∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅) |
21 | 2, 3, 4, 7, 20 | cmpo 7277 |
. 2
class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil
↦ if(∪ 𝑗 = ∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅)) |
22 | 1, 21 | wceq 1539 |
1
wff fClus =
(𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ if(∪ 𝑗 = ∪
𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅)) |