epttop

Description: The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Assertion	epttop	$⊢ (A \in V \land P \in A) \to \{x \in 𝒫 A \| (P \in x \to x = A)\} \in TopOn (A)$

Proof

Step	Hyp	Ref	Expression
1		ssrab	$⊢ y \subseteq \{x \in 𝒫 A \| (P \in x \to x = A)\} \leftrightarrow (y \subseteq 𝒫 A \land \forall x \in y (P \in x \to x = A))$
2		eleq2	$⊢ x = ⋃ y \to (P \in x \leftrightarrow P \in ⋃ y)$
3		eqeq1	$⊢ x = ⋃ y \to (x = A \leftrightarrow ⋃ y = A)$
4	2 3	imbi12d	$⊢ x = ⋃ y \to ((P \in x \to x = A) \leftrightarrow (P \in ⋃ y \to ⋃ y = A))$
5		simprl	$⊢ ((A \in V \land P \in A) \land (y \subseteq 𝒫 A \land \forall x \in y (P \in x \to x = A))) \to y \subseteq 𝒫 A$
6		sspwuni	$⊢ y \subseteq 𝒫 A \leftrightarrow ⋃ y \subseteq A$
7	5 6	sylib	$⊢ ((A \in V \land P \in A) \land (y \subseteq 𝒫 A \land \forall x \in y (P \in x \to x = A))) \to ⋃ y \subseteq A$
8		vuniex	$⊢ ⋃ y \in V$
9	8	elpw	$⊢ ⋃ y \in 𝒫 A \leftrightarrow ⋃ y \subseteq A$
10	7 9	sylibr	$⊢ ((A \in V \land P \in A) \land (y \subseteq 𝒫 A \land \forall x \in y (P \in x \to x = A))) \to ⋃ y \in 𝒫 A$
11		eluni2	$⊢ P \in ⋃ y \leftrightarrow \exists x \in y P \in x$
12		r19.29	$⊢ (\forall x \in y (P \in x \to x = A) \land \exists x \in y P \in x) \to \exists x \in y ((P \in x \to x = A) \land P \in x)$
13		simpr	$⊢ (x \in y \land (P \in x \to x = A)) \to (P \in x \to x = A)$
14	13	impr	$⊢ (x \in y \land ((P \in x \to x = A) \land P \in x)) \to x = A$
15		elssuni	$⊢ x \in y \to x \subseteq ⋃ y$
16	15	adantr	$⊢ (x \in y \land ((P \in x \to x = A) \land P \in x)) \to x \subseteq ⋃ y$
17	14 16	eqsstrrd	$⊢ (x \in y \land ((P \in x \to x = A) \land P \in x)) \to A \subseteq ⋃ y$
18	17	rexlimiva	$⊢ \exists x \in y ((P \in x \to x = A) \land P \in x) \to A \subseteq ⋃ y$
19	12 18	syl	$⊢ (\forall x \in y (P \in x \to x = A) \land \exists x \in y P \in x) \to A \subseteq ⋃ y$
20	19	ex	$⊢ \forall x \in y (P \in x \to x = A) \to (\exists x \in y P \in x \to A \subseteq ⋃ y)$
21	20	ad2antll	$⊢ ((A \in V \land P \in A) \land (y \subseteq 𝒫 A \land \forall x \in y (P \in x \to x = A))) \to (\exists x \in y P \in x \to A \subseteq ⋃ y)$
22	11 21	syl5bi	$⊢ ((A \in V \land P \in A) \land (y \subseteq 𝒫 A \land \forall x \in y (P \in x \to x = A))) \to (P \in ⋃ y \to A \subseteq ⋃ y)$
23	22 7	jctild	$⊢ ((A \in V \land P \in A) \land (y \subseteq 𝒫 A \land \forall x \in y (P \in x \to x = A))) \to (P \in ⋃ y \to (⋃ y \subseteq A \land A \subseteq ⋃ y))$
24		eqss	$⊢ ⋃ y = A \leftrightarrow (⋃ y \subseteq A \land A \subseteq ⋃ y)$
25	23 24	syl6ibr	$⊢ ((A \in V \land P \in A) \land (y \subseteq 𝒫 A \land \forall x \in y (P \in x \to x = A))) \to (P \in ⋃ y \to ⋃ y = A)$
26	4 10 25	elrabd	$⊢ ((A \in V \land P \in A) \land (y \subseteq 𝒫 A \land \forall x \in y (P \in x \to x = A))) \to ⋃ y \in \{x \in 𝒫 A \| (P \in x \to x = A)\}$
27	26	ex	$⊢ (A \in V \land P \in A) \to ((y \subseteq 𝒫 A \land \forall x \in y (P \in x \to x = A)) \to ⋃ y \in \{x \in 𝒫 A \| (P \in x \to x = A)\})$
28	1 27	syl5bi	$⊢ (A \in V \land P \in A) \to (y \subseteq \{x \in 𝒫 A \| (P \in x \to x = A)\} \to ⋃ y \in \{x \in 𝒫 A \| (P \in x \to x = A)\})$
29	28	alrimiv	$⊢ (A \in V \land P \in A) \to \forall y (y \subseteq \{x \in 𝒫 A \| (P \in x \to x = A)\} \to ⋃ y \in \{x \in 𝒫 A \| (P \in x \to x = A)\})$
30		inss1	$⊢ y \cap z \subseteq y$
31		simprll	$⊢ ((A \in V \land P \in A) \land ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))) \to y \in 𝒫 A$
32	31	elpwid	$⊢ ((A \in V \land P \in A) \land ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))) \to y \subseteq A$
33	30 32	sstrid	$⊢ ((A \in V \land P \in A) \land ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))) \to y \cap z \subseteq A$
34		vex	$⊢ y \in V$
35	34	inex1	$⊢ y \cap z \in V$
36	35	elpw	$⊢ y \cap z \in 𝒫 A \leftrightarrow y \cap z \subseteq A$
37	33 36	sylibr	$⊢ ((A \in V \land P \in A) \land ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))) \to y \cap z \in 𝒫 A$
38		elin	$⊢ P \in (y \cap z) \leftrightarrow (P \in y \land P \in z)$
39		simprlr	$⊢ ((A \in V \land P \in A) \land ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))) \to (P \in y \to y = A)$
40		simprrr	$⊢ ((A \in V \land P \in A) \land ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))) \to (P \in z \to z = A)$
41	39 40	anim12d	$⊢ ((A \in V \land P \in A) \land ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))) \to ((P \in y \land P \in z) \to (y = A \land z = A))$
42		ineq12	$⊢ (y = A \land z = A) \to y \cap z = A \cap A$
43		inidm	$⊢ A \cap A = A$
44	42 43	eqtrdi	$⊢ (y = A \land z = A) \to y \cap z = A$
45	41 44	syl6	$⊢ ((A \in V \land P \in A) \land ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))) \to ((P \in y \land P \in z) \to y \cap z = A)$
46	38 45	syl5bi	$⊢ ((A \in V \land P \in A) \land ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))) \to (P \in (y \cap z) \to y \cap z = A)$
47	37 46	jca	$⊢ ((A \in V \land P \in A) \land ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))) \to (y \cap z \in 𝒫 A \land (P \in (y \cap z) \to y \cap z = A))$
48	47	ex	$⊢ (A \in V \land P \in A) \to (((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A))) \to (y \cap z \in 𝒫 A \land (P \in (y \cap z) \to y \cap z = A)))$
49		eleq2	$⊢ x = y \to (P \in x \leftrightarrow P \in y)$
50		eqeq1	$⊢ x = y \to (x = A \leftrightarrow y = A)$
51	49 50	imbi12d	$⊢ x = y \to ((P \in x \to x = A) \leftrightarrow (P \in y \to y = A))$
52	51	elrab	$⊢ y \in \{x \in 𝒫 A \| (P \in x \to x = A)\} \leftrightarrow (y \in 𝒫 A \land (P \in y \to y = A))$
53		eleq2	$⊢ x = z \to (P \in x \leftrightarrow P \in z)$
54		eqeq1	$⊢ x = z \to (x = A \leftrightarrow z = A)$
55	53 54	imbi12d	$⊢ x = z \to ((P \in x \to x = A) \leftrightarrow (P \in z \to z = A))$
56	55	elrab	$⊢ z \in \{x \in 𝒫 A \| (P \in x \to x = A)\} \leftrightarrow (z \in 𝒫 A \land (P \in z \to z = A))$
57	52 56	anbi12i	$⊢ (y \in \{x \in 𝒫 A \| (P \in x \to x = A)\} \land z \in \{x \in 𝒫 A \| (P \in x \to x = A)\}) \leftrightarrow ((y \in 𝒫 A \land (P \in y \to y = A)) \land (z \in 𝒫 A \land (P \in z \to z = A)))$
58		eleq2	$⊢ x = y \cap z \to (P \in x \leftrightarrow P \in (y \cap z))$
59		eqeq1	$⊢ x = y \cap z \to (x = A \leftrightarrow y \cap z = A)$
60	58 59	imbi12d	$⊢ x = y \cap z \to ((P \in x \to x = A) \leftrightarrow (P \in (y \cap z) \to y \cap z = A))$
61	60	elrab	$⊢ y \cap z \in \{x \in 𝒫 A \| (P \in x \to x = A)\} \leftrightarrow (y \cap z \in 𝒫 A \land (P \in (y \cap z) \to y \cap z = A))$
62	48 57 61	3imtr4g	$⊢ (A \in V \land P \in A) \to ((y \in \{x \in 𝒫 A \| (P \in x \to x = A)\} \land z \in \{x \in 𝒫 A \| (P \in x \to x = A)\}) \to y \cap z \in \{x \in 𝒫 A \| (P \in x \to x = A)\})$
63	62	ralrimivv	$⊢ (A \in V \land P \in A) \to \forall y \in \{x \in 𝒫 A \| (P \in x \to x = A)\} \forall z \in \{x \in 𝒫 A \| (P \in x \to x = A)\} y \cap z \in \{x \in 𝒫 A \| (P \in x \to x = A)\}$
64		pwexg	$⊢ A \in V \to 𝒫 A \in V$
65	64	adantr	$⊢ (A \in V \land P \in A) \to 𝒫 A \in V$
66		rabexg	$⊢ 𝒫 A \in V \to \{x \in 𝒫 A \| (P \in x \to x = A)\} \in V$
67	65 66	syl	$⊢ (A \in V \land P \in A) \to \{x \in 𝒫 A \| (P \in x \to x = A)\} \in V$
68		istopg	$⊢ \{x \in 𝒫 A \| (P \in x \to x = A)\} \in V \to (\{x \in 𝒫 A \| (P \in x \to x = A)\} \in Top \leftrightarrow (\forall y (y \subseteq \{x \in 𝒫 A \| (P \in x \to x = A)\} \to ⋃ y \in \{x \in 𝒫 A \| (P \in x \to x = A)\}) \land \forall y \in \{x \in 𝒫 A \| (P \in x \to x = A)\} \forall z \in \{x \in 𝒫 A \| (P \in x \to x = A)\} y \cap z \in \{x \in 𝒫 A \| (P \in x \to x = A)\}))$
69	67 68	syl	$⊢ (A \in V \land P \in A) \to (\{x \in 𝒫 A \| (P \in x \to x = A)\} \in Top \leftrightarrow (\forall y (y \subseteq \{x \in 𝒫 A \| (P \in x \to x = A)\} \to ⋃ y \in \{x \in 𝒫 A \| (P \in x \to x = A)\}) \land \forall y \in \{x \in 𝒫 A \| (P \in x \to x = A)\} \forall z \in \{x \in 𝒫 A \| (P \in x \to x = A)\} y \cap z \in \{x \in 𝒫 A \| (P \in x \to x = A)\}))$
70	29 63 69	mpbir2and	$⊢ (A \in V \land P \in A) \to \{x \in 𝒫 A \| (P \in x \to x = A)\} \in Top$
71		eleq2	$⊢ x = A \to (P \in x \leftrightarrow P \in A)$
72		eqeq1	$⊢ x = A \to (x = A \leftrightarrow A = A)$
73	71 72	imbi12d	$⊢ x = A \to ((P \in x \to x = A) \leftrightarrow (P \in A \to A = A))$
74		pwidg	$⊢ A \in V \to A \in 𝒫 A$
75	74	adantr	$⊢ (A \in V \land P \in A) \to A \in 𝒫 A$
76		eqidd	$⊢ (A \in V \land P \in A) \to A = A$
77	76	a1d	$⊢ (A \in V \land P \in A) \to (P \in A \to A = A)$
78	73 75 77	elrabd	$⊢ (A \in V \land P \in A) \to A \in \{x \in 𝒫 A \| (P \in x \to x = A)\}$
79		elssuni	$⊢ A \in \{x \in 𝒫 A \| (P \in x \to x = A)\} \to A \subseteq ⋃ \{x \in 𝒫 A \| (P \in x \to x = A)\}$
80	78 79	syl	$⊢ (A \in V \land P \in A) \to A \subseteq ⋃ \{x \in 𝒫 A \| (P \in x \to x = A)\}$
81		ssrab2	$⊢ \{x \in 𝒫 A \| (P \in x \to x = A)\} \subseteq 𝒫 A$
82		sspwuni	$⊢ \{x \in 𝒫 A \| (P \in x \to x = A)\} \subseteq 𝒫 A \leftrightarrow ⋃ \{x \in 𝒫 A \| (P \in x \to x = A)\} \subseteq A$
83	81 82	mpbi	$⊢ ⋃ \{x \in 𝒫 A \| (P \in x \to x = A)\} \subseteq A$
84	83	a1i	$⊢ (A \in V \land P \in A) \to ⋃ \{x \in 𝒫 A \| (P \in x \to x = A)\} \subseteq A$
85	80 84	eqssd	$⊢ (A \in V \land P \in A) \to A = ⋃ \{x \in 𝒫 A \| (P \in x \to x = A)\}$
86		istopon	$⊢ \{x \in 𝒫 A \| (P \in x \to x = A)\} \in TopOn (A) \leftrightarrow (\{x \in 𝒫 A \| (P \in x \to x = A)\} \in Top \land A = ⋃ \{x \in 𝒫 A \| (P \in x \to x = A)\})$
87	70 85 86	sylanbrc	$⊢ (A \in V \land P \in A) \to \{x \in 𝒫 A \| (P \in x \to x = A)\} \in TopOn (A)$

Metamath Proof Explorer

Theorem epttop

Proof