| Colors of
variables: wff
setvar class |
| Syntax hints:
∈ wcel 2098 (class class class)co 7417
Cℋ cch 30795
∨ℋ chj 30799 |
| This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5364 ax-pr 5428 ax-un 7739 ax-inf2 9664 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216 ax-addf 11217 ax-mulf 11218 ax-hilex 30865 ax-hfvadd 30866 ax-hvcom 30867 ax-hvass 30868 ax-hv0cl 30869 ax-hvaddid 30870 ax-hfvmul 30871 ax-hvmulid 30872 ax-hvmulass 30873 ax-hvdistr1 30874 ax-hvdistr2 30875 ax-hvmul0 30876 ax-hfi 30945 ax-his1 30948 ax-his2 30949 ax-his3 30950 ax-his4 30951 ax-hcompl 31068 |
| This theorem depends on definitions:
df-bi 206 df-an 395
df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3965 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4909 df-int 4950 df-iun 4998 df-iin 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6499 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-isom 6556 df-riota 7373 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7683 df-om 7870 df-1st 7992 df-2nd 7993 df-supp 8164 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-er 8723 df-map 8845 df-pm 8846 df-ixp 8915 df-en 8963 df-dom 8964 df-sdom 8965 df-fin 8966 df-fsupp 9386 df-fi 9434 df-sup 9465 df-inf 9466 df-oi 9533 df-card 9962 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11476 df-neg 11477 df-div 11902 df-nn 12243 df-2 12305
df-3 12306 df-4 12307
df-5 12308 df-6 12309
df-7 12310 df-8 12311
df-9 12312 df-n0 12503 df-z 12589
df-dec 12708 df-uz 12853 df-q 12963
df-rp 13007 df-xneg 13124 df-xadd 13125 df-xmul 13126 df-ioo 13360 df-icc 13363 df-fz 13517 df-fzo 13660 df-seq 13999 df-exp 14059 df-hash 14322 df-cj 15078 df-re 15079 df-im 15080 df-sqrt 15214 df-abs 15215 df-clim 15464 df-sum 15665 df-struct 17115 df-sets 17132 df-slot 17150 df-ndx 17162 df-base 17180 df-ress 17209 df-plusg 17245 df-mulr 17246 df-starv 17247 df-sca 17248 df-vsca 17249 df-ip 17250 df-tset 17251 df-ple 17252 df-ds 17254 df-unif 17255 df-hom 17256 df-cco 17257 df-rest 17403 df-topn 17404 df-0g 17422 df-gsum 17423 df-topgen 17424 df-pt 17425 df-prds 17428 df-xrs 17483 df-qtop 17488 df-imas 17489 df-xps 17491 df-mre 17565 df-mrc 17566 df-acs 17568 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-submnd 18740 df-mulg 19028 df-cntz 19272 df-cmn 19741 df-psmet 21275 df-xmet 21276 df-met 21277 df-bl 21278 df-mopn 21279 df-cnfld 21284 df-top 22826 df-topon 22843 df-topsp 22865 df-bases 22879 df-cn 23161 df-cnp 23162 df-lm 23163 df-haus 23249 df-tx 23496 df-hmeo 23689 df-xms 24256 df-ms 24257 df-tms 24258 df-cau 25214 df-grpo 30359 df-gid 30360 df-ginv 30361 df-gdiv 30362 df-ablo 30411 df-vc 30425 df-nv 30458 df-va 30461 df-ba 30462 df-sm 30463 df-0v 30464 df-vs 30465 df-nmcv 30466 df-ims 30467 df-dip 30567 df-hnorm 30834 df-hvsub 30837 df-hlim 30838 df-hcau 30839 df-sh 31073 df-ch 31087 df-oc 31118 df-chj 31176 |
| This theorem is referenced by: chdmm1i
31343 chjassi
31352 chj1i
31355 chj4i
31389 lejdii
31404 pjoml2i
31451 pjoml3i
31452 pjoml4i
31453 pjoml5i
31454 cmcmlem
31457 cmbr2i
31462 cmj1i
31470 cmj2i
31471 fh3i
31489 fh4i
31490 qlaxr3i
31502 osumcor2i
31510 spansnji
31512 5oai
31527 3oalem5
31532 3oalem6
31533 3oai
31534 pjdsi
31578 pjds3i
31579 mayete3i
31594 mayetes3i
31595 pjscji
32036 pjci
32066 stlei
32106 golem2
32138 goeqi
32139 stcltrlem2
32143 mdslle1i
32183 mdslj1i
32185 mdslj2i
32186 mdslmd1lem1
32191 mdslmd1lem2
32192 mdslmd1i
32195 mdslmd2i
32196 mdsldmd1i
32197 mdexchi
32201 cvexchi
32235 atabsi
32267 atabs2i
32268 mdsymlem6
32274 sumdmdlem2
32285 dmdbr5ati
32288 mdcompli
32295 dmdcompli
32296 |
