Theorem mretopd 23410

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.)

Hypotheses

Ref	Expression
mretopd.m	⊢ (𝜑 → 𝑀 ∈ (Moore‘𝐵))
mretopd.z	⊢ (𝜑 → ∅ ∈ 𝑀)
mretopd.u	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝑥 ∪ 𝑦) ∈ 𝑀)
mretopd.j	⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀}

Assertion

Ref	Expression
mretopd	⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽)))

Distinct variable groups:   𝜑,𝑥,𝑦,𝑧   𝑥,𝑀,𝑦,𝑧   𝑥,𝐽,𝑦   𝑥,𝐵,𝑦,𝑧

Allowed substitution hint:   𝐽(𝑧)

Proof of Theorem mretopd

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4878	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∪ ∅)
2		uni0 4896	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	eqtrdi 2812	. . . . . . . 8 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∅)
4	3	eleq1d 2846	. . . . . . 7 ⊢ (𝑎 = ∅ → (∪ 𝑎 ∈ 𝐽 ↔ ∅ ∈ 𝐽))
5		mretopd.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀}
6	5	ssrab3 4030	. . . . . . . . . . . . 13 ⊢ 𝐽 ⊆ 𝒫 𝐵
7		sstr 3939	. . . . . . . . . . . . 13 ⊢ ((𝑎 ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝐵) → 𝑎 ⊆ 𝒫 𝐵)
8	6, 7	mpan2 704	. . . . . . . . . . . 12 ⊢ (𝑎 ⊆ 𝐽 → 𝑎 ⊆ 𝒫 𝐵)
9	8	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → 𝑎 ⊆ 𝒫 𝐵)
10		sspwuni 5060	. . . . . . . . . . 11 ⊢ (𝑎 ⊆ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵)
11	9, 10	sylib 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ⊆ 𝐵)
12		vuniex 7756	. . . . . . . . . . 11 ⊢ ∪ 𝑎 ∈ V
13	12	elpw 4561	. . . . . . . . . 10 ⊢ (∪ 𝑎 ∈ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵)
14	11, 13	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ∈ 𝒫 𝐵)
15	14	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∪ 𝑎 ∈ 𝒫 𝐵)
16		uniiun 5017	. . . . . . . . . 10 ⊢ ∪ 𝑎 = ∪ 𝑏 ∈ 𝑎 𝑏
17	16	difeq2i 4071	. . . . . . . . 9 ⊢ (𝐵 ∖ ∪ 𝑎) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏)
18		iindif2 5037	. . . . . . . . . . 11 ⊢ (𝑎 ≠ ∅ → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏))
19	18	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏))
20		mretopd.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (Moore‘𝐵))
21	20	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → 𝑀 ∈ (Moore‘𝐵))
22		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → 𝑎 ≠ ∅)
23		difeq2 4068	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑏 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑏))
24	23	eleq1d 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑏 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝑏) ∈ 𝑀))
25	24, 5	elrab2 3649	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝐽 ↔ (𝑏 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀))
26	25	simprbi 503	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝐽 → (𝐵 ∖ 𝑏) ∈ 𝑀)
27	26	rgen 3079	. . . . . . . . . . . . 13 ⊢ ∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀
28		ssralv 4000	. . . . . . . . . . . . . 14 ⊢ (𝑎 ⊆ 𝐽 → (∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀 → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀))
29	28	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → (∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀 → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀))
30	27, 29	mpi 21	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
31	30	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
32		mreiincl 17766	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Moore‘𝐵) ∧ 𝑎 ≠ ∅ ∧ ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
33	21, 22, 31, 32	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
34	19, 33	eqeltrrd 2862	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏) ∈ 𝑀)
35	17, 34	eqeltrid 2865	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 ∖ ∪ 𝑎) ∈ 𝑀)
36		difeq2 4068	. . . . . . . . . 10 ⊢ (𝑧 = ∪ 𝑎 → (𝐵 ∖ 𝑧) = (𝐵 ∖ ∪ 𝑎))
37	36	eleq1d 2846	. . . . . . . . 9 ⊢ (𝑧 = ∪ 𝑎 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ ∪ 𝑎) ∈ 𝑀))
38	37, 5	elrab2 3649	. . . . . . . 8 ⊢ (∪ 𝑎 ∈ 𝐽 ↔ (∪ 𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ ∪ 𝑎) ∈ 𝑀))
39	15, 35, 38	sylanbrc 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∪ 𝑎 ∈ 𝐽)
40		0elpw 5317	. . . . . . . . . 10 ⊢ ∅ ∈ 𝒫 𝐵
41	40	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ 𝒫 𝐵)
42		mre1cl 17764	. . . . . . . . . 10 ⊢ (𝑀 ∈ (Moore‘𝐵) → 𝐵 ∈ 𝑀)
43	20, 42	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ 𝑀)
44		difeq2 4068	. . . . . . . . . . . 12 ⊢ (𝑧 = ∅ → (𝐵 ∖ 𝑧) = (𝐵 ∖ ∅))
45		dif0 4327	. . . . . . . . . . . 12 ⊢ (𝐵 ∖ ∅) = 𝐵
46	44, 45	eqtrdi 2812	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → (𝐵 ∖ 𝑧) = 𝐵)
47	46	eleq1d 2846	. . . . . . . . . 10 ⊢ (𝑧 = ∅ → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ 𝐵 ∈ 𝑀))
48	47, 5	elrab2 3649	. . . . . . . . 9 ⊢ (∅ ∈ 𝐽 ↔ (∅ ∈ 𝒫 𝐵 ∧ 𝐵 ∈ 𝑀))
49	41, 43, 48	sylanbrc 595	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐽)
50	49	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∅ ∈ 𝐽)
51	4, 39, 50	pm2.61ne 3041	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ∈ 𝐽)
52	51	ex 418	. . . . 5 ⊢ (𝜑 → (𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽))
53	52	alrimiv 1960	. . . 4 ⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽))
54		inss1 4182	. . . . . . . 8 ⊢ (𝑎 ∩ 𝑏) ⊆ 𝑎
55		difeq2 4068	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑎))
56	55	eleq1d 2846	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑎 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝑎) ∈ 𝑀))
57	56, 5	elrab2 3649	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐽 ↔ (𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝑎) ∈ 𝑀))
58	57	simplbi 502	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐽 → 𝑎 ∈ 𝒫 𝐵)
59	58	elpwid 4566	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐽 → 𝑎 ⊆ 𝐵)
60	59	ad2antrl 741	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → 𝑎 ⊆ 𝐵)
61	54, 60	sstrid 3942	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ⊆ 𝐵)
62		vex 3455	. . . . . . . . 9 ⊢ 𝑎 ∈ V
63	62	inex1 5277	. . . . . . . 8 ⊢ (𝑎 ∩ 𝑏) ∈ V
64	63	elpw 4561	. . . . . . 7 ⊢ ((𝑎 ∩ 𝑏) ∈ 𝒫 𝐵 ↔ (𝑎 ∩ 𝑏) ⊆ 𝐵)
65	61, 64	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ∈ 𝒫 𝐵)
66		difindi 4238	. . . . . . 7 ⊢ (𝐵 ∖ (𝑎 ∩ 𝑏)) = ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏))
67	57	simprbi 503	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐽 → (𝐵 ∖ 𝑎) ∈ 𝑀)
68	67	ad2antrl 741	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ 𝑎) ∈ 𝑀)
69	26	ad2antll 742	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ 𝑏) ∈ 𝑀)
70		simpl 488	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → 𝜑)
71		uneq1 4108	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → (𝑥 ∪ 𝑦) = ((𝐵 ∖ 𝑎) ∪ 𝑦))
72	71	eleq1d 2846	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → ((𝑥 ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀))
73	72	imbi2d 343	. . . . . . . . . 10 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → ((𝜑 → (𝑥 ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀)))
74		uneq2 4109	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → ((𝐵 ∖ 𝑎) ∪ 𝑦) = ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)))
75	74	eleq1d 2846	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → (((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀))
76	75	imbi2d 343	. . . . . . . . . 10 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → ((𝜑 → ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)))
77		mretopd.u	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝑥 ∪ 𝑦) ∈ 𝑀)
78	77	3expb 1138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀)) → (𝑥 ∪ 𝑦) ∈ 𝑀)
79	78	expcom 419	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝜑 → (𝑥 ∪ 𝑦) ∈ 𝑀))
80	73, 76, 79	vtocl2ga 3538	. . . . . . . . 9 ⊢ (((𝐵 ∖ 𝑎) ∈ 𝑀 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀) → (𝜑 → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀))
81	80	imp 412	. . . . . . . 8 ⊢ ((((𝐵 ∖ 𝑎) ∈ 𝑀 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀) ∧ 𝜑) → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)
82	68, 69, 70, 81	syl21anc 851	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)
83	66, 82	eqeltrid 2865	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀)
84		difeq2 4068	. . . . . . . 8 ⊢ (𝑧 = (𝑎 ∩ 𝑏) → (𝐵 ∖ 𝑧) = (𝐵 ∖ (𝑎 ∩ 𝑏)))
85	84	eleq1d 2846	. . . . . . 7 ⊢ (𝑧 = (𝑎 ∩ 𝑏) → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀))
86	85, 5	elrab2 3649	. . . . . 6 ⊢ ((𝑎 ∩ 𝑏) ∈ 𝐽 ↔ ((𝑎 ∩ 𝑏) ∈ 𝒫 𝐵 ∧ (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀))
87	65, 83, 86	sylanbrc 595	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ∈ 𝐽)
88	87	ralrimivva 3206	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)
89	43	pwexd 5341	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
90	5, 89	rabexd 5301	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ V)
91		istopg 23213	. . . . 5 ⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽) ∧ ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)))
92	90, 91	syl 18	. . . 4 ⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽) ∧ ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)))
93	53, 88, 92	mpbir2and 726	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
94	6	unissi 4876	. . . . . 6 ⊢ ∪ 𝐽 ⊆ ∪ 𝒫 𝐵
95		unipw 5418	. . . . . 6 ⊢ ∪ 𝒫 𝐵 = 𝐵
96	94, 95	sseqtri 3979	. . . . 5 ⊢ ∪ 𝐽 ⊆ 𝐵
97		pwidg 4577	. . . . . . 7 ⊢ (𝐵 ∈ 𝑀 → 𝐵 ∈ 𝒫 𝐵)
98	43, 97	syl 18	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵)
99		difid 4325	. . . . . . 7 ⊢ (𝐵 ∖ 𝐵) = ∅
100		mretopd.z	. . . . . . 7 ⊢ (𝜑 → ∅ ∈ 𝑀)
101	99, 100	eqeltrid 2865	. . . . . 6 ⊢ (𝜑 → (𝐵 ∖ 𝐵) ∈ 𝑀)
102		difeq2 4068	. . . . . . . 8 ⊢ (𝑧 = 𝐵 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝐵))
103	102	eleq1d 2846	. . . . . . 7 ⊢ (𝑧 = 𝐵 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝐵) ∈ 𝑀))
104	103, 5	elrab2 3649	. . . . . 6 ⊢ (𝐵 ∈ 𝐽 ↔ (𝐵 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝐵) ∈ 𝑀))
105	98, 101, 104	sylanbrc 595	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝐽)
106		unissel 4900	. . . . 5 ⊢ ((∪ 𝐽 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐽) → ∪ 𝐽 = 𝐵)
107	96, 105, 106	sylancr 599	. . . 4 ⊢ (𝜑 → ∪ 𝐽 = 𝐵)
108	107	eqcomd 2767	. . 3 ⊢ (𝜑 → 𝐵 = ∪ 𝐽)
109		istopon 23230	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
110	93, 108, 109	sylanbrc 595	. 2 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵))
111		eqid 2761	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
112	111	cldval 23341	. . . 4 ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽})
113	93, 112	syl 18	. . 3 ⊢ (𝜑 → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽})
114	107	pweqd 4574	. . . 4 ⊢ (𝜑 → 𝒫 ∪ 𝐽 = 𝒫 𝐵)
115	107	difeq1d 4073	. . . . 5 ⊢ (𝜑 → (∪ 𝐽 ∖ 𝑥) = (𝐵 ∖ 𝑥))
116	115	eleq1d 2846	. . . 4 ⊢ (𝜑 → ((∪ 𝐽 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ 𝑥) ∈ 𝐽))
117	114, 116	rabeqbidv 3430	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽})
118	5	eleq2i 2853	. . . . . . 7 ⊢ ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀})
119		difss 4083	. . . . . . . . . 10 ⊢ (𝐵 ∖ 𝑥) ⊆ 𝐵
120		elpw2g 5295	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑀 → ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑥) ⊆ 𝐵))
121	43, 120	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑥) ⊆ 𝐵))
122	119, 121	mpbiri 261	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ 𝑥) ∈ 𝒫 𝐵)
123		difeq2 4068	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐵 ∖ 𝑥) → (𝐵 ∖ 𝑧) = (𝐵 ∖ (𝐵 ∖ 𝑥)))
124	123	eleq1d 2846	. . . . . . . . . 10 ⊢ (𝑧 = (𝐵 ∖ 𝑥) → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
125	124	elrab3 3646	. . . . . . . . 9 ⊢ ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
126	122, 125	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
127	126	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
128	118, 127	bitrid 286	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
129		elpwi 4564	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵)
130		dfss4 4215	. . . . . . . . 9 ⊢ (𝑥 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
131	129, 130	sylib 221	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
132	131	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
133	132	eleq1d 2846	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀 ↔ 𝑥 ∈ 𝑀))
134	128, 133	bitrd 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ 𝑥 ∈ 𝑀))
135	134	rabbidva 3419	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀})
136		incom 4155	. . . . . 6 ⊢ (𝑀 ∩ 𝒫 𝐵) = (𝒫 𝐵 ∩ 𝑀)
137		dfin5 3907	. . . . . 6 ⊢ (𝒫 𝐵 ∩ 𝑀) = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀}
138	136, 137	eqtri 2784	. . . . 5 ⊢ (𝑀 ∩ 𝒫 𝐵) = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀}
139		mresspw 17762	. . . . . . 7 ⊢ (𝑀 ∈ (Moore‘𝐵) → 𝑀 ⊆ 𝒫 𝐵)
140	20, 139	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑀 ⊆ 𝒫 𝐵)
141		dfss2 3917	. . . . . 6 ⊢ (𝑀 ⊆ 𝒫 𝐵 ↔ (𝑀 ∩ 𝒫 𝐵) = 𝑀)
142	140, 141	sylib 221	. . . . 5 ⊢ (𝜑 → (𝑀 ∩ 𝒫 𝐵) = 𝑀)
143	138, 142	eqtr3id 2810	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀} = 𝑀)
144	135, 143	eqtrd 2796	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽} = 𝑀)
145	113, 117, 144	3eqtrrd 2801	. 2 ⊢ (𝜑 → 𝑀 = (Clsd‘𝐽))
146	110, 145	jca 521	1 ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  {crab 3413  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  ∪ cuni 4867  ∪ ciun 4951  ∩ ciin 4952  ‘cfv 6538  Moorecmre 17752  Topctop 23211  TopOnctopon 23228  Clsdccld 23334

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-mre 17756  df-top 23212  df-topon 23229  df-cld 23337

This theorem is used by:  iscldtop  23413  zartopn  34507  istopclsd  43710