Metamath Proof Explorer

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 ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
ntrnei.f ⊢ F = 𝒫 B O B
ntrnei.r ⊢ φ → I F N
Assertion ntrneixb ⊢ φ → ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∪ t = B → I ⁡ s ∪ I ⁡ t = B ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∪ t = B → s ∈ N ⁡ x ∨ t ∈ N ⁡ x

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
2 ntrnei.f ⊢ F = 𝒫 B O B
3 ntrnei.r ⊢ φ → I F N
4 eqss ⊢ I ⁡ s ∪ I ⁡ t = B ↔ I ⁡ s ∪ I ⁡ t ⊆ B ∧ B ⊆ I ⁡ s ∪ I ⁡ t
5 4 a1i ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ I ⁡ t = B ↔ I ⁡ s ∪ I ⁡ t ⊆ B ∧ B ⊆ I ⁡ s ∪ I ⁡ t
6 1 2 3 ntrneiiex ⊢ φ → I ∈ 𝒫 B 𝒫 B
7 elmapi ⊢ I ∈ 𝒫 B 𝒫 B → I : 𝒫 B ⟶ 𝒫 B
8 6 7 syl ⊢ φ → I : 𝒫 B ⟶ 𝒫 B
9 8 ffvelrnda ⊢ φ ∧ s ∈ 𝒫 B → I ⁡ s ∈ 𝒫 B
10 9 elpwid ⊢ φ ∧ s ∈ 𝒫 B → I ⁡ s ⊆ B
11 10 adantr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ⊆ B
12 8 ffvelrnda ⊢ φ ∧ t ∈ 𝒫 B → I ⁡ t ∈ 𝒫 B
13 12 elpwid ⊢ φ ∧ t ∈ 𝒫 B → I ⁡ t ⊆ B
14 13 adantlr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ t ⊆ B
15 11 14 unssd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ I ⁡ t ⊆ B
16 15 biantrurd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → B ⊆ I ⁡ s ∪ I ⁡ t ↔ I ⁡ s ∪ I ⁡ t ⊆ B ∧ B ⊆ I ⁡ s ∪ I ⁡ t
17 dfss3 ⊢ B ⊆ I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∪ I ⁡ t
18 elun ⊢ x ∈ I ⁡ s ∪ I ⁡ t ↔ x ∈ I ⁡ s ∨ x ∈ I ⁡ t
19 18 ralbii ⊢ ∀ x ∈ B x ∈ I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∨ x ∈ I ⁡ t
20 17 19 bitri ⊢ B ⊆ I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∨ x ∈ I ⁡ t
21 20 a1i ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → B ⊆ I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∨ x ∈ I ⁡ t
22 5 16 21 3bitr2d ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ I ⁡ t = B ↔ ∀ x ∈ B x ∈ I ⁡ s ∨ x ∈ I ⁡ t
23 22 imbi2d ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → s ∪ t = B → I ⁡ s ∪ I ⁡ t = B ↔ s ∪ t = B → ∀ x ∈ B x ∈ I ⁡ s ∨ x ∈ I ⁡ t
24 r19.21v ⊢ ∀ x ∈ B s ∪ t = B → x ∈ I ⁡ s ∨ x ∈ I ⁡ t ↔ s ∪ t = B → ∀ x ∈ B x ∈ I ⁡ s ∨ x ∈ I ⁡ t
25 24 a1i ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → ∀ x ∈ B s ∪ t = B → x ∈ I ⁡ s ∨ x ∈ I ⁡ t ↔ s ∪ t = B → ∀ x ∈ B x ∈ I ⁡ s ∨ x ∈ I ⁡ t
26 3 ad3antrrr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → I F N
27 simpr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ B
28 simpllr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → s ∈ 𝒫 B
29 1 2 26 27 28 ntrneiel ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ s ↔ s ∈ N ⁡ x
30 simplr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → t ∈ 𝒫 B
31 1 2 26 27 30 ntrneiel ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ t ↔ t ∈ N ⁡ x
32 29 31 orbi12d ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ s ∨ x ∈ I ⁡ t ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
33 32 imbi2d ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → s ∪ t = B → x ∈ I ⁡ s ∨ x ∈ I ⁡ t ↔ s ∪ t = B → s ∈ N ⁡ x ∨ t ∈ N ⁡ x
34 33 ralbidva ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → ∀ x ∈ B s ∪ t = B → x ∈ I ⁡ s ∨ x ∈ I ⁡ t ↔ ∀ x ∈ B s ∪ t = B → s ∈ N ⁡ x ∨ t ∈ N ⁡ x
35 23 25 34 3bitr2d ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → s ∪ t = B → I ⁡ s ∪ I ⁡ t = B ↔ ∀ x ∈ B s ∪ t = B → s ∈ N ⁡ x ∨ t ∈ N ⁡ x
36 35 ralbidva ⊢ φ ∧ s ∈ 𝒫 B → ∀ t ∈ 𝒫 B s ∪ t = B → I ⁡ s ∪ I ⁡ t = B ↔ ∀ t ∈ 𝒫 B ∀ x ∈ B s ∪ t = B → s ∈ N ⁡ x ∨ t ∈ N ⁡ x
37 36 ralbidva ⊢ φ → ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∪ t = B → I ⁡ s ∪ I ⁡ t = B ↔ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B ∀ x ∈ B s ∪ t = B → s ∈ N ⁡ x ∨ t ∈ N ⁡ x
38 ralrot3 ⊢ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B ∀ x ∈ B s ∪ t = B → s ∈ N ⁡ x ∨ t ∈ N ⁡ x ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∪ t = B → s ∈ N ⁡ x ∨ t ∈ N ⁡ x
39 37 38 syl6bb ⊢ φ → ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∪ t = B → I ⁡ s ∪ I ⁡ t = B ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∪ t = B → s ∈ N ⁡ x ∨ t ∈ N ⁡ x