fctop

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

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

Proof

Step	Hyp	Ref	Expression
1		difeq2	$⊢ x = ⋃ y \to A ∖ x = A ∖ ⋃ y$
2	1	eleq1d	$⊢ x = ⋃ y \to (A ∖ x \in Fin \leftrightarrow A ∖ ⋃ y \in Fin)$
3		eqeq1	$⊢ x = ⋃ y \to (x = \emptyset \leftrightarrow ⋃ y = \emptyset)$
4	2 3	orbi12d	$⊢ x = ⋃ y \to ((A ∖ x \in Fin \lor x = \emptyset) \leftrightarrow (A ∖ ⋃ y \in Fin \lor ⋃ y = \emptyset))$
5		uniss	$⊢ y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to ⋃ y \subseteq ⋃ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}$
6		ssrab2	$⊢ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \subseteq 𝒫 A$
7		sspwuni	$⊢ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \subseteq 𝒫 A \leftrightarrow ⋃ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \subseteq A$
8	6 7	mpbi	$⊢ ⋃ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \subseteq A$
9	5 8	sstrdi	$⊢ y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \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 \in Fin \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 \in Fin \lor x = \emptyset)\} \land z \in y) \to z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}$
18		difeq2	$⊢ x = z \to A ∖ x = A ∖ z$
19	18	eleq1d	$⊢ x = z \to (A ∖ x \in Fin \leftrightarrow A ∖ z \in Fin)$
20		eqeq1	$⊢ x = z \to (x = \emptyset \leftrightarrow z = \emptyset)$
21	19 20	orbi12d	$⊢ x = z \to ((A ∖ x \in Fin \lor x = \emptyset) \leftrightarrow (A ∖ z \in Fin \lor z = \emptyset))$
22	21	elrab	$⊢ z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \leftrightarrow (z \in 𝒫 A \land (A ∖ z \in Fin \lor z = \emptyset))$
23	17 22	sylib	$⊢ (y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \land z \in y) \to (z \in 𝒫 A \land (A ∖ z \in Fin \lor z = \emptyset))$
24	23	simprd	$⊢ (y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \land z \in y) \to (A ∖ z \in Fin \lor z = \emptyset)$
25	24	ord	$⊢ (y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \land z \in y) \to (\neg A ∖ z \in Fin \to z = \emptyset)$
26	25	con1d	$⊢ (y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \land z \in y) \to (\neg z = \emptyset \to A ∖ z \in Fin)$
27	26	imp	$⊢ ((y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \land z \in y) \land \neg z = \emptyset) \to A ∖ z \in Fin$
28		elssuni	$⊢ z \in y \to z \subseteq ⋃ y$
29	28	sscond	$⊢ z \in y \to A ∖ ⋃ y \subseteq A ∖ z$
30		ssfi	$⊢ (A ∖ z \in Fin \land A ∖ ⋃ y \subseteq A ∖ z) \to A ∖ ⋃ y \in Fin$
31	29 30	sylan2	$⊢ (A ∖ z \in Fin \land z \in y) \to A ∖ ⋃ y \in Fin$
32	31	expcom	$⊢ z \in y \to (A ∖ z \in Fin \to A ∖ ⋃ y \in Fin)$
33	32	ad2antlr	$⊢ ((y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \land z \in y) \land \neg z = \emptyset) \to (A ∖ z \in Fin \to A ∖ ⋃ y \in Fin)$
34	27 33	mpd	$⊢ ((y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \land z \in y) \land \neg z = \emptyset) \to A ∖ ⋃ y \in Fin$
35	34	rexlimdva2	$⊢ y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to (\exists z \in y \neg z = \emptyset \to A ∖ ⋃ y \in Fin)$
36	16 35	syl5bi	$⊢ y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to (\neg ⋃ y = \emptyset \to A ∖ ⋃ y \in Fin)$
37	36	con1d	$⊢ y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to (\neg A ∖ ⋃ y \in Fin \to ⋃ y = \emptyset)$
38	37	orrd	$⊢ y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to (A ∖ ⋃ y \in Fin \lor ⋃ y = \emptyset)$
39	4 12 38	elrabd	$⊢ y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to ⋃ y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}$
40	39	ax-gen	$⊢ \forall y (y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to ⋃ y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\})$
41		ssinss1	$⊢ y \subseteq A \to y \cap z \subseteq A$
42		vex	$⊢ y \in V$
43	42	elpw	$⊢ y \in 𝒫 A \leftrightarrow y \subseteq A$
44	42	inex1	$⊢ y \cap z \in V$
45	44	elpw	$⊢ y \cap z \in 𝒫 A \leftrightarrow y \cap z \subseteq A$
46	41 43 45	3imtr4i	$⊢ y \in 𝒫 A \to y \cap z \in 𝒫 A$
47	46	ad2antrr	$⊢ ((y \in 𝒫 A \land (A ∖ y \in Fin \lor y = \emptyset)) \land (z \in 𝒫 A \land (A ∖ z \in Fin \lor z = \emptyset))) \to y \cap z \in 𝒫 A$
48		difindi	$⊢ A ∖ (y \cap z) = (A ∖ y) \cup (A ∖ z)$
49		unfi	$⊢ (A ∖ y \in Fin \land A ∖ z \in Fin) \to (A ∖ y) \cup (A ∖ z) \in Fin$
50	48 49	eqeltrid	$⊢ (A ∖ y \in Fin \land A ∖ z \in Fin) \to A ∖ (y \cap z) \in Fin$
51	50	orcd	$⊢ (A ∖ y \in Fin \land A ∖ z \in Fin) \to (A ∖ (y \cap z) \in Fin \lor y \cap z = \emptyset)$
52		ineq1	$⊢ y = \emptyset \to y \cap z = \emptyset \cap z$
53		0in	$⊢ \emptyset \cap z = \emptyset$
54	52 53	eqtrdi	$⊢ y = \emptyset \to y \cap z = \emptyset$
55	54	olcd	$⊢ y = \emptyset \to (A ∖ (y \cap z) \in Fin \lor y \cap z = \emptyset)$
56		ineq2	$⊢ z = \emptyset \to y \cap z = y \cap \emptyset$
57		in0	$⊢ y \cap \emptyset = \emptyset$
58	56 57	eqtrdi	$⊢ z = \emptyset \to y \cap z = \emptyset$
59	58	olcd	$⊢ z = \emptyset \to (A ∖ (y \cap z) \in Fin \lor y \cap z = \emptyset)$
60	51 55 59	ccase2	$⊢ ((A ∖ y \in Fin \lor y = \emptyset) \land (A ∖ z \in Fin \lor z = \emptyset)) \to (A ∖ (y \cap z) \in Fin \lor y \cap z = \emptyset)$
61	60	ad2ant2l	$⊢ ((y \in 𝒫 A \land (A ∖ y \in Fin \lor y = \emptyset)) \land (z \in 𝒫 A \land (A ∖ z \in Fin \lor z = \emptyset))) \to (A ∖ (y \cap z) \in Fin \lor y \cap z = \emptyset)$
62	47 61	jca	$⊢ ((y \in 𝒫 A \land (A ∖ y \in Fin \lor y = \emptyset)) \land (z \in 𝒫 A \land (A ∖ z \in Fin \lor z = \emptyset))) \to (y \cap z \in 𝒫 A \land (A ∖ (y \cap z) \in Fin \lor y \cap z = \emptyset))$
63		difeq2	$⊢ x = y \to A ∖ x = A ∖ y$
64	63	eleq1d	$⊢ x = y \to (A ∖ x \in Fin \leftrightarrow A ∖ y \in Fin)$
65		eqeq1	$⊢ x = y \to (x = \emptyset \leftrightarrow y = \emptyset)$
66	64 65	orbi12d	$⊢ x = y \to ((A ∖ x \in Fin \lor x = \emptyset) \leftrightarrow (A ∖ y \in Fin \lor y = \emptyset))$
67	66	elrab	$⊢ y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \leftrightarrow (y \in 𝒫 A \land (A ∖ y \in Fin \lor y = \emptyset))$
68	67 22	anbi12i	$⊢ (y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \land z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}) \leftrightarrow ((y \in 𝒫 A \land (A ∖ y \in Fin \lor y = \emptyset)) \land (z \in 𝒫 A \land (A ∖ z \in Fin \lor z = \emptyset)))$
69		difeq2	$⊢ x = y \cap z \to A ∖ x = A ∖ (y \cap z)$
70	69	eleq1d	$⊢ x = y \cap z \to (A ∖ x \in Fin \leftrightarrow A ∖ (y \cap z) \in Fin)$
71		eqeq1	$⊢ x = y \cap z \to (x = \emptyset \leftrightarrow y \cap z = \emptyset)$
72	70 71	orbi12d	$⊢ x = y \cap z \to ((A ∖ x \in Fin \lor x = \emptyset) \leftrightarrow (A ∖ (y \cap z) \in Fin \lor y \cap z = \emptyset))$
73	72	elrab	$⊢ y \cap z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \leftrightarrow (y \cap z \in 𝒫 A \land (A ∖ (y \cap z) \in Fin \lor y \cap z = \emptyset))$
74	62 68 73	3imtr4i	$⊢ (y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \land z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}) \to y \cap z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}$
75	74	rgen2	$⊢ \forall y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \forall z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} y \cap z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}$
76	40 75	pm3.2i	$⊢ (\forall y (y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to ⋃ y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}) \land \forall y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \forall z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} y \cap z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\})$
77		pwexg	$⊢ A \in V \to 𝒫 A \in V$
78		rabexg	$⊢ 𝒫 A \in V \to \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \in V$
79		istopg	$⊢ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \in V \to (\{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \in Top \leftrightarrow (\forall y (y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to ⋃ y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}) \land \forall y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \forall z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} y \cap z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}))$
80	77 78 79	3syl	$⊢ A \in V \to (\{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \in Top \leftrightarrow (\forall y (y \subseteq \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to ⋃ y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}) \land \forall y \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \forall z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} y \cap z \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}))$
81	76 80	mpbiri	$⊢ A \in V \to \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \in Top$
82		difeq2	$⊢ x = A \to A ∖ x = A ∖ A$
83		difid	$⊢ A ∖ A = \emptyset$
84	82 83	eqtrdi	$⊢ x = A \to A ∖ x = \emptyset$
85	84	eleq1d	$⊢ x = A \to (A ∖ x \in Fin \leftrightarrow \emptyset \in Fin)$
86		eqeq1	$⊢ x = A \to (x = \emptyset \leftrightarrow A = \emptyset)$
87	85 86	orbi12d	$⊢ x = A \to ((A ∖ x \in Fin \lor x = \emptyset) \leftrightarrow (\emptyset \in Fin \lor A = \emptyset))$
88		pwidg	$⊢ A \in V \to A \in 𝒫 A$
89		0fin	$⊢ \emptyset \in Fin$
90	89	orci	$⊢ (\emptyset \in Fin \lor A = \emptyset)$
91	90	a1i	$⊢ A \in V \to (\emptyset \in Fin \lor A = \emptyset)$
92	87 88 91	elrabd	$⊢ A \in V \to A \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}$
93		elssuni	$⊢ A \in \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \to A \subseteq ⋃ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}$
94	92 93	syl	$⊢ A \in V \to A \subseteq ⋃ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}$
95	8	a1i	$⊢ A \in V \to ⋃ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \subseteq A$
96	94 95	eqssd	$⊢ A \in V \to A = ⋃ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\}$
97		istopon	$⊢ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \in TopOn (A) \leftrightarrow (\{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \in Top \land A = ⋃ \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\})$
98	81 96 97	sylanbrc	$⊢ A \in V \to \{x \in 𝒫 A \| (A ∖ x \in Fin \lor x = \emptyset)\} \in TopOn (A)$

Metamath Proof Explorer

Theorem fctop

Proof