Theorem chincli 31442

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

Syntax hints:   ∧ wa 395   ∈ wcel 2113   ≠ wne 2929   ∩ cin 3897   ⊆ wss 3898  ∅c0 4282  {cpr 4577  ∩ cint 4897   C_ℋ cch 30911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-1cn 11071  ax-addcl 11073  ax-hilex 30981  ax-hfvadd 30982  ax-hv0cl 30985  ax-hfvmul 30987

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-int 4898  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-map 8758  df-nn 12133  df-sh 31189  df-ch 31203

This theorem is referenced by:  chdmm1i  31459  chdmj1i  31463  chincl  31481  ledii  31518  lejdii  31520  lejdiri  31521  pjoml2i  31567  pjoml3i  31568  pjoml4i  31569  pjoml6i  31571  cmcmlem  31573  cmcm2i  31575  cmbr2i  31578  cmbr3i  31582  cmm1i  31588  fh3i  31605  fh4i  31606  cm2mi  31608  qlaxr3i  31618  osumcori  31625  osumcor2i  31626  spansnm0i  31632  5oai  31643  3oalem5  31648  3oalem6  31649  3oai  31650  pjssmii  31663  pjssge0ii  31664  pjcji  31666  pjocini  31680  mayetes3i  31711  pjssdif2i  32156  pjssdif1i  32157  pjin1i  32174  pjin3i  32176  pjclem1  32177  pjclem4  32181  pjci  32182  pjcmul1i  32183  pjcmul2i  32184  pj3si  32189  pj3cor1i  32191  stji1i  32224  stm1i  32225  stm1add3i  32229  jpi  32252  golem1  32253  golem2  32254  goeqi  32255  stcltrlem2  32259  mdslle1i  32299  mdslj1i  32301  mdslj2i  32302  mdsl1i  32303  mdsl2i  32304  mdsl2bi  32305  cvmdi  32306  mdslmd1lem1  32307  mdslmd1lem2  32308  mdslmd1i  32311  mdsldmd1i  32313  mdslmd3i  32314  mdslmd4i  32315  csmdsymi  32316  mdexchi  32317  hatomistici  32344  chrelat2i  32347  cvexchlem  32350  cvexchi  32351  sumdmdlem2  32401  mdcompli  32411  dmdcompli  32412  mddmdin0i  32413