Theorem mretopd 20896

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 4444	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∪ ∅)
2		uni0 4465	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	syl6eq 2672	. . . . . . . 8 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∅)
4	3	eleq1d 2686	. . . . . . 7 ⊢ (𝑎 = ∅ → (∪ 𝑎 ∈ 𝐽 ↔ ∅ ∈ 𝐽))
5		mretopd.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀}
6		ssrab2 3687	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ⊆ 𝒫 𝐵
7	5, 6	eqsstri 3635	. . . . . . . . . . . . 13 ⊢ 𝐽 ⊆ 𝒫 𝐵
8		sstr 3611	. . . . . . . . . . . . 13 ⊢ ((𝑎 ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝐵) → 𝑎 ⊆ 𝒫 𝐵)
9	7, 8	mpan2 707	. . . . . . . . . . . 12 ⊢ (𝑎 ⊆ 𝐽 → 𝑎 ⊆ 𝒫 𝐵)
10	9	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → 𝑎 ⊆ 𝒫 𝐵)
11		sspwuni 4611	. . . . . . . . . . 11 ⊢ (𝑎 ⊆ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵)
12	10, 11	sylib 208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ⊆ 𝐵)
13		vuniex 6954	. . . . . . . . . . 11 ⊢ ∪ 𝑎 ∈ V
14	13	elpw 4164	. . . . . . . . . 10 ⊢ (∪ 𝑎 ∈ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵)
15	12, 14	sylibr 224	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ∈ 𝒫 𝐵)
16	15	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∪ 𝑎 ∈ 𝒫 𝐵)
17		uniiun 4573	. . . . . . . . . 10 ⊢ ∪ 𝑎 = ∪ 𝑏 ∈ 𝑎 𝑏
18	17	difeq2i 3725	. . . . . . . . 9 ⊢ (𝐵 ∖ ∪ 𝑎) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏)
19		iindif2 4589	. . . . . . . . . . 11 ⊢ (𝑎 ≠ ∅ → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏))
20	19	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏))
21		mretopd.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (Moore‘𝐵))
22	21	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → 𝑀 ∈ (Moore‘𝐵))
23		simpr 477	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → 𝑎 ≠ ∅)
24		difeq2 3722	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑏 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑏))
25	24	eleq1d 2686	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑏 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝑏) ∈ 𝑀))
26	25, 5	elrab2 3366	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝐽 ↔ (𝑏 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀))
27	26	simprbi 480	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝐽 → (𝐵 ∖ 𝑏) ∈ 𝑀)
28	27	rgen 2922	. . . . . . . . . . . . 13 ⊢ ∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀
29		ssralv 3666	. . . . . . . . . . . . . 14 ⊢ (𝑎 ⊆ 𝐽 → (∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀 → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀))
30	29	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → (∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀 → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀))
31	28, 30	mpi 20	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
32	31	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
33		mreiincl 16256	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Moore‘𝐵) ∧ 𝑎 ≠ ∅ ∧ ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
34	22, 23, 32, 33	syl3anc 1326	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
35	20, 34	eqeltrrd 2702	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏) ∈ 𝑀)
36	18, 35	syl5eqel 2705	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 ∖ ∪ 𝑎) ∈ 𝑀)
37		difeq2 3722	. . . . . . . . . 10 ⊢ (𝑧 = ∪ 𝑎 → (𝐵 ∖ 𝑧) = (𝐵 ∖ ∪ 𝑎))
38	37	eleq1d 2686	. . . . . . . . 9 ⊢ (𝑧 = ∪ 𝑎 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ ∪ 𝑎) ∈ 𝑀))
39	38, 5	elrab2 3366	. . . . . . . 8 ⊢ (∪ 𝑎 ∈ 𝐽 ↔ (∪ 𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ ∪ 𝑎) ∈ 𝑀))
40	16, 36, 39	sylanbrc 698	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∪ 𝑎 ∈ 𝐽)
41		0elpw 4834	. . . . . . . . . 10 ⊢ ∅ ∈ 𝒫 𝐵
42	41	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ 𝒫 𝐵)
43		mre1cl 16254	. . . . . . . . . 10 ⊢ (𝑀 ∈ (Moore‘𝐵) → 𝐵 ∈ 𝑀)
44	21, 43	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ 𝑀)
45		difeq2 3722	. . . . . . . . . . . 12 ⊢ (𝑧 = ∅ → (𝐵 ∖ 𝑧) = (𝐵 ∖ ∅))
46		dif0 3950	. . . . . . . . . . . 12 ⊢ (𝐵 ∖ ∅) = 𝐵
47	45, 46	syl6eq 2672	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → (𝐵 ∖ 𝑧) = 𝐵)
48	47	eleq1d 2686	. . . . . . . . . 10 ⊢ (𝑧 = ∅ → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ 𝐵 ∈ 𝑀))
49	48, 5	elrab2 3366	. . . . . . . . 9 ⊢ (∅ ∈ 𝐽 ↔ (∅ ∈ 𝒫 𝐵 ∧ 𝐵 ∈ 𝑀))
50	42, 44, 49	sylanbrc 698	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐽)
51	50	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∅ ∈ 𝐽)
52	4, 40, 51	pm2.61ne 2879	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ∈ 𝐽)
53	52	ex 450	. . . . 5 ⊢ (𝜑 → (𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽))
54	53	alrimiv 1855	. . . 4 ⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽))
55		inss1 3833	. . . . . . . 8 ⊢ (𝑎 ∩ 𝑏) ⊆ 𝑎
56		difeq2 3722	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑎))
57	56	eleq1d 2686	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑎 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝑎) ∈ 𝑀))
58	57, 5	elrab2 3366	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐽 ↔ (𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝑎) ∈ 𝑀))
59	58	simplbi 476	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐽 → 𝑎 ∈ 𝒫 𝐵)
60	59	elpwid 4170	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐽 → 𝑎 ⊆ 𝐵)
61	60	ad2antrl 764	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → 𝑎 ⊆ 𝐵)
62	55, 61	syl5ss 3614	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ⊆ 𝐵)
63		vex 3203	. . . . . . . . 9 ⊢ 𝑎 ∈ V
64	63	inex1 4799	. . . . . . . 8 ⊢ (𝑎 ∩ 𝑏) ∈ V
65	64	elpw 4164	. . . . . . 7 ⊢ ((𝑎 ∩ 𝑏) ∈ 𝒫 𝐵 ↔ (𝑎 ∩ 𝑏) ⊆ 𝐵)
66	62, 65	sylibr 224	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ∈ 𝒫 𝐵)
67		difindi 3881	. . . . . . 7 ⊢ (𝐵 ∖ (𝑎 ∩ 𝑏)) = ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏))
68	58	simprbi 480	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐽 → (𝐵 ∖ 𝑎) ∈ 𝑀)
69	68	ad2antrl 764	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ 𝑎) ∈ 𝑀)
70	27	ad2antll 765	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ 𝑏) ∈ 𝑀)
71		simpl 473	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → 𝜑)
72		uneq1 3760	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → (𝑥 ∪ 𝑦) = ((𝐵 ∖ 𝑎) ∪ 𝑦))
73	72	eleq1d 2686	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → ((𝑥 ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀))
74	73	imbi2d 330	. . . . . . . . . 10 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → ((𝜑 → (𝑥 ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀)))
75		uneq2 3761	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → ((𝐵 ∖ 𝑎) ∪ 𝑦) = ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)))
76	75	eleq1d 2686	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → (((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀))
77	76	imbi2d 330	. . . . . . . . . 10 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → ((𝜑 → ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)))
78		mretopd.u	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝑥 ∪ 𝑦) ∈ 𝑀)
79	78	3expb 1266	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀)) → (𝑥 ∪ 𝑦) ∈ 𝑀)
80	79	expcom 451	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝜑 → (𝑥 ∪ 𝑦) ∈ 𝑀))
81	74, 77, 80	vtocl2ga 3274	. . . . . . . . 9 ⊢ (((𝐵 ∖ 𝑎) ∈ 𝑀 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀) → (𝜑 → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀))
82	81	imp 445	. . . . . . . 8 ⊢ ((((𝐵 ∖ 𝑎) ∈ 𝑀 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀) ∧ 𝜑) → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)
83	69, 70, 71, 82	syl21anc 1325	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)
84	67, 83	syl5eqel 2705	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀)
85		difeq2 3722	. . . . . . . 8 ⊢ (𝑧 = (𝑎 ∩ 𝑏) → (𝐵 ∖ 𝑧) = (𝐵 ∖ (𝑎 ∩ 𝑏)))
86	85	eleq1d 2686	. . . . . . 7 ⊢ (𝑧 = (𝑎 ∩ 𝑏) → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀))
87	86, 5	elrab2 3366	. . . . . 6 ⊢ ((𝑎 ∩ 𝑏) ∈ 𝐽 ↔ ((𝑎 ∩ 𝑏) ∈ 𝒫 𝐵 ∧ (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀))
88	66, 84, 87	sylanbrc 698	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ∈ 𝐽)
89	88	ralrimivva 2971	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)
90		pwexg 4850	. . . . . . 7 ⊢ (𝐵 ∈ 𝑀 → 𝒫 𝐵 ∈ V)
91	44, 90	syl 17	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
92	5, 91	rabexd 4814	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ V)
93		istopg 20700	. . . . 5 ⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽) ∧ ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)))
94	92, 93	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽) ∧ ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)))
95	54, 89, 94	mpbir2and 957	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
96	7	unissi 4461	. . . . . 6 ⊢ ∪ 𝐽 ⊆ ∪ 𝒫 𝐵
97		unipw 4918	. . . . . 6 ⊢ ∪ 𝒫 𝐵 = 𝐵
98	96, 97	sseqtri 3637	. . . . 5 ⊢ ∪ 𝐽 ⊆ 𝐵
99		pwidg 4173	. . . . . . 7 ⊢ (𝐵 ∈ 𝑀 → 𝐵 ∈ 𝒫 𝐵)
100	44, 99	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵)
101		difid 3948	. . . . . . 7 ⊢ (𝐵 ∖ 𝐵) = ∅
102		mretopd.z	. . . . . . 7 ⊢ (𝜑 → ∅ ∈ 𝑀)
103	101, 102	syl5eqel 2705	. . . . . 6 ⊢ (𝜑 → (𝐵 ∖ 𝐵) ∈ 𝑀)
104		difeq2 3722	. . . . . . . 8 ⊢ (𝑧 = 𝐵 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝐵))
105	104	eleq1d 2686	. . . . . . 7 ⊢ (𝑧 = 𝐵 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝐵) ∈ 𝑀))
106	105, 5	elrab2 3366	. . . . . 6 ⊢ (𝐵 ∈ 𝐽 ↔ (𝐵 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝐵) ∈ 𝑀))
107	100, 103, 106	sylanbrc 698	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝐽)
108		unissel 4468	. . . . 5 ⊢ ((∪ 𝐽 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐽) → ∪ 𝐽 = 𝐵)
109	98, 107, 108	sylancr 695	. . . 4 ⊢ (𝜑 → ∪ 𝐽 = 𝐵)
110	109	eqcomd 2628	. . 3 ⊢ (𝜑 → 𝐵 = ∪ 𝐽)
111		istopon 20717	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
112	95, 110, 111	sylanbrc 698	. 2 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵))
113		eqid 2622	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
114	113	cldval 20827	. . . 4 ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽})
115	95, 114	syl 17	. . 3 ⊢ (𝜑 → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽})
116	109	pweqd 4163	. . . 4 ⊢ (𝜑 → 𝒫 ∪ 𝐽 = 𝒫 𝐵)
117	109	difeq1d 3727	. . . . 5 ⊢ (𝜑 → (∪ 𝐽 ∖ 𝑥) = (𝐵 ∖ 𝑥))
118	117	eleq1d 2686	. . . 4 ⊢ (𝜑 → ((∪ 𝐽 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ 𝑥) ∈ 𝐽))
119	116, 118	rabeqbidv 3195	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽})
120	5	eleq2i 2693	. . . . . . 7 ⊢ ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀})
121		difss 3737	. . . . . . . . . 10 ⊢ (𝐵 ∖ 𝑥) ⊆ 𝐵
122		elpw2g 4827	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑀 → ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑥) ⊆ 𝐵))
123	44, 122	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑥) ⊆ 𝐵))
124	121, 123	mpbiri 248	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ 𝑥) ∈ 𝒫 𝐵)
125		difeq2 3722	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐵 ∖ 𝑥) → (𝐵 ∖ 𝑧) = (𝐵 ∖ (𝐵 ∖ 𝑥)))
126	125	eleq1d 2686	. . . . . . . . . 10 ⊢ (𝑧 = (𝐵 ∖ 𝑥) → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
127	126	elrab3 3364	. . . . . . . . 9 ⊢ ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
128	124, 127	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
129	128	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
130	120, 129	syl5bb 272	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
131		elpwi 4168	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵)
132		dfss4 3858	. . . . . . . . 9 ⊢ (𝑥 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
133	131, 132	sylib 208	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
134	133	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
135	134	eleq1d 2686	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀 ↔ 𝑥 ∈ 𝑀))
136	130, 135	bitrd 268	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ 𝑥 ∈ 𝑀))
137	136	rabbidva 3188	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀})
138		incom 3805	. . . . . 6 ⊢ (𝑀 ∩ 𝒫 𝐵) = (𝒫 𝐵 ∩ 𝑀)
139		dfin5 3582	. . . . . 6 ⊢ (𝒫 𝐵 ∩ 𝑀) = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀}
140	138, 139	eqtri 2644	. . . . 5 ⊢ (𝑀 ∩ 𝒫 𝐵) = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀}
141		mresspw 16252	. . . . . . 7 ⊢ (𝑀 ∈ (Moore‘𝐵) → 𝑀 ⊆ 𝒫 𝐵)
142	21, 141	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ⊆ 𝒫 𝐵)
143		df-ss 3588	. . . . . 6 ⊢ (𝑀 ⊆ 𝒫 𝐵 ↔ (𝑀 ∩ 𝒫 𝐵) = 𝑀)
144	142, 143	sylib 208	. . . . 5 ⊢ (𝜑 → (𝑀 ∩ 𝒫 𝐵) = 𝑀)
145	140, 144	syl5eqr 2670	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀} = 𝑀)
146	137, 145	eqtrd 2656	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽} = 𝑀)
147	115, 119, 146	3eqtrrd 2661	. 2 ⊢ (𝜑 → 𝑀 = (Clsd‘𝐽))
148	112, 147	jca 554	1 ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037  ∀wal 1481   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  {crab 2916  Vcvv 3200   ∖ cdif 3571   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  𝒫 cpw 4158  ∪ cuni 4436  ∪ ciun 4520  ∩ ciin 4521  ‘cfv 5888  Moorecmre 16242  Topctop 20698  TopOnctopon 20715  Clsdccld 20820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-mre 16246  df-top 20699  df-topon 20716  df-cld 20823

This theorem is referenced by:  iscldtop  20899  istopclsd  37263