Theorem neicvgel1

Description: A subset being an element of a neighborhood of a point is equivalent to the complement of that subset not being a element of the convergent of that point. (Contributed by RP, 12-Jun-2021)

	Ref	Expression
Hypotheses	neicvg.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	neicvg.p	⊢ 𝑃 = ( 𝑛 ∈ V ↦ ( 𝑝 ∈ ( 𝒫 𝑛 ↑m 𝒫 𝑛 ) ↦ ( 𝑜 ∈ 𝒫 𝑛 ↦ ( 𝑛 ∖ ( 𝑝 ‘ ( 𝑛 ∖ 𝑜 ) ) ) ) ) )
	neicvg.d	⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
	neicvg.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	neicvg.g	⊢ 𝐺 = ( 𝐵 𝑂 𝒫 𝐵 )
	neicvg.h	⊢ 𝐻 = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
	neicvg.r	⊢ ( 𝜑 → 𝑁 𝐻 𝑀 )
	neicvgel.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	neicvgel.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
Assertion	neicvgel1	⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		neicvg.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		neicvg.p	⊢ 𝑃 = ( 𝑛 ∈ V ↦ ( 𝑝 ∈ ( 𝒫 𝑛 ↑m 𝒫 𝑛 ) ↦ ( 𝑜 ∈ 𝒫 𝑛 ↦ ( 𝑛 ∖ ( 𝑝 ‘ ( 𝑛 ∖ 𝑜 ) ) ) ) ) )
3		neicvg.d	⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
4		neicvg.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
5		neicvg.g	⊢ 𝐺 = ( 𝐵 𝑂 𝒫 𝐵 )
6		neicvg.h	⊢ 𝐻 = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
7		neicvg.r	⊢ ( 𝜑 → 𝑁 𝐻 𝑀 )
8		neicvgel.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9		neicvgel.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
10	3 6 7	neicvgbex	⊢ ( 𝜑 → 𝐵 ∈ V )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
12	11	pwexd	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝒫 𝐵 ∈ V )
13	1 12 11 4	fsovf1od	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
14		f1ofn	⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
15	13 14	syl	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
16	2 3 11	dssmapf1od	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
17		f1of	⊢ ( 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
18	16 17	syl	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
19	1 11 12 5	fsovfd	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐺 : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
20	6	breqi	⊢ ( 𝑁 𝐻 𝑀 ↔ 𝑁 ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) 𝑀 )
21	7 20	sylib	⊢ ( 𝜑 → 𝑁 ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) 𝑀 )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝑁 ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) 𝑀 )
23	15 18 19 22	brcofffn	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) )
24	10 23	mpdan	⊢ ( 𝜑 → ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) )
25		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) )
26	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → 𝑋 ∈ 𝐵 )
27	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → 𝑆 ∈ 𝒫 𝐵 )
28	2 3 25 26 27	ntrclselnel1	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑋 ∈ ( ( 𝐺 ‘ 𝑁 ) ‘ 𝑆 ) ↔ ¬ 𝑋 ∈ ( ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ‘ ( 𝐵 ∖ 𝑆 ) ) ) )
29		eqid	⊢ ( 𝒫 𝐵 𝑂 𝐵 ) = ( 𝒫 𝐵 𝑂 𝐵 )
30		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) )
31	5	breqi	⊢ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ↔ 𝑁 ( 𝐵 𝑂 𝒫 𝐵 ) ( 𝐺 ‘ 𝑁 ) )
32	31	a1i	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ↔ 𝑁 ( 𝐵 𝑂 𝒫 𝐵 ) ( 𝐺 ‘ 𝑁 ) ) )
33	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → 𝐵 ∈ V )
34		id	⊢ ( 𝐵 ∈ V → 𝐵 ∈ V )
35		pwexg	⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ∈ V )
36		eqid	⊢ ( 𝐵 𝑂 𝒫 𝐵 ) = ( 𝐵 𝑂 𝒫 𝐵 )
37	1 34 35 36	fsovf1od	⊢ ( 𝐵 ∈ V → ( 𝐵 𝑂 𝒫 𝐵 ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
38	33 37	syl	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝐵 𝑂 𝒫 𝐵 ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
39		f1orel	⊢ ( ( 𝐵 𝑂 𝒫 𝐵 ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → Rel ( 𝐵 𝑂 𝒫 𝐵 ) )
40		relbrcnvg	⊢ ( Rel ( 𝐵 𝑂 𝒫 𝐵 ) → ( ( 𝐺 ‘ 𝑁 ) ◡ ( 𝐵 𝑂 𝒫 𝐵 ) 𝑁 ↔ 𝑁 ( 𝐵 𝑂 𝒫 𝐵 ) ( 𝐺 ‘ 𝑁 ) ) )
41	38 39 40	3syl	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( ( 𝐺 ‘ 𝑁 ) ◡ ( 𝐵 𝑂 𝒫 𝐵 ) 𝑁 ↔ 𝑁 ( 𝐵 𝑂 𝒫 𝐵 ) ( 𝐺 ‘ 𝑁 ) ) )
42	1 34 35 36 29	fsovcnvd	⊢ ( 𝐵 ∈ V → ◡ ( 𝐵 𝑂 𝒫 𝐵 ) = ( 𝒫 𝐵 𝑂 𝐵 ) )
43	42	breqd	⊢ ( 𝐵 ∈ V → ( ( 𝐺 ‘ 𝑁 ) ◡ ( 𝐵 𝑂 𝒫 𝐵 ) 𝑁 ↔ ( 𝐺 ‘ 𝑁 ) ( 𝒫 𝐵 𝑂 𝐵 ) 𝑁 ) )
44	33 43	syl	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( ( 𝐺 ‘ 𝑁 ) ◡ ( 𝐵 𝑂 𝒫 𝐵 ) 𝑁 ↔ ( 𝐺 ‘ 𝑁 ) ( 𝒫 𝐵 𝑂 𝐵 ) 𝑁 ) )
45	32 41 44	3bitr2d	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ↔ ( 𝐺 ‘ 𝑁 ) ( 𝒫 𝐵 𝑂 𝐵 ) 𝑁 ) )
46	30 45	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝐺 ‘ 𝑁 ) ( 𝒫 𝐵 𝑂 𝐵 ) 𝑁 )
47	1 29 46 26 27	ntrneiel	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑋 ∈ ( ( 𝐺 ‘ 𝑁 ) ‘ 𝑆 ) ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ) )
48		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 )
49		difssd	⊢ ( 𝜑 → ( 𝐵 ∖ 𝑆 ) ⊆ 𝐵 )
50	10 49	sselpwd	⊢ ( 𝜑 → ( 𝐵 ∖ 𝑆 ) ∈ 𝒫 𝐵 )
51	50	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝐵 ∖ 𝑆 ) ∈ 𝒫 𝐵 )
52	1 4 48 26 51	ntrneiel	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑋 ∈ ( ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ‘ ( 𝐵 ∖ 𝑆 ) ) ↔ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )
53	52	notbid	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( ¬ 𝑋 ∈ ( ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ‘ ( 𝐵 ∖ 𝑆 ) ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )
54	28 47 53	3bitr3d	⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )
55	24 54	mpdan	⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )