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	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
	ntrnei.f	$⊢ F = 𝒫 B O B$
	ntrnei.r	$⊢ φ \to I F N$
Assertion	ntrneik2	$⊢ φ \to (\forall s \in 𝒫 B I (s) \subseteq s \leftrightarrow \forall x \in B \forall s \in 𝒫 B (s \in N (x) \to x \in s))$

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
2		ntrnei.f	$⊢ F = 𝒫 B O B$
3		ntrnei.r	$⊢ φ \to I F N$
4	1 2 3	ntrneiiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
5		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
6	4 5	syl	$⊢ φ \to I : 𝒫 B ⟶ 𝒫 B$
7	6	ffvelrnda	$⊢ (φ \land s \in 𝒫 B) \to I (s) \in 𝒫 B$
8	7	elpwid	$⊢ (φ \land s \in 𝒫 B) \to I (s) \subseteq B$
9	8	sselda	$⊢ ((φ \land s \in 𝒫 B) \land x \in I (s)) \to x \in B$
10		biimt	$⊢ x \in B \to (x \in s \leftrightarrow (x \in B \to x \in s))$
11	9 10	syl	$⊢ ((φ \land s \in 𝒫 B) \land x \in I (s)) \to (x \in s \leftrightarrow (x \in B \to x \in s))$
12	11	pm5.74da	$⊢ (φ \land s \in 𝒫 B) \to ((x \in I (s) \to x \in s) \leftrightarrow (x \in I (s) \to (x \in B \to x \in s)))$
13		bi2.04	$⊢ (x \in I (s) \to (x \in B \to x \in s)) \leftrightarrow (x \in B \to (x \in I (s) \to x \in s))$
14	12 13	bitrdi	$⊢ (φ \land s \in 𝒫 B) \to ((x \in I (s) \to x \in s) \leftrightarrow (x \in B \to (x \in I (s) \to x \in s)))$
15	14	albidv	$⊢ (φ \land s \in 𝒫 B) \to (\forall x (x \in I (s) \to x \in s) \leftrightarrow \forall x (x \in B \to (x \in I (s) \to x \in s)))$
16		dfss2	$⊢ I (s) \subseteq s \leftrightarrow \forall x (x \in I (s) \to x \in s)$
17		df-ral	$⊢ \forall x \in B (x \in I (s) \to x \in s) \leftrightarrow \forall x (x \in B \to (x \in I (s) \to x \in s))$
18	15 16 17	3bitr4g	$⊢ (φ \land s \in 𝒫 B) \to (I (s) \subseteq s \leftrightarrow \forall x \in B (x \in I (s) \to x \in s))$
19	3	ad2antrr	$⊢ ((φ \land s \in 𝒫 B) \land x \in B) \to I F N$
20		simpr	$⊢ ((φ \land s \in 𝒫 B) \land x \in B) \to x \in B$
21		simplr	$⊢ ((φ \land s \in 𝒫 B) \land x \in B) \to s \in 𝒫 B$
22	1 2 19 20 21	ntrneiel	$⊢ ((φ \land s \in 𝒫 B) \land x \in B) \to (x \in I (s) \leftrightarrow s \in N (x))$
23	22	imbi1d	$⊢ ((φ \land s \in 𝒫 B) \land x \in B) \to ((x \in I (s) \to x \in s) \leftrightarrow (s \in N (x) \to x \in s))$
24	23	ralbidva	$⊢ (φ \land s \in 𝒫 B) \to (\forall x \in B (x \in I (s) \to x \in s) \leftrightarrow \forall x \in B (s \in N (x) \to x \in s))$
25	18 24	bitrd	$⊢ (φ \land s \in 𝒫 B) \to (I (s) \subseteq s \leftrightarrow \forall x \in B (s \in N (x) \to x \in s))$
26	25	ralbidva	$⊢ φ \to (\forall s \in 𝒫 B I (s) \subseteq s \leftrightarrow \forall s \in 𝒫 B \forall x \in B (s \in N (x) \to x \in s))$
27		ralcom	$⊢ \forall s \in 𝒫 B \forall x \in B (s \in N (x) \to x \in s) \leftrightarrow \forall x \in B \forall s \in 𝒫 B (s \in N (x) \to x \in s)$
28	26 27	bitrdi	$⊢ φ \to (\forall s \in 𝒫 B I (s) \subseteq s \leftrightarrow \forall x \in B \forall s \in 𝒫 B (s \in N (x) \to x \in s))$

Metamath Proof Explorer

Theorem ntrneik2

Proof