![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > HSE Home > Th. List > choccli | Structured version Unicode version |
Description: Closure of ![]() |
Ref | Expression |
---|---|
choccl.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
choccli |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | choccl.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | choccl 24844 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4501 ax-sep 4511 ax-nul 4519 ax-pow 4568 ax-pr 4629 ax-un 6472 ax-inf2 7948 ax-cnex 9439 ax-resscn 9440 ax-1cn 9441 ax-icn 9442 ax-addcl 9443 ax-addrcl 9444 ax-mulcl 9445 ax-mulrcl 9446 ax-mulcom 9447 ax-addass 9448 ax-mulass 9449 ax-distr 9450 ax-i2m1 9451 ax-1ne0 9452 ax-1rid 9453 ax-rnegex 9454 ax-rrecex 9455 ax-cnre 9456 ax-pre-lttri 9457 ax-pre-lttrn 9458 ax-pre-ltadd 9459 ax-pre-mulgt0 9460 ax-pre-sup 9461 ax-addf 9462 ax-mulf 9463 ax-hilex 24536 ax-hfvadd 24537 ax-hvcom 24538 ax-hvass 24539 ax-hv0cl 24540 ax-hvaddid 24541 ax-hfvmul 24542 ax-hvmulid 24543 ax-hvmulass 24544 ax-hvdistr1 24545 ax-hvdistr2 24546 ax-hvmul0 24547 ax-hfi 24616 ax-his1 24619 ax-his2 24620 ax-his3 24621 ax-his4 24622 ax-hcompl 24739 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3070 df-sbc 3285 df-csb 3387 df-dif 3429 df-un 3431 df-in 3433 df-ss 3440 df-pss 3442 df-nul 3736 df-if 3890 df-pw 3960 df-sn 3976 df-pr 3978 df-tp 3980 df-op 3982 df-uni 4190 df-int 4227 df-iun 4271 df-iin 4272 df-br 4391 df-opab 4449 df-mpt 4450 df-tr 4484 df-eprel 4730 df-id 4734 df-po 4739 df-so 4740 df-fr 4777 df-se 4778 df-we 4779 df-ord 4820 df-on 4821 df-lim 4822 df-suc 4823 df-xp 4944 df-rel 4945 df-cnv 4946 df-co 4947 df-dm 4948 df-rn 4949 df-res 4950 df-ima 4951 df-iota 5479 df-fun 5518 df-fn 5519 df-f 5520 df-f1 5521 df-fo 5522 df-f1o 5523 df-fv 5524 df-isom 5525 df-riota 6151 df-ov 6193 df-oprab 6194 df-mpt2 6195 df-of 6420 df-om 6577 df-1st 6677 df-2nd 6678 df-supp 6791 df-recs 6932 df-rdg 6966 df-1o 7020 df-2o 7021 df-oadd 7024 df-er 7201 df-map 7316 df-pm 7317 df-ixp 7364 df-en 7411 df-dom 7412 df-sdom 7413 df-fin 7414 df-fsupp 7722 df-fi 7762 df-sup 7792 df-oi 7825 df-card 8210 df-cda 8438 df-pnf 9521 df-mnf 9522 df-xr 9523 df-ltxr 9524 df-le 9525 df-sub 9698 df-neg 9699 df-div 10095 df-nn 10424 df-2 10481 df-3 10482 df-4 10483 df-5 10484 df-6 10485 df-7 10486 df-8 10487 df-9 10488 df-10 10489 df-n0 10681 df-z 10748 df-dec 10857 df-uz 10963 df-q 11055 df-rp 11093 df-xneg 11190 df-xadd 11191 df-xmul 11192 df-ioo 11405 df-icc 11408 df-fz 11539 df-fzo 11650 df-seq 11908 df-exp 11967 df-hash 12205 df-cj 12690 df-re 12691 df-im 12692 df-sqr 12826 df-abs 12827 df-clim 13068 df-sum 13266 df-struct 14278 df-ndx 14279 df-slot 14280 df-base 14281 df-sets 14282 df-ress 14283 df-plusg 14353 df-mulr 14354 df-starv 14355 df-sca 14356 df-vsca 14357 df-ip 14358 df-tset 14359 df-ple 14360 df-ds 14362 df-unif 14363 df-hom 14364 df-cco 14365 df-rest 14463 df-topn 14464 df-0g 14482 df-gsum 14483 df-topgen 14484 df-pt 14485 df-prds 14488 df-xrs 14542 df-qtop 14547 df-imas 14548 df-xps 14550 df-mre 14626 df-mrc 14627 df-acs 14629 df-mnd 15517 df-submnd 15567 df-mulg 15650 df-cntz 15937 df-cmn 16383 df-psmet 17918 df-xmet 17919 df-met 17920 df-bl 17921 df-mopn 17922 df-cnfld 17928 df-top 18619 df-bases 18621 df-topon 18622 df-topsp 18623 df-cn 18947 df-cnp 18948 df-lm 18949 df-haus 19035 df-tx 19251 df-hmeo 19444 df-xms 20011 df-ms 20012 df-tms 20013 df-cau 20883 df-grpo 23813 df-gid 23814 df-ginv 23815 df-gdiv 23816 df-ablo 23904 df-vc 24059 df-nv 24105 df-va 24108 df-ba 24109 df-sm 24110 df-0v 24111 df-vs 24112 df-nmcv 24113 df-ims 24114 df-dip 24231 df-hnorm 24505 df-hvsub 24508 df-hlim 24509 df-hcau 24510 df-sh 24744 df-ch 24759 df-oc 24790 |
This theorem is referenced by: pjoc1i 24969 pjoc2i 24976 chsscon3i 24999 chsscon1i 25000 chdmm1i 25015 chdmm2i 25016 chdmm3i 25017 chdmm4i 25018 chdmj1i 25019 chdmj2i 25020 chdmj3i 25021 chdmj4i 25022 sshhococi 25084 h1de2bi 25092 h1de2ctlem 25093 h1de2ci 25094 spanunsni 25117 pjoml2i 25123 pjoml3i 25124 pjoml4i 25125 pjoml6i 25127 cmcmlem 25129 cmcm2i 25131 cmcm3i 25132 cmcm4i 25133 cmbr2i 25134 cmbr3i 25138 cmbr4i 25139 cm0 25147 fh3i 25161 fh4i 25162 cm2mi 25164 qlax5i 25169 qlaxr3i 25174 osumcori 25181 osumcor2i 25182 spansnji 25184 3oalem5 25204 3oalem6 25205 3oai 25206 pjcompi 25210 pjadjii 25212 pjaddii 25213 pjmulii 25215 pjss2i 25218 pjssmii 25219 pjssge0ii 25220 pjcji 25222 pjocini 25236 pjds3i 25251 pjnormi 25259 pjpythi 25260 pjneli 25261 mayetes3i 25268 riesz3i 25601 pjnormssi 25707 pjssdif2i 25713 pjssdif1i 25714 pjimai 25715 pjoccoi 25717 pjtoi 25718 pjoci 25719 pjclem1 25734 pjci 25739 hst0 25772 sto1i 25775 sto2i 25776 stlei 25779 stji1i 25781 golem1 25810 golem2 25811 goeqi 25812 stcltrlem1 25815 stcltrlem2 25816 mdsldmd1i 25870 hatomistici 25901 cvexchi 25908 atomli 25921 atordi 25923 chirredlem4 25932 chirredi 25933 mdsymi 25950 cmmdi 25955 cmdmdi 25956 mdoc1i 25964 mdoc2i 25965 dmdoc1i 25966 dmdoc2i 25967 mdcompli 25968 dmdcompli 25969 mddmdin0i 25970 |
Copyright terms: Public domain | W3C validator |