MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  indistps2 Structured version   Visualization version   GIF version

Theorem indistps2 21057
Description: The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 21056. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 21058 and indistps2ALT 21059 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.)
Hypotheses
Ref Expression
indistps2.a (Base‘𝐾) = 𝐴
indistps2.j (TopOpen‘𝐾) = {∅, 𝐴}
Assertion
Ref Expression
indistps2 𝐾 ∈ TopSp

Proof of Theorem indistps2
StepHypRef Expression
1 indistps2.a . 2 (Base‘𝐾) = 𝐴
2 indistps2.j . 2 (TopOpen‘𝐾) = {∅, 𝐴}
3 0ex 4937 . . . 4 ∅ ∈ V
4 fvex 6359 . . . . 5 (Base‘𝐾) ∈ V
51, 4eqeltrri 2850 . . . 4 𝐴 ∈ V
63, 5unipr 4598 . . 3 {∅, 𝐴} = (∅ ∪ 𝐴)
7 uncom 3915 . . 3 (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
8 un0 4122 . . 3 (𝐴 ∪ ∅) = 𝐴
96, 7, 83eqtrri 2801 . 2 𝐴 = {∅, 𝐴}
10 indistop 21047 . 2 {∅, 𝐴} ∈ Top
111, 2, 9, 10istpsi 20987 1 𝐾 ∈ TopSp
Colors of variables: wff setvar class
Syntax hints:   = wceq 1634  wcel 2148  Vcvv 3355  cun 3727  c0 4073  {cpr 4328   cuni 4585  cfv 6042  Basecbs 16084  TopOpenctopn 16310  TopSpctps 20977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3357  df-sbc 3594  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-opab 4860  df-mpt 4877  df-id 5171  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-iota 6005  df-fun 6044  df-fv 6050  df-top 20939  df-topon 20956  df-topsp 20978
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator