Theorem istps 22821

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

Hypotheses

Ref	Expression
istps.a	⊢ 𝐴 = (Base‘𝐾)
istps.j	⊢ 𝐽 = (TopOpen‘𝐾)

Assertion

Ref	Expression
istps	⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴))

Proof of Theorem istps

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-topsp 22820	. . 3 ⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
2	1	eleq2i 2820	. 2 ⊢ (𝐾 ∈ TopSp ↔ 𝐾 ∈ {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))})
3		topontop 22800	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 ∈ Top)
4		0ntop 22792	. . . . . 6 ⊢ ¬ ∅ ∈ Top
5		istps.j	. . . . . . . 8 ⊢ 𝐽 = (TopOpen‘𝐾)
6		fvprc 6850	. . . . . . . 8 ⊢ (¬ 𝐾 ∈ V → (TopOpen‘𝐾) = ∅)
7	5, 6	eqtrid 2776	. . . . . . 7 ⊢ (¬ 𝐾 ∈ V → 𝐽 = ∅)
8	7	eleq1d 2813	. . . . . 6 ⊢ (¬ 𝐾 ∈ V → (𝐽 ∈ Top ↔ ∅ ∈ Top))
9	4, 8	mtbiri 327	. . . . 5 ⊢ (¬ 𝐾 ∈ V → ¬ 𝐽 ∈ Top)
10	9	con4i 114	. . . 4 ⊢ (𝐽 ∈ Top → 𝐾 ∈ V)
11	3, 10	syl 17	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ V)
12		fveq2 6858	. . . . 5 ⊢ (𝑓 = 𝐾 → (TopOpen‘𝑓) = (TopOpen‘𝐾))
13	12, 5	eqtr4di 2782	. . . 4 ⊢ (𝑓 = 𝐾 → (TopOpen‘𝑓) = 𝐽)
14		fveq2 6858	. . . . . 6 ⊢ (𝑓 = 𝐾 → (Base‘𝑓) = (Base‘𝐾))
15		istps.a	. . . . . 6 ⊢ 𝐴 = (Base‘𝐾)
16	14, 15	eqtr4di 2782	. . . . 5 ⊢ (𝑓 = 𝐾 → (Base‘𝑓) = 𝐴)
17	16	fveq2d 6862	. . . 4 ⊢ (𝑓 = 𝐾 → (TopOn‘(Base‘𝑓)) = (TopOn‘𝐴))
18	13, 17	eleq12d 2822	. . 3 ⊢ (𝑓 = 𝐾 → ((TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓)) ↔ 𝐽 ∈ (TopOn‘𝐴)))
19	11, 18	elab3 3653	. 2 ⊢ (𝐾 ∈ {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} ↔ 𝐽 ∈ (TopOn‘𝐴))
20	2, 19	bitri 275	1 ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴))

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  Vcvv 3447  ∅c0 4296  ‘cfv 6511  Basecbs 17179  TopOpenctopn 17384  Topctop 22780  TopOnctopon 22797  TopSpctps 22819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-top 22781  df-topon 22798  df-topsp 22820

This theorem is referenced by:  istps2  22822  tpspropd  22825  tsettps  22828  indistps2ALT  22901  resstps  23074  prdstps  23516  imastps  23608  xpstopnlem2  23698  tmdtopon  23968  tgptopon  23969  istgp2  23978  oppgtmd  23984  distgp  23986  indistgp  23987  efmndtmd  23988  qustgplem  24008  prdstmdd  24011  eltsms  24020  tsmscls  24025  tsmsgsum  24026  tsmsid  24027  tsmsmhm  24033  tsmsadd  24034  dvrcn  24071  cnmpt1vsca  24081  cnmpt2vsca  24082  tlmtgp  24083  ressusp  24152  tustps  24160  ucncn  24172  neipcfilu  24183  cnextucn  24190  ucnextcn  24191  isxms2  24336  ressxms  24413  prdsxmslem2  24417  nrgtrg  24578  cnfldtopon  24670  cnmpt1ds  24731  cnmpt2ds  24732  nmcn  24733  cnmpt1ip  25147  cnmpt2ip  25148  csscld  25149  clsocv  25150  minveclem4a  25330  rspectps  33873  mhmhmeotmd  33917  rrxtopon  46286  qndenserrnopnlem  46295