Theorem chincli 31435

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 4772	. . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ↔ {𝐴, 𝐵} ⊆ Cℋ )
8	6, 7	mpbi 230	. . . 4 ⊢ {𝐴, 𝐵} ⊆ Cℋ
9	2	prnz 4730	. . . 4 ⊢ {𝐴, 𝐵} ≠ ∅
10	8, 9	pm3.2i 470	. . 3 ⊢ ({𝐴, 𝐵} ⊆ Cℋ ∧ {𝐴, 𝐵} ≠ ∅)
11	10	chintcli 31306	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2828	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

Syntax hints:   ∧ wa 395   ∈ wcel 2111   ≠ wne 2928   ∩ cin 3901   ⊆ wss 3902  ∅c0 4283  {cpr 4578  ∩ cint 4897   C_ℋ cch 30904

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5217  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-cnex 11059  ax-1cn 11061  ax-addcl 11063  ax-hilex 30974  ax-hfvadd 30975  ax-hv0cl 30978  ax-hfvmul 30980

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-int 4898  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-map 8752  df-nn 12123  df-sh 31182  df-ch 31196

This theorem is referenced by:  chdmm1i  31452  chdmj1i  31456  chincl  31474  ledii  31511  lejdii  31513  lejdiri  31514  pjoml2i  31560  pjoml3i  31561  pjoml4i  31562  pjoml6i  31564  cmcmlem  31566  cmcm2i  31568  cmbr2i  31571  cmbr3i  31575  cmm1i  31581  fh3i  31598  fh4i  31599  cm2mi  31601  qlaxr3i  31611  osumcori  31618  osumcor2i  31619  spansnm0i  31625  5oai  31636  3oalem5  31641  3oalem6  31642  3oai  31643  pjssmii  31656  pjssge0ii  31657  pjcji  31659  pjocini  31673  mayetes3i  31704  pjssdif2i  32149  pjssdif1i  32150  pjin1i  32167  pjin3i  32169  pjclem1  32170  pjclem4  32174  pjci  32175  pjcmul1i  32176  pjcmul2i  32177  pj3si  32182  pj3cor1i  32184  stji1i  32217  stm1i  32218  stm1add3i  32222  jpi  32245  golem1  32246  golem2  32247  goeqi  32248  stcltrlem2  32252  mdslle1i  32292  mdslj1i  32294  mdslj2i  32295  mdsl1i  32296  mdsl2i  32297  mdsl2bi  32298  cvmdi  32299  mdslmd1lem1  32300  mdslmd1lem2  32301  mdslmd1i  32304  mdsldmd1i  32306  mdslmd3i  32307  mdslmd4i  32308  csmdsymi  32309  mdexchi  32310  hatomistici  32337  chrelat2i  32340  cvexchlem  32343  cvexchi  32344  sumdmdlem2  32394  mdcompli  32404  dmdcompli  32405  mddmdin0i  32406