Theorem istopg 22811

Description: Express the predicate "𝐽 is a topology". See istop2g 22812 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 4564	. . . . 5 ⊢ (𝑧 = 𝐽 → 𝒫 𝑧 = 𝒫 𝐽)
2		eleq2 2820	. . . . 5 ⊢ (𝑧 = 𝐽 → (∪ 𝑥 ∈ 𝑧 ↔ ∪ 𝑥 ∈ 𝐽))
3	1, 2	raleqbidv 3312	. . . 4 ⊢ (𝑧 = 𝐽 → (∀𝑥 ∈ 𝒫 𝑧∪ 𝑥 ∈ 𝑧 ↔ ∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽))
4		eleq2 2820	. . . . . 6 ⊢ (𝑧 = 𝐽 → ((𝑥 ∩ 𝑦) ∈ 𝑧 ↔ (𝑥 ∩ 𝑦) ∈ 𝐽))
5	4	raleqbi1dv 3304	. . . . 5 ⊢ (𝑧 = 𝐽 → (∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))
6	5	raleqbi1dv 3304	. . . 4 ⊢ (𝑧 = 𝐽 → (∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))
7	3, 6	anbi12d 632	. . 3 ⊢ (𝑧 = 𝐽 → ((∀𝑥 ∈ 𝒫 𝑧∪ 𝑥 ∈ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) ↔ (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
8		df-top 22810	. . 3 ⊢ Top = {𝑧 ∣ (∀𝑥 ∈ 𝒫 𝑧∪ 𝑥 ∈ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)}
9	7, 8	elab2g 3636	. 2 ⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
10		df-ral 3048	. . . 4 ⊢ (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐽 → ∪ 𝑥 ∈ 𝐽))
11		elpw2g 5271	. . . . . 6 ⊢ (𝐽 ∈ 𝐴 → (𝑥 ∈ 𝒫 𝐽 ↔ 𝑥 ⊆ 𝐽))
12	11	imbi1d 341	. . . . 5 ⊢ (𝐽 ∈ 𝐴 → ((𝑥 ∈ 𝒫 𝐽 → ∪ 𝑥 ∈ 𝐽) ↔ (𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽)))
13	12	albidv 1921	. . . 4 ⊢ (𝐽 ∈ 𝐴 → (∀𝑥(𝑥 ∈ 𝒫 𝐽 → ∪ 𝑥 ∈ 𝐽) ↔ ∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽)))
14	10, 13	bitrid 283	. . 3 ⊢ (𝐽 ∈ 𝐴 → (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ↔ ∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽)))
15	14	anbi1d 631	. 2 ⊢ (𝐽 ∈ 𝐴 → ((∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽) ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
16	9, 15	bitrd 279	1 ⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2111  ∀wral 3047   ∩ cin 3901   ⊆ wss 3902  𝒫 cpw 4550  ∪ cuni 4859  Topctop 22809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-in 3909  df-ss 3919  df-pw 4552  df-top 22810

This theorem is referenced by:  istop2g  22812  uniopn  22813  inopn  22815  tgcl  22885  distop  22911  indistopon  22917  fctop  22920  cctop  22922  ppttop  22923  epttop  22925  mretopd  23008  toponmre  23009  neiptoptop  23047  kgentopon  23454  qtoptop2  23615  filconn  23799  utoptop  24150  neibastop1  36399