Detailed syntax breakdown of Definition df-fcls
Step | Hyp | Ref
| Expression |
1 | | cfcls 22688 |
. 2
class
fClus |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | ctop 21645 |
. . 3
class
Top |
5 | | cfil 22597 |
. . . . 5
class
Fil |
6 | 5 | crn 5527 |
. . . 4
class ran
Fil |
7 | 6 | cuni 4797 |
. . 3
class ∪ ran Fil |
8 | 2 | cv 1541 |
. . . . . 6
class 𝑗 |
9 | 8 | cuni 4797 |
. . . . 5
class ∪ 𝑗 |
10 | 3 | cv 1541 |
. . . . . 6
class 𝑓 |
11 | 10 | cuni 4797 |
. . . . 5
class ∪ 𝑓 |
12 | 9, 11 | wceq 1542 |
. . . 4
wff ∪ 𝑗 =
∪ 𝑓 |
13 | | vx |
. . . . 5
setvar 𝑥 |
14 | 13 | cv 1541 |
. . . . . 6
class 𝑥 |
15 | | ccl 21770 |
. . . . . . 7
class
cls |
16 | 8, 15 | cfv 6340 |
. . . . . 6
class
(cls‘𝑗) |
17 | 14, 16 | cfv 6340 |
. . . . 5
class
((cls‘𝑗)‘𝑥) |
18 | 13, 10, 17 | ciin 4883 |
. . . 4
class ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥) |
19 | | c0 4212 |
. . . 4
class
∅ |
20 | 12, 18, 19 | cif 4415 |
. . 3
class if(∪ 𝑗 =
∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅) |
21 | 2, 3, 4, 7, 20 | cmpo 7173 |
. 2
class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil
↦ if(∪ 𝑗 = ∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅)) |
22 | 1, 21 | wceq 1542 |
1
wff fClus =
(𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ if(∪ 𝑗 = ∪
𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅)) |