Theorem chincli 28319

Description: Closure of Hilbert lattice intersection. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ch0le.1	|- A e. CH
chjcl.2	|- B e. CH

Assertion

Ref	Expression
chincli	|- ( A i^i B ) e. CH

Proof of Theorem chincli

Step	Hyp	Ref	Expression
1		ch0le.1	. . . 4 |- A e. CH
2	1	elexi 3213	. . 3 |- A e. _V
3		chjcl.2	. . . 4 |- B e. CH
4	3	elexi 3213	. . 3 |- B e. _V
5	2, 4	intpr 4510	. 2 |- |^| { A , B } = ( A i^i B )
6	1, 3	pm3.2i 471	. . . . 5 |- ( A e. CH /\ B e. CH )
7	2, 4	prss 4351	. . . . 5 |- ( ( A e. CH /\ B e. CH ) <-> { A , B } C_ CH )
8	6, 7	mpbi 220	. . . 4 |- { A , B } C_ CH
9	2	prnz 4310	. . . 4 |- { A , B } =/= (/)
10	8, 9	pm3.2i 471	. . 3 |- ( { A , B } C_ CH /\ { A , B } =/= (/) )
11	10	chintcli 28190	. 2 |- |^| { A , B } e. CH
12	5, 11	eqeltrri 2698	1 |- ( A i^i B ) e. CH

Syntax hints:   /\ wa 384   e. wcel 1990   =/= wne 2794   i^i cin 3573   C_ wss 3574   (/)c0 3915   {cpr 4179   |^|cint 4475   CHcch 27786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009  ax-hilex 27856  ax-hfvadd 27857  ax-hv0cl 27860  ax-hfvmul 27862

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-map 7859  df-nn 11021  df-sh 28064  df-ch 28078

This theorem is referenced by:  chdmm1i  28336  chdmj1i  28340  chincl  28358  ledii  28395  lejdii  28397  lejdiri  28398  pjoml2i  28444  pjoml3i  28445  pjoml4i  28446  pjoml6i  28448  cmcmlem  28450  cmcm2i  28452  cmbr2i  28455  cmbr3i  28459  cmm1i  28465  fh3i  28482  fh4i  28483  cm2mi  28485  qlaxr3i  28495  osumcori  28502  osumcor2i  28503  spansnm0i  28509  5oai  28520  3oalem5  28525  3oalem6  28526  3oai  28527  pjssmii  28540  pjssge0ii  28541  pjcji  28543  pjocini  28557  mayetes3i  28588  pjssdif2i  29033  pjssdif1i  29034  pjin1i  29051  pjin3i  29053  pjclem1  29054  pjclem4  29058  pjci  29059  pjcmul1i  29060  pjcmul2i  29061  pj3si  29066  pj3cor1i  29068  stji1i  29101  stm1i  29102  stm1add3i  29106  jpi  29129  golem1  29130  golem2  29131  goeqi  29132  stcltrlem2  29136  mdslle1i  29176  mdslj1i  29178  mdslj2i  29179  mdsl1i  29180  mdsl2i  29181  mdsl2bi  29182  cvmdi  29183  mdslmd1lem1  29184  mdslmd1lem2  29185  mdslmd1i  29188  mdsldmd1i  29190  mdslmd3i  29191  mdslmd4i  29192  csmdsymi  29193  mdexchi  29194  hatomistici  29221  chrelat2i  29224  cvexchlem  29227  cvexchi  29228  sumdmdlem2  29278  mdcompli  29288  dmdcompli  29289  mddmdin0i  29290