HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  chincli Structured version   Visualization version   GIF version

Theorem chincli 28649
Description: Closure of Hilbert lattice intersection. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
Hypotheses
Ref Expression
ch0le.1 𝐴C
chjcl.2 𝐵C
Assertion
Ref Expression
chincli (𝐴𝐵) ∈ C

Proof of Theorem chincli
StepHypRef Expression
1 ch0le.1 . . . 4 𝐴C
21elexi 3353 . . 3 𝐴 ∈ V
3 chjcl.2 . . . 4 𝐵C
43elexi 3353 . . 3 𝐵 ∈ V
52, 4intpr 4662 . 2 {𝐴, 𝐵} = (𝐴𝐵)
61, 3pm3.2i 470 . . . . 5 (𝐴C𝐵C )
72, 4prss 4496 . . . . 5 ((𝐴C𝐵C ) ↔ {𝐴, 𝐵} ⊆ C )
86, 7mpbi 220 . . . 4 {𝐴, 𝐵} ⊆ C
92prnz 4453 . . . 4 {𝐴, 𝐵} ≠ ∅
108, 9pm3.2i 470 . . 3 ({𝐴, 𝐵} ⊆ C ∧ {𝐴, 𝐵} ≠ ∅)
1110chintcli 28520 . 2 {𝐴, 𝐵} ∈ C
125, 11eqeltrri 2836 1 (𝐴𝐵) ∈ C
Colors of variables: wff setvar class
Syntax hints:  wa 383  wcel 2139  wne 2932  cin 3714  wss 3715  c0 4058  {cpr 4323   cint 4627   C cch 28116
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 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-i2m1 10216  ax-1ne0 10217  ax-rrecex 10220  ax-cnre 10221  ax-hilex 28186  ax-hfvadd 28187  ax-hv0cl 28190  ax-hfvmul 28192
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  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-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  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-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  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 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-map 8027  df-nn 11233  df-sh 28394  df-ch 28408
This theorem is referenced by:  chdmm1i  28666  chdmj1i  28670  chincl  28688  ledii  28725  lejdii  28727  lejdiri  28728  pjoml2i  28774  pjoml3i  28775  pjoml4i  28776  pjoml6i  28778  cmcmlem  28780  cmcm2i  28782  cmbr2i  28785  cmbr3i  28789  cmm1i  28795  fh3i  28812  fh4i  28813  cm2mi  28815  qlaxr3i  28825  osumcori  28832  osumcor2i  28833  spansnm0i  28839  5oai  28850  3oalem5  28855  3oalem6  28856  3oai  28857  pjssmii  28870  pjssge0ii  28871  pjcji  28873  pjocini  28887  mayetes3i  28918  pjssdif2i  29363  pjssdif1i  29364  pjin1i  29381  pjin3i  29383  pjclem1  29384  pjclem4  29388  pjci  29389  pjcmul1i  29390  pjcmul2i  29391  pj3si  29396  pj3cor1i  29398  stji1i  29431  stm1i  29432  stm1add3i  29436  jpi  29459  golem1  29460  golem2  29461  goeqi  29462  stcltrlem2  29466  mdslle1i  29506  mdslj1i  29508  mdslj2i  29509  mdsl1i  29510  mdsl2i  29511  mdsl2bi  29512  cvmdi  29513  mdslmd1lem1  29514  mdslmd1lem2  29515  mdslmd1i  29518  mdsldmd1i  29520  mdslmd3i  29521  mdslmd4i  29522  csmdsymi  29523  mdexchi  29524  hatomistici  29551  chrelat2i  29554  cvexchlem  29557  cvexchi  29558  sumdmdlem2  29608  mdcompli  29618  dmdcompli  29619  mddmdin0i  29620
  Copyright terms: Public domain W3C validator