Step |
Hyp |
Ref |
Expression |
1 |
|
istps.a |
⊢ 𝐴 = ( Base ‘ 𝐾 ) |
2 |
|
istps.j |
⊢ 𝐽 = ( TopOpen ‘ 𝐾 ) |
3 |
|
df-topsp |
⊢ TopSp = { 𝑓 ∣ ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) } |
4 |
3
|
eleq2i |
⊢ ( 𝐾 ∈ TopSp ↔ 𝐾 ∈ { 𝑓 ∣ ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) } ) |
5 |
|
topontop |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐽 ∈ Top ) |
6 |
|
0ntop |
⊢ ¬ ∅ ∈ Top |
7 |
|
fvprc |
⊢ ( ¬ 𝐾 ∈ V → ( TopOpen ‘ 𝐾 ) = ∅ ) |
8 |
2 7
|
syl5eq |
⊢ ( ¬ 𝐾 ∈ V → 𝐽 = ∅ ) |
9 |
8
|
eleq1d |
⊢ ( ¬ 𝐾 ∈ V → ( 𝐽 ∈ Top ↔ ∅ ∈ Top ) ) |
10 |
6 9
|
mtbiri |
⊢ ( ¬ 𝐾 ∈ V → ¬ 𝐽 ∈ Top ) |
11 |
10
|
con4i |
⊢ ( 𝐽 ∈ Top → 𝐾 ∈ V ) |
12 |
5 11
|
syl |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ V ) |
13 |
|
fveq2 |
⊢ ( 𝑓 = 𝐾 → ( TopOpen ‘ 𝑓 ) = ( TopOpen ‘ 𝐾 ) ) |
14 |
13 2
|
eqtr4di |
⊢ ( 𝑓 = 𝐾 → ( TopOpen ‘ 𝑓 ) = 𝐽 ) |
15 |
|
fveq2 |
⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐾 ) ) |
16 |
15 1
|
eqtr4di |
⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = 𝐴 ) |
17 |
16
|
fveq2d |
⊢ ( 𝑓 = 𝐾 → ( TopOn ‘ ( Base ‘ 𝑓 ) ) = ( TopOn ‘ 𝐴 ) ) |
18 |
14 17
|
eleq12d |
⊢ ( 𝑓 = 𝐾 → ( ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) ↔ 𝐽 ∈ ( TopOn ‘ 𝐴 ) ) ) |
19 |
12 18
|
elab3 |
⊢ ( 𝐾 ∈ { 𝑓 ∣ ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) } ↔ 𝐽 ∈ ( TopOn ‘ 𝐴 ) ) |
20 |
4 19
|
bitri |
⊢ ( 𝐾 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐴 ) ) |