Theorem 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	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion	ntrneiiso	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4		df-ss	⊢ ( ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
5	4	imbi2i	⊢ ( ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ⊆ 𝑡 → ∀ 𝑥 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
6		19.21v	⊢ ( ∀ 𝑥 ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( 𝑠 ⊆ 𝑡 → ∀ 𝑥 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
7	5 6	bitr4i	⊢ ( ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
8		ax-1	⊢ ( ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) → ( 𝑥 ∈ 𝐵 → ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) )
9		simpll	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝜑 )
10	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
11		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
12	9 10 11	3syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
13		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
14	12 13	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
15	14	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 )
16	15	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) → 𝑥 ∈ 𝐵 )
17	16	pm2.24d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
18	17	ex	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
19	18	com23	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ¬ 𝑥 ∈ 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
20	19	a1dd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ¬ 𝑥 ∈ 𝐵 → ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) )
21		idd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) → ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) )
22	20 21	jad	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝑥 ∈ 𝐵 → ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) → ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) )
23	8 22	impbid2	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) ) )
24	23	albidv	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) ) )
25		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) )
26	24 25	bitr4di	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) )
27	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
28		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
29		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
30	1 2 27 28 29	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
31		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
32	1 2 27 28 31	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ↔ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
33	30 32	imbi12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
34	33	imbi2d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( 𝑠 ⊆ 𝑡 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
35		impexp	⊢ ( ( ( 𝑠 ⊆ 𝑡 ∧ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ( 𝑠 ⊆ 𝑡 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
36		ancomst	⊢ ( ( ( 𝑠 ⊆ 𝑡 ∧ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
37	35 36	bitr3i	⊢ ( ( 𝑠 ⊆ 𝑡 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ↔ ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
38	34 37	bitrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
39	38	ralbidva	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
40	26 39	bitrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ( 𝑠 ⊆ 𝑡 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
41	7 40	bitrid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
42	41	ralbidva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
43		ralcom	⊢ ( ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
44	42 43	bitrdi	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
45	44	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
46		ralcom	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
47	45 46	bitrdi	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )