Theorem distop 23313

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 4874	. . . . . 6 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ⊆ ∪ 𝒫 𝐴)
2		unipw 5417	. . . . . 6 ⊢ ∪ 𝒫 𝐴 = 𝐴
3	1, 2	sseqtrdi 3948	. . . . 5 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ⊆ 𝐴)
4		vuniex 7756	. . . . . 6 ⊢ ∪ 𝑥 ∈ V
5	4	elpw 4560	. . . . 5 ⊢ (∪ 𝑥 ∈ 𝒫 𝐴 ↔ ∪ 𝑥 ⊆ 𝐴)
6	3, 5	sylibr 237	. . . 4 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴)
7	6	ax-gen 1827	. . 3 ⊢ ∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴)
8	7	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴))
9		velpw 4561	. . . . . 6 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
10		velpw 4561	. . . . . . . 8 ⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴)
11		ssinss1 4142	. . . . . . . . . 10 ⊢ (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ⊆ 𝐴)
12	11	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ⊆ 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ⊆ 𝐴))
13		vex 3454	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
14	13	inex2 5277	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝑦) ∈ V
15	14	elpw 4560	. . . . . . . . 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 3153	. . . 4 ⊢ (𝑥 ∈ 𝒫 𝐴 → ∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)
21	20	rgen 3078	. . 3 ⊢ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴
22	21	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)
23		pwexg 5339	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
24		istopg 23213	. . 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 1567   ∈ wcel 2144  ∀wral 3076  Vcvv 3450   ⊆ wss 3895   ∩ cin 4089  𝒫 cpw 4556  ∪ cuni 4866  Topctop 23211

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  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  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 3896  df-in 4091  df-un 4151  df-pw 4558  df-sn 4584  df-pr 4586  df-uni 4867  df-top 23212

This theorem is used by:  topnex  23314  distopon  23315  distps  23333  discld  23407  restdis  23496  dishaus  23700  discmp  23716  dis2ndc  23779  dislly  23816  dis1stc  23818  dissnlocfin  23848  locfindis  23849  txdis  23951  xkopt  23974  xkofvcn  24003  efmndtmd  24420  symgtgp  24425  dispcmp  34491  tmachlem-tpbase  47949  tmachlem-tpopen  47951