Step |
Hyp |
Ref |
Expression |
1 |
|
ishaus2 |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Haus ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) |
2 |
|
topontop |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top ) |
3 |
|
simp1 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → 𝐽 ∈ Top ) |
4 |
|
simp2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → 𝑚 ∈ 𝐽 ) |
5 |
|
simp1 |
⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → 𝑥 ∈ 𝑚 ) |
6 |
|
opnneip |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑥 ∈ 𝑚 ) → 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
7 |
3 4 5 6
|
syl2an3an |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) → 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
8 |
|
simp3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → 𝑛 ∈ 𝐽 ) |
9 |
|
simp2 |
⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → 𝑦 ∈ 𝑛 ) |
10 |
|
opnneip |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑛 ∈ 𝐽 ∧ 𝑦 ∈ 𝑛 ) → 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) |
11 |
3 8 9 10
|
syl2an3an |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) → 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) |
12 |
|
simpr3 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) → ( 𝑚 ∩ 𝑛 ) = ∅ ) |
13 |
|
ineq1 |
⊢ ( 𝑢 = 𝑚 → ( 𝑢 ∩ 𝑣 ) = ( 𝑚 ∩ 𝑣 ) ) |
14 |
13
|
eqeq1d |
⊢ ( 𝑢 = 𝑚 → ( ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ( 𝑚 ∩ 𝑣 ) = ∅ ) ) |
15 |
|
ineq2 |
⊢ ( 𝑣 = 𝑛 → ( 𝑚 ∩ 𝑣 ) = ( 𝑚 ∩ 𝑛 ) ) |
16 |
15
|
eqeq1d |
⊢ ( 𝑣 = 𝑛 → ( ( 𝑚 ∩ 𝑣 ) = ∅ ↔ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) |
17 |
14 16
|
rspc2ev |
⊢ ( ( 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) |
18 |
7 11 12 17
|
syl3anc |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) |
19 |
18
|
ex |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) |
20 |
19
|
3expib |
⊢ ( 𝐽 ∈ Top → ( ( 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
21 |
20
|
rexlimdvv |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) |
22 |
|
neii2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ) |
23 |
22
|
ex |
⊢ ( 𝐽 ∈ Top → ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ) ) |
24 |
|
neii2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) → ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) |
25 |
24
|
ex |
⊢ ( 𝐽 ∈ Top → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) → ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) |
26 |
|
vex |
⊢ 𝑥 ∈ V |
27 |
26
|
snss |
⊢ ( 𝑥 ∈ 𝑚 ↔ { 𝑥 } ⊆ 𝑚 ) |
28 |
27
|
anbi1i |
⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ↔ ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ) |
29 |
|
vex |
⊢ 𝑦 ∈ V |
30 |
29
|
snss |
⊢ ( 𝑦 ∈ 𝑛 ↔ { 𝑦 } ⊆ 𝑛 ) |
31 |
30
|
anbi1i |
⊢ ( ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ↔ ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) |
32 |
|
simp1l |
⊢ ( ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → 𝑥 ∈ 𝑚 ) |
33 |
|
simp2l |
⊢ ( ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → 𝑦 ∈ 𝑛 ) |
34 |
|
ss2in |
⊢ ( ( 𝑚 ⊆ 𝑢 ∧ 𝑛 ⊆ 𝑣 ) → ( 𝑚 ∩ 𝑛 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) |
35 |
|
ssn0 |
⊢ ( ( ( 𝑚 ∩ 𝑛 ) ⊆ ( 𝑢 ∩ 𝑣 ) ∧ ( 𝑚 ∩ 𝑛 ) ≠ ∅ ) → ( 𝑢 ∩ 𝑣 ) ≠ ∅ ) |
36 |
35
|
ex |
⊢ ( ( 𝑚 ∩ 𝑛 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( ( 𝑚 ∩ 𝑛 ) ≠ ∅ → ( 𝑢 ∩ 𝑣 ) ≠ ∅ ) ) |
37 |
36
|
necon4d |
⊢ ( ( 𝑚 ∩ 𝑛 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( 𝑚 ∩ 𝑛 ) = ∅ ) ) |
38 |
34 37
|
syl |
⊢ ( ( 𝑚 ⊆ 𝑢 ∧ 𝑛 ⊆ 𝑣 ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( 𝑚 ∩ 𝑛 ) = ∅ ) ) |
39 |
38
|
ad2ant2l |
⊢ ( ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( 𝑚 ∩ 𝑛 ) = ∅ ) ) |
40 |
39
|
3impia |
⊢ ( ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ( 𝑚 ∩ 𝑛 ) = ∅ ) |
41 |
32 33 40
|
3jca |
⊢ ( ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) |
42 |
41
|
3exp |
⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ( ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) |
43 |
31 42
|
syl5bir |
⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ( ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) |
44 |
43
|
com3r |
⊢ ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ( ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) |
45 |
44
|
imp |
⊢ ( ( ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ) → ( ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) |
46 |
45
|
3adant1 |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ) → ( ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) |
47 |
46
|
reximdv |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ) → ( ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) |
48 |
47
|
3exp |
⊢ ( 𝐽 ∈ Top → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ( ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) ) |
49 |
48
|
com34 |
⊢ ( 𝐽 ∈ Top → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) ) |
50 |
49
|
3imp |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) → ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) |
51 |
28 50
|
syl5bir |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) → ( ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) |
52 |
51
|
reximdv |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) → ( ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) |
53 |
52
|
3exp |
⊢ ( 𝐽 ∈ Top → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) ) |
54 |
53
|
com24 |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ( ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) ) |
55 |
54
|
impd |
⊢ ( 𝐽 ∈ Top → ( ( ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) |
56 |
23 25 55
|
syl2and |
⊢ ( 𝐽 ∈ Top → ( ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) |
57 |
56
|
rexlimdvv |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) |
58 |
21 57
|
impbid |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) |
59 |
58
|
imbi2d |
⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
60 |
59
|
2ralbidv |
⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
61 |
2 60
|
syl |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
62 |
1 61
|
bitrd |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Haus ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |