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

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
2 ntrnei.f ⊢F=𝒫BOB
3 ntrnei.r ⊢φ→IFN
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 ffvelcdmda ⊢φ∧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 ffvelcdmda ⊢φ∧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∈Bx∈I⁡s∪I⁡t
18 elun ⊢x∈I⁡s∪I⁡t↔x∈I⁡s∨x∈I⁡t
19 18 ralbii ⊢∀x∈Bx∈I⁡s∪I⁡t↔∀x∈Bx∈I⁡s∨x∈I⁡t
20 17 19 bitri ⊢B⊆I⁡s∪I⁡t↔∀x∈Bx∈I⁡s∨x∈I⁡t
21 20 a1i ⊢φ∧s∈𝒫B∧t∈𝒫B→B⊆I⁡s∪I⁡t↔∀x∈Bx∈I⁡s∨x∈I⁡t
22 5 16 21 3bitr2d ⊢φ∧s∈𝒫B∧t∈𝒫B→I⁡s∪I⁡t=B↔∀x∈Bx∈I⁡s∨x∈I⁡t
23 22 imbi2d ⊢φ∧s∈𝒫B∧t∈𝒫B→s∪t=B→I⁡s∪I⁡t=B↔s∪t=B→∀x∈Bx∈I⁡s∨x∈I⁡t
24 r19.21v ⊢∀x∈Bs∪t=B→x∈I⁡s∨x∈I⁡t↔s∪t=B→∀x∈Bx∈I⁡s∨x∈I⁡t
25 24 a1i ⊢φ∧s∈𝒫B∧t∈𝒫B→∀x∈Bs∪t=B→x∈I⁡s∨x∈I⁡t↔s∪t=B→∀x∈Bx∈I⁡s∨x∈I⁡t
26 3 ad3antrrr ⊢φ∧s∈𝒫B∧t∈𝒫B∧x∈B→IFN
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∈Bs∪t=B→x∈I⁡s∨x∈I⁡t↔∀x∈Bs∪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∈Bs∪t=B→s∈N⁡x∨t∈N⁡x
36 35 ralbidva ⊢φ∧s∈𝒫B→∀t∈𝒫Bs∪t=B→I⁡s∪I⁡t=B↔∀t∈𝒫B∀x∈Bs∪t=B→s∈N⁡x∨t∈N⁡x
37 36 ralbidva ⊢φ→∀s∈𝒫B∀t∈𝒫Bs∪t=B→I⁡s∪I⁡t=B↔∀s∈𝒫B∀t∈𝒫B∀x∈Bs∪t=B→s∈N⁡x∨t∈N⁡x
38 ralrot3 ⊢∀s∈𝒫B∀t∈𝒫B∀x∈Bs∪t=B→s∈N⁡x∨t∈N⁡x↔∀x∈B∀s∈𝒫B∀t∈𝒫Bs∪t=B→s∈N⁡x∨t∈N⁡x
39 37 38 bitrdi ⊢φ→∀s∈𝒫B∀t∈𝒫Bs∪t=B→I⁡s∪I⁡t=B↔∀x∈B∀s∈𝒫B∀t∈𝒫Bs∪t=B→s∈N⁡x∨t∈N⁡x