Theorem chincli 32092

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 3476	. . 3 ⊢ 𝐴 ∈ V
3		chjcl.2	. . . 4 ⊢ 𝐵 ∈ Cℋ
4	3	elexi 3476	. . 3 ⊢ 𝐵 ∈ V
5	2, 4	intpr 4945	. 2 ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
6	1, 3	pm3.2i 476	. . . . 5 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ )
7	2, 4	prss 4779	. . . . 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 31963	. 2 ⊢ ∩ {𝐴, 𝐵} ∈ Cℋ
12	5, 11	eqeltrri 2861	1 ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2147   ≠ wne 2959   ⊆ wss 3900   ∩ cin 4092  ∅c0 4281  {cpr 4590  ∩ cint 4910   C_ℋ cch 31561

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-1cn 11285  ax-addcl 11287  ax-hilex 31631  ax-hfvadd 31632  ax-hv0cl 31635  ax-hfvmul 31637

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-map 8877  df-nn 12363  df-sh 31839  df-ch 31853

This theorem is used by:  chdmm1i  32109  chdmj1i  32113  chincl  32131  ledii  32168  lejdii  32170  lejdiri  32171  pjoml2i  32217  pjoml3i  32218  pjoml4i  32219  pjoml6i  32221  cmcmlem  32223  cmcm2i  32225  cmbr2i  32228  cmbr3i  32232  cmm1i  32238  fh3i  32255  fh4i  32256  cm2mi  32258  qlaxr3i  32268  osumcori  32275  osumcor2i  32276  spansnm0i  32282  5oai  32293  3oalem5  32298  3oalem6  32299  3oai  32300  pjssmii  32313  pjssge0ii  32314  pjcji  32316  pjocini  32330  mayetes3i  32361  pjssdif2i  32806  pjssdif1i  32807  pjin1i  32824  pjin3i  32826  pjclem1  32827  pjclem4  32831  pjci  32832  pjcmul1i  32833  pjcmul2i  32834  pj3si  32839  pj3cor1i  32841  stji1i  32874  stm1i  32875  stm1add3i  32879  jpi  32902  golem1  32903  golem2  32904  goeqi  32905  stcltrlem2  32909  mdslle1i  32949  mdslj1i  32951  mdslj2i  32952  mdsl1i  32953  mdsl2i  32954  mdsl2bi  32955  cvmdi  32956  mdslmd1lem1  32957  mdslmd1lem2  32958  mdslmd1i  32961  mdsldmd1i  32963  mdslmd3i  32964  mdslmd4i  32965  csmdsymi  32966  mdexchi  32967  hatomistici  32994  chrelat2i  32997  cvexchlem  33000  cvexchi  33001  sumdmdlem2  33051  mdcompli  33061  dmdcompli  33062  mddmdin0i  33063