Theorem mretopd

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)

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

Proof

Step	Hyp	Ref	Expression
1		mretopd.m	⊢ ( 𝜑 → 𝑀 ∈ ( Moore ‘ 𝐵 ) )
2		mretopd.z	⊢ ( 𝜑 → ∅ ∈ 𝑀 )
3		mretopd.u	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 )
4		mretopd.j	⊢ 𝐽 = { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 }
5		unieq	⊢ ( 𝑎 = ∅ → ∪ 𝑎 = ∪ ∅ )
6		uni0	⊢ ∪ ∅ = ∅
7	5 6	eqtrdi	⊢ ( 𝑎 = ∅ → ∪ 𝑎 = ∅ )
8	7	eleq1d	⊢ ( 𝑎 = ∅ → ( ∪ 𝑎 ∈ 𝐽 ↔ ∅ ∈ 𝐽 ) )
9	4	ssrab3	⊢ 𝐽 ⊆ 𝒫 𝐵
10		sstr	⊢ ( ( 𝑎 ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝐵 ) → 𝑎 ⊆ 𝒫 𝐵 )
11	9 10	mpan2	⊢ ( 𝑎 ⊆ 𝐽 → 𝑎 ⊆ 𝒫 𝐵 )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → 𝑎 ⊆ 𝒫 𝐵 )
13		sspwuni	⊢ ( 𝑎 ⊆ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵 )
14	12 13	sylib	⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ∪ 𝑎 ⊆ 𝐵 )
15		vuniex	⊢ ∪ 𝑎 ∈ V
16	15	elpw	⊢ ( ∪ 𝑎 ∈ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵 )
17	14 16	sylibr	⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ∪ 𝑎 ∈ 𝒫 𝐵 )
18	17	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ∪ 𝑎 ∈ 𝒫 𝐵 )
19		uniiun	⊢ ∪ 𝑎 = ∪ 𝑏 ∈ 𝑎 𝑏
20	19	difeq2i	⊢ ( 𝐵 ∖ ∪ 𝑎 ) = ( 𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏 )
21		iindif2	⊢ ( 𝑎 ≠ ∅ → ∩ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) = ( 𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏 ) )
22	21	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ∩ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) = ( 𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏 ) )
23	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → 𝑀 ∈ ( Moore ‘ 𝐵 ) )
24		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → 𝑎 ≠ ∅ )
25		difeq2	⊢ ( 𝑧 = 𝑏 → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ 𝑏 ) )
26	25	eleq1d	⊢ ( 𝑧 = 𝑏 → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) )
27	26 4	elrab2	⊢ ( 𝑏 ∈ 𝐽 ↔ ( 𝑏 ∈ 𝒫 𝐵 ∧ ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) )
28	27	simprbi	⊢ ( 𝑏 ∈ 𝐽 → ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
29	28	rgen	⊢ ∀ 𝑏 ∈ 𝐽 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀
30		ssralv	⊢ ( 𝑎 ⊆ 𝐽 → ( ∀ 𝑏 ∈ 𝐽 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 → ∀ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) )
31	30	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ( ∀ 𝑏 ∈ 𝐽 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 → ∀ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) )
32	29 31	mpi	⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ∀ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
33	32	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ∀ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
34		mreiincl	⊢ ( ( 𝑀 ∈ ( Moore ‘ 𝐵 ) ∧ 𝑎 ≠ ∅ ∧ ∀ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) → ∩ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
35	23 24 33 34	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ∩ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
36	22 35	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ( 𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏 ) ∈ 𝑀 )
37	20 36	eqeltrid	⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ( 𝐵 ∖ ∪ 𝑎 ) ∈ 𝑀 )
38		difeq2	⊢ ( 𝑧 = ∪ 𝑎 → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ ∪ 𝑎 ) )
39	38	eleq1d	⊢ ( 𝑧 = ∪ 𝑎 → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ ∪ 𝑎 ) ∈ 𝑀 ) )
40	39 4	elrab2	⊢ ( ∪ 𝑎 ∈ 𝐽 ↔ ( ∪ 𝑎 ∈ 𝒫 𝐵 ∧ ( 𝐵 ∖ ∪ 𝑎 ) ∈ 𝑀 ) )
41	18 37 40	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ∪ 𝑎 ∈ 𝐽 )
42		0elpw	⊢ ∅ ∈ 𝒫 𝐵
43	42	a1i	⊢ ( 𝜑 → ∅ ∈ 𝒫 𝐵 )
44		mre1cl	⊢ ( 𝑀 ∈ ( Moore ‘ 𝐵 ) → 𝐵 ∈ 𝑀 )
45	1 44	syl	⊢ ( 𝜑 → 𝐵 ∈ 𝑀 )
46		difeq2	⊢ ( 𝑧 = ∅ → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ ∅ ) )
47		dif0	⊢ ( 𝐵 ∖ ∅ ) = 𝐵
48	46 47	eqtrdi	⊢ ( 𝑧 = ∅ → ( 𝐵 ∖ 𝑧 ) = 𝐵 )
49	48	eleq1d	⊢ ( 𝑧 = ∅ → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ 𝐵 ∈ 𝑀 ) )
50	49 4	elrab2	⊢ ( ∅ ∈ 𝐽 ↔ ( ∅ ∈ 𝒫 𝐵 ∧ 𝐵 ∈ 𝑀 ) )
51	43 45 50	sylanbrc	⊢ ( 𝜑 → ∅ ∈ 𝐽 )
52	51	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ∅ ∈ 𝐽 )
53	8 41 52	pm2.61ne	⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ∪ 𝑎 ∈ 𝐽 )
54	53	ex	⊢ ( 𝜑 → ( 𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽 ) )
55	54	alrimiv	⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽 ) )
56		inss1	⊢ ( 𝑎 ∩ 𝑏 ) ⊆ 𝑎
57		difeq2	⊢ ( 𝑧 = 𝑎 → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ 𝑎 ) )
58	57	eleq1d	⊢ ( 𝑧 = 𝑎 → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 ) )
59	58 4	elrab2	⊢ ( 𝑎 ∈ 𝐽 ↔ ( 𝑎 ∈ 𝒫 𝐵 ∧ ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 ) )
60	59	simplbi	⊢ ( 𝑎 ∈ 𝐽 → 𝑎 ∈ 𝒫 𝐵 )
61	60	elpwid	⊢ ( 𝑎 ∈ 𝐽 → 𝑎 ⊆ 𝐵 )
62	61	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → 𝑎 ⊆ 𝐵 )
63	56 62	sstrid	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝑎 ∩ 𝑏 ) ⊆ 𝐵 )
64		vex	⊢ 𝑎 ∈ V
65	64	inex1	⊢ ( 𝑎 ∩ 𝑏 ) ∈ V
66	65	elpw	⊢ ( ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐵 ↔ ( 𝑎 ∩ 𝑏 ) ⊆ 𝐵 )
67	63 66	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐵 )
68		difindi	⊢ ( 𝐵 ∖ ( 𝑎 ∩ 𝑏 ) ) = ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) )
69	59	simprbi	⊢ ( 𝑎 ∈ 𝐽 → ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 )
70	69	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 )
71	28	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
72		simpl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → 𝜑 )
73		uneq1	⊢ ( 𝑥 = ( 𝐵 ∖ 𝑎 ) → ( 𝑥 ∪ 𝑦 ) = ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) )
74	73	eleq1d	⊢ ( 𝑥 = ( 𝐵 ∖ 𝑎 ) → ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 ↔ ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) ∈ 𝑀 ) )
75	74	imbi2d	⊢ ( 𝑥 = ( 𝐵 ∖ 𝑎 ) → ( ( 𝜑 → ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 ) ↔ ( 𝜑 → ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) ∈ 𝑀 ) ) )
76		uneq2	⊢ ( 𝑦 = ( 𝐵 ∖ 𝑏 ) → ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) = ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) )
77	76	eleq1d	⊢ ( 𝑦 = ( 𝐵 ∖ 𝑏 ) → ( ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) ∈ 𝑀 ↔ ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) ∈ 𝑀 ) )
78	77	imbi2d	⊢ ( 𝑦 = ( 𝐵 ∖ 𝑏 ) → ( ( 𝜑 → ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) ∈ 𝑀 ) ↔ ( 𝜑 → ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) ∈ 𝑀 ) ) )
79	3	3expb	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 )
80	79	expcom	⊢ ( ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) → ( 𝜑 → ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 ) )
81	75 78 80	vtocl2ga	⊢ ( ( ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 ∧ ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) → ( 𝜑 → ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) ∈ 𝑀 ) )
82	81	imp	⊢ ( ( ( ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 ∧ ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) ∧ 𝜑 ) → ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) ∈ 𝑀 )
83	70 71 72 82	syl21anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) ∈ 𝑀 )
84	68 83	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝐵 ∖ ( 𝑎 ∩ 𝑏 ) ) ∈ 𝑀 )
85		difeq2	⊢ ( 𝑧 = ( 𝑎 ∩ 𝑏 ) → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ ( 𝑎 ∩ 𝑏 ) ) )
86	85	eleq1d	⊢ ( 𝑧 = ( 𝑎 ∩ 𝑏 ) → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ ( 𝑎 ∩ 𝑏 ) ) ∈ 𝑀 ) )
87	86 4	elrab2	⊢ ( ( 𝑎 ∩ 𝑏 ) ∈ 𝐽 ↔ ( ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐵 ∧ ( 𝐵 ∖ ( 𝑎 ∩ 𝑏 ) ) ∈ 𝑀 ) )
88	67 84 87	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝐽 )
89	88	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐽 ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∩ 𝑏 ) ∈ 𝐽 )
90	45	pwexd	⊢ ( 𝜑 → 𝒫 𝐵 ∈ V )
91	4 90	rabexd	⊢ ( 𝜑 → 𝐽 ∈ V )
92		istopg	⊢ ( 𝐽 ∈ V → ( 𝐽 ∈ Top ↔ ( ∀ 𝑎 ( 𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽 ) ∧ ∀ 𝑎 ∈ 𝐽 ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∩ 𝑏 ) ∈ 𝐽 ) ) )
93	91 92	syl	⊢ ( 𝜑 → ( 𝐽 ∈ Top ↔ ( ∀ 𝑎 ( 𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽 ) ∧ ∀ 𝑎 ∈ 𝐽 ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∩ 𝑏 ) ∈ 𝐽 ) ) )
94	55 89 93	mpbir2and	⊢ ( 𝜑 → 𝐽 ∈ Top )
95	9	unissi	⊢ ∪ 𝐽 ⊆ ∪ 𝒫 𝐵
96		unipw	⊢ ∪ 𝒫 𝐵 = 𝐵
97	95 96	sseqtri	⊢ ∪ 𝐽 ⊆ 𝐵
98		pwidg	⊢ ( 𝐵 ∈ 𝑀 → 𝐵 ∈ 𝒫 𝐵 )
99	45 98	syl	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐵 )
100		difid	⊢ ( 𝐵 ∖ 𝐵 ) = ∅
101	100 2	eqeltrid	⊢ ( 𝜑 → ( 𝐵 ∖ 𝐵 ) ∈ 𝑀 )
102		difeq2	⊢ ( 𝑧 = 𝐵 → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ 𝐵 ) )
103	102	eleq1d	⊢ ( 𝑧 = 𝐵 → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ 𝐵 ) ∈ 𝑀 ) )
104	103 4	elrab2	⊢ ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ∈ 𝒫 𝐵 ∧ ( 𝐵 ∖ 𝐵 ) ∈ 𝑀 ) )
105	99 101 104	sylanbrc	⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
106		unissel	⊢ ( ( ∪ 𝐽 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐽 ) → ∪ 𝐽 = 𝐵 )
107	97 105 106	sylancr	⊢ ( 𝜑 → ∪ 𝐽 = 𝐵 )
108	107	eqcomd	⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
109		istopon	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) )
110	94 108 109	sylanbrc	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
111		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
112	111	cldval	⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) = { 𝑥 ∈ 𝒫 ∪ 𝐽 ∣ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 } )
113	94 112	syl	⊢ ( 𝜑 → ( Clsd ‘ 𝐽 ) = { 𝑥 ∈ 𝒫 ∪ 𝐽 ∣ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 } )
114	107	pweqd	⊢ ( 𝜑 → 𝒫 ∪ 𝐽 = 𝒫 𝐵 )
115	107	difeq1d	⊢ ( 𝜑 → ( ∪ 𝐽 ∖ 𝑥 ) = ( 𝐵 ∖ 𝑥 ) )
116	115	eleq1d	⊢ ( 𝜑 → ( ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ↔ ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 ) )
117	114 116	rabeqbidv	⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 ∪ 𝐽 ∣ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 } = { 𝑥 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 } )
118	4	eleq2i	⊢ ( ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 ↔ ( 𝐵 ∖ 𝑥 ) ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 } )
119		difss	⊢ ( 𝐵 ∖ 𝑥 ) ⊆ 𝐵
120		elpw2g	⊢ ( 𝐵 ∈ 𝑀 → ( ( 𝐵 ∖ 𝑥 ) ∈ 𝒫 𝐵 ↔ ( 𝐵 ∖ 𝑥 ) ⊆ 𝐵 ) )
121	45 120	syl	⊢ ( 𝜑 → ( ( 𝐵 ∖ 𝑥 ) ∈ 𝒫 𝐵 ↔ ( 𝐵 ∖ 𝑥 ) ⊆ 𝐵 ) )
122	119 121	mpbiri	⊢ ( 𝜑 → ( 𝐵 ∖ 𝑥 ) ∈ 𝒫 𝐵 )
123		difeq2	⊢ ( 𝑧 = ( 𝐵 ∖ 𝑥 ) → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) )
124	123	eleq1d	⊢ ( 𝑧 = ( 𝐵 ∖ 𝑥 ) → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ) )
125	124	elrab3	⊢ ( ( 𝐵 ∖ 𝑥 ) ∈ 𝒫 𝐵 → ( ( 𝐵 ∖ 𝑥 ) ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 } ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ) )
126	122 125	syl	⊢ ( 𝜑 → ( ( 𝐵 ∖ 𝑥 ) ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 } ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ) )
127	126	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ 𝑥 ) ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 } ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ) )
128	118 127	bitrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ) )
129		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵 )
130		dfss4	⊢ ( 𝑥 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) = 𝑥 )
131	129 130	sylib	⊢ ( 𝑥 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) = 𝑥 )
132	131	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) = 𝑥 )
133	132	eleq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ↔ 𝑥 ∈ 𝑀 ) )
134	128 133	bitrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 ↔ 𝑥 ∈ 𝑀 ) )
135	134	rabbidva	⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 } = { 𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀 } )
136		incom	⊢ ( 𝑀 ∩ 𝒫 𝐵 ) = ( 𝒫 𝐵 ∩ 𝑀 )
137		dfin5	⊢ ( 𝒫 𝐵 ∩ 𝑀 ) = { 𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀 }
138	136 137	eqtri	⊢ ( 𝑀 ∩ 𝒫 𝐵 ) = { 𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀 }
139		mresspw	⊢ ( 𝑀 ∈ ( Moore ‘ 𝐵 ) → 𝑀 ⊆ 𝒫 𝐵 )
140	1 139	syl	⊢ ( 𝜑 → 𝑀 ⊆ 𝒫 𝐵 )
141		dfss2	⊢ ( 𝑀 ⊆ 𝒫 𝐵 ↔ ( 𝑀 ∩ 𝒫 𝐵 ) = 𝑀 )
142	140 141	sylib	⊢ ( 𝜑 → ( 𝑀 ∩ 𝒫 𝐵 ) = 𝑀 )
143	138 142	eqtr3id	⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀 } = 𝑀 )
144	135 143	eqtrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 } = 𝑀 )
145	113 117 144	3eqtrrd	⊢ ( 𝜑 → 𝑀 = ( Clsd ‘ 𝐽 ) )
146	110 145	jca	⊢ ( 𝜑 → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝑀 = ( Clsd ‘ 𝐽 ) ) )