Theorem neicvgfv

Description: The value of the neighborhoods (convergents) in terms of the convergents (neighborhoods) function. (Contributed by RP, 27-Jun-2021)

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

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		neicvgfv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9		dfin5	⊢ ( 𝒫 𝐵 ∩ ( 𝑁 ‘ 𝑋 ) ) = { 𝑠 ∈ 𝒫 𝐵 ∣ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) }
10	1 2 3 4 5 6 7	neicvgnex	⊢ ( 𝜑 → 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
11		elmapi	⊢ ( 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
12	10 11	syl	⊢ ( 𝜑 → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
13	12 8	ffvelcdmd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ 𝒫 𝒫 𝐵 )
14	13	elpwid	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 )
15		sseqin2	⊢ ( ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 ↔ ( 𝒫 𝐵 ∩ ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ 𝑋 ) )
16	14 15	sylib	⊢ ( 𝜑 → ( 𝒫 𝐵 ∩ ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ 𝑋 ) )
17	7	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑁 𝐻 𝑀 )
18	8	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑋 ∈ 𝐵 )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
20	1 2 3 4 5 6 17 18 19	neicvgel1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ¬ ( 𝐵 ∖ 𝑠 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )
21	20	rabbidva	⊢ ( 𝜑 → { 𝑠 ∈ 𝒫 𝐵 ∣ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) } = { 𝑠 ∈ 𝒫 𝐵 ∣ ¬ ( 𝐵 ∖ 𝑠 ) ∈ ( 𝑀 ‘ 𝑋 ) } )
22	9 16 21	3eqtr3a	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) = { 𝑠 ∈ 𝒫 𝐵 ∣ ¬ ( 𝐵 ∖ 𝑠 ) ∈ ( 𝑀 ‘ 𝑋 ) } )