Theorem mretopd 20706

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 4380	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∪ ∅)
2		uni0 4401	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	syl6eq 2660	. . . . . . . 8 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∅)
4	3	eleq1d 2672	. . . . . . 7 ⊢ (𝑎 = ∅ → (∪ 𝑎 ∈ 𝐽 ↔ ∅ ∈ 𝐽))
5		mretopd.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀}
6		ssrab2 3650	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ⊆ 𝒫 𝐵
7	5, 6	eqsstri 3598	. . . . . . . . . . . . 13 ⊢ 𝐽 ⊆ 𝒫 𝐵
8		sstr 3576	. . . . . . . . . . . . 13 ⊢ ((𝑎 ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝐵) → 𝑎 ⊆ 𝒫 𝐵)
9	7, 8	mpan2 703	. . . . . . . . . . . 12 ⊢ (𝑎 ⊆ 𝐽 → 𝑎 ⊆ 𝒫 𝐵)
10	9	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → 𝑎 ⊆ 𝒫 𝐵)
11		sspwuni 4547	. . . . . . . . . . 11 ⊢ (𝑎 ⊆ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵)
12	10, 11	sylib 207	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ⊆ 𝐵)
13		vuniex 6852	. . . . . . . . . . 11 ⊢ ∪ 𝑎 ∈ V
14	13	elpw 4114	. . . . . . . . . 10 ⊢ (∪ 𝑎 ∈ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵)
15	12, 14	sylibr 223	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ∈ 𝒫 𝐵)
16	15	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∪ 𝑎 ∈ 𝒫 𝐵)
17		uniiun 4509	. . . . . . . . . 10 ⊢ ∪ 𝑎 = ∪ 𝑏 ∈ 𝑎 𝑏
18	17	difeq2i 3687	. . . . . . . . 9 ⊢ (𝐵 ∖ ∪ 𝑎) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏)
19		iindif2 4525	. . . . . . . . . . 11 ⊢ (𝑎 ≠ ∅ → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏))
20	19	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏))
21		mretopd.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (Moore‘𝐵))
22	21	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → 𝑀 ∈ (Moore‘𝐵))
23		simpr 476	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → 𝑎 ≠ ∅)
24		difeq2 3684	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑏 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑏))
25	24	eleq1d 2672	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑏 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝑏) ∈ 𝑀))
26	25, 5	elrab2 3333	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝐽 ↔ (𝑏 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀))
27	26	simprbi 479	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝐽 → (𝐵 ∖ 𝑏) ∈ 𝑀)
28	27	rgen 2906	. . . . . . . . . . . . 13 ⊢ ∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀
29		ssralv 3629	. . . . . . . . . . . . . 14 ⊢ (𝑎 ⊆ 𝐽 → (∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀 → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀))
30	29	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → (∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀 → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀))
31	28, 30	mpi 20	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
32	31	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
33		mreiincl 16079	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Moore‘𝐵) ∧ 𝑎 ≠ ∅ ∧ ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
34	22, 23, 32, 33	syl3anc 1318	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
35	20, 34	eqeltrrd 2689	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏) ∈ 𝑀)
36	18, 35	syl5eqel 2692	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 ∖ ∪ 𝑎) ∈ 𝑀)
37		difeq2 3684	. . . . . . . . . 10 ⊢ (𝑧 = ∪ 𝑎 → (𝐵 ∖ 𝑧) = (𝐵 ∖ ∪ 𝑎))
38	37	eleq1d 2672	. . . . . . . . 9 ⊢ (𝑧 = ∪ 𝑎 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ ∪ 𝑎) ∈ 𝑀))
39	38, 5	elrab2 3333	. . . . . . . 8 ⊢ (∪ 𝑎 ∈ 𝐽 ↔ (∪ 𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ ∪ 𝑎) ∈ 𝑀))
40	16, 36, 39	sylanbrc 695	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∪ 𝑎 ∈ 𝐽)
41		0elpw 4760	. . . . . . . . . 10 ⊢ ∅ ∈ 𝒫 𝐵
42	41	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ 𝒫 𝐵)
43		mre1cl 16077	. . . . . . . . . 10 ⊢ (𝑀 ∈ (Moore‘𝐵) → 𝐵 ∈ 𝑀)
44	21, 43	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ 𝑀)
45		difeq2 3684	. . . . . . . . . . . 12 ⊢ (𝑧 = ∅ → (𝐵 ∖ 𝑧) = (𝐵 ∖ ∅))
46		dif0 3904	. . . . . . . . . . . 12 ⊢ (𝐵 ∖ ∅) = 𝐵
47	45, 46	syl6eq 2660	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → (𝐵 ∖ 𝑧) = 𝐵)
48	47	eleq1d 2672	. . . . . . . . . 10 ⊢ (𝑧 = ∅ → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ 𝐵 ∈ 𝑀))
49	48, 5	elrab2 3333	. . . . . . . . 9 ⊢ (∅ ∈ 𝐽 ↔ (∅ ∈ 𝒫 𝐵 ∧ 𝐵 ∈ 𝑀))
50	42, 44, 49	sylanbrc 695	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐽)
51	50	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∅ ∈ 𝐽)
52	4, 40, 51	pm2.61ne 2867	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ∈ 𝐽)
53	52	ex 449	. . . . 5 ⊢ (𝜑 → (𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽))
54	53	alrimiv 1842	. . . 4 ⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽))
55		inss1 3795	. . . . . . . 8 ⊢ (𝑎 ∩ 𝑏) ⊆ 𝑎
56		difeq2 3684	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑎))
57	56	eleq1d 2672	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑎 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝑎) ∈ 𝑀))
58	57, 5	elrab2 3333	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐽 ↔ (𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝑎) ∈ 𝑀))
59	58	simplbi 475	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐽 → 𝑎 ∈ 𝒫 𝐵)
60	59	elpwid 4118	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐽 → 𝑎 ⊆ 𝐵)
61	60	ad2antrl 760	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → 𝑎 ⊆ 𝐵)
62	55, 61	syl5ss 3579	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ⊆ 𝐵)
63		vex 3176	. . . . . . . . 9 ⊢ 𝑎 ∈ V
64	63	inex1 4727	. . . . . . . 8 ⊢ (𝑎 ∩ 𝑏) ∈ V
65	64	elpw 4114	. . . . . . 7 ⊢ ((𝑎 ∩ 𝑏) ∈ 𝒫 𝐵 ↔ (𝑎 ∩ 𝑏) ⊆ 𝐵)
66	62, 65	sylibr 223	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ∈ 𝒫 𝐵)
67		difindi 3840	. . . . . . 7 ⊢ (𝐵 ∖ (𝑎 ∩ 𝑏)) = ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏))
68	58	simprbi 479	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐽 → (𝐵 ∖ 𝑎) ∈ 𝑀)
69	68	ad2antrl 760	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ 𝑎) ∈ 𝑀)
70	27	ad2antll 761	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ 𝑏) ∈ 𝑀)
71		simpl 472	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → 𝜑)
72		uneq1 3722	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → (𝑥 ∪ 𝑦) = ((𝐵 ∖ 𝑎) ∪ 𝑦))
73	72	eleq1d 2672	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → ((𝑥 ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀))
74	73	imbi2d 329	. . . . . . . . . 10 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → ((𝜑 → (𝑥 ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀)))
75		uneq2 3723	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → ((𝐵 ∖ 𝑎) ∪ 𝑦) = ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)))
76	75	eleq1d 2672	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → (((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀))
77	76	imbi2d 329	. . . . . . . . . 10 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → ((𝜑 → ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)))
78		mretopd.u	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝑥 ∪ 𝑦) ∈ 𝑀)
79	78	3expb 1258	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀)) → (𝑥 ∪ 𝑦) ∈ 𝑀)
80	79	expcom 450	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝜑 → (𝑥 ∪ 𝑦) ∈ 𝑀))
81	74, 77, 80	vtocl2ga 3247	. . . . . . . . 9 ⊢ (((𝐵 ∖ 𝑎) ∈ 𝑀 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀) → (𝜑 → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀))
82	81	imp 444	. . . . . . . 8 ⊢ ((((𝐵 ∖ 𝑎) ∈ 𝑀 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀) ∧ 𝜑) → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)
83	69, 70, 71, 82	syl21anc 1317	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)
84	67, 83	syl5eqel 2692	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀)
85		difeq2 3684	. . . . . . . 8 ⊢ (𝑧 = (𝑎 ∩ 𝑏) → (𝐵 ∖ 𝑧) = (𝐵 ∖ (𝑎 ∩ 𝑏)))
86	85	eleq1d 2672	. . . . . . 7 ⊢ (𝑧 = (𝑎 ∩ 𝑏) → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀))
87	86, 5	elrab2 3333	. . . . . 6 ⊢ ((𝑎 ∩ 𝑏) ∈ 𝐽 ↔ ((𝑎 ∩ 𝑏) ∈ 𝒫 𝐵 ∧ (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀))
88	66, 84, 87	sylanbrc 695	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ∈ 𝐽)
89	88	ralrimivva 2954	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)
90		pwexg 4776	. . . . . . 7 ⊢ (𝐵 ∈ 𝑀 → 𝒫 𝐵 ∈ V)
91	44, 90	syl 17	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
92	5, 91	rabexd 4741	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ V)
93		istopg 20525	. . . . 5 ⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽) ∧ ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)))
94	92, 93	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽) ∧ ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)))
95	54, 89, 94	mpbir2and 959	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
96	7	unissi 4397	. . . . . 6 ⊢ ∪ 𝐽 ⊆ ∪ 𝒫 𝐵
97		unipw 4845	. . . . . 6 ⊢ ∪ 𝒫 𝐵 = 𝐵
98	96, 97	sseqtri 3600	. . . . 5 ⊢ ∪ 𝐽 ⊆ 𝐵
99		pwidg 4121	. . . . . . 7 ⊢ (𝐵 ∈ 𝑀 → 𝐵 ∈ 𝒫 𝐵)
100	44, 99	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵)
101		difid 3902	. . . . . . 7 ⊢ (𝐵 ∖ 𝐵) = ∅
102		mretopd.z	. . . . . . 7 ⊢ (𝜑 → ∅ ∈ 𝑀)
103	101, 102	syl5eqel 2692	. . . . . 6 ⊢ (𝜑 → (𝐵 ∖ 𝐵) ∈ 𝑀)
104		difeq2 3684	. . . . . . . 8 ⊢ (𝑧 = 𝐵 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝐵))
105	104	eleq1d 2672	. . . . . . 7 ⊢ (𝑧 = 𝐵 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝐵) ∈ 𝑀))
106	105, 5	elrab2 3333	. . . . . 6 ⊢ (𝐵 ∈ 𝐽 ↔ (𝐵 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝐵) ∈ 𝑀))
107	100, 103, 106	sylanbrc 695	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝐽)
108		unissel 4404	. . . . 5 ⊢ ((∪ 𝐽 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐽) → ∪ 𝐽 = 𝐵)
109	98, 107, 108	sylancr 694	. . . 4 ⊢ (𝜑 → ∪ 𝐽 = 𝐵)
110	109	eqcomd 2616	. . 3 ⊢ (𝜑 → 𝐵 = ∪ 𝐽)
111		istopon 20540	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
112	95, 110, 111	sylanbrc 695	. 2 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵))
113		eqid 2610	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
114	113	cldval 20637	. . . 4 ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽})
115	95, 114	syl 17	. . 3 ⊢ (𝜑 → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽})
116	109	pweqd 4113	. . . 4 ⊢ (𝜑 → 𝒫 ∪ 𝐽 = 𝒫 𝐵)
117	109	difeq1d 3689	. . . . 5 ⊢ (𝜑 → (∪ 𝐽 ∖ 𝑥) = (𝐵 ∖ 𝑥))
118	117	eleq1d 2672	. . . 4 ⊢ (𝜑 → ((∪ 𝐽 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ 𝑥) ∈ 𝐽))
119	116, 118	rabeqbidv 3168	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽})
120	5	eleq2i 2680	. . . . . . 7 ⊢ ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀})
121		difss 3699	. . . . . . . . . 10 ⊢ (𝐵 ∖ 𝑥) ⊆ 𝐵
122		elpw2g 4754	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑀 → ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑥) ⊆ 𝐵))
123	44, 122	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑥) ⊆ 𝐵))
124	121, 123	mpbiri 247	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ 𝑥) ∈ 𝒫 𝐵)
125		difeq2 3684	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐵 ∖ 𝑥) → (𝐵 ∖ 𝑧) = (𝐵 ∖ (𝐵 ∖ 𝑥)))
126	125	eleq1d 2672	. . . . . . . . . 10 ⊢ (𝑧 = (𝐵 ∖ 𝑥) → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
127	126	elrab3 3332	. . . . . . . . 9 ⊢ ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
128	124, 127	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
129	128	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
130	120, 129	syl5bb 271	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
131		elpwi 4117	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵)
132		dfss4 3820	. . . . . . . . 9 ⊢ (𝑥 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
133	131, 132	sylib 207	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
134	133	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
135	134	eleq1d 2672	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀 ↔ 𝑥 ∈ 𝑀))
136	130, 135	bitrd 267	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ 𝑥 ∈ 𝑀))
137	136	rabbidva 3163	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀})
138		incom 3767	. . . . . 6 ⊢ (𝑀 ∩ 𝒫 𝐵) = (𝒫 𝐵 ∩ 𝑀)
139		dfin5 3548	. . . . . 6 ⊢ (𝒫 𝐵 ∩ 𝑀) = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀}
140	138, 139	eqtri 2632	. . . . 5 ⊢ (𝑀 ∩ 𝒫 𝐵) = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀}
141		mresspw 16075	. . . . . . 7 ⊢ (𝑀 ∈ (Moore‘𝐵) → 𝑀 ⊆ 𝒫 𝐵)
142	21, 141	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ⊆ 𝒫 𝐵)
143		df-ss 3554	. . . . . 6 ⊢ (𝑀 ⊆ 𝒫 𝐵 ↔ (𝑀 ∩ 𝒫 𝐵) = 𝑀)
144	142, 143	sylib 207	. . . . 5 ⊢ (𝜑 → (𝑀 ∩ 𝒫 𝐵) = 𝑀)
145	140, 144	syl5eqr 2658	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀} = 𝑀)
146	137, 145	eqtrd 2644	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽} = 𝑀)
147	115, 119, 146	3eqtrrd 2649	. 2 ⊢ (𝜑 → 𝑀 = (Clsd‘𝐽))
148	112, 147	jca 553	1 ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  ∪ cuni 4372  ∪ ciun 4455  ∩ ciin 4456  ‘cfv 5804  Moorecmre 16065  Topctop 20517  TopOnctopon 20518  Clsdccld 20630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-mre 16069  df-top 20521  df-topon 20523  df-cld 20633

This theorem is referenced by:  iscldtop  20709  istopclsd  36281