Theorem chincli 30700

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

Step	Hyp	Ref	Expression
1		ch0le.1	. . . 4 ⊢ 𝐴 ∈ Cℋ
2	1	elexi 3493	. . 3 ⊢ 𝐴 ∈ V
3		chjcl.2	. . . 4 ⊢ 𝐵 ∈ Cℋ
4	3	elexi 3493	. . 3 ⊢ 𝐵 ∈ V
5	2, 4	intpr 4985	. 2 ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
6	1, 3	pm3.2i 471	. . . . 5 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ )
7	2, 4	prss 4822	. . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ↔ {𝐴, 𝐵} ⊆ Cℋ )
8	6, 7	mpbi 229	. . . 4 ⊢ {𝐴, 𝐵} ⊆ Cℋ
9	2	prnz 4780	. . . 4 ⊢ {𝐴, 𝐵} ≠ ∅
10	8, 9	pm3.2i 471	. . 3 ⊢ ({𝐴, 𝐵} ⊆ Cℋ ∧ {𝐴, 𝐵} ≠ ∅)
11	10	chintcli 30571	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2830	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

Syntax hints:   ∧ wa 396   ∈ wcel 2106   ≠ wne 2940   ∩ cin 3946   ⊆ wss 3947  ∅c0 4321  {cpr 4629  ∩ cint 4949   C_ℋ cch 30169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-1cn 11164  ax-addcl 11166  ax-hilex 30239  ax-hfvadd 30240  ax-hv0cl 30243  ax-hfvmul 30245

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-map 8818  df-nn 12209  df-sh 30447  df-ch 30461

This theorem is referenced by:  chdmm1i  30717  chdmj1i  30721  chincl  30739  ledii  30776  lejdii  30778  lejdiri  30779  pjoml2i  30825  pjoml3i  30826  pjoml4i  30827  pjoml6i  30829  cmcmlem  30831  cmcm2i  30833  cmbr2i  30836  cmbr3i  30840  cmm1i  30846  fh3i  30863  fh4i  30864  cm2mi  30866  qlaxr3i  30876  osumcori  30883  osumcor2i  30884  spansnm0i  30890  5oai  30901  3oalem5  30906  3oalem6  30907  3oai  30908  pjssmii  30921  pjssge0ii  30922  pjcji  30924  pjocini  30938  mayetes3i  30969  pjssdif2i  31414  pjssdif1i  31415  pjin1i  31432  pjin3i  31434  pjclem1  31435  pjclem4  31439  pjci  31440  pjcmul1i  31441  pjcmul2i  31442  pj3si  31447  pj3cor1i  31449  stji1i  31482  stm1i  31483  stm1add3i  31487  jpi  31510  golem1  31511  golem2  31512  goeqi  31513  stcltrlem2  31517  mdslle1i  31557  mdslj1i  31559  mdslj2i  31560  mdsl1i  31561  mdsl2i  31562  mdsl2bi  31563  cvmdi  31564  mdslmd1lem1  31565  mdslmd1lem2  31566  mdslmd1i  31569  mdsldmd1i  31571  mdslmd3i  31572  mdslmd4i  31573  csmdsymi  31574  mdexchi  31575  hatomistici  31602  chrelat2i  31605  cvexchlem  31608  cvexchi  31609  sumdmdlem2  31659  mdcompli  31669  dmdcompli  31670  mddmdin0i  31671