Step |
Hyp |
Ref |
Expression |
1 |
|
0opn |
⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 ) |
2 |
1
|
adantr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 = ∅ ) → ∅ ∈ 𝐽 ) |
3 |
|
eleq1 |
⊢ ( 𝑆 = ∅ → ( 𝑆 ∈ 𝐽 ↔ ∅ ∈ 𝐽 ) ) |
4 |
3
|
adantl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 = ∅ ) → ( 𝑆 ∈ 𝐽 ↔ ∅ ∈ 𝐽 ) ) |
5 |
2 4
|
mpbird |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 = ∅ ) → 𝑆 ∈ 𝐽 ) |
6 |
|
rzal |
⊢ ( 𝑆 = ∅ → ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
7 |
6
|
adantl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 = ∅ ) → ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
8 |
5 7
|
2thd |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 = ∅ ) → ( 𝑆 ∈ 𝐽 ↔ ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ) |
9 |
|
opnneip |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
10 |
9
|
3expia |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑆 → 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ) |
11 |
10
|
ralrimiv |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
12 |
11
|
ex |
⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ 𝐽 → ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ) |
13 |
12
|
adantr |
⊢ ( ( 𝐽 ∈ Top ∧ ¬ 𝑆 = ∅ ) → ( 𝑆 ∈ 𝐽 → ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ) |
14 |
|
df-ne |
⊢ ( 𝑆 ≠ ∅ ↔ ¬ 𝑆 = ∅ ) |
15 |
|
r19.2z |
⊢ ( ( 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ∃ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
16 |
15
|
ex |
⊢ ( 𝑆 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ∃ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ) |
17 |
14 16
|
sylbir |
⊢ ( ¬ 𝑆 = ∅ → ( ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ∃ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ) |
18 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
19 |
18
|
neii1 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑆 ⊆ ∪ 𝐽 ) |
20 |
19
|
ex |
⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆 ⊆ ∪ 𝐽 ) ) |
21 |
20
|
rexlimdvw |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆 ⊆ ∪ 𝐽 ) ) |
22 |
17 21
|
sylan9r |
⊢ ( ( 𝐽 ∈ Top ∧ ¬ 𝑆 = ∅ ) → ( ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆 ⊆ ∪ 𝐽 ) ) |
23 |
18
|
ntrss2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) |
24 |
23
|
adantr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) |
25 |
|
vex |
⊢ 𝑥 ∈ V |
26 |
25
|
snss |
⊢ ( 𝑥 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↔ { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) |
27 |
26
|
ralbii |
⊢ ( ∀ 𝑥 ∈ 𝑆 𝑥 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) |
28 |
|
dfss3 |
⊢ ( 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 𝑥 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) |
29 |
28
|
biimpri |
⊢ ( ∀ 𝑥 ∈ 𝑆 𝑥 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) → 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) |
30 |
29
|
adantl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) |
31 |
27 30
|
sylan2br |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) |
32 |
24 31
|
eqssd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) |
33 |
32
|
ex |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ∀ 𝑥 ∈ 𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) ) |
34 |
25
|
snss |
⊢ ( 𝑥 ∈ 𝑆 ↔ { 𝑥 } ⊆ 𝑆 ) |
35 |
|
sstr2 |
⊢ ( { 𝑥 } ⊆ 𝑆 → ( 𝑆 ⊆ ∪ 𝐽 → { 𝑥 } ⊆ ∪ 𝐽 ) ) |
36 |
35
|
com12 |
⊢ ( 𝑆 ⊆ ∪ 𝐽 → ( { 𝑥 } ⊆ 𝑆 → { 𝑥 } ⊆ ∪ 𝐽 ) ) |
37 |
36
|
adantl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( { 𝑥 } ⊆ 𝑆 → { 𝑥 } ⊆ ∪ 𝐽 ) ) |
38 |
34 37
|
syl5bi |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑥 ∈ 𝑆 → { 𝑥 } ⊆ ∪ 𝐽 ) ) |
39 |
38
|
imp |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) ∧ 𝑥 ∈ 𝑆 ) → { 𝑥 } ⊆ ∪ 𝐽 ) |
40 |
18
|
neiint |
⊢ ( ( 𝐽 ∈ Top ∧ { 𝑥 } ⊆ ∪ 𝐽 ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↔ { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) |
41 |
40
|
3com23 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ { 𝑥 } ⊆ ∪ 𝐽 ) → ( 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↔ { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) |
42 |
41
|
3expa |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) ∧ { 𝑥 } ⊆ ∪ 𝐽 ) → ( 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↔ { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) |
43 |
39 42
|
syldan |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↔ { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) |
44 |
43
|
ralbidva |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↔ ∀ 𝑥 ∈ 𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) |
45 |
18
|
isopn3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑆 ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) ) |
46 |
33 44 45
|
3imtr4d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆 ∈ 𝐽 ) ) |
47 |
46
|
ex |
⊢ ( 𝐽 ∈ Top → ( 𝑆 ⊆ ∪ 𝐽 → ( ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆 ∈ 𝐽 ) ) ) |
48 |
47
|
com23 |
⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ( 𝑆 ⊆ ∪ 𝐽 → 𝑆 ∈ 𝐽 ) ) ) |
49 |
48
|
adantr |
⊢ ( ( 𝐽 ∈ Top ∧ ¬ 𝑆 = ∅ ) → ( ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ( 𝑆 ⊆ ∪ 𝐽 → 𝑆 ∈ 𝐽 ) ) ) |
50 |
22 49
|
mpdd |
⊢ ( ( 𝐽 ∈ Top ∧ ¬ 𝑆 = ∅ ) → ( ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆 ∈ 𝐽 ) ) |
51 |
13 50
|
impbid |
⊢ ( ( 𝐽 ∈ Top ∧ ¬ 𝑆 = ∅ ) → ( 𝑆 ∈ 𝐽 ↔ ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ) |
52 |
8 51
|
pm2.61dan |
⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ 𝐽 ↔ ∀ 𝑥 ∈ 𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ) |