mretopd

Description: A Moore collection which is closed under finite unions called topological; such a collection is the closed sets of a canonically associated topology. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	mretopd.m	$⊢ φ \to M \in Moore (B)$
	mretopd.z	$⊢ φ \to \emptyset \in M$
	mretopd.u	$⊢ (φ \land x \in M \land y \in M) \to x \cup y \in M$
	mretopd.j	$⊢ J = \{z \in 𝒫 B \| B ∖ z \in M\}$
Assertion	mretopd	$⊢ φ \to (J \in TopOn (B) \land M = Clsd (J))$

Proof

Step	Hyp	Ref	Expression
1		mretopd.m	$⊢ φ \to M \in Moore (B)$
2		mretopd.z	$⊢ φ \to \emptyset \in M$
3		mretopd.u	$⊢ (φ \land x \in M \land y \in M) \to x \cup y \in M$
4		mretopd.j	$⊢ J = \{z \in 𝒫 B \| B ∖ z \in M\}$
5		unieq	$⊢ a = \emptyset \to ⋃ a = ⋃ \emptyset$
6		uni0	$⊢ ⋃ \emptyset = \emptyset$
7	5 6	eqtrdi	$⊢ a = \emptyset \to ⋃ a = \emptyset$
8	7	eleq1d	$⊢ a = \emptyset \to (⋃ a \in J \leftrightarrow \emptyset \in J)$
9	4	ssrab3	$⊢ J \subseteq 𝒫 B$
10		sstr	$⊢ (a \subseteq J \land J \subseteq 𝒫 B) \to a \subseteq 𝒫 B$
11	9 10	mpan2	$⊢ a \subseteq J \to a \subseteq 𝒫 B$
12	11	adantl	$⊢ (φ \land a \subseteq J) \to a \subseteq 𝒫 B$
13		sspwuni	$⊢ a \subseteq 𝒫 B \leftrightarrow ⋃ a \subseteq B$
14	12 13	sylib	$⊢ (φ \land a \subseteq J) \to ⋃ a \subseteq B$
15		vuniex	$⊢ ⋃ a \in V$
16	15	elpw	$⊢ ⋃ a \in 𝒫 B \leftrightarrow ⋃ a \subseteq B$
17	14 16	sylibr	$⊢ (φ \land a \subseteq J) \to ⋃ a \in 𝒫 B$
18	17	adantr	$⊢ ((φ \land a \subseteq J) \land a \neq \emptyset) \to ⋃ a \in 𝒫 B$
19		uniiun	$⊢ ⋃ a = ⋃_{b \in a} b$
20	19	difeq2i	$⊢ B ∖ ⋃ a = B ∖ ⋃_{b \in a} b$
21		iindif2	$⊢ a \neq \emptyset \to ⋂_{b \in a} (B ∖ b) = B ∖ ⋃_{b \in a} b$
22	21	adantl	$⊢ ((φ \land a \subseteq J) \land a \neq \emptyset) \to ⋂_{b \in a} (B ∖ b) = B ∖ ⋃_{b \in a} b$
23	1	ad2antrr	$⊢ ((φ \land a \subseteq J) \land a \neq \emptyset) \to M \in Moore (B)$
24		simpr	$⊢ ((φ \land a \subseteq J) \land a \neq \emptyset) \to a \neq \emptyset$
25		difeq2	$⊢ z = b \to B ∖ z = B ∖ b$
26	25	eleq1d	$⊢ z = b \to (B ∖ z \in M \leftrightarrow B ∖ b \in M)$
27	26 4	elrab2	$⊢ b \in J \leftrightarrow (b \in 𝒫 B \land B ∖ b \in M)$
28	27	simprbi	$⊢ b \in J \to B ∖ b \in M$
29	28	rgen	$⊢ \forall b \in J B ∖ b \in M$
30		ssralv	$⊢ a \subseteq J \to (\forall b \in J B ∖ b \in M \to \forall b \in a B ∖ b \in M)$
31	30	adantl	$⊢ (φ \land a \subseteq J) \to (\forall b \in J B ∖ b \in M \to \forall b \in a B ∖ b \in M)$
32	29 31	mpi	$⊢ (φ \land a \subseteq J) \to \forall b \in a B ∖ b \in M$
33	32	adantr	$⊢ ((φ \land a \subseteq J) \land a \neq \emptyset) \to \forall b \in a B ∖ b \in M$
34		mreiincl	$⊢ (M \in Moore (B) \land a \neq \emptyset \land \forall b \in a B ∖ b \in M) \to ⋂_{b \in a} (B ∖ b) \in M$
35	23 24 33 34	syl3anc	$⊢ ((φ \land a \subseteq J) \land a \neq \emptyset) \to ⋂_{b \in a} (B ∖ b) \in M$
36	22 35	eqeltrrd	$⊢ ((φ \land a \subseteq J) \land a \neq \emptyset) \to B ∖ ⋃_{b \in a} b \in M$
37	20 36	eqeltrid	$⊢ ((φ \land a \subseteq J) \land a \neq \emptyset) \to B ∖ ⋃ a \in M$
38		difeq2	$⊢ z = ⋃ a \to B ∖ z = B ∖ ⋃ a$
39	38	eleq1d	$⊢ z = ⋃ a \to (B ∖ z \in M \leftrightarrow B ∖ ⋃ a \in M)$
40	39 4	elrab2	$⊢ ⋃ a \in J \leftrightarrow (⋃ a \in 𝒫 B \land B ∖ ⋃ a \in M)$
41	18 37 40	sylanbrc	$⊢ ((φ \land a \subseteq J) \land a \neq \emptyset) \to ⋃ a \in J$
42		0elpw	$⊢ \emptyset \in 𝒫 B$
43	42	a1i	$⊢ φ \to \emptyset \in 𝒫 B$
44		mre1cl	$⊢ M \in Moore (B) \to B \in M$
45	1 44	syl	$⊢ φ \to B \in M$
46		difeq2	$⊢ z = \emptyset \to B ∖ z = B ∖ \emptyset$
47		dif0	$⊢ B ∖ \emptyset = B$
48	46 47	eqtrdi	$⊢ z = \emptyset \to B ∖ z = B$
49	48	eleq1d	$⊢ z = \emptyset \to (B ∖ z \in M \leftrightarrow B \in M)$
50	49 4	elrab2	$⊢ \emptyset \in J \leftrightarrow (\emptyset \in 𝒫 B \land B \in M)$
51	43 45 50	sylanbrc	$⊢ φ \to \emptyset \in J$
52	51	adantr	$⊢ (φ \land a \subseteq J) \to \emptyset \in J$
53	8 41 52	pm2.61ne	$⊢ (φ \land a \subseteq J) \to ⋃ a \in J$
54	53	ex	$⊢ φ \to (a \subseteq J \to ⋃ a \in J)$
55	54	alrimiv	$⊢ φ \to \forall a (a \subseteq J \to ⋃ a \in J)$
56		inss1	$⊢ a \cap b \subseteq a$
57		difeq2	$⊢ z = a \to B ∖ z = B ∖ a$
58	57	eleq1d	$⊢ z = a \to (B ∖ z \in M \leftrightarrow B ∖ a \in M)$
59	58 4	elrab2	$⊢ a \in J \leftrightarrow (a \in 𝒫 B \land B ∖ a \in M)$
60	59	simplbi	$⊢ a \in J \to a \in 𝒫 B$
61	60	elpwid	$⊢ a \in J \to a \subseteq B$
62	61	ad2antrl	$⊢ (φ \land (a \in J \land b \in J)) \to a \subseteq B$
63	56 62	sstrid	$⊢ (φ \land (a \in J \land b \in J)) \to a \cap b \subseteq B$
64		vex	$⊢ a \in V$
65	64	inex1	$⊢ a \cap b \in V$
66	65	elpw	$⊢ a \cap b \in 𝒫 B \leftrightarrow a \cap b \subseteq B$
67	63 66	sylibr	$⊢ (φ \land (a \in J \land b \in J)) \to a \cap b \in 𝒫 B$
68		difindi	$⊢ B ∖ (a \cap b) = (B ∖ a) \cup (B ∖ b)$
69	59	simprbi	$⊢ a \in J \to B ∖ a \in M$
70	69	ad2antrl	$⊢ (φ \land (a \in J \land b \in J)) \to B ∖ a \in M$
71	28	ad2antll	$⊢ (φ \land (a \in J \land b \in J)) \to B ∖ b \in M$
72		simpl	$⊢ (φ \land (a \in J \land b \in J)) \to φ$
73		uneq1	$⊢ x = B ∖ a \to x \cup y = (B ∖ a) \cup y$
74	73	eleq1d	$⊢ x = B ∖ a \to (x \cup y \in M \leftrightarrow (B ∖ a) \cup y \in M)$
75	74	imbi2d	$⊢ x = B ∖ a \to ((φ \to x \cup y \in M) \leftrightarrow (φ \to (B ∖ a) \cup y \in M))$
76		uneq2	$⊢ y = B ∖ b \to (B ∖ a) \cup y = (B ∖ a) \cup (B ∖ b)$
77	76	eleq1d	$⊢ y = B ∖ b \to ((B ∖ a) \cup y \in M \leftrightarrow (B ∖ a) \cup (B ∖ b) \in M)$
78	77	imbi2d	$⊢ y = B ∖ b \to ((φ \to (B ∖ a) \cup y \in M) \leftrightarrow (φ \to (B ∖ a) \cup (B ∖ b) \in M))$
79	3	3expb	$⊢ (φ \land (x \in M \land y \in M)) \to x \cup y \in M$
80	79	expcom	$⊢ (x \in M \land y \in M) \to (φ \to x \cup y \in M)$
81	75 78 80	vtocl2ga	$⊢ (B ∖ a \in M \land B ∖ b \in M) \to (φ \to (B ∖ a) \cup (B ∖ b) \in M)$
82	81	imp	$⊢ ((B ∖ a \in M \land B ∖ b \in M) \land φ) \to (B ∖ a) \cup (B ∖ b) \in M$
83	70 71 72 82	syl21anc	$⊢ (φ \land (a \in J \land b \in J)) \to (B ∖ a) \cup (B ∖ b) \in M$
84	68 83	eqeltrid	$⊢ (φ \land (a \in J \land b \in J)) \to B ∖ (a \cap b) \in M$
85		difeq2	$⊢ z = a \cap b \to B ∖ z = B ∖ (a \cap b)$
86	85	eleq1d	$⊢ z = a \cap b \to (B ∖ z \in M \leftrightarrow B ∖ (a \cap b) \in M)$
87	86 4	elrab2	$⊢ a \cap b \in J \leftrightarrow (a \cap b \in 𝒫 B \land B ∖ (a \cap b) \in M)$
88	67 84 87	sylanbrc	$⊢ (φ \land (a \in J \land b \in J)) \to a \cap b \in J$
89	88	ralrimivva	$⊢ φ \to \forall a \in J \forall b \in J a \cap b \in J$
90	45	pwexd	$⊢ φ \to 𝒫 B \in V$
91	4 90	rabexd	$⊢ φ \to J \in V$
92		istopg	$⊢ J \in V \to (J \in Top \leftrightarrow (\forall a (a \subseteq J \to ⋃ a \in J) \land \forall a \in J \forall b \in J a \cap b \in J))$
93	91 92	syl	$⊢ φ \to (J \in Top \leftrightarrow (\forall a (a \subseteq J \to ⋃ a \in J) \land \forall a \in J \forall b \in J a \cap b \in J))$
94	55 89 93	mpbir2and	$⊢ φ \to J \in Top$
95	9	unissi	$⊢ ⋃ J \subseteq ⋃ 𝒫 B$
96		unipw	$⊢ ⋃ 𝒫 B = B$
97	95 96	sseqtri	$⊢ ⋃ J \subseteq B$
98		pwidg	$⊢ B \in M \to B \in 𝒫 B$
99	45 98	syl	$⊢ φ \to B \in 𝒫 B$
100		difid	$⊢ B ∖ B = \emptyset$
101	100 2	eqeltrid	$⊢ φ \to B ∖ B \in M$
102		difeq2	$⊢ z = B \to B ∖ z = B ∖ B$
103	102	eleq1d	$⊢ z = B \to (B ∖ z \in M \leftrightarrow B ∖ B \in M)$
104	103 4	elrab2	$⊢ B \in J \leftrightarrow (B \in 𝒫 B \land B ∖ B \in M)$
105	99 101 104	sylanbrc	$⊢ φ \to B \in J$
106		unissel	$⊢ (⋃ J \subseteq B \land B \in J) \to ⋃ J = B$
107	97 105 106	sylancr	$⊢ φ \to ⋃ J = B$
108	107	eqcomd	$⊢ φ \to B = ⋃ J$
109		istopon	$⊢ J \in TopOn (B) \leftrightarrow (J \in Top \land B = ⋃ J)$
110	94 108 109	sylanbrc	$⊢ φ \to J \in TopOn (B)$
111		eqid	$⊢ ⋃ J = ⋃ J$
112	111	cldval	$⊢ J \in Top \to Clsd (J) = \{x \in 𝒫 ⋃ J \| ⋃ J ∖ x \in J\}$
113	94 112	syl	$⊢ φ \to Clsd (J) = \{x \in 𝒫 ⋃ J \| ⋃ J ∖ x \in J\}$
114	107	pweqd	$⊢ φ \to 𝒫 ⋃ J = 𝒫 B$
115	107	difeq1d	$⊢ φ \to ⋃ J ∖ x = B ∖ x$
116	115	eleq1d	$⊢ φ \to (⋃ J ∖ x \in J \leftrightarrow B ∖ x \in J)$
117	114 116	rabeqbidv	$⊢ φ \to \{x \in 𝒫 ⋃ J \| ⋃ J ∖ x \in J\} = \{x \in 𝒫 B \| B ∖ x \in J\}$
118	4	eleq2i	$⊢ B ∖ x \in J \leftrightarrow B ∖ x \in \{z \in 𝒫 B \| B ∖ z \in M\}$
119		difss	$⊢ B ∖ x \subseteq B$
120		elpw2g	$⊢ B \in M \to (B ∖ x \in 𝒫 B \leftrightarrow B ∖ x \subseteq B)$
121	45 120	syl	$⊢ φ \to (B ∖ x \in 𝒫 B \leftrightarrow B ∖ x \subseteq B)$
122	119 121	mpbiri	$⊢ φ \to B ∖ x \in 𝒫 B$
123		difeq2	$⊢ z = B ∖ x \to B ∖ z = B ∖ (B ∖ x)$
124	123	eleq1d	$⊢ z = B ∖ x \to (B ∖ z \in M \leftrightarrow B ∖ (B ∖ x) \in M)$
125	124	elrab3	$⊢ B ∖ x \in 𝒫 B \to (B ∖ x \in \{z \in 𝒫 B \| B ∖ z \in M\} \leftrightarrow B ∖ (B ∖ x) \in M)$
126	122 125	syl	$⊢ φ \to (B ∖ x \in \{z \in 𝒫 B \| B ∖ z \in M\} \leftrightarrow B ∖ (B ∖ x) \in M)$
127	126	adantr	$⊢ (φ \land x \in 𝒫 B) \to (B ∖ x \in \{z \in 𝒫 B \| B ∖ z \in M\} \leftrightarrow B ∖ (B ∖ x) \in M)$
128	118 127	bitrid	$⊢ (φ \land x \in 𝒫 B) \to (B ∖ x \in J \leftrightarrow B ∖ (B ∖ x) \in M)$
129		elpwi	$⊢ x \in 𝒫 B \to x \subseteq B$
130		dfss4	$⊢ x \subseteq B \leftrightarrow B ∖ (B ∖ x) = x$
131	129 130	sylib	$⊢ x \in 𝒫 B \to B ∖ (B ∖ x) = x$
132	131	adantl	$⊢ (φ \land x \in 𝒫 B) \to B ∖ (B ∖ x) = x$
133	132	eleq1d	$⊢ (φ \land x \in 𝒫 B) \to (B ∖ (B ∖ x) \in M \leftrightarrow x \in M)$
134	128 133	bitrd	$⊢ (φ \land x \in 𝒫 B) \to (B ∖ x \in J \leftrightarrow x \in M)$
135	134	rabbidva	$⊢ φ \to \{x \in 𝒫 B \| B ∖ x \in J\} = \{x \in 𝒫 B \| x \in M\}$
136		incom	$⊢ M \cap 𝒫 B = 𝒫 B \cap M$
137		dfin5	$⊢ 𝒫 B \cap M = \{x \in 𝒫 B \| x \in M\}$
138	136 137	eqtri	$⊢ M \cap 𝒫 B = \{x \in 𝒫 B \| x \in M\}$
139		mresspw	$⊢ M \in Moore (B) \to M \subseteq 𝒫 B$
140	1 139	syl	$⊢ φ \to M \subseteq 𝒫 B$
141		dfss2	$⊢ M \subseteq 𝒫 B \leftrightarrow M \cap 𝒫 B = M$
142	140 141	sylib	$⊢ φ \to M \cap 𝒫 B = M$
143	138 142	eqtr3id	$⊢ φ \to \{x \in 𝒫 B \| x \in M\} = M$
144	135 143	eqtrd	$⊢ φ \to \{x \in 𝒫 B \| B ∖ x \in J\} = M$
145	113 117 144	3eqtrrd	$⊢ φ \to M = Clsd (J)$
146	110 145	jca	$⊢ φ \to (J \in TopOn (B) \land M = Clsd (J))$

Metamath Proof Explorer

Theorem mretopd

Proof