Theorem ntrneik2

Description: An interior function is contracting if and only if all the neighborhoods of a point contain that point. (Contributed by RP, 11-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
5		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
6	4 5	syl	⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
7	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
8	7	elpwid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 )
9	8	sselda	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) → 𝑥 ∈ 𝐵 )
10		biimt	⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝑠 ↔ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑠 ) ) )
11	9 10	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) → ( 𝑥 ∈ 𝑠 ↔ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑠 ) ) )
12	11	pm5.74da	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ↔ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑠 ) ) ) )
13		bi2.04	⊢ ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑠 ) ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ) )
14	12 13	bitrdi	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ) ) )
15	14	albidv	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ) ) )
16		df-ss	⊢ ( ( 𝐼 ‘ 𝑠 ) ⊆ 𝑠 ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) )
17		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ) )
18	15 16 17	3bitr4g	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ 𝑠 ) ⊆ 𝑠 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ) )
19	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
20		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
21		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
22	1 2 19 20 21	ntrneiel	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
23	22	imbi1d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑥 ∈ 𝑠 ) ) )
24	23	ralbidva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑥 ∈ 𝑠 ) ) )
25	18 24	bitrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ 𝑠 ) ⊆ 𝑠 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑥 ∈ 𝑠 ) ) )
26	25	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼 ‘ 𝑠 ) ⊆ 𝑠 ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑥 ∈ 𝑠 ) ) )
27		ralcom	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑥 ∈ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑥 ∈ 𝑠 ) )
28	26 27	bitrdi	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼 ‘ 𝑠 ) ⊆ 𝑠 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑥 ∈ 𝑠 ) ) )