Step |
Hyp |
Ref |
Expression |
0 |
|
cha |
⊢ Haus |
1 |
|
vj |
⊢ 𝑗 |
2 |
|
ctop |
⊢ Top |
3 |
|
vx |
⊢ 𝑥 |
4 |
1
|
cv |
⊢ 𝑗 |
5 |
4
|
cuni |
⊢ ∪ 𝑗 |
6 |
|
vy |
⊢ 𝑦 |
7 |
3
|
cv |
⊢ 𝑥 |
8 |
6
|
cv |
⊢ 𝑦 |
9 |
7 8
|
wne |
⊢ 𝑥 ≠ 𝑦 |
10 |
|
vn |
⊢ 𝑛 |
11 |
|
vm |
⊢ 𝑚 |
12 |
10
|
cv |
⊢ 𝑛 |
13 |
7 12
|
wcel |
⊢ 𝑥 ∈ 𝑛 |
14 |
11
|
cv |
⊢ 𝑚 |
15 |
8 14
|
wcel |
⊢ 𝑦 ∈ 𝑚 |
16 |
12 14
|
cin |
⊢ ( 𝑛 ∩ 𝑚 ) |
17 |
|
c0 |
⊢ ∅ |
18 |
16 17
|
wceq |
⊢ ( 𝑛 ∩ 𝑚 ) = ∅ |
19 |
13 15 18
|
w3a |
⊢ ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) |
20 |
19 11 4
|
wrex |
⊢ ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) |
21 |
20 10 4
|
wrex |
⊢ ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) |
22 |
9 21
|
wi |
⊢ ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) |
23 |
22 6 5
|
wral |
⊢ ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) |
24 |
23 3 5
|
wral |
⊢ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) |
25 |
24 1 2
|
crab |
⊢ { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) } |
26 |
0 25
|
wceq |
⊢ Haus = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) } |