cctop

Description: The countable complement topology on a set A . Example 4 in Munkres p. 77. (Contributed by FL, 23-Aug-2006) (Revised by Mario Carneiro, 13-Aug-2015)

		Ref	Expression
	Assertion	cctop	$⊢ A \in V \to \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \in TopOn (A)$

Proof

Step	Hyp	Ref	Expression
1		difeq2	$⊢ x = ⋃ y \to A ∖ x = A ∖ ⋃ y$
2	1	breq1d	$⊢ x = ⋃ y \to ((A ∖ x) ≼ ω \leftrightarrow (A ∖ ⋃ y) ≼ ω)$
3		eqeq1	$⊢ x = ⋃ y \to (x = \emptyset \leftrightarrow ⋃ y = \emptyset)$
4	2 3	orbi12d	$⊢ x = ⋃ y \to (((A ∖ x) ≼ ω \lor x = \emptyset) \leftrightarrow ((A ∖ ⋃ y) ≼ ω \lor ⋃ y = \emptyset))$
5		uniss	$⊢ y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to ⋃ y \subseteq ⋃ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}$
6		ssrab2	$⊢ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \subseteq 𝒫 A$
7		sspwuni	$⊢ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \subseteq 𝒫 A \leftrightarrow ⋃ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \subseteq A$
8	6 7	mpbi	$⊢ ⋃ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \subseteq A$
9	5 8	sstrdi	$⊢ y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to ⋃ y \subseteq A$
10		vuniex	$⊢ ⋃ y \in V$
11	10	elpw	$⊢ ⋃ y \in 𝒫 A \leftrightarrow ⋃ y \subseteq A$
12	9 11	sylibr	$⊢ y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to ⋃ y \in 𝒫 A$
13		uni0c	$⊢ ⋃ y = \emptyset \leftrightarrow \forall z \in y z = \emptyset$
14	13	notbii	$⊢ \neg ⋃ y = \emptyset \leftrightarrow \neg \forall z \in y z = \emptyset$
15		rexnal	$⊢ \exists z \in y \neg z = \emptyset \leftrightarrow \neg \forall z \in y z = \emptyset$
16	14 15	bitr4i	$⊢ \neg ⋃ y = \emptyset \leftrightarrow \exists z \in y \neg z = \emptyset$
17		ssel2	$⊢ (y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \to z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}$
18		difeq2	$⊢ x = z \to A ∖ x = A ∖ z$
19	18	breq1d	$⊢ x = z \to ((A ∖ x) ≼ ω \leftrightarrow (A ∖ z) ≼ ω)$
20		eqeq1	$⊢ x = z \to (x = \emptyset \leftrightarrow z = \emptyset)$
21	19 20	orbi12d	$⊢ x = z \to (((A ∖ x) ≼ ω \lor x = \emptyset) \leftrightarrow ((A ∖ z) ≼ ω \lor z = \emptyset))$
22	21	elrab	$⊢ z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \leftrightarrow (z \in 𝒫 A \land ((A ∖ z) ≼ ω \lor z = \emptyset))$
23	17 22	sylib	$⊢ (y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \to (z \in 𝒫 A \land ((A ∖ z) ≼ ω \lor z = \emptyset))$
24	23	simprd	$⊢ (y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \to ((A ∖ z) ≼ ω \lor z = \emptyset)$
25	24	ord	$⊢ (y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \to (\neg (A ∖ z) ≼ ω \to z = \emptyset)$
26	25	con1d	$⊢ (y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \to (\neg z = \emptyset \to (A ∖ z) ≼ ω)$
27	26	imp	$⊢ ((y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \land \neg z = \emptyset) \to (A ∖ z) ≼ ω$
28		ctex	$⊢ (A ∖ z) ≼ ω \to A ∖ z \in V$
29	28	adantl	$⊢ (((y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \land \neg z = \emptyset) \land (A ∖ z) ≼ ω) \to A ∖ z \in V$
30		simpllr	$⊢ (((y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \land \neg z = \emptyset) \land (A ∖ z) ≼ ω) \to z \in y$
31		elssuni	$⊢ z \in y \to z \subseteq ⋃ y$
32		sscon	$⊢ z \subseteq ⋃ y \to A ∖ ⋃ y \subseteq A ∖ z$
33	30 31 32	3syl	$⊢ (((y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \land \neg z = \emptyset) \land (A ∖ z) ≼ ω) \to A ∖ ⋃ y \subseteq A ∖ z$
34		ssdomg	$⊢ A ∖ z \in V \to (A ∖ ⋃ y \subseteq A ∖ z \to (A ∖ ⋃ y) ≼ (A ∖ z))$
35	29 33 34	sylc	$⊢ (((y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \land \neg z = \emptyset) \land (A ∖ z) ≼ ω) \to (A ∖ ⋃ y) ≼ (A ∖ z)$
36		domtr	$⊢ ((A ∖ ⋃ y) ≼ (A ∖ z) \land (A ∖ z) ≼ ω) \to (A ∖ ⋃ y) ≼ ω$
37	35 36	sylancom	$⊢ (((y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \land \neg z = \emptyset) \land (A ∖ z) ≼ ω) \to (A ∖ ⋃ y) ≼ ω$
38	27 37	mpdan	$⊢ ((y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in y) \land \neg z = \emptyset) \to (A ∖ ⋃ y) ≼ ω$
39	38	rexlimdva2	$⊢ y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to (\exists z \in y \neg z = \emptyset \to (A ∖ ⋃ y) ≼ ω)$
40	16 39	biimtrid	$⊢ y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to (\neg ⋃ y = \emptyset \to (A ∖ ⋃ y) ≼ ω)$
41	40	con1d	$⊢ y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to (\neg (A ∖ ⋃ y) ≼ ω \to ⋃ y = \emptyset)$
42	41	orrd	$⊢ y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to ((A ∖ ⋃ y) ≼ ω \lor ⋃ y = \emptyset)$
43	4 12 42	elrabd	$⊢ y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to ⋃ y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}$
44	43	ax-gen	$⊢ \forall y (y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to ⋃ y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\})$
45		difeq2	$⊢ x = y \to A ∖ x = A ∖ y$
46	45	breq1d	$⊢ x = y \to ((A ∖ x) ≼ ω \leftrightarrow (A ∖ y) ≼ ω)$
47		eqeq1	$⊢ x = y \to (x = \emptyset \leftrightarrow y = \emptyset)$
48	46 47	orbi12d	$⊢ x = y \to (((A ∖ x) ≼ ω \lor x = \emptyset) \leftrightarrow ((A ∖ y) ≼ ω \lor y = \emptyset))$
49	48	elrab	$⊢ y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \leftrightarrow (y \in 𝒫 A \land ((A ∖ y) ≼ ω \lor y = \emptyset))$
50		ssinss1	$⊢ y \subseteq A \to y \cap z \subseteq A$
51		vex	$⊢ y \in V$
52	51	elpw	$⊢ y \in 𝒫 A \leftrightarrow y \subseteq A$
53	51	inex1	$⊢ y \cap z \in V$
54	53	elpw	$⊢ y \cap z \in 𝒫 A \leftrightarrow y \cap z \subseteq A$
55	50 52 54	3imtr4i	$⊢ y \in 𝒫 A \to y \cap z \in 𝒫 A$
56	55	ad2antrr	$⊢ ((y \in 𝒫 A \land ((A ∖ y) ≼ ω \lor y = \emptyset)) \land (z \in 𝒫 A \land ((A ∖ z) ≼ ω \lor z = \emptyset))) \to y \cap z \in 𝒫 A$
57		difindi	$⊢ A ∖ (y \cap z) = (A ∖ y) \cup (A ∖ z)$
58		unctb	$⊢ ((A ∖ y) ≼ ω \land (A ∖ z) ≼ ω) \to ((A ∖ y) \cup (A ∖ z)) ≼ ω$
59	57 58	eqbrtrid	$⊢ ((A ∖ y) ≼ ω \land (A ∖ z) ≼ ω) \to (A ∖ (y \cap z)) ≼ ω$
60	59	orcd	$⊢ ((A ∖ y) ≼ ω \land (A ∖ z) ≼ ω) \to ((A ∖ (y \cap z)) ≼ ω \lor y \cap z = \emptyset)$
61		ineq1	$⊢ y = \emptyset \to y \cap z = \emptyset \cap z$
62		0in	$⊢ \emptyset \cap z = \emptyset$
63	61 62	eqtrdi	$⊢ y = \emptyset \to y \cap z = \emptyset$
64	63	olcd	$⊢ y = \emptyset \to ((A ∖ (y \cap z)) ≼ ω \lor y \cap z = \emptyset)$
65		ineq2	$⊢ z = \emptyset \to y \cap z = y \cap \emptyset$
66		in0	$⊢ y \cap \emptyset = \emptyset$
67	65 66	eqtrdi	$⊢ z = \emptyset \to y \cap z = \emptyset$
68	67	olcd	$⊢ z = \emptyset \to ((A ∖ (y \cap z)) ≼ ω \lor y \cap z = \emptyset)$
69	60 64 68	ccase2	$⊢ (((A ∖ y) ≼ ω \lor y = \emptyset) \land ((A ∖ z) ≼ ω \lor z = \emptyset)) \to ((A ∖ (y \cap z)) ≼ ω \lor y \cap z = \emptyset)$
70	69	ad2ant2l	$⊢ ((y \in 𝒫 A \land ((A ∖ y) ≼ ω \lor y = \emptyset)) \land (z \in 𝒫 A \land ((A ∖ z) ≼ ω \lor z = \emptyset))) \to ((A ∖ (y \cap z)) ≼ ω \lor y \cap z = \emptyset)$
71	56 70	jca	$⊢ ((y \in 𝒫 A \land ((A ∖ y) ≼ ω \lor y = \emptyset)) \land (z \in 𝒫 A \land ((A ∖ z) ≼ ω \lor z = \emptyset))) \to (y \cap z \in 𝒫 A \land ((A ∖ (y \cap z)) ≼ ω \lor y \cap z = \emptyset))$
72	49 22 71	syl2anb	$⊢ (y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}) \to (y \cap z \in 𝒫 A \land ((A ∖ (y \cap z)) ≼ ω \lor y \cap z = \emptyset))$
73		difeq2	$⊢ x = y \cap z \to A ∖ x = A ∖ (y \cap z)$
74	73	breq1d	$⊢ x = y \cap z \to ((A ∖ x) ≼ ω \leftrightarrow (A ∖ (y \cap z)) ≼ ω)$
75		eqeq1	$⊢ x = y \cap z \to (x = \emptyset \leftrightarrow y \cap z = \emptyset)$
76	74 75	orbi12d	$⊢ x = y \cap z \to (((A ∖ x) ≼ ω \lor x = \emptyset) \leftrightarrow ((A ∖ (y \cap z)) ≼ ω \lor y \cap z = \emptyset))$
77	76	elrab	$⊢ y \cap z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \leftrightarrow (y \cap z \in 𝒫 A \land ((A ∖ (y \cap z)) ≼ ω \lor y \cap z = \emptyset))$
78	72 77	sylibr	$⊢ (y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \land z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}) \to y \cap z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}$
79	78	rgen2	$⊢ \forall y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \forall z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} y \cap z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}$
80	44 79	pm3.2i	$⊢ (\forall y (y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to ⋃ y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}) \land \forall y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \forall z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} y \cap z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\})$
81		pwexg	$⊢ A \in V \to 𝒫 A \in V$
82		rabexg	$⊢ 𝒫 A \in V \to \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \in V$
83		istopg	$⊢ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \in V \to (\{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \in Top \leftrightarrow (\forall y (y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to ⋃ y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}) \land \forall y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \forall z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} y \cap z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}))$
84	81 82 83	3syl	$⊢ A \in V \to (\{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \in Top \leftrightarrow (\forall y (y \subseteq \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to ⋃ y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}) \land \forall y \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \forall z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} y \cap z \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}))$
85	80 84	mpbiri	$⊢ A \in V \to \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \in Top$
86		difeq2	$⊢ x = A \to A ∖ x = A ∖ A$
87		difid	$⊢ A ∖ A = \emptyset$
88	86 87	eqtrdi	$⊢ x = A \to A ∖ x = \emptyset$
89	88	breq1d	$⊢ x = A \to ((A ∖ x) ≼ ω \leftrightarrow \emptyset ≼ ω)$
90		eqeq1	$⊢ x = A \to (x = \emptyset \leftrightarrow A = \emptyset)$
91	89 90	orbi12d	$⊢ x = A \to (((A ∖ x) ≼ ω \lor x = \emptyset) \leftrightarrow (\emptyset ≼ ω \lor A = \emptyset))$
92		pwidg	$⊢ A \in V \to A \in 𝒫 A$
93		omex	$⊢ ω \in V$
94	93	0dom	$⊢ \emptyset ≼ ω$
95	94	orci	$⊢ (\emptyset ≼ ω \lor A = \emptyset)$
96	95	a1i	$⊢ A \in V \to (\emptyset ≼ ω \lor A = \emptyset)$
97	91 92 96	elrabd	$⊢ A \in V \to A \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}$
98		elssuni	$⊢ A \in \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \to A \subseteq ⋃ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}$
99	97 98	syl	$⊢ A \in V \to A \subseteq ⋃ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}$
100	8	a1i	$⊢ A \in V \to ⋃ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \subseteq A$
101	99 100	eqssd	$⊢ A \in V \to A = ⋃ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\}$
102		istopon	$⊢ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \in TopOn (A) \leftrightarrow (\{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \in Top \land A = ⋃ \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\})$
103	85 101 102	sylanbrc	$⊢ A \in V \to \{x \in 𝒫 A \| ((A ∖ x) ≼ ω \lor x = \emptyset)\} \in TopOn (A)$

Metamath Proof Explorer

Theorem cctop

Proof