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

Theorem istopg 21503
Description: Express the predicate "𝐽 is a topology". See istop2g 21504 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 4538 . . . . 5 (𝑧 = 𝐽 → 𝒫 𝑧 = 𝒫 𝐽)
2 eleq2 2904 . . . . 5 (𝑧 = 𝐽 → ( 𝑥𝑧 𝑥𝐽))
31, 2raleqbidv 3392 . . . 4 (𝑧 = 𝐽 → (∀𝑥 ∈ 𝒫 𝑧 𝑥𝑧 ↔ ∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽))
4 eleq2 2904 . . . . . 6 (𝑧 = 𝐽 → ((𝑥𝑦) ∈ 𝑧 ↔ (𝑥𝑦) ∈ 𝐽))
54raleqbi1dv 3394 . . . . 5 (𝑧 = 𝐽 → (∀𝑦𝑧 (𝑥𝑦) ∈ 𝑧 ↔ ∀𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
65raleqbi1dv 3394 . . . 4 (𝑧 = 𝐽 → (∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧 ↔ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
73, 6anbi12d 633 . . 3 (𝑧 = 𝐽 → ((∀𝑥 ∈ 𝒫 𝑧 𝑥𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧) ↔ (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
8 df-top 21502 . . 3 Top = {𝑧 ∣ (∀𝑥 ∈ 𝒫 𝑧 𝑥𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)}
97, 8elab2g 3654 . 2 (𝐽𝐴 → (𝐽 ∈ Top ↔ (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
10 df-ral 3138 . . . 4 (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐽 𝑥𝐽))
11 elpw2g 5233 . . . . . 6 (𝐽𝐴 → (𝑥 ∈ 𝒫 𝐽𝑥𝐽))
1211imbi1d 345 . . . . 5 (𝐽𝐴 → ((𝑥 ∈ 𝒫 𝐽 𝑥𝐽) ↔ (𝑥𝐽 𝑥𝐽)))
1312albidv 1922 . . . 4 (𝐽𝐴 → (∀𝑥(𝑥 ∈ 𝒫 𝐽 𝑥𝐽) ↔ ∀𝑥(𝑥𝐽 𝑥𝐽)))
1410, 13syl5bb 286 . . 3 (𝐽𝐴 → (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ↔ ∀𝑥(𝑥𝐽 𝑥𝐽)))
1514anbi1d 632 . 2 (𝐽𝐴 → ((∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽) ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
169, 15bitrd 282 1 (𝐽𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536   = wceq 1538  wcel 2115  wral 3133  cin 3918  wss 3919  𝒫 cpw 4522   cuni 4824  Topctop 21501
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rab 3142  df-v 3482  df-in 3926  df-ss 3936  df-pw 4524  df-top 21502
This theorem is referenced by:  istop2g  21504  uniopn  21505  inopn  21507  tgcl  21577  distop  21603  indistopon  21609  fctop  21612  cctop  21614  ppttop  21615  epttop  21617  mretopd  21700  toponmre  21701  neiptoptop  21739  kgentopon  22146  qtoptop2  22307  filconn  22491  utoptop  22843  neibastop1  33764
  Copyright terms: Public domain W3C validator