Theorem chincli 32044

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 3473	. . 3 ⊢ 𝐴 ∈ V
3		chjcl.2	. . . 4 ⊢ 𝐵 ∈ Cℋ
4	3	elexi 3473	. . 3 ⊢ 𝐵 ∈ V
5	2, 4	intpr 4942	. 2 ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
6	1, 3	pm3.2i 476	. . . . 5 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ )
7	2, 4	prss 4781	. . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ↔ {𝐴, 𝐵} ⊆ Cℋ )
8	6, 7	mpbi 233	. . . 4 ⊢ {𝐴, 𝐵} ⊆ Cℋ
9	2	prnz 4738	. . . 4 ⊢ {𝐴, 𝐵} ≠ ∅
10	8, 9	pm3.2i 476	. . 3 ⊢ ({𝐴, 𝐵} ⊆ Cℋ ∧ {𝐴, 𝐵} ≠ ∅)
11	10	chintcli 31915	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2858	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145   ≠ wne 2956   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  {cpr 4586  ∩ cint 4907   C_ℋ cch 31513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-1cn 11239  ax-addcl 11241  ax-hilex 31583  ax-hfvadd 31584  ax-hv0cl 31587  ax-hfvmul 31589

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-map 8833  df-nn 12317  df-sh 31791  df-ch 31805

This theorem is used by:  chdmm1i  32061  chdmj1i  32065  chincl  32083  ledii  32120  lejdii  32122  lejdiri  32123  pjoml2i  32169  pjoml3i  32170  pjoml4i  32171  pjoml6i  32173  cmcmlem  32175  cmcm2i  32177  cmbr2i  32180  cmbr3i  32184  cmm1i  32190  fh3i  32207  fh4i  32208  cm2mi  32210  qlaxr3i  32220  osumcori  32227  osumcor2i  32228  spansnm0i  32234  5oai  32245  3oalem5  32250  3oalem6  32251  3oai  32252  pjssmii  32265  pjssge0ii  32266  pjcji  32268  pjocini  32282  mayetes3i  32313  pjssdif2i  32758  pjssdif1i  32759  pjin1i  32776  pjin3i  32778  pjclem1  32779  pjclem4  32783  pjci  32784  pjcmul1i  32785  pjcmul2i  32786  pj3si  32791  pj3cor1i  32793  stji1i  32826  stm1i  32827  stm1add3i  32831  jpi  32854  golem1  32855  golem2  32856  goeqi  32857  stcltrlem2  32861  mdslle1i  32901  mdslj1i  32903  mdslj2i  32904  mdsl1i  32905  mdsl2i  32906  mdsl2bi  32907  cvmdi  32908  mdslmd1lem1  32909  mdslmd1lem2  32910  mdslmd1i  32913  mdsldmd1i  32915  mdslmd3i  32916  mdslmd4i  32917  csmdsymi  32918  mdexchi  32919  hatomistici  32946  chrelat2i  32949  cvexchlem  32952  cvexchi  32953  sumdmdlem2  33003  mdcompli  33013  dmdcompli  33014  mddmdin0i  33015