Theorem chincli 29239

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 3515	. . 3 ⊢ 𝐴 ∈ V
3		chjcl.2	. . . 4 ⊢ 𝐵 ∈ Cℋ
4	3	elexi 3515	. . 3 ⊢ 𝐵 ∈ V
5	2, 4	intpr 4911	. 2 ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
6	1, 3	pm3.2i 473	. . . . 5 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ )
7	2, 4	prss 4755	. . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ↔ {𝐴, 𝐵} ⊆ Cℋ )
8	6, 7	mpbi 232	. . . 4 ⊢ {𝐴, 𝐵} ⊆ Cℋ
9	2	prnz 4714	. . . 4 ⊢ {𝐴, 𝐵} ≠ ∅
10	8, 9	pm3.2i 473	. . 3 ⊢ ({𝐴, 𝐵} ⊆ Cℋ ∧ {𝐴, 𝐵} ≠ ∅)
11	10	chintcli 29110	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2912	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

Syntax hints:   ∧ wa 398   ∈ wcel 2114   ≠ wne 3018   ∩ cin 3937   ⊆ wss 3938  ∅c0 4293  {cpr 4571  ∩ cint 4878   C_ℋ cch 28708

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-1cn 10597  ax-addcl 10599  ax-hilex 28778  ax-hfvadd 28779  ax-hv0cl 28782  ax-hfvmul 28784

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-map 8410  df-nn 11641  df-sh 28986  df-ch 29000

This theorem is referenced by:  chdmm1i  29256  chdmj1i  29260  chincl  29278  ledii  29315  lejdii  29317  lejdiri  29318  pjoml2i  29364  pjoml3i  29365  pjoml4i  29366  pjoml6i  29368  cmcmlem  29370  cmcm2i  29372  cmbr2i  29375  cmbr3i  29379  cmm1i  29385  fh3i  29402  fh4i  29403  cm2mi  29405  qlaxr3i  29415  osumcori  29422  osumcor2i  29423  spansnm0i  29429  5oai  29440  3oalem5  29445  3oalem6  29446  3oai  29447  pjssmii  29460  pjssge0ii  29461  pjcji  29463  pjocini  29477  mayetes3i  29508  pjssdif2i  29953  pjssdif1i  29954  pjin1i  29971  pjin3i  29973  pjclem1  29974  pjclem4  29978  pjci  29979  pjcmul1i  29980  pjcmul2i  29981  pj3si  29986  pj3cor1i  29988  stji1i  30021  stm1i  30022  stm1add3i  30026  jpi  30049  golem1  30050  golem2  30051  goeqi  30052  stcltrlem2  30056  mdslle1i  30096  mdslj1i  30098  mdslj2i  30099  mdsl1i  30100  mdsl2i  30101  mdsl2bi  30102  cvmdi  30103  mdslmd1lem1  30104  mdslmd1lem2  30105  mdslmd1i  30108  mdsldmd1i  30110  mdslmd3i  30111  mdslmd4i  30112  csmdsymi  30113  mdexchi  30114  hatomistici  30141  chrelat2i  30144  cvexchlem  30147  cvexchi  30148  sumdmdlem2  30198  mdcompli  30208  dmdcompli  30209  mddmdin0i  30210