Step |
Hyp |
Ref |
Expression |
1 |
|
eltpsi.k |
⊢ 𝐾 = { 〈 ( Base ‘ ndx ) , 𝐴 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } |
2 |
|
df-tset |
⊢ TopSet = Slot 9 |
3 |
|
1lt9 |
⊢ 1 < 9 |
4 |
|
9nn |
⊢ 9 ∈ ℕ |
5 |
1 2 3 4
|
2strop |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐽 = ( TopSet ‘ 𝐾 ) ) |
6 |
|
toponmax |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ 𝐽 ) |
7 |
1 2 3 4
|
2strbas |
⊢ ( 𝐴 ∈ 𝐽 → 𝐴 = ( Base ‘ 𝐾 ) ) |
8 |
6 7
|
syl |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐴 = ( Base ‘ 𝐾 ) ) |
9 |
8
|
fveq2d |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → ( TopOn ‘ 𝐴 ) = ( TopOn ‘ ( Base ‘ 𝐾 ) ) ) |
10 |
5 9
|
eleq12d |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) ↔ ( TopSet ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) ) ) |
11 |
10
|
ibi |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → ( TopSet ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) ) |
12 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
13 |
|
eqid |
⊢ ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐾 ) |
14 |
12 13
|
tsettps |
⊢ ( ( TopSet ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ TopSp ) |
15 |
11 14
|
syl |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp ) |