Theorem chincli 28875

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 3431	. . 3 ⊢ 𝐴 ∈ V
3		chjcl.2	. . . 4 ⊢ 𝐵 ∈ Cℋ
4	3	elexi 3431	. . 3 ⊢ 𝐵 ∈ V
5	2, 4	intpr 4731	. 2 ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
6	1, 3	pm3.2i 464	. . . . 5 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ )
7	2, 4	prss 4570	. . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ↔ {𝐴, 𝐵} ⊆ Cℋ )
8	6, 7	mpbi 222	. . . 4 ⊢ {𝐴, 𝐵} ⊆ Cℋ
9	2	prnz 4530	. . . 4 ⊢ {𝐴, 𝐵} ≠ ∅
10	8, 9	pm3.2i 464	. . 3 ⊢ ({𝐴, 𝐵} ⊆ Cℋ ∧ {𝐴, 𝐵} ≠ ∅)
11	10	chintcli 28746	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2904	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

Syntax hints:   ∧ wa 386   ∈ wcel 2166   ≠ wne 3000   ∩ cin 3798   ⊆ wss 3799  ∅c0 4145  {cpr 4400  ∩ cint 4698   C_ℋ cch 28342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-cnex 10309  ax-1cn 10311  ax-addcl 10313  ax-hilex 28412  ax-hfvadd 28413  ax-hv0cl 28416  ax-hfvmul 28418

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-ral 3123  df-rex 3124  df-reu 3125  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-int 4699  df-iun 4743  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-om 7328  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-map 8125  df-nn 11352  df-sh 28620  df-ch 28634

This theorem is referenced by:  chdmm1i  28892  chdmj1i  28896  chincl  28914  ledii  28951  lejdii  28953  lejdiri  28954  pjoml2i  29000  pjoml3i  29001  pjoml4i  29002  pjoml6i  29004  cmcmlem  29006  cmcm2i  29008  cmbr2i  29011  cmbr3i  29015  cmm1i  29021  fh3i  29038  fh4i  29039  cm2mi  29041  qlaxr3i  29051  osumcori  29058  osumcor2i  29059  spansnm0i  29065  5oai  29076  3oalem5  29081  3oalem6  29082  3oai  29083  pjssmii  29096  pjssge0ii  29097  pjcji  29099  pjocini  29113  mayetes3i  29144  pjssdif2i  29589  pjssdif1i  29590  pjin1i  29607  pjin3i  29609  pjclem1  29610  pjclem4  29614  pjci  29615  pjcmul1i  29616  pjcmul2i  29617  pj3si  29622  pj3cor1i  29624  stji1i  29657  stm1i  29658  stm1add3i  29662  jpi  29685  golem1  29686  golem2  29687  goeqi  29688  stcltrlem2  29692  mdslle1i  29732  mdslj1i  29734  mdslj2i  29735  mdsl1i  29736  mdsl2i  29737  mdsl2bi  29738  cvmdi  29739  mdslmd1lem1  29740  mdslmd1lem2  29741  mdslmd1i  29744  mdsldmd1i  29746  mdslmd3i  29747  mdslmd4i  29748  csmdsymi  29749  mdexchi  29750  hatomistici  29777  chrelat2i  29780  cvexchlem  29783  cvexchi  29784  sumdmdlem2  29834  mdcompli  29844  dmdcompli  29845  mddmdin0i  29846