Theorem chincli 31290

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 4989	. 2 ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
6	1, 3	pm3.2i 469	. . . . 5 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ )
7	2, 4	prss 4828	. . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ↔ {𝐴, 𝐵} ⊆ Cℋ )
8	6, 7	mpbi 229	. . . 4 ⊢ {𝐴, 𝐵} ⊆ Cℋ
9	2	prnz 4786	. . . 4 ⊢ {𝐴, 𝐵} ≠ ∅
10	8, 9	pm3.2i 469	. . 3 ⊢ ({𝐴, 𝐵} ⊆ Cℋ ∧ {𝐴, 𝐵} ≠ ∅)
11	10	chintcli 31161	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2826	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

Syntax hints:   ∧ wa 394   ∈ wcel 2098   ≠ wne 2937   ∩ cin 3948   ⊆ wss 3949  ∅c0 4326  {cpr 4634  ∩ cint 4953   C_ℋ cch 30759

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-1cn 11204  ax-addcl 11206  ax-hilex 30829  ax-hfvadd 30830  ax-hv0cl 30833  ax-hfvmul 30835

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-map 8853  df-nn 12251  df-sh 31037  df-ch 31051

This theorem is referenced by:  chdmm1i  31307  chdmj1i  31311  chincl  31329  ledii  31366  lejdii  31368  lejdiri  31369  pjoml2i  31415  pjoml3i  31416  pjoml4i  31417  pjoml6i  31419  cmcmlem  31421  cmcm2i  31423  cmbr2i  31426  cmbr3i  31430  cmm1i  31436  fh3i  31453  fh4i  31454  cm2mi  31456  qlaxr3i  31466  osumcori  31473  osumcor2i  31474  spansnm0i  31480  5oai  31491  3oalem5  31496  3oalem6  31497  3oai  31498  pjssmii  31511  pjssge0ii  31512  pjcji  31514  pjocini  31528  mayetes3i  31559  pjssdif2i  32004  pjssdif1i  32005  pjin1i  32022  pjin3i  32024  pjclem1  32025  pjclem4  32029  pjci  32030  pjcmul1i  32031  pjcmul2i  32032  pj3si  32037  pj3cor1i  32039  stji1i  32072  stm1i  32073  stm1add3i  32077  jpi  32100  golem1  32101  golem2  32102  goeqi  32103  stcltrlem2  32107  mdslle1i  32147  mdslj1i  32149  mdslj2i  32150  mdsl1i  32151  mdsl2i  32152  mdsl2bi  32153  cvmdi  32154  mdslmd1lem1  32155  mdslmd1lem2  32156  mdslmd1i  32159  mdsldmd1i  32161  mdslmd3i  32162  mdslmd4i  32163  csmdsymi  32164  mdexchi  32165  hatomistici  32192  chrelat2i  32195  cvexchlem  32198  cvexchi  32199  sumdmdlem2  32249  mdcompli  32259  dmdcompli  32260  mddmdin0i  32261