Metamath Proof Explorer

Theorem istps

Description: Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses istps.a ⊢ A = Base K
istps.j ⊢ J = TopOpen ⁡ K
Assertion istps ⊢ K ∈ TopSp ↔ J ∈ TopOn ⁡ A

Proof

Step Hyp Ref Expression
1 istps.a ⊢ A = Base K
2 istps.j ⊢ J = TopOpen ⁡ K
3 df-topsp ⊢ TopSp = f | TopOpen ⁡ f ∈ TopOn ⁡ Base f
4 3 eleq2i ⊢ K ∈ TopSp ↔ K ∈ f | TopOpen ⁡ f ∈ TopOn ⁡ Base f
5 topontop ⊢ J ∈ TopOn ⁡ A → J ∈ Top
6 0ntop ⊢ ¬ ∅ ∈ Top
7 fvprc ⊢ ¬ K ∈ V → TopOpen ⁡ K = ∅
8 2 7 eqtrid ⊢ ¬ K ∈ V → J = ∅
9 8 eleq1d ⊢ ¬ K ∈ V → J ∈ Top ↔ ∅ ∈ Top
10 6 9 mtbiri ⊢ ¬ K ∈ V → ¬ J ∈ Top
11 10 con4i ⊢ J ∈ Top → K ∈ V
12 5 11 syl ⊢ J ∈ TopOn ⁡ A → K ∈ V
13 fveq2 ⊢ f = K → TopOpen ⁡ f = TopOpen ⁡ K
14 13 2 eqtr4di ⊢ f = K → TopOpen ⁡ f = J
15 fveq2 ⊢ f = K → Base f = Base K
16 15 1 eqtr4di ⊢ f = K → Base f = A
17 16 fveq2d ⊢ f = K → TopOn ⁡ Base f = TopOn ⁡ A
18 14 17 eleq12d ⊢ f = K → TopOpen ⁡ f ∈ TopOn ⁡ Base f ↔ J ∈ TopOn ⁡ A
19 12 18 elab3 ⊢ K ∈ f | TopOpen ⁡ f ∈ TopOn ⁡ Base f ↔ J ∈ TopOn ⁡ A
20 4 19 bitri ⊢ K ∈ TopSp ↔ J ∈ TopOn ⁡ A