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

Theorem istopg 22619
Description: Express the predicate "𝐽 is a topology". See istop2g 22620 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 4617 . . . . 5 (𝑧 = 𝐽 → 𝒫 𝑧 = 𝒫 𝐽)
2 eleq2 2820 . . . . 5 (𝑧 = 𝐽 → ( 𝑥𝑧 𝑥𝐽))
31, 2raleqbidv 3340 . . . 4 (𝑧 = 𝐽 → (∀𝑥 ∈ 𝒫 𝑧 𝑥𝑧 ↔ ∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽))
4 eleq2 2820 . . . . . 6 (𝑧 = 𝐽 → ((𝑥𝑦) ∈ 𝑧 ↔ (𝑥𝑦) ∈ 𝐽))
54raleqbi1dv 3331 . . . . 5 (𝑧 = 𝐽 → (∀𝑦𝑧 (𝑥𝑦) ∈ 𝑧 ↔ ∀𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
65raleqbi1dv 3331 . . . 4 (𝑧 = 𝐽 → (∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧 ↔ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
73, 6anbi12d 629 . . 3 (𝑧 = 𝐽 → ((∀𝑥 ∈ 𝒫 𝑧 𝑥𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧) ↔ (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
8 df-top 22618 . . 3 Top = {𝑧 ∣ (∀𝑥 ∈ 𝒫 𝑧 𝑥𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)}
97, 8elab2g 3671 . 2 (𝐽𝐴 → (𝐽 ∈ Top ↔ (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
10 df-ral 3060 . . . 4 (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐽 𝑥𝐽))
11 elpw2g 5345 . . . . . 6 (𝐽𝐴 → (𝑥 ∈ 𝒫 𝐽𝑥𝐽))
1211imbi1d 340 . . . . 5 (𝐽𝐴 → ((𝑥 ∈ 𝒫 𝐽 𝑥𝐽) ↔ (𝑥𝐽 𝑥𝐽)))
1312albidv 1921 . . . 4 (𝐽𝐴 → (∀𝑥(𝑥 ∈ 𝒫 𝐽 𝑥𝐽) ↔ ∀𝑥(𝑥𝐽 𝑥𝐽)))
1410, 13bitrid 282 . . 3 (𝐽𝐴 → (∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ↔ ∀𝑥(𝑥𝐽 𝑥𝐽)))
1514anbi1d 628 . 2 (𝐽𝐴 → ((∀𝑥 ∈ 𝒫 𝐽 𝑥𝐽 ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽) ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
169, 15bitrd 278 1 (𝐽𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1537   = wceq 1539  wcel 2104  wral 3059  cin 3948  wss 3949  𝒫 cpw 4603   cuni 4909  Topctop 22617
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-in 3956  df-ss 3966  df-pw 4605  df-top 22618
This theorem is referenced by:  istop2g  22620  uniopn  22621  inopn  22623  tgcl  22694  distop  22720  indistopon  22726  fctop  22729  cctop  22731  ppttop  22732  epttop  22734  mretopd  22818  toponmre  22819  neiptoptop  22857  kgentopon  23264  qtoptop2  23425  filconn  23609  utoptop  23961  neibastop1  35549
  Copyright terms: Public domain W3C validator