Theorem chincli 31488

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 3500	. . 3 ⊢ 𝐴 ∈ V
3		chjcl.2	. . . 4 ⊢ 𝐵 ∈ Cℋ
4	3	elexi 3500	. . 3 ⊢ 𝐵 ∈ V
5	2, 4	intpr 4986	. 2 ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
6	1, 3	pm3.2i 470	. . . . 5 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ )
7	2, 4	prss 4824	. . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ↔ {𝐴, 𝐵} ⊆ Cℋ )
8	6, 7	mpbi 230	. . . 4 ⊢ {𝐴, 𝐵} ⊆ Cℋ
9	2	prnz 4781	. . . 4 ⊢ {𝐴, 𝐵} ≠ ∅
10	8, 9	pm3.2i 470	. . 3 ⊢ ({𝐴, 𝐵} ⊆ Cℋ ∧ {𝐴, 𝐵} ≠ ∅)
11	10	chintcli 31359	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2835	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

Syntax hints:   ∧ wa 395   ∈ wcel 2105   ≠ wne 2937   ∩ cin 3961   ⊆ wss 3962  ∅c0 4338  {cpr 4632  ∩ cint 4950   C_ℋ cch 30957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-1cn 11210  ax-addcl 11212  ax-hilex 31027  ax-hfvadd 31028  ax-hv0cl 31031  ax-hfvmul 31033

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-map 8866  df-nn 12264  df-sh 31235  df-ch 31249

This theorem is referenced by:  chdmm1i  31505  chdmj1i  31509  chincl  31527  ledii  31564  lejdii  31566  lejdiri  31567  pjoml2i  31613  pjoml3i  31614  pjoml4i  31615  pjoml6i  31617  cmcmlem  31619  cmcm2i  31621  cmbr2i  31624  cmbr3i  31628  cmm1i  31634  fh3i  31651  fh4i  31652  cm2mi  31654  qlaxr3i  31664  osumcori  31671  osumcor2i  31672  spansnm0i  31678  5oai  31689  3oalem5  31694  3oalem6  31695  3oai  31696  pjssmii  31709  pjssge0ii  31710  pjcji  31712  pjocini  31726  mayetes3i  31757  pjssdif2i  32202  pjssdif1i  32203  pjin1i  32220  pjin3i  32222  pjclem1  32223  pjclem4  32227  pjci  32228  pjcmul1i  32229  pjcmul2i  32230  pj3si  32235  pj3cor1i  32237  stji1i  32270  stm1i  32271  stm1add3i  32275  jpi  32298  golem1  32299  golem2  32300  goeqi  32301  stcltrlem2  32305  mdslle1i  32345  mdslj1i  32347  mdslj2i  32348  mdsl1i  32349  mdsl2i  32350  mdsl2bi  32351  cvmdi  32352  mdslmd1lem1  32353  mdslmd1lem2  32354  mdslmd1i  32357  mdsldmd1i  32359  mdslmd3i  32360  mdslmd4i  32361  csmdsymi  32362  mdexchi  32363  hatomistici  32390  chrelat2i  32393  cvexchlem  32396  cvexchi  32397  sumdmdlem2  32447  mdcompli  32457  dmdcompli  32458  mddmdin0i  32459