Theorem distop 23340

Description: The discrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 17-Jul-2006.) (Revised by Mario Carneiro, 19-Mar-2015.)

Assertion

Ref	Expression
distop	⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top)

Proof of Theorem distop

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uniss 4878	. . . . . 6 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ⊆ ∪ 𝒫 𝐴)
2		unipw 5422	. . . . . 6 ⊢ ∪ 𝒫 𝐴 = 𝐴
3	1, 2	sseqtrdi 3953	. . . . 5 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ⊆ 𝐴)
4		vuniex 7777	. . . . . 6 ⊢ ∪ 𝑥 ∈ V
5	4	elpw 4564	. . . . 5 ⊢ (∪ 𝑥 ∈ 𝒫 𝐴 ↔ ∪ 𝑥 ⊆ 𝐴)
6	3, 5	sylibr 237	. . . 4 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴)
7	6	ax-gen 1828	. . 3 ⊢ ∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴)
8	7	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴))
9		velpw 4565	. . . . . 6 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
10		velpw 4565	. . . . . . . 8 ⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴)
11		ssinss1 4145	. . . . . . . . . 10 ⊢ (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ⊆ 𝐴)
12	11	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ⊆ 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ⊆ 𝐴))
13		vex 3458	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
14	13	inex2 5282	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝑦) ∈ V
15	14	elpw 4564	. . . . . . . . 9 ⊢ ((𝑥 ∩ 𝑦) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝑦) ⊆ 𝐴)
16	12, 15	imbitrrdi 255	. . . . . . . 8 ⊢ (𝑦 ⊆ 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))
17	10, 16	sylbi 220	. . . . . . 7 ⊢ (𝑦 ∈ 𝒫 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))
18	17	com12 33	. . . . . 6 ⊢ (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))
19	9, 18	sylbi 220	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))
20	19	ralrimiv 3157	. . . 4 ⊢ (𝑥 ∈ 𝒫 𝐴 → ∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)
21	20	rgen 3082	. . 3 ⊢ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴
22	21	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)
23		pwexg 5344	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
24		istopg 23240	. . 3 ⊢ (𝒫 𝐴 ∈ V → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)))
25	23, 24	syl 18	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)))
26	8, 22, 25	mpbir2and 726	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2147  ∀wral 3080  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092  𝒫 cpw 4560  ∪ cuni 4870  Topctop 23238

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-un 4154  df-pw 4562  df-sn 4589  df-pr 4591  df-uni 4871  df-top 23239

This theorem is used by:  topnex  23341  distopon  23342  distps  23360  discld  23434  restdis  23523  dishaus  23727  discmp  23743  dis2ndc  23806  dislly  23843  dis1stc  23845  dissnlocfin  23875  locfindis  23876  txdis  23978  xkopt  24001  xkofvcn  24030  efmndtmd  24447  symgtgp  24452  dispcmp  34558  tmachlem-tpbase  48152  tmachlem-tpopen  48154