Theorem distop 23017

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 4919	. . . . . 6 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ⊆ ∪ 𝒫 𝐴)
2		unipw 5460	. . . . . 6 ⊢ ∪ 𝒫 𝐴 = 𝐴
3	1, 2	sseqtrdi 4045	. . . . 5 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ⊆ 𝐴)
4		vuniex 7757	. . . . . 6 ⊢ ∪ 𝑥 ∈ V
5	4	elpw 4608	. . . . 5 ⊢ (∪ 𝑥 ∈ 𝒫 𝐴 ↔ ∪ 𝑥 ⊆ 𝐴)
6	3, 5	sylibr 234	. . . 4 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴)
7	6	ax-gen 1791	. . 3 ⊢ ∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴)
8	7	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴))
9		velpw 4609	. . . . . 6 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
10		velpw 4609	. . . . . . . 8 ⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴)
11		ssinss1 4253	. . . . . . . . . 10 ⊢ (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ⊆ 𝐴)
12	11	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ⊆ 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ⊆ 𝐴))
13		vex 3481	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
14	13	inex2 5323	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝑦) ∈ V
15	14	elpw 4608	. . . . . . . . 9 ⊢ ((𝑥 ∩ 𝑦) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝑦) ⊆ 𝐴)
16	12, 15	imbitrrdi 252	. . . . . . . 8 ⊢ (𝑦 ⊆ 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))
17	10, 16	sylbi 217	. . . . . . 7 ⊢ (𝑦 ∈ 𝒫 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))
18	17	com12 32	. . . . . 6 ⊢ (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))
19	9, 18	sylbi 217	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))
20	19	ralrimiv 3142	. . . 4 ⊢ (𝑥 ∈ 𝒫 𝐴 → ∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)
21	20	rgen 3060	. . 3 ⊢ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴
22	21	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)
23		pwexg 5383	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
24		istopg 22916	. . 3 ⊢ (𝒫 𝐴 ∈ V → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)))
25	23, 24	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)))
26	8, 22, 25	mpbir2and 713	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1534   ∈ wcel 2105  ∀wral 3058  Vcvv 3477   ∩ cin 3961   ⊆ wss 3962  𝒫 cpw 4604  ∪ cuni 4911  Topctop 22914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-un 3967  df-in 3969  df-ss 3979  df-pw 4606  df-sn 4631  df-pr 4633  df-uni 4912  df-top 22915

This theorem is referenced by:  topnex  23018  distopon  23019  distps  23038  discld  23112  restdis  23201  dishaus  23405  discmp  23421  dis2ndc  23483  dislly  23520  dis1stc  23522  dissnlocfin  23552  locfindis  23553  txdis  23655  xkopt  23678  xkofvcn  23707  efmndtmd  24124  symgtgp  24129  dispcmp  33819