Theorem dscopn

Description: The discrete metric generates the discrete topology. In particular, the discrete topology is metrizable. (Contributed by Mario Carneiro, 29-Jan-2014)

	Ref	Expression
Hypothesis	dscmet.1	⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 = 𝑦 , 0 , 1 ) )
Assertion	dscopn	⊢ ( 𝑋 ∈ 𝑉 → ( MetOpen ‘ 𝐷 ) = 𝒫 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		dscmet.1	⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 = 𝑦 , 0 , 1 ) )
2	1	dscmet	⊢ ( 𝑋 ∈ 𝑉 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4	2 3	syl	⊢ ( 𝑋 ∈ 𝑉 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
5		eqid	⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
6	5	elmopn	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑢 ∈ ( MetOpen ‘ 𝐷 ) ↔ ( 𝑢 ⊆ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) ) )
7	4 6	syl	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑢 ∈ ( MetOpen ‘ 𝐷 ) ↔ ( 𝑢 ⊆ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) ) )
8		simpll	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑢 ⊆ 𝑋 ) ∧ 𝑣 ∈ 𝑢 ) → 𝑋 ∈ 𝑉 )
9		ssel2	⊢ ( ( 𝑢 ⊆ 𝑋 ∧ 𝑣 ∈ 𝑢 ) → 𝑣 ∈ 𝑋 )
10	9	adantll	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑢 ⊆ 𝑋 ) ∧ 𝑣 ∈ 𝑢 ) → 𝑣 ∈ 𝑋 )
11	8 10	jca	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑢 ⊆ 𝑋 ) ∧ 𝑣 ∈ 𝑢 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) )
12		velsn	⊢ ( 𝑤 ∈ { 𝑣 } ↔ 𝑤 = 𝑣 )
13		eleq1a	⊢ ( 𝑣 ∈ 𝑋 → ( 𝑤 = 𝑣 → 𝑤 ∈ 𝑋 ) )
14		simpl	⊢ ( ( 𝑤 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑤 ) < 1 ) → 𝑤 ∈ 𝑋 )
15	14	a1i	⊢ ( 𝑣 ∈ 𝑋 → ( ( 𝑤 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑤 ) < 1 ) → 𝑤 ∈ 𝑋 ) )
16		eqeq12	⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( 𝑥 = 𝑦 ↔ 𝑣 = 𝑤 ) )
17	16	ifbid	⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → if ( 𝑥 = 𝑦 , 0 , 1 ) = if ( 𝑣 = 𝑤 , 0 , 1 ) )
18		0re	⊢ 0 ∈ ℝ
19		1re	⊢ 1 ∈ ℝ
20	18 19	ifcli	⊢ if ( 𝑣 = 𝑤 , 0 , 1 ) ∈ ℝ
21	20	elexi	⊢ if ( 𝑣 = 𝑤 , 0 , 1 ) ∈ V
22	17 1 21	ovmpoa	⊢ ( ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑣 𝐷 𝑤 ) = if ( 𝑣 = 𝑤 , 0 , 1 ) )
23	22	breq1d	⊢ ( ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑣 𝐷 𝑤 ) < 1 ↔ if ( 𝑣 = 𝑤 , 0 , 1 ) < 1 ) )
24	19	ltnri	⊢ ¬ 1 < 1
25		iffalse	⊢ ( ¬ 𝑣 = 𝑤 → if ( 𝑣 = 𝑤 , 0 , 1 ) = 1 )
26	25	breq1d	⊢ ( ¬ 𝑣 = 𝑤 → ( if ( 𝑣 = 𝑤 , 0 , 1 ) < 1 ↔ 1 < 1 ) )
27	24 26	mtbiri	⊢ ( ¬ 𝑣 = 𝑤 → ¬ if ( 𝑣 = 𝑤 , 0 , 1 ) < 1 )
28	27	con4i	⊢ ( if ( 𝑣 = 𝑤 , 0 , 1 ) < 1 → 𝑣 = 𝑤 )
29		iftrue	⊢ ( 𝑣 = 𝑤 → if ( 𝑣 = 𝑤 , 0 , 1 ) = 0 )
30		0lt1	⊢ 0 < 1
31	29 30	eqbrtrdi	⊢ ( 𝑣 = 𝑤 → if ( 𝑣 = 𝑤 , 0 , 1 ) < 1 )
32	28 31	impbii	⊢ ( if ( 𝑣 = 𝑤 , 0 , 1 ) < 1 ↔ 𝑣 = 𝑤 )
33		equcom	⊢ ( 𝑣 = 𝑤 ↔ 𝑤 = 𝑣 )
34	32 33	bitri	⊢ ( if ( 𝑣 = 𝑤 , 0 , 1 ) < 1 ↔ 𝑤 = 𝑣 )
35	23 34	bitr2di	⊢ ( ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 = 𝑣 ↔ ( 𝑣 𝐷 𝑤 ) < 1 ) )
36		simpr	⊢ ( ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → 𝑤 ∈ 𝑋 )
37	36	biantrurd	⊢ ( ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑣 𝐷 𝑤 ) < 1 ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑤 ) < 1 ) ) )
38	35 37	bitrd	⊢ ( ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 = 𝑣 ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑤 ) < 1 ) ) )
39	38	ex	⊢ ( 𝑣 ∈ 𝑋 → ( 𝑤 ∈ 𝑋 → ( 𝑤 = 𝑣 ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑤 ) < 1 ) ) ) )
40	13 15 39	pm5.21ndd	⊢ ( 𝑣 ∈ 𝑋 → ( 𝑤 = 𝑣 ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑤 ) < 1 ) ) )
41	40	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) → ( 𝑤 = 𝑣 ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑤 ) < 1 ) ) )
42		1xr	⊢ 1 ∈ ℝ*
43		elbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑋 ∧ 1 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝑣 ( ball ‘ 𝐷 ) 1 ) ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑤 ) < 1 ) ) )
44	42 43	mp3an3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑋 ) → ( 𝑤 ∈ ( 𝑣 ( ball ‘ 𝐷 ) 1 ) ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑤 ) < 1 ) ) )
45	4 44	sylan	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) → ( 𝑤 ∈ ( 𝑣 ( ball ‘ 𝐷 ) 1 ) ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑤 ) < 1 ) ) )
46	41 45	bitr4d	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) → ( 𝑤 = 𝑣 ↔ 𝑤 ∈ ( 𝑣 ( ball ‘ 𝐷 ) 1 ) ) )
47	12 46	syl5bb	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) → ( 𝑤 ∈ { 𝑣 } ↔ 𝑤 ∈ ( 𝑣 ( ball ‘ 𝐷 ) 1 ) ) )
48	47	eqrdv	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) → { 𝑣 } = ( 𝑣 ( ball ‘ 𝐷 ) 1 ) )
49		blelrn	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑋 ∧ 1 ∈ ℝ* ) → ( 𝑣 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) )
50	42 49	mp3an3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑋 ) → ( 𝑣 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) )
51	4 50	sylan	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) → ( 𝑣 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) )
52	48 51	eqeltrd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) → { 𝑣 } ∈ ran ( ball ‘ 𝐷 ) )
53		snssi	⊢ ( 𝑣 ∈ 𝑢 → { 𝑣 } ⊆ 𝑢 )
54		vsnid	⊢ 𝑣 ∈ { 𝑣 }
55	53 54	jctil	⊢ ( 𝑣 ∈ 𝑢 → ( 𝑣 ∈ { 𝑣 } ∧ { 𝑣 } ⊆ 𝑢 ) )
56		eleq2	⊢ ( 𝑤 = { 𝑣 } → ( 𝑣 ∈ 𝑤 ↔ 𝑣 ∈ { 𝑣 } ) )
57		sseq1	⊢ ( 𝑤 = { 𝑣 } → ( 𝑤 ⊆ 𝑢 ↔ { 𝑣 } ⊆ 𝑢 ) )
58	56 57	anbi12d	⊢ ( 𝑤 = { 𝑣 } → ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ↔ ( 𝑣 ∈ { 𝑣 } ∧ { 𝑣 } ⊆ 𝑢 ) ) )
59	58	rspcev	⊢ ( ( { 𝑣 } ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝑣 ∈ { 𝑣 } ∧ { 𝑣 } ⊆ 𝑢 ) ) → ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
60	52 55 59	syl2an	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑢 ) → ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
61	11 60	sylancom	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑢 ⊆ 𝑋 ) ∧ 𝑣 ∈ 𝑢 ) → ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
62	61	ralrimiva	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑢 ⊆ 𝑋 ) → ∀ 𝑣 ∈ 𝑢 ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
63	62	ex	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑢 ⊆ 𝑋 → ∀ 𝑣 ∈ 𝑢 ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) )
64	63	pm4.71d	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑢 ⊆ 𝑋 ↔ ( 𝑢 ⊆ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) ) )
65	7 64	bitr4d	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑢 ∈ ( MetOpen ‘ 𝐷 ) ↔ 𝑢 ⊆ 𝑋 ) )
66		velpw	⊢ ( 𝑢 ∈ 𝒫 𝑋 ↔ 𝑢 ⊆ 𝑋 )
67	65 66	bitr4di	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑢 ∈ ( MetOpen ‘ 𝐷 ) ↔ 𝑢 ∈ 𝒫 𝑋 ) )
68	67	eqrdv	⊢ ( 𝑋 ∈ 𝑉 → ( MetOpen ‘ 𝐷 ) = 𝒫 𝑋 )