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 38895
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 3759 . . . . . . . 8 (((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵 ↔ (((𝐼𝑠) ∪ (𝐼𝑡)) ⊆ 𝐵𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡))))
21a1i 11 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵 ↔ (((𝐼𝑠) ∪ (𝐼𝑡)) ⊆ 𝐵𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)))))
3 ntrnei.o . . . . . . . . . . . . . 14 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))
4 ntrnei.f . . . . . . . . . . . . . 14 𝐹 = (𝒫 𝐵𝑂𝐵)
5 ntrnei.r . . . . . . . . . . . . . 14 (𝜑𝐼𝐹𝑁)
63, 4, 5ntrneiiex 38876 . . . . . . . . . . . . 13 (𝜑𝐼 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
7 elmapi 8045 . . . . . . . . . . . . 13 (𝐼 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
86, 7syl 17 . . . . . . . . . . . 12 (𝜑𝐼:𝒫 𝐵⟶𝒫 𝐵)
98ffvelrnda 6522 . . . . . . . . . . 11 ((𝜑𝑠 ∈ 𝒫 𝐵) → (𝐼𝑠) ∈ 𝒫 𝐵)
109elpwid 4314 . . . . . . . . . 10 ((𝜑𝑠 ∈ 𝒫 𝐵) → (𝐼𝑠) ⊆ 𝐵)
1110adantr 472 . . . . . . . . 9 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼𝑠) ⊆ 𝐵)
128ffvelrnda 6522 . . . . . . . . . . 11 ((𝜑𝑡 ∈ 𝒫 𝐵) → (𝐼𝑡) ∈ 𝒫 𝐵)
1312elpwid 4314 . . . . . . . . . 10 ((𝜑𝑡 ∈ 𝒫 𝐵) → (𝐼𝑡) ⊆ 𝐵)
1413adantlr 753 . . . . . . . . 9 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼𝑡) ⊆ 𝐵)
1511, 14unssd 3932 . . . . . . . 8 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼𝑠) ∪ (𝐼𝑡)) ⊆ 𝐵)
1615biantrurd 530 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ (((𝐼𝑠) ∪ (𝐼𝑡)) ⊆ 𝐵𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)))))
17 dfss3 3733 . . . . . . . . 9 (𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ ∀𝑥𝐵 𝑥 ∈ ((𝐼𝑠) ∪ (𝐼𝑡)))
18 elun 3896 . . . . . . . . . 10 (𝑥 ∈ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)))
1918ralbii 3118 . . . . . . . . 9 (∀𝑥𝐵 𝑥 ∈ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)))
2017, 19bitri 264 . . . . . . . 8 (𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)))
2120a1i 11 . . . . . . 7 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))))
222, 16, 213bitr2d 296 . . . . . 6 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵 ↔ ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))))
2322imbi2d 329 . . . . 5 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ((𝑠𝑡) = 𝐵 → ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)))))
24 r19.21v 3098 . . . . . 6 (∀𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))) ↔ ((𝑠𝑡) = 𝐵 → ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))))
2524a1i 11 . . . . 5 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))) ↔ ((𝑠𝑡) = 𝐵 → ∀𝑥𝐵 (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)))))
265ad3antrrr 768 . . . . . . . . 9 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → 𝐼𝐹𝑁)
27 simpr 479 . . . . . . . . 9 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → 𝑥𝐵)
28 simpllr 817 . . . . . . . . 9 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → 𝑠 ∈ 𝒫 𝐵)
293, 4, 26, 27, 28ntrneiel 38881 . . . . . . . 8 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → (𝑥 ∈ (𝐼𝑠) ↔ 𝑠 ∈ (𝑁𝑥)))
30 simplr 809 . . . . . . . . 9 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → 𝑡 ∈ 𝒫 𝐵)
313, 4, 26, 27, 30ntrneiel 38881 . . . . . . . 8 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → (𝑥 ∈ (𝐼𝑡) ↔ 𝑡 ∈ (𝑁𝑥)))
3229, 31orbi12d 748 . . . . . . 7 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → ((𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡)) ↔ (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥))))
3332imbi2d 329 . . . . . 6 ((((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥𝐵) → (((𝑠𝑡) = 𝐵 → (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))) ↔ ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
3433ralbidva 3123 . . . . 5 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑥 ∈ (𝐼𝑠) ∨ 𝑥 ∈ (𝐼𝑡))) ↔ ∀𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
3523, 25, 343bitr2d 296 . . . 4 (((𝜑𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ∀𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
3635ralbidva 3123 . . 3 ((𝜑𝑠 ∈ 𝒫 𝐵) → (∀𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ∀𝑡 ∈ 𝒫 𝐵𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
3736ralbidva 3123 . 2 (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
38 alrot3 2187 . . . 4 (∀𝑥𝑠𝑡((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))) ↔ ∀𝑠𝑡𝑥((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
39 3anrot 1087 . . . . . . 7 ((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) ↔ (𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵))
4039imbi1i 338 . . . . . 6 (((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))) ↔ ((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
4140albii 1896 . . . . 5 (∀𝑥((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))) ↔ ∀𝑥((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
42412albii 1897 . . . 4 (∀𝑠𝑡𝑥((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))) ↔ ∀𝑠𝑡𝑥((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
4338, 42bitr2i 265 . . 3 (∀𝑠𝑡𝑥((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))) ↔ ∀𝑥𝑠𝑡((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
44 r3al 3078 . . 3 (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥))) ↔ ∀𝑠𝑡𝑥((𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
45 r3al 3078 . . 3 (∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥))) ↔ ∀𝑥𝑠𝑡((𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵) → ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
4643, 44, 453bitr4i 292 . 2 (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵𝑥𝐵 ((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥))) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥))))
4737, 46syl6bb 276 1 (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  w3a 1072  wal 1630   = wceq 1632  wcel 2139  wral 3050  {crab 3054  Vcvv 3340  cun 3713  wss 3715  𝒫 cpw 4302   class class class wbr 4804  cmpt 4881  wf 6045  cfv 6049  (class class class)co 6813  cmpt2 6815  𝑚 cmap 8023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-1st 7333  df-2nd 7334  df-map 8025
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator