Step |
Hyp |
Ref |
Expression |
1 |
|
topontop |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top ) |
2 |
|
0opn |
⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 ) |
3 |
1 2
|
syl |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∅ ∈ 𝐽 ) |
4 |
|
toponmax |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 ) |
5 |
3 4
|
prssd |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → { ∅ , 𝑋 } ⊆ 𝐽 ) |
6 |
|
toponuni |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
7 |
|
eqimss2 |
⊢ ( 𝑋 = ∪ 𝐽 → ∪ 𝐽 ⊆ 𝑋 ) |
8 |
6 7
|
syl |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∪ 𝐽 ⊆ 𝑋 ) |
9 |
|
sspwuni |
⊢ ( 𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽 ⊆ 𝑋 ) |
10 |
8 9
|
sylibr |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ⊆ 𝒫 𝑋 ) |
11 |
5 10
|
jca |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( { ∅ , 𝑋 } ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋 ) ) |