Theorem mretopd 22986

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 4885	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∪ ∅)
2		uni0 4902	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	eqtrdi 2781	. . . . . . . 8 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∅)
4	3	eleq1d 2814	. . . . . . 7 ⊢ (𝑎 = ∅ → (∪ 𝑎 ∈ 𝐽 ↔ ∅ ∈ 𝐽))
5		mretopd.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀}
6	5	ssrab3 4048	. . . . . . . . . . . . 13 ⊢ 𝐽 ⊆ 𝒫 𝐵
7		sstr 3958	. . . . . . . . . . . . 13 ⊢ ((𝑎 ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝐵) → 𝑎 ⊆ 𝒫 𝐵)
8	6, 7	mpan2 691	. . . . . . . . . . . 12 ⊢ (𝑎 ⊆ 𝐽 → 𝑎 ⊆ 𝒫 𝐵)
9	8	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → 𝑎 ⊆ 𝒫 𝐵)
10		sspwuni 5067	. . . . . . . . . . 11 ⊢ (𝑎 ⊆ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵)
11	9, 10	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ⊆ 𝐵)
12		vuniex 7718	. . . . . . . . . . 11 ⊢ ∪ 𝑎 ∈ V
13	12	elpw 4570	. . . . . . . . . 10 ⊢ (∪ 𝑎 ∈ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵)
14	11, 13	sylibr 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ∈ 𝒫 𝐵)
15	14	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∪ 𝑎 ∈ 𝒫 𝐵)
16		uniiun 5025	. . . . . . . . . 10 ⊢ ∪ 𝑎 = ∪ 𝑏 ∈ 𝑎 𝑏
17	16	difeq2i 4089	. . . . . . . . 9 ⊢ (𝐵 ∖ ∪ 𝑎) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏)
18		iindif2 5044	. . . . . . . . . . 11 ⊢ (𝑎 ≠ ∅ → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏))
19	18	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏))
20		mretopd.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (Moore‘𝐵))
21	20	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → 𝑀 ∈ (Moore‘𝐵))
22		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → 𝑎 ≠ ∅)
23		difeq2 4086	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑏 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑏))
24	23	eleq1d 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑏 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝑏) ∈ 𝑀))
25	24, 5	elrab2 3665	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝐽 ↔ (𝑏 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀))
26	25	simprbi 496	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝐽 → (𝐵 ∖ 𝑏) ∈ 𝑀)
27	26	rgen 3047	. . . . . . . . . . . . 13 ⊢ ∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀
28		ssralv 4018	. . . . . . . . . . . . . 14 ⊢ (𝑎 ⊆ 𝐽 → (∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀 → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀))
29	28	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → (∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀 → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀))
30	27, 29	mpi 20	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
31	30	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
32		mreiincl 17564	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Moore‘𝐵) ∧ 𝑎 ≠ ∅ ∧ ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
33	21, 22, 31, 32	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
34	19, 33	eqeltrrd 2830	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏) ∈ 𝑀)
35	17, 34	eqeltrid 2833	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 ∖ ∪ 𝑎) ∈ 𝑀)
36		difeq2 4086	. . . . . . . . . 10 ⊢ (𝑧 = ∪ 𝑎 → (𝐵 ∖ 𝑧) = (𝐵 ∖ ∪ 𝑎))
37	36	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑧 = ∪ 𝑎 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ ∪ 𝑎) ∈ 𝑀))
38	37, 5	elrab2 3665	. . . . . . . 8 ⊢ (∪ 𝑎 ∈ 𝐽 ↔ (∪ 𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ ∪ 𝑎) ∈ 𝑀))
39	15, 35, 38	sylanbrc 583	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∪ 𝑎 ∈ 𝐽)
40		0elpw 5314	. . . . . . . . . 10 ⊢ ∅ ∈ 𝒫 𝐵
41	40	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ 𝒫 𝐵)
42		mre1cl 17562	. . . . . . . . . 10 ⊢ (𝑀 ∈ (Moore‘𝐵) → 𝐵 ∈ 𝑀)
43	20, 42	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ 𝑀)
44		difeq2 4086	. . . . . . . . . . . 12 ⊢ (𝑧 = ∅ → (𝐵 ∖ 𝑧) = (𝐵 ∖ ∅))
45		dif0 4344	. . . . . . . . . . . 12 ⊢ (𝐵 ∖ ∅) = 𝐵
46	44, 45	eqtrdi 2781	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → (𝐵 ∖ 𝑧) = 𝐵)
47	46	eleq1d 2814	. . . . . . . . . 10 ⊢ (𝑧 = ∅ → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ 𝐵 ∈ 𝑀))
48	47, 5	elrab2 3665	. . . . . . . . 9 ⊢ (∅ ∈ 𝐽 ↔ (∅ ∈ 𝒫 𝐵 ∧ 𝐵 ∈ 𝑀))
49	41, 43, 48	sylanbrc 583	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐽)
50	49	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∅ ∈ 𝐽)
51	4, 39, 50	pm2.61ne 3011	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ∈ 𝐽)
52	51	ex 412	. . . . 5 ⊢ (𝜑 → (𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽))
53	52	alrimiv 1927	. . . 4 ⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽))
54		inss1 4203	. . . . . . . 8 ⊢ (𝑎 ∩ 𝑏) ⊆ 𝑎
55		difeq2 4086	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑎))
56	55	eleq1d 2814	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑎 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝑎) ∈ 𝑀))
57	56, 5	elrab2 3665	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐽 ↔ (𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝑎) ∈ 𝑀))
58	57	simplbi 497	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐽 → 𝑎 ∈ 𝒫 𝐵)
59	58	elpwid 4575	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐽 → 𝑎 ⊆ 𝐵)
60	59	ad2antrl 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → 𝑎 ⊆ 𝐵)
61	54, 60	sstrid 3961	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ⊆ 𝐵)
62		vex 3454	. . . . . . . . 9 ⊢ 𝑎 ∈ V
63	62	inex1 5275	. . . . . . . 8 ⊢ (𝑎 ∩ 𝑏) ∈ V
64	63	elpw 4570	. . . . . . 7 ⊢ ((𝑎 ∩ 𝑏) ∈ 𝒫 𝐵 ↔ (𝑎 ∩ 𝑏) ⊆ 𝐵)
65	61, 64	sylibr 234	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ∈ 𝒫 𝐵)
66		difindi 4258	. . . . . . 7 ⊢ (𝐵 ∖ (𝑎 ∩ 𝑏)) = ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏))
67	57	simprbi 496	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐽 → (𝐵 ∖ 𝑎) ∈ 𝑀)
68	67	ad2antrl 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ 𝑎) ∈ 𝑀)
69	26	ad2antll 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ 𝑏) ∈ 𝑀)
70		simpl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → 𝜑)
71		uneq1 4127	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → (𝑥 ∪ 𝑦) = ((𝐵 ∖ 𝑎) ∪ 𝑦))
72	71	eleq1d 2814	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → ((𝑥 ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀))
73	72	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → ((𝜑 → (𝑥 ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀)))
74		uneq2 4128	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → ((𝐵 ∖ 𝑎) ∪ 𝑦) = ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)))
75	74	eleq1d 2814	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → (((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀))
76	75	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → ((𝜑 → ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)))
77		mretopd.u	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝑥 ∪ 𝑦) ∈ 𝑀)
78	77	3expb 1120	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀)) → (𝑥 ∪ 𝑦) ∈ 𝑀)
79	78	expcom 413	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝜑 → (𝑥 ∪ 𝑦) ∈ 𝑀))
80	73, 76, 79	vtocl2ga 3547	. . . . . . . . 9 ⊢ (((𝐵 ∖ 𝑎) ∈ 𝑀 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀) → (𝜑 → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀))
81	80	imp 406	. . . . . . . 8 ⊢ ((((𝐵 ∖ 𝑎) ∈ 𝑀 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀) ∧ 𝜑) → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)
82	68, 69, 70, 81	syl21anc 837	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)
83	66, 82	eqeltrid 2833	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀)
84		difeq2 4086	. . . . . . . 8 ⊢ (𝑧 = (𝑎 ∩ 𝑏) → (𝐵 ∖ 𝑧) = (𝐵 ∖ (𝑎 ∩ 𝑏)))
85	84	eleq1d 2814	. . . . . . 7 ⊢ (𝑧 = (𝑎 ∩ 𝑏) → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀))
86	85, 5	elrab2 3665	. . . . . 6 ⊢ ((𝑎 ∩ 𝑏) ∈ 𝐽 ↔ ((𝑎 ∩ 𝑏) ∈ 𝒫 𝐵 ∧ (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀))
87	65, 83, 86	sylanbrc 583	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ∈ 𝐽)
88	87	ralrimivva 3181	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)
89	43	pwexd 5337	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
90	5, 89	rabexd 5298	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ V)
91		istopg 22789	. . . . 5 ⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽) ∧ ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)))
92	90, 91	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽) ∧ ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)))
93	53, 88, 92	mpbir2and 713	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
94	6	unissi 4883	. . . . . 6 ⊢ ∪ 𝐽 ⊆ ∪ 𝒫 𝐵
95		unipw 5413	. . . . . 6 ⊢ ∪ 𝒫 𝐵 = 𝐵
96	94, 95	sseqtri 3998	. . . . 5 ⊢ ∪ 𝐽 ⊆ 𝐵
97		pwidg 4586	. . . . . . 7 ⊢ (𝐵 ∈ 𝑀 → 𝐵 ∈ 𝒫 𝐵)
98	43, 97	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵)
99		difid 4342	. . . . . . 7 ⊢ (𝐵 ∖ 𝐵) = ∅
100		mretopd.z	. . . . . . 7 ⊢ (𝜑 → ∅ ∈ 𝑀)
101	99, 100	eqeltrid 2833	. . . . . 6 ⊢ (𝜑 → (𝐵 ∖ 𝐵) ∈ 𝑀)
102		difeq2 4086	. . . . . . . 8 ⊢ (𝑧 = 𝐵 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝐵))
103	102	eleq1d 2814	. . . . . . 7 ⊢ (𝑧 = 𝐵 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝐵) ∈ 𝑀))
104	103, 5	elrab2 3665	. . . . . 6 ⊢ (𝐵 ∈ 𝐽 ↔ (𝐵 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝐵) ∈ 𝑀))
105	98, 101, 104	sylanbrc 583	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝐽)
106		unissel 4905	. . . . 5 ⊢ ((∪ 𝐽 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐽) → ∪ 𝐽 = 𝐵)
107	96, 105, 106	sylancr 587	. . . 4 ⊢ (𝜑 → ∪ 𝐽 = 𝐵)
108	107	eqcomd 2736	. . 3 ⊢ (𝜑 → 𝐵 = ∪ 𝐽)
109		istopon 22806	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
110	93, 108, 109	sylanbrc 583	. 2 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵))
111		eqid 2730	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
112	111	cldval 22917	. . . 4 ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽})
113	93, 112	syl 17	. . 3 ⊢ (𝜑 → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽})
114	107	pweqd 4583	. . . 4 ⊢ (𝜑 → 𝒫 ∪ 𝐽 = 𝒫 𝐵)
115	107	difeq1d 4091	. . . . 5 ⊢ (𝜑 → (∪ 𝐽 ∖ 𝑥) = (𝐵 ∖ 𝑥))
116	115	eleq1d 2814	. . . 4 ⊢ (𝜑 → ((∪ 𝐽 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ 𝑥) ∈ 𝐽))
117	114, 116	rabeqbidv 3427	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽})
118	5	eleq2i 2821	. . . . . . 7 ⊢ ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀})
119		difss 4102	. . . . . . . . . 10 ⊢ (𝐵 ∖ 𝑥) ⊆ 𝐵
120		elpw2g 5291	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑀 → ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑥) ⊆ 𝐵))
121	43, 120	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑥) ⊆ 𝐵))
122	119, 121	mpbiri 258	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ 𝑥) ∈ 𝒫 𝐵)
123		difeq2 4086	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐵 ∖ 𝑥) → (𝐵 ∖ 𝑧) = (𝐵 ∖ (𝐵 ∖ 𝑥)))
124	123	eleq1d 2814	. . . . . . . . . 10 ⊢ (𝑧 = (𝐵 ∖ 𝑥) → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
125	124	elrab3 3663	. . . . . . . . 9 ⊢ ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
126	122, 125	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
127	126	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
128	118, 127	bitrid 283	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
129		elpwi 4573	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵)
130		dfss4 4235	. . . . . . . . 9 ⊢ (𝑥 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
131	129, 130	sylib 218	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
132	131	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
133	132	eleq1d 2814	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀 ↔ 𝑥 ∈ 𝑀))
134	128, 133	bitrd 279	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ 𝑥 ∈ 𝑀))
135	134	rabbidva 3415	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀})
136		incom 4175	. . . . . 6 ⊢ (𝑀 ∩ 𝒫 𝐵) = (𝒫 𝐵 ∩ 𝑀)
137		dfin5 3925	. . . . . 6 ⊢ (𝒫 𝐵 ∩ 𝑀) = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀}
138	136, 137	eqtri 2753	. . . . 5 ⊢ (𝑀 ∩ 𝒫 𝐵) = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀}
139		mresspw 17560	. . . . . . 7 ⊢ (𝑀 ∈ (Moore‘𝐵) → 𝑀 ⊆ 𝒫 𝐵)
140	20, 139	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ⊆ 𝒫 𝐵)
141		dfss2 3935	. . . . . 6 ⊢ (𝑀 ⊆ 𝒫 𝐵 ↔ (𝑀 ∩ 𝒫 𝐵) = 𝑀)
142	140, 141	sylib 218	. . . . 5 ⊢ (𝜑 → (𝑀 ∩ 𝒫 𝐵) = 𝑀)
143	138, 142	eqtr3id 2779	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀} = 𝑀)
144	135, 143	eqtrd 2765	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽} = 𝑀)
145	113, 117, 144	3eqtrrd 2770	. 2 ⊢ (𝜑 → 𝑀 = (Clsd‘𝐽))
146	110, 145	jca 511	1 ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  {crab 3408  Vcvv 3450   ∖ cdif 3914   ∪ cun 3915   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299  𝒫 cpw 4566  ∪ cuni 4874  ∪ ciun 4958  ∩ ciin 4959  ‘cfv 6514  Moorecmre 17550  Topctop 22787  TopOnctopon 22804  Clsdccld 22910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-iin 4961  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-mre 17554  df-top 22788  df-topon 22805  df-cld 22913

This theorem is referenced by:  iscldtop  22989  zartopn  33872  istopclsd  42695