Theorem indistps2 23041

Description: The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 23040. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 23042 and indistps2ALT 23043 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

Step	Hyp	Ref	Expression
1		indistps2.a	. 2 ⊢ (Base‘𝐾) = 𝐴
2		indistps2.j	. 2 ⊢ (TopOpen‘𝐾) = {∅, 𝐴}
3		0ex 5247	. . . 4 ⊢ ∅ ∈ V
4		fvex 6865	. . . . 5 ⊢ (Base‘𝐾) ∈ V
5	1, 4	eqeltrri 2849	. . . 4 ⊢ 𝐴 ∈ V
6	3, 5	unipr 4872	. . 3 ⊢ ∪ {∅, 𝐴} = (∅ ∪ 𝐴)
7		uncom 4102	. . 3 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
8		un0 4338	. . 3 ⊢ (𝐴 ∪ ∅) = 𝐴
9	6, 7, 8	3eqtrri 2780	. 2 ⊢ 𝐴 = ∪ {∅, 𝐴}
10		indistop 23031	. 2 ⊢ {∅, 𝐴} ∈ Top
11	1, 2, 9, 10	istpsi 22971	1 ⊢ 𝐾 ∈ TopSp

Syntax hints:   = wceq 1550   ∈ wcel 2132  Vcvv 3444   ∪ cun 3893  ∅c0 4276  {cpr 4574  ∪ cuni 4855  ‘cfv 6506  Basecbs 17217  TopOpenctopn 17422  TopSpctps 22961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-iota 6462  df-fun 6508  df-fv 6514  df-top 22923  df-topon 22940  df-topsp 22962

This theorem is referenced by: (None)