Metamath Proof Explorer

Theorem tpspropd

Description: A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses tpspropd.1 ⊢ φ → Base K = Base L
tpspropd.2 ⊢ φ → TopOpen ⁡ K = TopOpen ⁡ L
Assertion tpspropd ⊢ φ → K ∈ TopSp ↔ L ∈ TopSp

Proof

Step Hyp Ref Expression
1 tpspropd.1 ⊢ φ → Base K = Base L
2 tpspropd.2 ⊢ φ → TopOpen ⁡ K = TopOpen ⁡ L
3 1 fveq2d ⊢ φ → TopOn ⁡ Base K = TopOn ⁡ Base L
4 2 3 eleq12d ⊢ φ → TopOpen ⁡ K ∈ TopOn ⁡ Base K ↔ TopOpen ⁡ L ∈ TopOn ⁡ Base L
5 eqid ⊢ Base K = Base K
6 eqid ⊢ TopOpen ⁡ K = TopOpen ⁡ K
7 5 6 istps ⊢ K ∈ TopSp ↔ TopOpen ⁡ K ∈ TopOn ⁡ Base K
8 eqid ⊢ Base L = Base L
9 eqid ⊢ TopOpen ⁡ L = TopOpen ⁡ L
10 8 9 istps ⊢ L ∈ TopSp ↔ TopOpen ⁡ L ∈ TopOn ⁡ Base L
11 4 7 10 3bitr4g ⊢ φ → K ∈ TopSp ↔ L ∈ TopSp