Theorem istopg 22281

Description: Express the predicate "𝐽 is a topology". See istop2g 22282 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.

Step	Hyp	Ref	Expression
1		pweq 4579	. . . . 5 ⊢ (𝑧 = 𝐽 → 𝒫 𝑧 = 𝒫 𝐽)
2		eleq2 2821	. . . . 5 ⊢ (𝑧 = 𝐽 → (∪ 𝑥 ∈ 𝑧 ↔ ∪ 𝑥 ∈ 𝐽))
3	1, 2	raleqbidv 3317	. . . 4 ⊢ (𝑧 = 𝐽 → (∀𝑥 ∈ 𝒫 𝑧∪ 𝑥 ∈ 𝑧 ↔ ∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽))
4		eleq2 2821	. . . . . 6 ⊢ (𝑧 = 𝐽 → ((𝑥 ∩ 𝑦) ∈ 𝑧 ↔ (𝑥 ∩ 𝑦) ∈ 𝐽))
5	4	raleqbi1dv 3305	. . . . 5 ⊢ (𝑧 = 𝐽 → (∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))
6	5	raleqbi1dv 3305	. . . 4 ⊢ (𝑧 = 𝐽 → (∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))
7	3, 6	anbi12d 631	. . 3 ⊢ (𝑧 = 𝐽 → ((∀𝑥 ∈ 𝒫 𝑧∪ 𝑥 ∈ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) ↔ (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
8		df-top 22280	. . 3 ⊢ Top = {𝑧 ∣ (∀𝑥 ∈ 𝒫 𝑧∪ 𝑥 ∈ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)}
9	7, 8	elab2g 3635	. 2 ⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
10		df-ral 3061	. . . 4 ⊢ (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐽 → ∪ 𝑥 ∈ 𝐽))
11		elpw2g 5306	. . . . . 6 ⊢ (𝐽 ∈ 𝐴 → (𝑥 ∈ 𝒫 𝐽 ↔ 𝑥 ⊆ 𝐽))
12	11	imbi1d 341	. . . . 5 ⊢ (𝐽 ∈ 𝐴 → ((𝑥 ∈ 𝒫 𝐽 → ∪ 𝑥 ∈ 𝐽) ↔ (𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽)))
13	12	albidv 1923	. . . 4 ⊢ (𝐽 ∈ 𝐴 → (∀𝑥(𝑥 ∈ 𝒫 𝐽 → ∪ 𝑥 ∈ 𝐽) ↔ ∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽)))
14	10, 13	bitrid 282	. . 3 ⊢ (𝐽 ∈ 𝐴 → (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ↔ ∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽)))
15	14	anbi1d 630	. 2 ⊢ (𝐽 ∈ 𝐴 → ((∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽) ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
16	9, 15	bitrd 278	1 ⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1539   = wceq 1541   ∈ wcel 2106  ∀wral 3060   ∩ cin 3912   ⊆ wss 3913  𝒫 cpw 4565  ∪ cuni 4870  Topctop 22279

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 2702  ax-sep 5261

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567  df-top 22280

This theorem is referenced by:  istop2g  22282  uniopn  22283  inopn  22285  tgcl  22356  distop  22382  indistopon  22388  fctop  22391  cctop  22393  ppttop  22394  epttop  22396  mretopd  22480  toponmre  22481  neiptoptop  22519  kgentopon  22926  qtoptop2  23087  filconn  23271  utoptop  23623  neibastop1  34907