Step |
Hyp |
Ref |
Expression |
1 |
|
toptopon2 |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
2 |
|
eqid |
⊢ ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) |
3 |
2
|
kqtopon |
⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) ) |
4 |
1 3
|
sylbi |
⊢ ( 𝐽 ∈ Top → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) ) |
5 |
|
topontop |
⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) → ( KQ ‘ 𝐽 ) ∈ Top ) |
6 |
4 5
|
syl |
⊢ ( 𝐽 ∈ Top → ( KQ ‘ 𝐽 ) ∈ Top ) |
7 |
|
0opn |
⊢ ( ( KQ ‘ 𝐽 ) ∈ Top → ∅ ∈ ( KQ ‘ 𝐽 ) ) |
8 |
|
elfvdm |
⊢ ( ∅ ∈ ( KQ ‘ 𝐽 ) → 𝐽 ∈ dom KQ ) |
9 |
7 8
|
syl |
⊢ ( ( KQ ‘ 𝐽 ) ∈ Top → 𝐽 ∈ dom KQ ) |
10 |
|
ovex |
⊢ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) ∈ V |
11 |
|
df-kq |
⊢ KQ = ( 𝑗 ∈ Top ↦ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) ) |
12 |
10 11
|
dmmpti |
⊢ dom KQ = Top |
13 |
9 12
|
eleqtrdi |
⊢ ( ( KQ ‘ 𝐽 ) ∈ Top → 𝐽 ∈ Top ) |
14 |
6 13
|
impbii |
⊢ ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Top ) |