Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > chjcli | Structured version Visualization version GIF version |
Description: Closure of Cℋ join. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ch0le.1 | ⊢ 𝐴 ∈ Cℋ |
chjcl.2 | ⊢ 𝐵 ∈ Cℋ |
Ref | Expression |
---|---|
chjcli | ⊢ (𝐴 ∨ℋ 𝐵) ∈ Cℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ch0le.1 | . . 3 ⊢ 𝐴 ∈ Cℋ | |
2 | 1 | chshii 29162 | . 2 ⊢ 𝐴 ∈ Sℋ |
3 | chjcl.2 | . . 3 ⊢ 𝐵 ∈ Cℋ | |
4 | 3 | chshii 29162 | . 2 ⊢ 𝐵 ∈ Sℋ |
5 | 2, 4 | shjcli 29310 | 1 ⊢ (𝐴 ∨ℋ 𝐵) ∈ Cℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 (class class class)co 7171 Cℋ cch 28864 ∨ℋ chj 28868 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5155 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7480 ax-inf2 9178 ax-cnex 10672 ax-resscn 10673 ax-1cn 10674 ax-icn 10675 ax-addcl 10676 ax-addrcl 10677 ax-mulcl 10678 ax-mulrcl 10679 ax-mulcom 10680 ax-addass 10681 ax-mulass 10682 ax-distr 10683 ax-i2m1 10684 ax-1ne0 10685 ax-1rid 10686 ax-rnegex 10687 ax-rrecex 10688 ax-cnre 10689 ax-pre-lttri 10690 ax-pre-lttrn 10691 ax-pre-ltadd 10692 ax-pre-mulgt0 10693 ax-pre-sup 10694 ax-addf 10695 ax-mulf 10696 ax-hilex 28934 ax-hfvadd 28935 ax-hvcom 28936 ax-hvass 28937 ax-hv0cl 28938 ax-hvaddid 28939 ax-hfvmul 28940 ax-hvmulid 28941 ax-hvmulass 28942 ax-hvdistr1 28943 ax-hvdistr2 28944 ax-hvmul0 28945 ax-hfi 29014 ax-his1 29017 ax-his2 29018 ax-his3 29019 ax-his4 29020 ax-hcompl 29137 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3683 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-int 4838 df-iun 4884 df-iin 4885 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-se 5485 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-isom 6349 df-riota 7128 df-ov 7174 df-oprab 7175 df-mpo 7176 df-of 7426 df-om 7601 df-1st 7715 df-2nd 7716 df-supp 7858 df-wrecs 7977 df-recs 8038 df-rdg 8076 df-1o 8132 df-2o 8133 df-er 8321 df-map 8440 df-pm 8441 df-ixp 8509 df-en 8557 df-dom 8558 df-sdom 8559 df-fin 8560 df-fsupp 8908 df-fi 8949 df-sup 8980 df-inf 8981 df-oi 9048 df-card 9442 df-pnf 10756 df-mnf 10757 df-xr 10758 df-ltxr 10759 df-le 10760 df-sub 10951 df-neg 10952 df-div 11377 df-nn 11718 df-2 11780 df-3 11781 df-4 11782 df-5 11783 df-6 11784 df-7 11785 df-8 11786 df-9 11787 df-n0 11978 df-z 12064 df-dec 12181 df-uz 12326 df-q 12432 df-rp 12474 df-xneg 12591 df-xadd 12592 df-xmul 12593 df-ioo 12826 df-icc 12829 df-fz 12983 df-fzo 13126 df-seq 13462 df-exp 13523 df-hash 13784 df-cj 14549 df-re 14550 df-im 14551 df-sqrt 14685 df-abs 14686 df-clim 14936 df-sum 15137 df-struct 16589 df-ndx 16590 df-slot 16591 df-base 16593 df-sets 16594 df-ress 16595 df-plusg 16682 df-mulr 16683 df-starv 16684 df-sca 16685 df-vsca 16686 df-ip 16687 df-tset 16688 df-ple 16689 df-ds 16691 df-unif 16692 df-hom 16693 df-cco 16694 df-rest 16800 df-topn 16801 df-0g 16819 df-gsum 16820 df-topgen 16821 df-pt 16822 df-prds 16825 df-xrs 16879 df-qtop 16884 df-imas 16885 df-xps 16887 df-mre 16961 df-mrc 16962 df-acs 16964 df-mgm 17969 df-sgrp 18018 df-mnd 18029 df-submnd 18074 df-mulg 18344 df-cntz 18566 df-cmn 19027 df-psmet 20210 df-xmet 20211 df-met 20212 df-bl 20213 df-mopn 20214 df-cnfld 20219 df-top 21646 df-topon 21663 df-topsp 21685 df-bases 21698 df-cn 21979 df-cnp 21980 df-lm 21981 df-haus 22067 df-tx 22314 df-hmeo 22507 df-xms 23074 df-ms 23075 df-tms 23076 df-cau 24009 df-grpo 28428 df-gid 28429 df-ginv 28430 df-gdiv 28431 df-ablo 28480 df-vc 28494 df-nv 28527 df-va 28530 df-ba 28531 df-sm 28532 df-0v 28533 df-vs 28534 df-nmcv 28535 df-ims 28536 df-dip 28636 df-hnorm 28903 df-hvsub 28906 df-hlim 28907 df-hcau 28908 df-sh 29142 df-ch 29156 df-oc 29187 df-chj 29245 |
This theorem is referenced by: chdmm1i 29412 chjassi 29421 chj1i 29424 chj4i 29458 lejdii 29473 pjoml2i 29520 pjoml3i 29521 pjoml4i 29522 pjoml5i 29523 cmcmlem 29526 cmbr2i 29531 cmj1i 29539 cmj2i 29540 fh3i 29558 fh4i 29559 qlaxr3i 29571 osumcor2i 29579 spansnji 29581 5oai 29596 3oalem5 29601 3oalem6 29602 3oai 29603 pjdsi 29647 pjds3i 29648 mayete3i 29663 mayetes3i 29664 pjscji 30105 pjci 30135 stlei 30175 golem2 30207 goeqi 30208 stcltrlem2 30212 mdslle1i 30252 mdslj1i 30254 mdslj2i 30255 mdslmd1lem1 30260 mdslmd1lem2 30261 mdslmd1i 30264 mdslmd2i 30265 mdsldmd1i 30266 mdexchi 30270 cvexchi 30304 atabsi 30336 atabs2i 30337 mdsymlem6 30343 sumdmdlem2 30354 dmdbr5ati 30357 mdcompli 30364 dmdcompli 30365 |
Copyright terms: Public domain | W3C validator |