Step |
Hyp |
Ref |
Expression |
1 |
|
indistpsALT.a |
⊢ 𝐴 ∈ V |
2 |
|
indistpsALT.k |
⊢ 𝐾 = { 〈 ( Base ‘ ndx ) , 𝐴 〉 , 〈 ( TopSet ‘ ndx ) , { ∅ , 𝐴 } 〉 } |
3 |
|
indistopon |
⊢ ( 𝐴 ∈ V → { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) ) |
4 |
|
df-tset |
⊢ TopSet = Slot 9 |
5 |
|
1lt9 |
⊢ 1 < 9 |
6 |
|
9nn |
⊢ 9 ∈ ℕ |
7 |
2 4 5 6
|
2strbas |
⊢ ( 𝐴 ∈ V → 𝐴 = ( Base ‘ 𝐾 ) ) |
8 |
1 7
|
ax-mp |
⊢ 𝐴 = ( Base ‘ 𝐾 ) |
9 |
|
prex |
⊢ { ∅ , 𝐴 } ∈ V |
10 |
2 4 5 6
|
2strop |
⊢ ( { ∅ , 𝐴 } ∈ V → { ∅ , 𝐴 } = ( TopSet ‘ 𝐾 ) ) |
11 |
9 10
|
ax-mp |
⊢ { ∅ , 𝐴 } = ( TopSet ‘ 𝐾 ) |
12 |
8 11
|
tsettps |
⊢ ( { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp ) |
13 |
1 3 12
|
mp2b |
⊢ 𝐾 ∈ TopSp |