Theorem mretopd 21699

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 4848	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∪ ∅)
2		uni0 4865	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
3	1, 2	syl6eq 2872	. . . . . . . 8 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∅)
4	3	eleq1d 2897	. . . . . . 7 ⊢ (𝑎 = ∅ → (∪ 𝑎 ∈ 𝐽 ↔ ∅ ∈ 𝐽))
5		mretopd.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀}
6	5	ssrab3 4056	. . . . . . . . . . . . 13 ⊢ 𝐽 ⊆ 𝒫 𝐵
7		sstr 3974	. . . . . . . . . . . . 13 ⊢ ((𝑎 ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝐵) → 𝑎 ⊆ 𝒫 𝐵)
8	6, 7	mpan2 689	. . . . . . . . . . . 12 ⊢ (𝑎 ⊆ 𝐽 → 𝑎 ⊆ 𝒫 𝐵)
9	8	adantl 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → 𝑎 ⊆ 𝒫 𝐵)
10		sspwuni 5021	. . . . . . . . . . 11 ⊢ (𝑎 ⊆ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵)
11	9, 10	sylib 220	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ⊆ 𝐵)
12		vuniex 7464	. . . . . . . . . . 11 ⊢ ∪ 𝑎 ∈ V
13	12	elpw 4542	. . . . . . . . . 10 ⊢ (∪ 𝑎 ∈ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵)
14	11, 13	sylibr 236	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ∈ 𝒫 𝐵)
15	14	adantr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∪ 𝑎 ∈ 𝒫 𝐵)
16		uniiun 4981	. . . . . . . . . 10 ⊢ ∪ 𝑎 = ∪ 𝑏 ∈ 𝑎 𝑏
17	16	difeq2i 4095	. . . . . . . . 9 ⊢ (𝐵 ∖ ∪ 𝑎) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏)
18		iindif2 4998	. . . . . . . . . . 11 ⊢ (𝑎 ≠ ∅ → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏))
19	18	adantl 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) = (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏))
20		mretopd.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (Moore‘𝐵))
21	20	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → 𝑀 ∈ (Moore‘𝐵))
22		simpr 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → 𝑎 ≠ ∅)
23		difeq2 4092	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑏 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑏))
24	23	eleq1d 2897	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑏 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝑏) ∈ 𝑀))
25	24, 5	elrab2 3682	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝐽 ↔ (𝑏 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀))
26	25	simprbi 499	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝐽 → (𝐵 ∖ 𝑏) ∈ 𝑀)
27	26	rgen 3148	. . . . . . . . . . . . 13 ⊢ ∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀
28		ssralv 4032	. . . . . . . . . . . . . 14 ⊢ (𝑎 ⊆ 𝐽 → (∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀 → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀))
29	28	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → (∀𝑏 ∈ 𝐽 (𝐵 ∖ 𝑏) ∈ 𝑀 → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀))
30	27, 29	mpi 20	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
31	30	adantr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
32		mreiincl 16866	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Moore‘𝐵) ∧ 𝑎 ≠ ∅ ∧ ∀𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
33	21, 22, 31, 32	syl3anc 1367	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∩ 𝑏 ∈ 𝑎 (𝐵 ∖ 𝑏) ∈ 𝑀)
34	19, 33	eqeltrrd 2914	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏) ∈ 𝑀)
35	17, 34	eqeltrid 2917	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 ∖ ∪ 𝑎) ∈ 𝑀)
36		difeq2 4092	. . . . . . . . . 10 ⊢ (𝑧 = ∪ 𝑎 → (𝐵 ∖ 𝑧) = (𝐵 ∖ ∪ 𝑎))
37	36	eleq1d 2897	. . . . . . . . 9 ⊢ (𝑧 = ∪ 𝑎 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ ∪ 𝑎) ∈ 𝑀))
38	37, 5	elrab2 3682	. . . . . . . 8 ⊢ (∪ 𝑎 ∈ 𝐽 ↔ (∪ 𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ ∪ 𝑎) ∈ 𝑀))
39	15, 35, 38	sylanbrc 585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑎 ≠ ∅) → ∪ 𝑎 ∈ 𝐽)
40		0elpw 5255	. . . . . . . . . 10 ⊢ ∅ ∈ 𝒫 𝐵
41	40	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ 𝒫 𝐵)
42		mre1cl 16864	. . . . . . . . . 10 ⊢ (𝑀 ∈ (Moore‘𝐵) → 𝐵 ∈ 𝑀)
43	20, 42	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ 𝑀)
44		difeq2 4092	. . . . . . . . . . . 12 ⊢ (𝑧 = ∅ → (𝐵 ∖ 𝑧) = (𝐵 ∖ ∅))
45		dif0 4331	. . . . . . . . . . . 12 ⊢ (𝐵 ∖ ∅) = 𝐵
46	44, 45	syl6eq 2872	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → (𝐵 ∖ 𝑧) = 𝐵)
47	46	eleq1d 2897	. . . . . . . . . 10 ⊢ (𝑧 = ∅ → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ 𝐵 ∈ 𝑀))
48	47, 5	elrab2 3682	. . . . . . . . 9 ⊢ (∅ ∈ 𝐽 ↔ (∅ ∈ 𝒫 𝐵 ∧ 𝐵 ∈ 𝑀))
49	41, 43, 48	sylanbrc 585	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐽)
50	49	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∅ ∈ 𝐽)
51	4, 39, 50	pm2.61ne 3102	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐽) → ∪ 𝑎 ∈ 𝐽)
52	51	ex 415	. . . . 5 ⊢ (𝜑 → (𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽))
53	52	alrimiv 1924	. . . 4 ⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽))
54		inss1 4204	. . . . . . . 8 ⊢ (𝑎 ∩ 𝑏) ⊆ 𝑎
55		difeq2 4092	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑎))
56	55	eleq1d 2897	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑎 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝑎) ∈ 𝑀))
57	56, 5	elrab2 3682	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐽 ↔ (𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝑎) ∈ 𝑀))
58	57	simplbi 500	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐽 → 𝑎 ∈ 𝒫 𝐵)
59	58	elpwid 4549	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐽 → 𝑎 ⊆ 𝐵)
60	59	ad2antrl 726	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → 𝑎 ⊆ 𝐵)
61	54, 60	sstrid 3977	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ⊆ 𝐵)
62		vex 3497	. . . . . . . . 9 ⊢ 𝑎 ∈ V
63	62	inex1 5220	. . . . . . . 8 ⊢ (𝑎 ∩ 𝑏) ∈ V
64	63	elpw 4542	. . . . . . 7 ⊢ ((𝑎 ∩ 𝑏) ∈ 𝒫 𝐵 ↔ (𝑎 ∩ 𝑏) ⊆ 𝐵)
65	61, 64	sylibr 236	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ∈ 𝒫 𝐵)
66		difindi 4257	. . . . . . 7 ⊢ (𝐵 ∖ (𝑎 ∩ 𝑏)) = ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏))
67	57	simprbi 499	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐽 → (𝐵 ∖ 𝑎) ∈ 𝑀)
68	67	ad2antrl 726	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ 𝑎) ∈ 𝑀)
69	26	ad2antll 727	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ 𝑏) ∈ 𝑀)
70		simpl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → 𝜑)
71		uneq1 4131	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → (𝑥 ∪ 𝑦) = ((𝐵 ∖ 𝑎) ∪ 𝑦))
72	71	eleq1d 2897	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → ((𝑥 ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀))
73	72	imbi2d 343	. . . . . . . . . 10 ⊢ (𝑥 = (𝐵 ∖ 𝑎) → ((𝜑 → (𝑥 ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀)))
74		uneq2 4132	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → ((𝐵 ∖ 𝑎) ∪ 𝑦) = ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)))
75	74	eleq1d 2897	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → (((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀))
76	75	imbi2d 343	. . . . . . . . . 10 ⊢ (𝑦 = (𝐵 ∖ 𝑏) → ((𝜑 → ((𝐵 ∖ 𝑎) ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)))
77		mretopd.u	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝑥 ∪ 𝑦) ∈ 𝑀)
78	77	3expb 1116	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀)) → (𝑥 ∪ 𝑦) ∈ 𝑀)
79	78	expcom 416	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝜑 → (𝑥 ∪ 𝑦) ∈ 𝑀))
80	73, 76, 79	vtocl2ga 3574	. . . . . . . . 9 ⊢ (((𝐵 ∖ 𝑎) ∈ 𝑀 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀) → (𝜑 → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀))
81	80	imp 409	. . . . . . . 8 ⊢ ((((𝐵 ∖ 𝑎) ∈ 𝑀 ∧ (𝐵 ∖ 𝑏) ∈ 𝑀) ∧ 𝜑) → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)
82	68, 69, 70, 81	syl21anc 835	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → ((𝐵 ∖ 𝑎) ∪ (𝐵 ∖ 𝑏)) ∈ 𝑀)
83	66, 82	eqeltrid 2917	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀)
84		difeq2 4092	. . . . . . . 8 ⊢ (𝑧 = (𝑎 ∩ 𝑏) → (𝐵 ∖ 𝑧) = (𝐵 ∖ (𝑎 ∩ 𝑏)))
85	84	eleq1d 2897	. . . . . . 7 ⊢ (𝑧 = (𝑎 ∩ 𝑏) → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀))
86	85, 5	elrab2 3682	. . . . . 6 ⊢ ((𝑎 ∩ 𝑏) ∈ 𝐽 ↔ ((𝑎 ∩ 𝑏) ∈ 𝒫 𝐵 ∧ (𝐵 ∖ (𝑎 ∩ 𝑏)) ∈ 𝑀))
87	65, 83, 86	sylanbrc 585	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽)) → (𝑎 ∩ 𝑏) ∈ 𝐽)
88	87	ralrimivva 3191	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)
89	43	pwexd 5279	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
90	5, 89	rabexd 5235	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ V)
91		istopg 21502	. . . . 5 ⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽) ∧ ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)))
92	90, 91	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑎(𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽) ∧ ∀𝑎 ∈ 𝐽 ∀𝑏 ∈ 𝐽 (𝑎 ∩ 𝑏) ∈ 𝐽)))
93	53, 88, 92	mpbir2and 711	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
94	6	unissi 4846	. . . . . 6 ⊢ ∪ 𝐽 ⊆ ∪ 𝒫 𝐵
95		unipw 5342	. . . . . 6 ⊢ ∪ 𝒫 𝐵 = 𝐵
96	94, 95	sseqtri 4002	. . . . 5 ⊢ ∪ 𝐽 ⊆ 𝐵
97		pwidg 4560	. . . . . . 7 ⊢ (𝐵 ∈ 𝑀 → 𝐵 ∈ 𝒫 𝐵)
98	43, 97	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵)
99		difid 4329	. . . . . . 7 ⊢ (𝐵 ∖ 𝐵) = ∅
100		mretopd.z	. . . . . . 7 ⊢ (𝜑 → ∅ ∈ 𝑀)
101	99, 100	eqeltrid 2917	. . . . . 6 ⊢ (𝜑 → (𝐵 ∖ 𝐵) ∈ 𝑀)
102		difeq2 4092	. . . . . . . 8 ⊢ (𝑧 = 𝐵 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝐵))
103	102	eleq1d 2897	. . . . . . 7 ⊢ (𝑧 = 𝐵 → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ 𝐵) ∈ 𝑀))
104	103, 5	elrab2 3682	. . . . . 6 ⊢ (𝐵 ∈ 𝐽 ↔ (𝐵 ∈ 𝒫 𝐵 ∧ (𝐵 ∖ 𝐵) ∈ 𝑀))
105	98, 101, 104	sylanbrc 585	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝐽)
106		unissel 4868	. . . . 5 ⊢ ((∪ 𝐽 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐽) → ∪ 𝐽 = 𝐵)
107	96, 105, 106	sylancr 589	. . . 4 ⊢ (𝜑 → ∪ 𝐽 = 𝐵)
108	107	eqcomd 2827	. . 3 ⊢ (𝜑 → 𝐵 = ∪ 𝐽)
109		istopon 21519	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
110	93, 108, 109	sylanbrc 585	. 2 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵))
111		eqid 2821	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
112	111	cldval 21630	. . . 4 ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽})
113	93, 112	syl 17	. . 3 ⊢ (𝜑 → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽})
114	107	pweqd 4557	. . . 4 ⊢ (𝜑 → 𝒫 ∪ 𝐽 = 𝒫 𝐵)
115	107	difeq1d 4097	. . . . 5 ⊢ (𝜑 → (∪ 𝐽 ∖ 𝑥) = (𝐵 ∖ 𝑥))
116	115	eleq1d 2897	. . . 4 ⊢ (𝜑 → ((∪ 𝐽 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ 𝑥) ∈ 𝐽))
117	114, 116	rabeqbidv 3485	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝒫 ∪ 𝐽 ∣ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽})
118	5	eleq2i 2904	. . . . . . 7 ⊢ ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀})
119		difss 4107	. . . . . . . . . 10 ⊢ (𝐵 ∖ 𝑥) ⊆ 𝐵
120		elpw2g 5246	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑀 → ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑥) ⊆ 𝐵))
121	43, 120	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑥) ⊆ 𝐵))
122	119, 121	mpbiri 260	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ 𝑥) ∈ 𝒫 𝐵)
123		difeq2 4092	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐵 ∖ 𝑥) → (𝐵 ∖ 𝑧) = (𝐵 ∖ (𝐵 ∖ 𝑥)))
124	123	eleq1d 2897	. . . . . . . . . 10 ⊢ (𝑧 = (𝐵 ∖ 𝑥) → ((𝐵 ∖ 𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
125	124	elrab3 3680	. . . . . . . . 9 ⊢ ((𝐵 ∖ 𝑥) ∈ 𝒫 𝐵 → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
126	122, 125	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
127	126	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
128	118, 127	syl5bb 285	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀))
129		elpwi 4547	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵)
130		dfss4 4234	. . . . . . . . 9 ⊢ (𝑥 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
131	129, 130	sylib 220	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
132	131	adantl 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑥)) = 𝑥)
133	132	eleq1d 2897	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐵 ∖ 𝑥)) ∈ 𝑀 ↔ 𝑥 ∈ 𝑀))
134	128, 133	bitrd 281	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑥) ∈ 𝐽 ↔ 𝑥 ∈ 𝑀))
135	134	rabbidva 3478	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀})
136		incom 4177	. . . . . 6 ⊢ (𝑀 ∩ 𝒫 𝐵) = (𝒫 𝐵 ∩ 𝑀)
137		dfin5 3943	. . . . . 6 ⊢ (𝒫 𝐵 ∩ 𝑀) = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀}
138	136, 137	eqtri 2844	. . . . 5 ⊢ (𝑀 ∩ 𝒫 𝐵) = {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀}
139		mresspw 16862	. . . . . . 7 ⊢ (𝑀 ∈ (Moore‘𝐵) → 𝑀 ⊆ 𝒫 𝐵)
140	20, 139	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ⊆ 𝒫 𝐵)
141		df-ss 3951	. . . . . 6 ⊢ (𝑀 ⊆ 𝒫 𝐵 ↔ (𝑀 ∩ 𝒫 𝐵) = 𝑀)
142	140, 141	sylib 220	. . . . 5 ⊢ (𝜑 → (𝑀 ∩ 𝒫 𝐵) = 𝑀)
143	138, 142	syl5eqr 2870	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀} = 𝑀)
144	135, 143	eqtrd 2856	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑥) ∈ 𝐽} = 𝑀)
145	113, 117, 144	3eqtrrd 2861	. 2 ⊢ (𝜑 → 𝑀 = (Clsd‘𝐽))
146	110, 145	jca 514	1 ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083  ∀wal 1531   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  {crab 3142  Vcvv 3494   ∖ cdif 3932   ∪ cun 3933   ∩ cin 3934   ⊆ wss 3935  ∅c0 4290  𝒫 cpw 4538  ∪ cuni 4837  ∪ ciun 4918  ∩ ciin 4919  ‘cfv 6354  Moorecmre 16852  Topctop 21500  TopOnctopon 21517  Clsdccld 21623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-int 4876  df-iun 4920  df-iin 4921  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-iota 6313  df-fun 6356  df-fv 6362  df-mre 16856  df-top 21501  df-topon 21518  df-cld 21626

This theorem is referenced by:  iscldtop  21702  istopclsd  39295