Step |
Hyp |
Ref |
Expression |
0 |
|
cfcls |
⊢ fClus |
1 |
|
vj |
⊢ 𝑗 |
2 |
|
ctop |
⊢ Top |
3 |
|
vf |
⊢ 𝑓 |
4 |
|
cfil |
⊢ Fil |
5 |
4
|
crn |
⊢ ran Fil |
6 |
5
|
cuni |
⊢ ∪ ran Fil |
7 |
1
|
cv |
⊢ 𝑗 |
8 |
7
|
cuni |
⊢ ∪ 𝑗 |
9 |
3
|
cv |
⊢ 𝑓 |
10 |
9
|
cuni |
⊢ ∪ 𝑓 |
11 |
8 10
|
wceq |
⊢ ∪ 𝑗 = ∪ 𝑓 |
12 |
|
vx |
⊢ 𝑥 |
13 |
|
ccl |
⊢ cls |
14 |
7 13
|
cfv |
⊢ ( cls ‘ 𝑗 ) |
15 |
12
|
cv |
⊢ 𝑥 |
16 |
15 14
|
cfv |
⊢ ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) |
17 |
12 9 16
|
ciin |
⊢ ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) |
18 |
|
c0 |
⊢ ∅ |
19 |
11 17 18
|
cif |
⊢ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) |
20 |
1 3 2 6 19
|
cmpo |
⊢ ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) ) |
21 |
0 20
|
wceq |
⊢ fClus = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) ) |