Theorem istopg 23222

Description: Express the predicate "𝐽 is a topology". See istop2g 23223 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 4570	. . . . 5 ⊢ (𝑧 = 𝐽 → 𝒫 𝑧 = 𝒫 𝐽)
2		eleq2 2849	. . . . 5 ⊢ (𝑧 = 𝐽 → (∪ 𝑥 ∈ 𝑧 ↔ ∪ 𝑥 ∈ 𝐽))
3	1, 2	raleqbidv 3334	. . . 4 ⊢ (𝑧 = 𝐽 → (∀𝑥 ∈ 𝒫 𝑧∪ 𝑥 ∈ 𝑧 ↔ ∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽))
4		eleq2 2849	. . . . . 6 ⊢ (𝑧 = 𝐽 → ((𝑥 ∩ 𝑦) ∈ 𝑧 ↔ (𝑥 ∩ 𝑦) ∈ 𝐽))
5	4	raleqbi1dv 3329	. . . . 5 ⊢ (𝑧 = 𝐽 → (∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))
6	5	raleqbi1dv 3329	. . . 4 ⊢ (𝑧 = 𝐽 → (∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))
7	3, 6	anbi12d 644	. . 3 ⊢ (𝑧 = 𝐽 → ((∀𝑥 ∈ 𝒫 𝑧∪ 𝑥 ∈ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) ↔ (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
8		df-top 23221	. . 3 ⊢ Top = {𝑧 ∣ (∀𝑥 ∈ 𝒫 𝑧∪ 𝑥 ∈ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)}
9	7, 8	elab2g 3633	. 2 ⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
10		df-ral 3077	. . . 4 ⊢ (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐽 → ∪ 𝑥 ∈ 𝐽))
11		elpw2g 5295	. . . . . 6 ⊢ (𝐽 ∈ 𝐴 → (𝑥 ∈ 𝒫 𝐽 ↔ 𝑥 ⊆ 𝐽))
12	11	imbi1d 344	. . . . 5 ⊢ (𝐽 ∈ 𝐴 → ((𝑥 ∈ 𝒫 𝐽 → ∪ 𝑥 ∈ 𝐽) ↔ (𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽)))
13	12	albidv 1952	. . . 4 ⊢ (𝐽 ∈ 𝐴 → (∀𝑥(𝑥 ∈ 𝒫 𝐽 → ∪ 𝑥 ∈ 𝐽) ↔ ∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽)))
14	10, 13	bitrid 286	. . 3 ⊢ (𝐽 ∈ 𝐴 → (∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ↔ ∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽)))
15	14	anbi1d 643	. 2 ⊢ (𝐽 ∈ 𝐴 → ((∀𝑥 ∈ 𝒫 𝐽∪ 𝑥 ∈ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽) ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
16	9, 15	bitrd 282	1 ⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569   ∈ wcel 2144  ∀wral 3076   ⊆ wss 3896   ∩ cin 4088  𝒫 cpw 4556  ∪ cuni 4866  Topctop 23220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090  df-pw 4558  df-top 23221

This theorem is used by:  istop2g  23223  uniopn  23224  inopn  23226  tgcl  23296  distop  23322  indistopon  23328  fctop  23331  cctop  23333  ppttop  23334  epttop  23336  mretopd  23419  toponmre  23420  neiptoptop  23458  kgentopon  23866  qtoptop2  24027  filconn  24211  utoptop  24562  neibastop1  37271