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

Theorem dissnlocfin 23033
Description: The set of singletons is locally finite in the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020.)
Hypothesis
Ref Expression
dissnref.c 𝐢 = {𝑒 ∣ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}}
Assertion
Ref Expression
dissnlocfin (𝑋 ∈ 𝑉 β†’ 𝐢 ∈ (LocFinβ€˜π’« 𝑋))
Distinct variable groups:   𝑒,𝐢,π‘₯   𝑒,𝑉,π‘₯   𝑒,𝑋,π‘₯

Proof of Theorem dissnlocfin
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 distop 22498 . 2 (𝑋 ∈ 𝑉 β†’ 𝒫 𝑋 ∈ Top)
2 eqidd 2734 . 2 (𝑋 ∈ 𝑉 β†’ 𝑋 = 𝑋)
3 snelpwi 5444 . . . . 5 (𝑧 ∈ 𝑋 β†’ {𝑧} ∈ 𝒫 𝑋)
43adantl 483 . . . 4 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ {𝑧} ∈ 𝒫 𝑋)
5 vsnid 4666 . . . . 5 𝑧 ∈ {𝑧}
65a1i 11 . . . 4 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ 𝑧 ∈ {𝑧})
7 nfv 1918 . . . . . 6 Ⅎ𝑒(𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋)
8 nfrab1 3452 . . . . . 6 Ⅎ𝑒{𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…}
9 nfcv 2904 . . . . . 6 Ⅎ𝑒{{𝑧}}
10 dissnref.c . . . . . . . . . 10 𝐢 = {𝑒 ∣ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}}
1110eqabri 2878 . . . . . . . . 9 (𝑒 ∈ 𝐢 ↔ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯})
1211anbi1i 625 . . . . . . . 8 ((𝑒 ∈ 𝐢 ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ↔ (βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…))
13 simpr 486 . . . . . . . . . . . . 13 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ 𝑒 = {π‘₯})
14 simplr 768 . . . . . . . . . . . . . . . . . 18 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ 𝑒 = {π‘₯})
1514ineq1d 4212 . . . . . . . . . . . . . . . . 17 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ (𝑒 ∩ {𝑧}) = ({π‘₯} ∩ {𝑧}))
16 disjsn2 4717 . . . . . . . . . . . . . . . . . 18 (π‘₯ β‰  𝑧 β†’ ({π‘₯} ∩ {𝑧}) = βˆ…)
1716adantl 483 . . . . . . . . . . . . . . . . 17 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ ({π‘₯} ∩ {𝑧}) = βˆ…)
1815, 17eqtrd 2773 . . . . . . . . . . . . . . . 16 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ (𝑒 ∩ {𝑧}) = βˆ…)
19 simp-4r 783 . . . . . . . . . . . . . . . . 17 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ (𝑒 ∩ {𝑧}) β‰  βˆ…)
2019neneqd 2946 . . . . . . . . . . . . . . . 16 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ Β¬ (𝑒 ∩ {𝑧}) = βˆ…)
2118, 20pm2.65da 816 . . . . . . . . . . . . . . 15 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ Β¬ π‘₯ β‰  𝑧)
22 nne 2945 . . . . . . . . . . . . . . 15 (Β¬ π‘₯ β‰  𝑧 ↔ π‘₯ = 𝑧)
2321, 22sylib 217 . . . . . . . . . . . . . 14 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ π‘₯ = 𝑧)
2423sneqd 4641 . . . . . . . . . . . . 13 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ {π‘₯} = {𝑧})
2513, 24eqtrd 2773 . . . . . . . . . . . 12 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ 𝑒 = {𝑧})
2625r19.29an 3159 . . . . . . . . . . 11 ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}) β†’ 𝑒 = {𝑧})
2726an32s 651 . . . . . . . . . 10 ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) β†’ 𝑒 = {𝑧})
2827anasss 468 . . . . . . . . 9 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…)) β†’ 𝑒 = {𝑧})
29 sneq 4639 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ {π‘₯} = {𝑧})
3029rspceeqv 3634 . . . . . . . . . . 11 ((𝑧 ∈ 𝑋 ∧ 𝑒 = {𝑧}) β†’ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯})
3130adantll 713 . . . . . . . . . 10 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯})
32 simpr 486 . . . . . . . . . . . . 13 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ 𝑒 = {𝑧})
3332ineq1d 4212 . . . . . . . . . . . 12 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (𝑒 ∩ {𝑧}) = ({𝑧} ∩ {𝑧}))
34 inidm 4219 . . . . . . . . . . . 12 ({𝑧} ∩ {𝑧}) = {𝑧}
3533, 34eqtrdi 2789 . . . . . . . . . . 11 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (𝑒 ∩ {𝑧}) = {𝑧})
36 vex 3479 . . . . . . . . . . . . 13 𝑧 ∈ V
3736snnz 4781 . . . . . . . . . . . 12 {𝑧} β‰  βˆ…
3837a1i 11 . . . . . . . . . . 11 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ {𝑧} β‰  βˆ…)
3935, 38eqnetrd 3009 . . . . . . . . . 10 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (𝑒 ∩ {𝑧}) β‰  βˆ…)
4031, 39jca 513 . . . . . . . . 9 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…))
4128, 40impbida 800 . . . . . . . 8 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ ((βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ↔ 𝑒 = {𝑧}))
4212, 41bitrid 283 . . . . . . 7 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ ((𝑒 ∈ 𝐢 ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ↔ 𝑒 = {𝑧}))
43 rabid 3453 . . . . . . 7 (𝑒 ∈ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ↔ (𝑒 ∈ 𝐢 ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…))
44 velsn 4645 . . . . . . 7 (𝑒 ∈ {{𝑧}} ↔ 𝑒 = {𝑧})
4542, 43, 443bitr4g 314 . . . . . 6 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ (𝑒 ∈ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ↔ 𝑒 ∈ {{𝑧}}))
467, 8, 9, 45eqrd 4002 . . . . 5 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} = {{𝑧}})
47 snfi 9044 . . . . 5 {{𝑧}} ∈ Fin
4846, 47eqeltrdi 2842 . . . 4 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin)
49 eleq2 2823 . . . . . 6 (𝑦 = {𝑧} β†’ (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑧}))
50 ineq2 4207 . . . . . . . . 9 (𝑦 = {𝑧} β†’ (𝑒 ∩ 𝑦) = (𝑒 ∩ {𝑧}))
5150neeq1d 3001 . . . . . . . 8 (𝑦 = {𝑧} β†’ ((𝑒 ∩ 𝑦) β‰  βˆ… ↔ (𝑒 ∩ {𝑧}) β‰  βˆ…))
5251rabbidv 3441 . . . . . . 7 (𝑦 = {𝑧} β†’ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} = {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…})
5352eleq1d 2819 . . . . . 6 (𝑦 = {𝑧} β†’ ({𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin ↔ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin))
5449, 53anbi12d 632 . . . . 5 (𝑦 = {𝑧} β†’ ((𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin) ↔ (𝑧 ∈ {𝑧} ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin)))
5554rspcev 3613 . . . 4 (({𝑧} ∈ 𝒫 𝑋 ∧ (𝑧 ∈ {𝑧} ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin)) β†’ βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin))
564, 6, 48, 55syl12anc 836 . . 3 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin))
5756ralrimiva 3147 . 2 (𝑋 ∈ 𝑉 β†’ βˆ€π‘§ ∈ 𝑋 βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin))
58 unipw 5451 . . . 4 βˆͺ 𝒫 𝑋 = 𝑋
5958eqcomi 2742 . . 3 𝑋 = βˆͺ 𝒫 𝑋
6010unisngl 23031 . . 3 𝑋 = βˆͺ 𝐢
6159, 60islocfin 23021 . 2 (𝐢 ∈ (LocFinβ€˜π’« 𝑋) ↔ (𝒫 𝑋 ∈ Top ∧ 𝑋 = 𝑋 ∧ βˆ€π‘§ ∈ 𝑋 βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin)))
621, 2, 57, 61syl3anbrc 1344 1 (𝑋 ∈ 𝑉 β†’ 𝐢 ∈ (LocFinβ€˜π’« 𝑋))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433   ∩ cin 3948  βˆ…c0 4323  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909  β€˜cfv 6544  Fincfn 8939  Topctop 22395  LocFinclocfin 23008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-om 7856  df-1o 8466  df-en 8940  df-fin 8943  df-top 22396  df-locfin 23011
This theorem is referenced by:  dispcmp  32839
  Copyright terms: Public domain W3C validator