ntrneiiso

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that the interior function is isotonic hold equally. (Contributed by RP, 3-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	ntrneiiso	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x)))$

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		dfss2	$⊢ I (s) \subseteq I (t) \leftrightarrow \forall x (x \in I (s) \to x \in I (t))$
5	4	imbi2i	$⊢ (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow (s \subseteq t \to \forall x (x \in I (s) \to x \in I (t)))$
6		19.21v	$⊢ \forall x (s \subseteq t \to (x \in I (s) \to x \in I (t))) \leftrightarrow (s \subseteq t \to \forall x (x \in I (s) \to x \in I (t)))$
7	5 6	bitr4i	$⊢ (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall x (s \subseteq t \to (x \in I (s) \to x \in I (t)))$
8		ax-1	$⊢ (s \subseteq t \to (x \in I (s) \to x \in I (t))) \to (x \in B \to (s \subseteq t \to (x \in I (s) \to x \in I (t))))$
9		simpll	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to φ$
10	1 2 3	ntrneiiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
11		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
12	9 10 11	3syl	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I : 𝒫 B ⟶ 𝒫 B$
13		simplr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to s \in 𝒫 B$
14	12 13	ffvelrnd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I (s) \in 𝒫 B$
15	14	elpwid	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I (s) \subseteq B$
16	15	sselda	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in I (s)) \to x \in B$
17	16	pm2.24d	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in I (s)) \to (\neg x \in B \to x \in I (t))$
18	17	ex	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (x \in I (s) \to (\neg x \in B \to x \in I (t)))$
19	18	com23	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\neg x \in B \to (x \in I (s) \to x \in I (t)))$
20	19	a1dd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\neg x \in B \to (s \subseteq t \to (x \in I (s) \to x \in I (t))))$
21		idd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to ((s \subseteq t \to (x \in I (s) \to x \in I (t))) \to (s \subseteq t \to (x \in I (s) \to x \in I (t))))$
22	20 21	jad	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to ((x \in B \to (s \subseteq t \to (x \in I (s) \to x \in I (t)))) \to (s \subseteq t \to (x \in I (s) \to x \in I (t))))$
23	8 22	impbid2	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to ((s \subseteq t \to (x \in I (s) \to x \in I (t))) \leftrightarrow (x \in B \to (s \subseteq t \to (x \in I (s) \to x \in I (t)))))$
24	23	albidv	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x (s \subseteq t \to (x \in I (s) \to x \in I (t))) \leftrightarrow \forall x (x \in B \to (s \subseteq t \to (x \in I (s) \to x \in I (t)))))$
25		df-ral	$⊢ \forall x \in B (s \subseteq t \to (x \in I (s) \to x \in I (t))) \leftrightarrow \forall x (x \in B \to (s \subseteq t \to (x \in I (s) \to x \in I (t))))$
26	24 25	bitr4di	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x (s \subseteq t \to (x \in I (s) \to x \in I (t))) \leftrightarrow \forall x \in B (s \subseteq t \to (x \in I (s) \to x \in I (t))))$
27	3	ad3antrrr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to I F N$
28		simpr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to x \in B$
29		simpllr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \in 𝒫 B$
30	1 2 27 28 29	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (s) \leftrightarrow s \in N (x))$
31		simplr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to t \in 𝒫 B$
32	1 2 27 28 31	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (t) \leftrightarrow t \in N (x))$
33	30 32	imbi12d	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to ((x \in I (s) \to x \in I (t)) \leftrightarrow (s \in N (x) \to t \in N (x)))$
34	33	imbi2d	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to ((s \subseteq t \to (x \in I (s) \to x \in I (t))) \leftrightarrow (s \subseteq t \to (s \in N (x) \to t \in N (x))))$
35		impexp	$⊢ ((s \subseteq t \land s \in N (x)) \to t \in N (x)) \leftrightarrow (s \subseteq t \to (s \in N (x) \to t \in N (x)))$
36		ancomst	$⊢ ((s \subseteq t \land s \in N (x)) \to t \in N (x)) \leftrightarrow ((s \in N (x) \land s \subseteq t) \to t \in N (x))$
37	35 36	bitr3i	$⊢ (s \subseteq t \to (s \in N (x) \to t \in N (x))) \leftrightarrow ((s \in N (x) \land s \subseteq t) \to t \in N (x))$
38	34 37	bitrdi	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to ((s \subseteq t \to (x \in I (s) \to x \in I (t))) \leftrightarrow ((s \in N (x) \land s \subseteq t) \to t \in N (x)))$
39	38	ralbidva	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x \in B (s \subseteq t \to (x \in I (s) \to x \in I (t))) \leftrightarrow \forall x \in B ((s \in N (x) \land s \subseteq t) \to t \in N (x)))$
40	26 39	bitrd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x (s \subseteq t \to (x \in I (s) \to x \in I (t))) \leftrightarrow \forall x \in B ((s \in N (x) \land s \subseteq t) \to t \in N (x)))$
41	7 40	syl5bb	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to ((s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall x \in B ((s \in N (x) \land s \subseteq t) \to t \in N (x)))$
42	41	ralbidva	$⊢ (φ \land s \in 𝒫 B) \to (\forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall t \in 𝒫 B \forall x \in B ((s \in N (x) \land s \subseteq t) \to t \in N (x)))$
43		ralcom	$⊢ \forall t \in 𝒫 B \forall x \in B ((s \in N (x) \land s \subseteq t) \to t \in N (x)) \leftrightarrow \forall x \in B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x))$
44	42 43	bitrdi	$⊢ (φ \land s \in 𝒫 B) \to (\forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall x \in B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x)))$
45	44	ralbidva	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall s \in 𝒫 B \forall x \in B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x)))$
46		ralcom	$⊢ \forall s \in 𝒫 B \forall x \in B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x)) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x))$
47	45 46	bitrdi	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x)))$

Metamath Proof Explorer

Theorem ntrneiiso

Proof