Theorem ntrneik4w

Description: Idempotence of the interior function is equivalent to saying a set is a neighborhood of a point if and only if the interior of the set is a neighborhood of a point. (Contributed by RP, 11-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4		dfcleq	⊢ ( ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) )
5		eqcom	⊢ ( ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) )
6		ralv	⊢ ( ∀ 𝑥 ∈ V ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) )
7	4 5 6	3bitr4i	⊢ ( ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ V ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) )
8		ssv	⊢ 𝐵 ⊆ V
9	8	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐵 ⊆ V )
10		vex	⊢ 𝑥 ∈ V
11		eldif	⊢ ( 𝑥 ∈ ( V ∖ 𝐵 ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐵 ) )
12	10 11	mpbiran	⊢ ( 𝑥 ∈ ( V ∖ 𝐵 ) ↔ ¬ 𝑥 ∈ 𝐵 )
13	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
14		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
15	13 14	syl	⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
16	15	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
17	16	elpwid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 )
18	17	sseld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝐵 ) )
19	18	con3dimp	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) )
20	15	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
21	20 16	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ∈ 𝒫 𝐵 )
22	21	elpwid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ⊆ 𝐵 )
23	22	sseld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) → 𝑥 ∈ 𝐵 ) )
24	23	con3dimp	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) )
25	19 24	2falsed	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) )
26	25	ex	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ¬ 𝑥 ∈ 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) ) )
27	12 26	syl5bi	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ ( V ∖ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) ) )
28	27	ralrimiv	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ∀ 𝑥 ∈ ( V ∖ 𝐵 ) ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) )
29	9 28	raldifeq	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) ↔ ∀ 𝑥 ∈ V ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) ) )
30	3	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐼 𝐹 𝑁 )
31	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
32		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
33		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
34	1 2 31 32 33	ntrneiel	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
35	16	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
36	1 2 31 32 35	ntrneiel	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) )
37	34 36	bibi12d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
38	37	ralbidva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
39	29 38	bitr3d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ V ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑥 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
40	7 39	syl5bb	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
41	40	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
42		ralcom	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) )
43	41 42	bitrdi	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑠 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )