MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opnfbas Structured version   Visualization version   GIF version

Theorem opnfbas 21939
Description: The collection of open supersets of a nonempty set in a topology is a neighborhoods of the set, one of the motivations for the filter concept. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Aug-2015.)
Hypothesis
Ref Expression
opnfbas.1 𝑋 = 𝐽
Assertion
Ref Expression
opnfbas ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → {𝑥𝐽𝑆𝑥} ∈ (fBas‘𝑋))
Distinct variable groups:   𝑥,𝐽   𝑥,𝑆   𝑥,𝑋

Proof of Theorem opnfbas
Dummy variables 𝑠 𝑟 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab2 3849 . . . 4 {𝑥𝐽𝑆𝑥} ⊆ 𝐽
2 opnfbas.1 . . . . . 6 𝑋 = 𝐽
32eqimss2i 3822 . . . . 5 𝐽𝑋
4 sspwuni 4770 . . . . 5 (𝐽 ⊆ 𝒫 𝑋 𝐽𝑋)
53, 4mpbir 222 . . . 4 𝐽 ⊆ 𝒫 𝑋
61, 5sstri 3772 . . 3 {𝑥𝐽𝑆𝑥} ⊆ 𝒫 𝑋
76a1i 11 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → {𝑥𝐽𝑆𝑥} ⊆ 𝒫 𝑋)
82topopn 21004 . . . . . . 7 (𝐽 ∈ Top → 𝑋𝐽)
98anim1i 608 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑋𝐽𝑆𝑋))
1093adant3 1162 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → (𝑋𝐽𝑆𝑋))
11 sseq2 3789 . . . . . 6 (𝑥 = 𝑋 → (𝑆𝑥𝑆𝑋))
1211elrab 3521 . . . . 5 (𝑋 ∈ {𝑥𝐽𝑆𝑥} ↔ (𝑋𝐽𝑆𝑋))
1310, 12sylibr 225 . . . 4 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → 𝑋 ∈ {𝑥𝐽𝑆𝑥})
1413ne0d 4088 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → {𝑥𝐽𝑆𝑥} ≠ ∅)
15 ss0 4138 . . . . . . 7 (𝑆 ⊆ ∅ → 𝑆 = ∅)
1615necon3ai 2962 . . . . . 6 (𝑆 ≠ ∅ → ¬ 𝑆 ⊆ ∅)
17163ad2ant3 1165 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → ¬ 𝑆 ⊆ ∅)
1817intnand 482 . . . 4 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → ¬ (∅ ∈ 𝐽𝑆 ⊆ ∅))
19 df-nel 3041 . . . . 5 (∅ ∉ {𝑥𝐽𝑆𝑥} ↔ ¬ ∅ ∈ {𝑥𝐽𝑆𝑥})
20 sseq2 3789 . . . . . . 7 (𝑥 = ∅ → (𝑆𝑥𝑆 ⊆ ∅))
2120elrab 3521 . . . . . 6 (∅ ∈ {𝑥𝐽𝑆𝑥} ↔ (∅ ∈ 𝐽𝑆 ⊆ ∅))
2221notbii 311 . . . . 5 (¬ ∅ ∈ {𝑥𝐽𝑆𝑥} ↔ ¬ (∅ ∈ 𝐽𝑆 ⊆ ∅))
2319, 22bitr2i 267 . . . 4 (¬ (∅ ∈ 𝐽𝑆 ⊆ ∅) ↔ ∅ ∉ {𝑥𝐽𝑆𝑥})
2418, 23sylib 209 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → ∅ ∉ {𝑥𝐽𝑆𝑥})
25 sseq2 3789 . . . . . . 7 (𝑥 = 𝑟 → (𝑆𝑥𝑆𝑟))
2625elrab 3521 . . . . . 6 (𝑟 ∈ {𝑥𝐽𝑆𝑥} ↔ (𝑟𝐽𝑆𝑟))
27 sseq2 3789 . . . . . . 7 (𝑥 = 𝑠 → (𝑆𝑥𝑆𝑠))
2827elrab 3521 . . . . . 6 (𝑠 ∈ {𝑥𝐽𝑆𝑥} ↔ (𝑠𝐽𝑆𝑠))
2926, 28anbi12i 620 . . . . 5 ((𝑟 ∈ {𝑥𝐽𝑆𝑥} ∧ 𝑠 ∈ {𝑥𝐽𝑆𝑥}) ↔ ((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠)))
30 simpl 474 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠))) → 𝐽 ∈ Top)
31 simprll 797 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠))) → 𝑟𝐽)
32 simprrl 799 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠))) → 𝑠𝐽)
33 inopn 20997 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑟𝐽𝑠𝐽) → (𝑟𝑠) ∈ 𝐽)
3430, 31, 32, 33syl3anc 1490 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ ((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠))) → (𝑟𝑠) ∈ 𝐽)
35 ssin 3996 . . . . . . . . . . . . 13 ((𝑆𝑟𝑆𝑠) ↔ 𝑆 ⊆ (𝑟𝑠))
3635biimpi 207 . . . . . . . . . . . 12 ((𝑆𝑟𝑆𝑠) → 𝑆 ⊆ (𝑟𝑠))
3736ad2ant2l 752 . . . . . . . . . . 11 (((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠)) → 𝑆 ⊆ (𝑟𝑠))
3837adantl 473 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ ((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠))) → 𝑆 ⊆ (𝑟𝑠))
3934, 38jca 507 . . . . . . . . 9 ((𝐽 ∈ Top ∧ ((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠))) → ((𝑟𝑠) ∈ 𝐽𝑆 ⊆ (𝑟𝑠)))
40393ad2antl1 1236 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) ∧ ((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠))) → ((𝑟𝑠) ∈ 𝐽𝑆 ⊆ (𝑟𝑠)))
41 sseq2 3789 . . . . . . . . 9 (𝑥 = (𝑟𝑠) → (𝑆𝑥𝑆 ⊆ (𝑟𝑠)))
4241elrab 3521 . . . . . . . 8 ((𝑟𝑠) ∈ {𝑥𝐽𝑆𝑥} ↔ ((𝑟𝑠) ∈ 𝐽𝑆 ⊆ (𝑟𝑠)))
4340, 42sylibr 225 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) ∧ ((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠))) → (𝑟𝑠) ∈ {𝑥𝐽𝑆𝑥})
44 ssid 3785 . . . . . . 7 (𝑟𝑠) ⊆ (𝑟𝑠)
45 sseq1 3788 . . . . . . . 8 (𝑡 = (𝑟𝑠) → (𝑡 ⊆ (𝑟𝑠) ↔ (𝑟𝑠) ⊆ (𝑟𝑠)))
4645rspcev 3462 . . . . . . 7 (((𝑟𝑠) ∈ {𝑥𝐽𝑆𝑥} ∧ (𝑟𝑠) ⊆ (𝑟𝑠)) → ∃𝑡 ∈ {𝑥𝐽𝑆𝑥}𝑡 ⊆ (𝑟𝑠))
4743, 44, 46sylancl 580 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) ∧ ((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠))) → ∃𝑡 ∈ {𝑥𝐽𝑆𝑥}𝑡 ⊆ (𝑟𝑠))
4847ex 401 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → (((𝑟𝐽𝑆𝑟) ∧ (𝑠𝐽𝑆𝑠)) → ∃𝑡 ∈ {𝑥𝐽𝑆𝑥}𝑡 ⊆ (𝑟𝑠)))
4929, 48syl5bi 233 . . . 4 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → ((𝑟 ∈ {𝑥𝐽𝑆𝑥} ∧ 𝑠 ∈ {𝑥𝐽𝑆𝑥}) → ∃𝑡 ∈ {𝑥𝐽𝑆𝑥}𝑡 ⊆ (𝑟𝑠)))
5049ralrimivv 3117 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → ∀𝑟 ∈ {𝑥𝐽𝑆𝑥}∀𝑠 ∈ {𝑥𝐽𝑆𝑥}∃𝑡 ∈ {𝑥𝐽𝑆𝑥}𝑡 ⊆ (𝑟𝑠))
5114, 24, 503jca 1158 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → ({𝑥𝐽𝑆𝑥} ≠ ∅ ∧ ∅ ∉ {𝑥𝐽𝑆𝑥} ∧ ∀𝑟 ∈ {𝑥𝐽𝑆𝑥}∀𝑠 ∈ {𝑥𝐽𝑆𝑥}∃𝑡 ∈ {𝑥𝐽𝑆𝑥}𝑡 ⊆ (𝑟𝑠)))
52 isfbas2 21932 . . . 4 (𝑋𝐽 → ({𝑥𝐽𝑆𝑥} ∈ (fBas‘𝑋) ↔ ({𝑥𝐽𝑆𝑥} ⊆ 𝒫 𝑋 ∧ ({𝑥𝐽𝑆𝑥} ≠ ∅ ∧ ∅ ∉ {𝑥𝐽𝑆𝑥} ∧ ∀𝑟 ∈ {𝑥𝐽𝑆𝑥}∀𝑠 ∈ {𝑥𝐽𝑆𝑥}∃𝑡 ∈ {𝑥𝐽𝑆𝑥}𝑡 ⊆ (𝑟𝑠)))))
538, 52syl 17 . . 3 (𝐽 ∈ Top → ({𝑥𝐽𝑆𝑥} ∈ (fBas‘𝑋) ↔ ({𝑥𝐽𝑆𝑥} ⊆ 𝒫 𝑋 ∧ ({𝑥𝐽𝑆𝑥} ≠ ∅ ∧ ∅ ∉ {𝑥𝐽𝑆𝑥} ∧ ∀𝑟 ∈ {𝑥𝐽𝑆𝑥}∀𝑠 ∈ {𝑥𝐽𝑆𝑥}∃𝑡 ∈ {𝑥𝐽𝑆𝑥}𝑡 ⊆ (𝑟𝑠)))))
54533ad2ant1 1163 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → ({𝑥𝐽𝑆𝑥} ∈ (fBas‘𝑋) ↔ ({𝑥𝐽𝑆𝑥} ⊆ 𝒫 𝑋 ∧ ({𝑥𝐽𝑆𝑥} ≠ ∅ ∧ ∅ ∉ {𝑥𝐽𝑆𝑥} ∧ ∀𝑟 ∈ {𝑥𝐽𝑆𝑥}∀𝑠 ∈ {𝑥𝐽𝑆𝑥}∃𝑡 ∈ {𝑥𝐽𝑆𝑥}𝑡 ⊆ (𝑟𝑠)))))
557, 51, 54mpbir2and 704 1 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → {𝑥𝐽𝑆𝑥} ∈ (fBas‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wnel 3040  wral 3055  wrex 3056  {crab 3059  cin 3733  wss 3734  c0 4081  𝒫 cpw 4317   cuni 4596  cfv 6070  fBascfbas 20021  Topctop 20991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fv 6078  df-fbas 20030  df-top 20992
This theorem is referenced by:  neifg  32830
  Copyright terms: Public domain W3C validator