![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > chincli | Structured version Visualization version GIF version |
Description: Closure of Hilbert lattice intersection. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ch0le.1 | ⊢ 𝐴 ∈ Cℋ |
chjcl.2 | ⊢ 𝐵 ∈ Cℋ |
Ref | Expression |
---|---|
chincli | ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ |
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ℋ |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |