Theorem chincli 31404

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 3459	. . 3 ⊢ 𝐴 ∈ V
3		chjcl.2	. . . 4 ⊢ 𝐵 ∈ Cℋ
4	3	elexi 3459	. . 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 31275	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2825	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

Syntax hints:   ∧ wa 395   ∈ wcel 2109   ≠ wne 2925   ∩ cin 3902   ⊆ wss 3903  ∅c0 4284  {cpr 4579  ∩ cint 4896   C_ℋ cch 30873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-1cn 11067  ax-addcl 11069  ax-hilex 30943  ax-hfvadd 30944  ax-hv0cl 30947  ax-hfvmul 30949

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  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 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-map 8755  df-nn 12129  df-sh 31151  df-ch 31165

This theorem is referenced by:  chdmm1i  31421  chdmj1i  31425  chincl  31443  ledii  31480  lejdii  31482  lejdiri  31483  pjoml2i  31529  pjoml3i  31530  pjoml4i  31531  pjoml6i  31533  cmcmlem  31535  cmcm2i  31537  cmbr2i  31540  cmbr3i  31544  cmm1i  31550  fh3i  31567  fh4i  31568  cm2mi  31570  qlaxr3i  31580  osumcori  31587  osumcor2i  31588  spansnm0i  31594  5oai  31605  3oalem5  31610  3oalem6  31611  3oai  31612  pjssmii  31625  pjssge0ii  31626  pjcji  31628  pjocini  31642  mayetes3i  31673  pjssdif2i  32118  pjssdif1i  32119  pjin1i  32136  pjin3i  32138  pjclem1  32139  pjclem4  32143  pjci  32144  pjcmul1i  32145  pjcmul2i  32146  pj3si  32151  pj3cor1i  32153  stji1i  32186  stm1i  32187  stm1add3i  32191  jpi  32214  golem1  32215  golem2  32216  goeqi  32217  stcltrlem2  32221  mdslle1i  32261  mdslj1i  32263  mdslj2i  32264  mdsl1i  32265  mdsl2i  32266  mdsl2bi  32267  cvmdi  32268  mdslmd1lem1  32269  mdslmd1lem2  32270  mdslmd1i  32273  mdsldmd1i  32275  mdslmd3i  32276  mdslmd4i  32277  csmdsymi  32278  mdexchi  32279  hatomistici  32306  chrelat2i  32309  cvexchlem  32312  cvexchi  32313  sumdmdlem2  32363  mdcompli  32373  dmdcompli  32374  mddmdin0i  32375