Step |
Hyp |
Ref |
Expression |
1 |
|
clscld.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
1
|
ntrval |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ) |
3 |
|
inss2 |
⊢ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝒫 𝑆 |
4 |
3
|
unissi |
⊢ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ ∪ 𝒫 𝑆 |
5 |
|
unipw |
⊢ ∪ 𝒫 𝑆 = 𝑆 |
6 |
4 5
|
sseqtri |
⊢ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝑆 |
7 |
6
|
a1i |
⊢ ( 𝑆 ∈ 𝐽 → ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝑆 ) |
8 |
|
id |
⊢ ( 𝑆 ∈ 𝐽 → 𝑆 ∈ 𝐽 ) |
9 |
|
pwidg |
⊢ ( 𝑆 ∈ 𝐽 → 𝑆 ∈ 𝒫 𝑆 ) |
10 |
8 9
|
elind |
⊢ ( 𝑆 ∈ 𝐽 → 𝑆 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) ) |
11 |
|
elssuni |
⊢ ( 𝑆 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) → 𝑆 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ) |
12 |
10 11
|
syl |
⊢ ( 𝑆 ∈ 𝐽 → 𝑆 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ) |
13 |
7 12
|
eqssd |
⊢ ( 𝑆 ∈ 𝐽 → ∪ ( 𝐽 ∩ 𝒫 𝑆 ) = 𝑆 ) |
14 |
2 13
|
sylan9eq |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑆 ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) |
15 |
14
|
ex |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐽 → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) ) |
16 |
1
|
ntropn |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 ) |
17 |
|
eleq1 |
⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 ↔ 𝑆 ∈ 𝐽 ) ) |
18 |
16 17
|
syl5ibcom |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 → 𝑆 ∈ 𝐽 ) ) |
19 |
15 18
|
impbid |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) ) |