Theorem ntrneixb

Description: The interiors (closures) of sets that span the base set also span the base set if and only if the neighborhoods (convergents) of every point contain at least one of every pair of sets that span the base set. (Contributed by RP, 11-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4		eqss	⊢ ( ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) = 𝐵 ↔ ( ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 ∧ 𝐵 ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) )
5	4	a1i	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) = 𝐵 ↔ ( ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 ∧ 𝐵 ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ) )
6	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
7		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
8	6 7	syl	⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
9	8	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
10	9	elpwid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 )
11	10	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 )
12	8	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑡 ) ∈ 𝒫 𝐵 )
13	12	elpwid	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑡 ) ⊆ 𝐵 )
14	13	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑡 ) ⊆ 𝐵 )
15	11 14	unssd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 )
16	15	biantrurd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ( ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 ∧ 𝐵 ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ) )
17		dfss3	⊢ ( 𝐵 ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) )
18		elun	⊢ ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
19	18	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐵 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
20	17 19	bitri	⊢ ( 𝐵 ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
21	20	a1i	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
22	5 16 21	3bitr2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) = 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
23	22	imbi2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) = 𝐵 ) ↔ ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) )
24		r19.21v	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
25	24	a1i	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ) )
26	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
27		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
28		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
29	1 2 26 27 28	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
30		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
31	1 2 26 27 30	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ↔ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
32	29 31	orbi12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
33	32	imbi2d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
34	33	ralbidva	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
35	23 25 34	3bitr2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) = 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
36	35	ralbidva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) = 𝐵 ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
37	36	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) = 𝐵 ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
38		ralrot3	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
39	37 38	bitrdi	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) = 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) = 𝐵 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )