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

Theorem istopg 20919
Description: Express the predicate "𝐽 is a topology." See istop2g 20920 for another characterization using nonempty finite intersections instead of binary intersections.

Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use 𝑇 to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)

Assertion
Ref Expression
istopg (𝐽𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝐴
Allowed substitution hint:   𝐴(𝑦)

Proof of Theorem istopg
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 pweq 4298 . . . . 5 (𝑧 = 𝐽 → 𝒫 𝑧 = 𝒫 𝐽)
2 eleq2 2838 . . . . 5 (𝑧 = 𝐽 → ( 𝑥𝑧 𝑥𝐽))
31, 2raleqbidv 3300 . . . 4 (𝑧 = 𝐽 → (∀𝑥 ∈ 𝒫 𝑧 𝑥𝑧 ↔ ∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽))
4 eleq2 2838 . . . . . 6 (𝑧 = 𝐽 → ((𝑥𝑦) ∈ 𝑧 ↔ (𝑥𝑦) ∈ 𝐽))
54raleqbi1dv 3294 . . . . 5 (𝑧 = 𝐽 → (∀𝑦𝑧 (𝑥𝑦) ∈ 𝑧 ↔ ∀𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
65raleqbi1dv 3294 . . . 4 (𝑧 = 𝐽 → (∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧 ↔ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
73, 6anbi12d 608 . . 3 (𝑧 = 𝐽 → ((∀𝑥 ∈ 𝒫 𝑧 𝑥𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧) ↔ (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
8 df-top 20918 . . 3 Top = {𝑧 ∣ (∀𝑥 ∈ 𝒫 𝑧 𝑥𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)}
97, 8elab2g 3502 . 2 (𝐽𝐴 → (𝐽 ∈ Top ↔ (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
10 df-ral 3065 . . . 4 (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐽 𝑥𝐽))
11 elpw2g 4955 . . . . . 6 (𝐽𝐴 → (𝑥 ∈ 𝒫 𝐽𝑥𝐽))
1211imbi1d 330 . . . . 5 (𝐽𝐴 → ((𝑥 ∈ 𝒫 𝐽 𝑥𝐽) ↔ (𝑥𝐽 𝑥𝐽)))
1312albidv 2000 . . . 4 (𝐽𝐴 → (∀𝑥(𝑥 ∈ 𝒫 𝐽 𝑥𝐽) ↔ ∀𝑥(𝑥𝐽 𝑥𝐽)))
1410, 13syl5bb 272 . . 3 (𝐽𝐴 → (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ↔ ∀𝑥(𝑥𝐽 𝑥𝐽)))
1514anbi1d 607 . 2 (𝐽𝐴 → ((∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽) ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
169, 15bitrd 268 1 (𝐽𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wal 1628   = wceq 1630  wcel 2144  wral 3060  cin 3720  wss 3721  𝒫 cpw 4295   cuni 4572  Topctop 20917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-v 3351  df-in 3728  df-ss 3735  df-pw 4297  df-top 20918
This theorem is referenced by:  istop2g  20920  uniopn  20921  inopn  20923  tgcl  20993  distop  21019  indistopon  21025  fctop  21028  cctop  21030  ppttop  21031  epttop  21033  mretopd  21116  toponmre  21117  neiptoptop  21155  kgentopon  21561  qtoptop2  21722  filconn  21906  utoptop  22257  neibastop1  32685
  Copyright terms: Public domain W3C validator