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		vex	$⊢ x \in V$
3	2	snelpw	$⊢ x \in X \leftrightarrow \{x\} \in 𝒫 X$
4	3	bilani	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\to\{x\} \in 𝒫 X))$
5		vsnid	$⊢ x \in \{x\}$
6	5	a1i	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\tox \in \{x\}))$
7		llyi	$⊢ (𝒫 X \in LocallyA\land\{x\} \in 𝒫 X\landx \in \{x\}\to\exists y \in 𝒫 X)$
8	1 4 6 7	syl3anc	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\to\exists y \in 𝒫 X))$
9		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\})))$
10		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)))$
11	10	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)))$
12	9 11	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\})))$
13	12	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\})))$
14		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)))$
15		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)))$
16	15	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)))$
17		restdis	$⊢ (X \in V \land \{x\} \subseteq X) \to 𝒫 X ↾_{𝑡} \{x\} = 𝒫 \{x\}$
18	14 16 17	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\})))$
19	13 18	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\})))$
20		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)))$
21	19 20	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)))$
22	21	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)))$
23	22	rexlimdvw	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\to(\exists y \in 𝒫 X \to 𝒫 \{x\} \in A)))$
24	8 23	mpd	$⊢ ((X \in V \land 𝒫 X \in LocallyA\landx \in X\to𝒫 \{x\} \in A))$
25	24	ralrimiva	$⊢ (X \in V \land 𝒫 X \in LocallyA\to\forall x \in X)$
26		distop	$⊢ X \in V \to 𝒫 X \in Top$
27	26	adantr	$⊢ (X \in V \land \forall x \in X 𝒫 \{x\} \in A) \to 𝒫 X \in Top$
28		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
29	28	adantl	$⊢ (X \in V \land y \in 𝒫 X) \to y \subseteq X$
30		ssralv	$⊢ y \subseteq X \to (\forall x \in X 𝒫 \{x\} \in A \to \forall x \in y 𝒫 \{x\} \in A)$
31	29 30	syl	$⊢ (X \in V \land y \in 𝒫 X) \to (\forall x \in X 𝒫 \{x\} \in A \to \forall x \in y 𝒫 \{x\} \in A)$
32		simprl	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to x \in y$
33	32	snssd	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \{x\} \subseteq y$
34	29	adantr	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to y \subseteq X$
35	33 34	sstrd	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \{x\} \subseteq X$
36		vsnex	$⊢ \{x\} \in V$
37	36	elpw	$⊢ \{x\} \in 𝒫 X \leftrightarrow \{x\} \subseteq X$
38	35 37	sylibr	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \{x\} \in 𝒫 X$
39	36	elpw	$⊢ \{x\} \in 𝒫 y \leftrightarrow \{x\} \subseteq y$
40	33 39	sylibr	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \{x\} \in 𝒫 y$
41	38 40	elind	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to \{x\} \in (𝒫 X \cap 𝒫 y)$
42		snidg	$⊢ x \in y \to x \in \{x\}$
43	42	ad2antrl	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to x \in \{x\}$
44		simpll	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to X \in V$
45	44 35 17	syl2anc	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to 𝒫 X ↾_{𝑡} \{x\} = 𝒫 \{x\}$
46		simprr	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to 𝒫 \{x\} \in A$
47	45 46	eqeltrd	$⊢ ((X \in V \land y \in 𝒫 X) \land (x \in y \land 𝒫 \{x\} \in A)) \to 𝒫 X ↾_{𝑡} \{x\} \in A$
48		eleq2	$⊢ u = \{x\} \to (x \in u \leftrightarrow x \in \{x\})$
49		oveq2	$⊢ u = \{x\} \to 𝒫 X ↾_{𝑡} u = 𝒫 X ↾_{𝑡} \{x\}$
50	49	eleq1d	$⊢ u = \{x\} \to (𝒫 X ↾_{𝑡} u \in A \leftrightarrow 𝒫 X ↾_{𝑡} \{x\} \in A)$
51	48 50	anbi12d	$⊢ u = \{x\} \to ((x \in u \land 𝒫 X ↾_{𝑡} u \in A) \leftrightarrow (x \in \{x\} \land 𝒫 X ↾_{𝑡} \{x\} \in A))$
52	51	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)$
53	41 43 47 52	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)$
54	53	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))$
55	54	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))$
56	31 55	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))$
57	56	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)$
58	57	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)$
59	58	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)$
60		islly	$⊢ 𝒫 X \in LocallyA\leftrightarrow(𝒫 X \in Top \land \forall y \in 𝒫 X)$
61	27 59 60	sylanbrc	$⊢ (X \in V \land \forall x \in X 𝒫 \{x\} \in A) \to 𝒫 X \in LocallyA$
62	25 61	impbida	$⊢ X \in V \to (𝒫 X \in LocallyA\leftrightarrow\forall x \in X)$

Metamath Proof Explorer

Theorem dislly

Proof