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

Theorem isreg 22835
Description: The predicate "is a regular space". In a regular space, any open neighborhood has a closed subneighborhood. Note that some authors require the space to be Hausdorff (which would make it the same as T3), but we reserve the phrase "regular Hausdorff" for that as many topologists do. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.)
Assertion
Ref Expression
isreg (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑥𝐽𝑦𝑥𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
Distinct variable group:   𝑥,𝑦,𝑧,𝐽

Proof of Theorem isreg
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6891 . . . . . . . 8 (𝑗 = 𝐽 → (cls‘𝑗) = (cls‘𝐽))
21fveq1d 6893 . . . . . . 7 (𝑗 = 𝐽 → ((cls‘𝑗)‘𝑧) = ((cls‘𝐽)‘𝑧))
32sseq1d 4013 . . . . . 6 (𝑗 = 𝐽 → (((cls‘𝑗)‘𝑧) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))
43anbi2d 629 . . . . 5 (𝑗 = 𝐽 → ((𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥) ↔ (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
54rexeqbi1dv 3334 . . . 4 (𝑗 = 𝐽 → (∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥) ↔ ∃𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
65ralbidv 3177 . . 3 (𝑗 = 𝐽 → (∀𝑦𝑥𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥) ↔ ∀𝑦𝑥𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
76raleqbi1dv 3333 . 2 (𝑗 = 𝐽 → (∀𝑥𝑗𝑦𝑥𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥) ↔ ∀𝑥𝐽𝑦𝑥𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
8 df-reg 22819 . 2 Reg = {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦𝑥𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
97, 8elrab2 3686 1 (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑥𝐽𝑦𝑥𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3061  wrex 3070  wss 3948  cfv 6543  Topctop 22394  clsccl 22521  Regcreg 22812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-reg 22819
This theorem is referenced by:  regtop  22836  regsep  22837  isreg2  22880  kqreglem1  23244  kqreglem2  23245  nrmr0reg  23252  reghmph  23296  utopreg  23756
  Copyright terms: Public domain W3C validator