Step |
Hyp |
Ref |
Expression |
0 |
|
clocfin |
⊢ LocFin |
1 |
|
vx |
⊢ 𝑥 |
2 |
|
ctop |
⊢ Top |
3 |
|
vy |
⊢ 𝑦 |
4 |
1
|
cv |
⊢ 𝑥 |
5 |
4
|
cuni |
⊢ ∪ 𝑥 |
6 |
3
|
cv |
⊢ 𝑦 |
7 |
6
|
cuni |
⊢ ∪ 𝑦 |
8 |
5 7
|
wceq |
⊢ ∪ 𝑥 = ∪ 𝑦 |
9 |
|
vp |
⊢ 𝑝 |
10 |
|
vn |
⊢ 𝑛 |
11 |
9
|
cv |
⊢ 𝑝 |
12 |
10
|
cv |
⊢ 𝑛 |
13 |
11 12
|
wcel |
⊢ 𝑝 ∈ 𝑛 |
14 |
|
vs |
⊢ 𝑠 |
15 |
14
|
cv |
⊢ 𝑠 |
16 |
15 12
|
cin |
⊢ ( 𝑠 ∩ 𝑛 ) |
17 |
|
c0 |
⊢ ∅ |
18 |
16 17
|
wne |
⊢ ( 𝑠 ∩ 𝑛 ) ≠ ∅ |
19 |
18 14 6
|
crab |
⊢ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } |
20 |
|
cfn |
⊢ Fin |
21 |
19 20
|
wcel |
⊢ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin |
22 |
13 21
|
wa |
⊢ ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) |
23 |
22 10 4
|
wrex |
⊢ ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) |
24 |
23 9 5
|
wral |
⊢ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) |
25 |
8 24
|
wa |
⊢ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) |
26 |
25 3
|
cab |
⊢ { 𝑦 ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } |
27 |
1 2 26
|
cmpt |
⊢ ( 𝑥 ∈ Top ↦ { 𝑦 ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ) |
28 |
0 27
|
wceq |
⊢ LocFin = ( 𝑥 ∈ Top ↦ { 𝑦 ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑛 ∈ 𝑥 ( 𝑝 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑦 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) } ) |