Theorem ntrneik4

Description: Idempotence of the interior function is equivalent to stating a set, s , is a neighborhood of a point, x is equivalent to there existing a special neighborhood, u , of x such that a point is an element of the special neighborhood if and only if s is also a neighborhood of the point. (Contributed by RP, 11-Jul-2021)

	Ref	Expression
Hypotheses	ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion	ntrneik4	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4	1 2 3	ntrneik4w	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
5	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐼 𝐹 𝑁 )
6		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑥 ∈ 𝐵 )
7	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
8		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
9	7 8	syl	⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
10	9	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
11	10	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
12	1 2 5 6 11	ntrneiel	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) )
13		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
14	1 2 5 6 13	ntrneiel2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
15	12 14	bitr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
16	15	bibi2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
17	16	ralbidva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
18	17	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
19	4 18	bitrd	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )