dislly

Description: The discrete space ~P X is locally A if and only if every singleton space has property A . (Contributed by Mario Carneiro, 20-Mar-2015)

		Ref	Expression
	Assertion	dislly	$⊢ X \in V \to (𝒫 X \in LocallyA\leftrightarrow\forall x \in X)$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\to𝒫 X \in LocallyA))$
2		simpr	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\tox \in X))$
3		vex	$⊢ x \in V$
4	3	snelpw	$⊢ x \in X \leftrightarrow \{x\} \in 𝒫 X$
5	2 4	sylib	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\to\{x\} \in 𝒫 X))$
6		vsnid	$⊢ x \in \{x\}$
7	6	a1i	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\tox \in \{x\}))$
8		llyi	$⊢ (𝒫 X \in LocallyA\land\{x\} \in 𝒫 X\landx \in \{x\}\to\exists y \in 𝒫 X)$
9	1 5 7 8	syl3anc	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\to\exists y \in 𝒫 X))$
10		simpr1	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\toy \subseteq \{x\})))$
11		simpr2	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\tox \in y)))$
12	11	snssd	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\to\{x\} \subseteq y)))$
13	10 12	eqssd	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\toy = \{x\})))$
14	13	oveq2d	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\to𝒫 X ↾_{𝑡} y = 𝒫 X ↾_{𝑡} \{x\})))$
15		simplll	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\toX \in V)))$
16		simplr	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\tox \in X)))$
17	16	snssd	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\to\{x\} \subseteq X)))$
18		restdis	$⊢ (X \in V \land \{x\} \subseteq X) \to 𝒫 X ↾_{𝑡} \{x\} = 𝒫 \{x\}$
19	15 17 18	syl2anc	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\to𝒫 X ↾_{𝑡} \{x\} = 𝒫 \{x\})))$
20	14 19	eqtrd	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\to𝒫 X ↾_{𝑡} y = 𝒫 \{x\})))$
21		simpr3	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\to𝒫 X ↾_{𝑡} y \in A)))$
22	20 21	eqeltrrd	$⊢ (((X \in V \land 𝒫 X \in LocallyA\landx \in X\land(y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A)\to𝒫 \{x\} \in A)))$
23	22	ex	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\to((y \subseteq \{x\} \land x \in y \land 𝒫 X ↾_{𝑡} y \in A) \to 𝒫 \{x\} \in A)))$
24	23	rexlimdvw	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\to(\exists y \in 𝒫 X \to 𝒫 \{x\} \in A)))$
25	9 24	mpd	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\to𝒫 \{x\} \in A))$
26	25	ralrimiva	$⊢ (X \in V \land 𝒫 X \in LocallyA\to\forall x \in X)$
27		distop	$⊢ X \in V \to 𝒫 X \in Top$
28	27	adantr	$⊢ (X \in V \land \forall x \in X 𝒫 \{x\} \in A) \to 𝒫 X \in Top$
29		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
30	29	adantl	$⊢ (X \in V \land y \in 𝒫 X) \to y \subseteq X$
31		ssralv	$⊢ y \subseteq X \to (\forall x \in X 𝒫 \{x\} \in A \to \forall x \in y 𝒫 \{x\} \in A)$
32	30 31	syl	$⊢ (X \in V \land y \in 𝒫 X) \to (\forall x \in X 𝒫 \{x\} \in A \to \forall x \in y 𝒫 \{x\} \in A)$
33		simprl	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to x \in y$
34	33	snssd	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \{x\} \subseteq y$
35	30	adantr	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to y \subseteq X$
36	34 35	sstrd	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \{x\} \subseteq X$
37		snex	$⊢ \{x\} \in V$
38	37	elpw	$⊢ \{x\} \in 𝒫 X \leftrightarrow \{x\} \subseteq X$
39	36 38	sylibr	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \{x\} \in 𝒫 X$
40	37	elpw	$⊢ \{x\} \in 𝒫 y \leftrightarrow \{x\} \subseteq y$
41	34 40	sylibr	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \{x\} \in 𝒫 y$
42	39 41	elind	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \{x\} \in (𝒫 X \cap 𝒫 y)$
43		snidg	$⊢ x \in y \to x \in \{x\}$
44	43	ad2antrl	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to x \in \{x\}$
45		simpll	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to X \in V$
46	45 36 18	syl2anc	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to 𝒫 X ↾_{𝑡} \{x\} = 𝒫 \{x\}$
47		simprr	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to 𝒫 \{x\} \in A$
48	46 47	eqeltrd	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to 𝒫 X ↾_{𝑡} \{x\} \in A$
49		eleq2	$⊢ u = \{x\} \to (x \in u \leftrightarrow x \in \{x\})$
50		oveq2	$⊢ u = \{x\} \to 𝒫 X ↾_{𝑡} u = 𝒫 X ↾_{𝑡} \{x\}$
51	50	eleq1d	$⊢ u = \{x\} \to (𝒫 X ↾_{𝑡} u \in A \leftrightarrow 𝒫 X ↾_{𝑡} \{x\} \in A)$
52	49 51	anbi12d	$⊢ u = \{x\} \to ((x \in u \land 𝒫 X ↾_{𝑡} u \in A) \leftrightarrow (x \in \{x\} \land 𝒫 X ↾_{𝑡} \{x\} \in A))$
53	52	rspcev	$⊢ (\{x\} \in (𝒫 X \cap 𝒫 y) \land (x \in \{x\} \land 𝒫 X ↾_{𝑡} \{x\} \in A)) \to \exists u \in (𝒫 X \cap 𝒫 y) (x \in u \land 𝒫 X ↾_{𝑡} u \in A)$
54	42 44 48 53	syl12anc	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \exists u \in (𝒫 X \cap 𝒫 y) (x \in u \land 𝒫 X ↾_{𝑡} u \in A)$
55	54	expr	$⊢ ((X \in V \land y \in 𝒫 X) \land x \in y) \to (𝒫 \{x\} \in A \to \exists u \in (𝒫 X \cap 𝒫 y) (x \in u \land 𝒫 X ↾_{𝑡} u \in A))$
56	55	ralimdva	$⊢ (X \in V \land y \in 𝒫 X) \to (\forall x \in y 𝒫 \{x\} \in A \to \forall x \in y \exists u \in (𝒫 X \cap 𝒫 y) (x \in u \land 𝒫 X ↾_{𝑡} u \in A))$
57	32 56	syld	$⊢ (X \in V \land y \in 𝒫 X) \to (\forall x \in X 𝒫 \{x\} \in A \to \forall x \in y \exists u \in (𝒫 X \cap 𝒫 y) (x \in u \land 𝒫 X ↾_{𝑡} u \in A))$
58	57	imp	$⊢ ((X \in V \land y \in 𝒫 X) \land \forall x \in X 𝒫 \{x\} \in A) \to \forall x \in y \exists u \in (𝒫 X \cap 𝒫 y) (x \in u \land 𝒫 X ↾_{𝑡} u \in A)$
59	58	an32s	$⊢ ((X \in V \land \forall x \in X 𝒫 \{x\} \in A) \land y \in 𝒫 X) \to \forall x \in y \exists u \in (𝒫 X \cap 𝒫 y) (x \in u \land 𝒫 X ↾_{𝑡} u \in A)$
60	59	ralrimiva	$⊢ (X \in V \land \forall x \in X 𝒫 \{x\} \in A) \to \forall y \in 𝒫 X \forall x \in y \exists u \in (𝒫 X \cap 𝒫 y) (x \in u \land 𝒫 X ↾_{𝑡} u \in A)$
61		islly	$⊢ 𝒫 X \in LocallyA\leftrightarrow(𝒫 X \in Top \land \forall y \in 𝒫 X)$
62	28 60 61	sylanbrc	$⊢ (X \in V \land \forall x \in X 𝒫 \{x\} \in A) \to 𝒫 X \in LocallyA$
63	26 62	impbida	$⊢ X \in V \to (𝒫 X \in LocallyA\leftrightarrow\forall x \in X)$

Metamath Proof Explorer

Theorem dislly

Proof