Theorem chincli 31821

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 3477	. . 3 ⊢ 𝐴 ∈ V
3		chjcl.2	. . . 4 ⊢ 𝐵 ∈ Cℋ
4	3	elexi 3477	. . 3 ⊢ 𝐵 ∈ V
5	2, 4	intpr 4947	. 2 ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
6	1, 3	pm3.2i 475	. . . . 5 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ )
7	2, 4	prss 4786	. . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ↔ {𝐴, 𝐵} ⊆ Cℋ )
8	6, 7	mpbi 233	. . . 4 ⊢ {𝐴, 𝐵} ⊆ Cℋ
9	2	prnz 4743	. . . 4 ⊢ {𝐴, 𝐵} ≠ ∅
10	8, 9	pm3.2i 475	. . 3 ⊢ ({𝐴, 𝐵} ⊆ Cℋ ∧ {𝐴, 𝐵} ≠ ∅)
11	10	chintcli 31692	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2860	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

This proof depends on syntax axioms:   ∧ wa 400   ∈ wcel 2143   ≠ wne 2958   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  {cpr 4591  ∩ cint 4912   C_ℋ cch 31290

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11160  ax-1cn 11162  ax-addcl 11164  ax-hilex 31360  ax-hfvadd 31361  ax-hv0cl 31364  ax-hfvmul 31366

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-map 8822  df-nn 12238  df-sh 31568  df-ch 31582

This theorem is used by:  chdmm1i  31838  chdmj1i  31842  chincl  31860  ledii  31897  lejdii  31899  lejdiri  31900  pjoml2i  31946  pjoml3i  31947  pjoml4i  31948  pjoml6i  31950  cmcmlem  31952  cmcm2i  31954  cmbr2i  31957  cmbr3i  31961  cmm1i  31967  fh3i  31984  fh4i  31985  cm2mi  31987  qlaxr3i  31997  osumcori  32004  osumcor2i  32005  spansnm0i  32011  5oai  32022  3oalem5  32027  3oalem6  32028  3oai  32029  pjssmii  32042  pjssge0ii  32043  pjcji  32045  pjocini  32059  mayetes3i  32090  pjssdif2i  32535  pjssdif1i  32536  pjin1i  32553  pjin3i  32555  pjclem1  32556  pjclem4  32560  pjci  32561  pjcmul1i  32562  pjcmul2i  32563  pj3si  32568  pj3cor1i  32570  stji1i  32603  stm1i  32604  stm1add3i  32608  jpi  32631  golem1  32632  golem2  32633  goeqi  32634  stcltrlem2  32638  mdslle1i  32678  mdslj1i  32680  mdslj2i  32681  mdsl1i  32682  mdsl2i  32683  mdsl2bi  32684  cvmdi  32685  mdslmd1lem1  32686  mdslmd1lem2  32687  mdslmd1i  32690  mdsldmd1i  32692  mdslmd3i  32693  mdslmd4i  32694  csmdsymi  32695  mdexchi  32696  hatomistici  32723  chrelat2i  32726  cvexchlem  32729  cvexchi  32730  sumdmdlem2  32780  mdcompli  32790  dmdcompli  32791  mddmdin0i  32792