Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ntrneixb Structured version   Visualization version   GIF version

Theorem ntrneixb 37872
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.)
Hypotheses
Ref Expression
ntrnei.o 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))
ntrnei.f 𝐹 = (𝒫 𝐵𝑂𝐵)
ntrnei.r (𝜑𝐼𝐹𝑁)
Assertion
Ref Expression
ntrneixb (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
Distinct variable groups:   𝐵,𝑖,𝑗,𝑘,𝑙,𝑚,𝑠,𝑡,𝑥   𝑘,𝐼,𝑙,𝑚,𝑥   𝜑,𝑖,𝑗,𝑘,𝑙,𝑠,𝑡,𝑥
Allowed substitution hints:   𝜑(𝑚)   𝐹(𝑥,𝑡,𝑖,𝑗,𝑘,𝑚,𝑠,𝑙)   𝐼(𝑡,𝑖,𝑗,𝑠)   𝑁(𝑥,𝑡,𝑖,𝑗,𝑘,𝑚,𝑠,𝑙)   𝑂(𝑥,𝑡,𝑖,𝑗,𝑘,𝑚,𝑠,𝑙)

Proof of Theorem ntrneixb
StepHypRef Expression
1 eqss 3598 . . . . . . . 8 (((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵 ↔ (((𝐼𝑠) ∪ (𝐼𝑡)) ⊆ 𝐵𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡))))
21a1i 11 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵 ↔ (((𝐼𝑠) ∪ (𝐼𝑡)) ⊆ 𝐵𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)))))
3 ntrnei.o . . . . . . . . . . . . . 14 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))
4 ntrnei.f . . . . . . . . . . . . . 14 𝐹 = (𝒫 𝐵𝑂𝐵)
5 ntrnei.r . . . . . . . . . . . . . 14 (𝜑𝐼𝐹𝑁)
63, 4, 5ntrneiiex 37853 . . . . . . . . . . . . 13 (𝜑𝐼 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
7 elmapi 7823 . . . . . . . . . . . . 13 (𝐼 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
86, 7syl 17 . . . . . . . . . . . 12 (𝜑𝐼:𝒫 𝐵⟶𝒫 𝐵)
98ffvelrnda 6315 . . . . . . . . . . 11 ((𝜑𝑠 ∈ 𝒫 𝐵) → (𝐼𝑠) ∈ 𝒫 𝐵)
109elpwid 4141 . . . . . . . . . 10 ((𝜑𝑠 ∈ 𝒫 𝐵) → (𝐼𝑠) ⊆ 𝐵)
1110adantr 481 . . . . . . . . 9 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼𝑠) ⊆ 𝐵)
128ffvelrnda 6315 . . . . . . . . . . 11 ((𝜑𝑡 ∈ 𝒫 𝐵) → (𝐼𝑡) ∈ 𝒫 𝐵)
1312elpwid 4141 . . . . . . . . . 10 ((𝜑𝑡 ∈ 𝒫 𝐵) → (𝐼𝑡) ⊆ 𝐵)
1413adantlr 750 . . . . . . . . 9 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼𝑡) ⊆ 𝐵)
1511, 14unssd 3767 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼𝑠) ∪ (𝐼𝑡)) ⊆ 𝐵)
1615biantrurd 529 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ (((𝐼𝑠) ∪ (𝐼𝑡)) ⊆ 𝐵𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)))))
17 dfss3 3573 . . . . . . . . 9 (𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ ∀𝑥𝐵 𝑥 ∈ ((𝐼𝑠) ∪ (𝐼𝑡)))
18 elun 3731 . . . . . . . . . 10 (𝑥 ∈ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)))
1918ralbii 2974 . . . . . . . . 9 (∀𝑥𝐵 𝑥 ∈ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)))
2017, 19bitri 264 . . . . . . . 8 (𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)))
2120a1i 11 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))))
222, 16, 213bitr2d 296 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵 ↔ ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))))
2322imbi2d 330 . . . . 5 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ((𝑠𝑡) = 𝐵 → ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)))))
24 r19.21v 2954 . . . . . 6 (∀𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))) ↔ ((𝑠𝑡) = 𝐵 → ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))))
2524a1i 11 . . . . 5 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))) ↔ ((𝑠𝑡) = 𝐵 → ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)))))
265ad3antrrr 765 . . . . . . . . 9 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → 𝐼𝐹𝑁)
27 simpr 477 . . . . . . . . 9 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → 𝑥𝐵)
28 simpllr 798 . . . . . . . . 9 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → 𝑠 ∈ 𝒫 𝐵)
293, 4, 26, 27, 28ntrneiel 37858 . . . . . . . 8 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → (𝑥 ∈ (𝐼𝑠) ↔ 𝑠 ∈ (𝑁𝑥)))
30 simplr 791 . . . . . . . . 9 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → 𝑡 ∈ 𝒫 𝐵)
313, 4, 26, 27, 30ntrneiel 37858 . . . . . . . 8 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → (𝑥 ∈ (𝐼𝑡) ↔ 𝑡 ∈ (𝑁𝑥)))
3229, 31orbi12d 745 . . . . . . 7 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → ((𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)) ↔ (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥))))
3332imbi2d 330 . . . . . 6 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → (((𝑠𝑡) = 𝐵 → (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))) ↔ ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
3433ralbidva 2979 . . . . 5 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))) ↔ ∀𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
3523, 25, 343bitr2d 296 . . . 4 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ∀𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
3635ralbidva 2979 . . 3 ((𝜑𝑠 ∈ 𝒫 𝐵) → (∀𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ∀𝑡 ∈ 𝒫 𝐵𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
3736ralbidva 2979 . 2 (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
38 alrot3 2035 . . . 4 (∀𝑥𝑠𝑡((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))) ↔ ∀𝑠𝑡𝑥((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
39 3anrot 1041 . . . . . . 7 ((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) ↔ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵))
4039imbi1i 339 . . . . . 6 (((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))) ↔ ((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
4140albii 1744 . . . . 5 (∀𝑥((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))) ↔ ∀𝑥((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
42412albii 1745 . . . 4 (∀𝑠𝑡𝑥((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))) ↔ ∀𝑠𝑡𝑥((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
4338, 42bitr2i 265 . . 3 (∀𝑠𝑡𝑥((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))) ↔ ∀𝑥𝑠𝑡((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
44 r3al 2935 . . 3 (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥))) ↔ ∀𝑠𝑡𝑥((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
45 r3al 2935 . . 3 (∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥))) ↔ ∀𝑥𝑠𝑡((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
4643, 44, 453bitr4i 292 . 2 (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥))) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥))))
4737, 46syl6bb 276 1 (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3a 1036  wal 1478   = wceq 1480  wcel 1987  wral 2907  {crab 2911  Vcvv 3186  cun 3553  wss 3555  𝒫 cpw 4130   class class class wbr 4613  cmpt 4673  wf 5843  cfv 5847  (class class class)co 6604  cmpt2 6606  𝑚 cmap 7802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-1st 7113  df-2nd 7114  df-map 7804
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator