Theorem chincli 29850

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 3453	. . 3 ⊢ 𝐴 ∈ V
3		chjcl.2	. . . 4 ⊢ 𝐵 ∈ Cℋ
4	3	elexi 3453	. . 3 ⊢ 𝐵 ∈ V
5	2, 4	intpr 4916	. 2 ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
6	1, 3	pm3.2i 470	. . . . 5 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ )
7	2, 4	prss 4756	. . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ↔ {𝐴, 𝐵} ⊆ Cℋ )
8	6, 7	mpbi 229	. . . 4 ⊢ {𝐴, 𝐵} ⊆ Cℋ
9	2	prnz 4716	. . . 4 ⊢ {𝐴, 𝐵} ≠ ∅
10	8, 9	pm3.2i 470	. . 3 ⊢ ({𝐴, 𝐵} ⊆ Cℋ ∧ {𝐴, 𝐵} ≠ ∅)
11	10	chintcli 29721	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2831	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

Syntax hints:   ∧ wa 395   ∈ wcel 2101   ≠ wne 2938   ∩ cin 3888   ⊆ wss 3889  ∅c0 4259  {cpr 4566  ∩ cint 4882   C_ℋ cch 29319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-rep 5212  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7608  ax-cnex 10955  ax-1cn 10957  ax-addcl 10959  ax-hilex 29389  ax-hfvadd 29390  ax-hv0cl 29393  ax-hfvmul 29395

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3223  df-rab 3224  df-v 3436  df-sbc 3719  df-csb 3835  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3908  df-nul 4260  df-if 4463  df-pw 4538  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-int 4883  df-iun 4929  df-br 5078  df-opab 5140  df-mpt 5161  df-tr 5195  df-id 5491  df-eprel 5497  df-po 5505  df-so 5506  df-fr 5546  df-we 5548  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6399  df-fun 6449  df-fn 6450  df-f 6451  df-f1 6452  df-fo 6453  df-f1o 6454  df-fv 6455  df-ov 7298  df-oprab 7299  df-mpo 7300  df-om 7733  df-2nd 7852  df-frecs 8117  df-wrecs 8148  df-recs 8222  df-rdg 8261  df-map 8637  df-nn 12002  df-sh 29597  df-ch 29611

This theorem is referenced by:  chdmm1i  29867  chdmj1i  29871  chincl  29889  ledii  29926  lejdii  29928  lejdiri  29929  pjoml2i  29975  pjoml3i  29976  pjoml4i  29977  pjoml6i  29979  cmcmlem  29981  cmcm2i  29983  cmbr2i  29986  cmbr3i  29990  cmm1i  29996  fh3i  30013  fh4i  30014  cm2mi  30016  qlaxr3i  30026  osumcori  30033  osumcor2i  30034  spansnm0i  30040  5oai  30051  3oalem5  30056  3oalem6  30057  3oai  30058  pjssmii  30071  pjssge0ii  30072  pjcji  30074  pjocini  30088  mayetes3i  30119  pjssdif2i  30564  pjssdif1i  30565  pjin1i  30582  pjin3i  30584  pjclem1  30585  pjclem4  30589  pjci  30590  pjcmul1i  30591  pjcmul2i  30592  pj3si  30597  pj3cor1i  30599  stji1i  30632  stm1i  30633  stm1add3i  30637  jpi  30660  golem1  30661  golem2  30662  goeqi  30663  stcltrlem2  30667  mdslle1i  30707  mdslj1i  30709  mdslj2i  30710  mdsl1i  30711  mdsl2i  30712  mdsl2bi  30713  cvmdi  30714  mdslmd1lem1  30715  mdslmd1lem2  30716  mdslmd1i  30719  mdsldmd1i  30721  mdslmd3i  30722  mdslmd4i  30723  csmdsymi  30724  mdexchi  30725  hatomistici  30752  chrelat2i  30755  cvexchlem  30758  cvexchi  30759  sumdmdlem2  30809  mdcompli  30819  dmdcompli  30820  mddmdin0i  30821