This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem istpsi

Description: Properties that determine a topological space. (Contributed by NM, 20-Oct-2012)

Ref Expression
Hypotheses istpsi.b ⊢ Base K = A
istpsi.j ⊢ TopOpen ⁡ K = J
istpsi.1 ⊢ A = ⋃ J
istpsi.2 ⊢ J ∈ Top
Assertion istpsi ⊢ K ∈ TopSp

Proof

Step Hyp Ref Expression
1 istpsi.b ⊢ Base K = A
2 istpsi.j ⊢ TopOpen ⁡ K = J
3 istpsi.1 ⊢ A = ⋃ J
4 istpsi.2 ⊢ J ∈ Top
5 1 eqcomi ⊢ A = Base K
6 2 eqcomi ⊢ J = TopOpen ⁡ K
7 5 6 istps2 ⊢ K ∈ TopSp ↔ J ∈ Top ∧ A = ⋃ J
8 4 3 7 mpbir2an ⊢ K ∈ TopSp