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

Metamath Proof Explorer

Theorem indistps2ALT

Description: The indiscrete topology on a set A expressed as a topological space, using direct component assignments. Here we show how to derive the direct component assignment version indistps2 from the structural version indistps . (Contributed by NM, 24-Oct-2012) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses indistps2ALT.a ⊢ Base K = A
indistps2ALT.j ⊢ TopOpen ⁡ K = ∅ A
Assertion indistps2ALT ⊢ K ∈ TopSp

Proof

Step Hyp Ref Expression
1 indistps2ALT.a ⊢ Base K = A
2 indistps2ALT.j ⊢ TopOpen ⁡ K = ∅ A
3 fvex ⊢ Base K ∈ V
4 1 3 eqeltrri ⊢ A ∈ V
5 indistopon ⊢ A ∈ V → ∅ A ∈ TopOn ⁡ A
6 4 5 ax-mp ⊢ ∅ A ∈ TopOn ⁡ A
7 1 eqcomi ⊢ A = Base K
8 2 eqcomi ⊢ ∅ A = TopOpen ⁡ K
9 7 8 istps ⊢ K ∈ TopSp ↔ ∅ A ∈ TopOn ⁡ A
10 6 9 mpbir ⊢ K ∈ TopSp