| Colors of
variables: wff
setvar class |
| Syntax hints:
∈ wcel 2106 ⊆ wss 3928
(class class class)co 7377
Cℋ cch 29968
∨ℋ chj 29972 |
| This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5262 ax-sep 5276 ax-nul 5283 ax-pow 5340 ax-pr 5404 ax-un 7692 ax-inf2 9601 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153 ax-addf 11154 ax-mulf 11155 ax-hilex 30038 ax-hfvadd 30039 ax-hvcom 30040 ax-hvass 30041 ax-hv0cl 30042 ax-hvaddid 30043 ax-hfvmul 30044 ax-hvmulid 30045 ax-hvmulass 30046 ax-hvdistr1 30047 ax-hvdistr2 30048 ax-hvmul0 30049 ax-hfi 30118 ax-his1 30121 ax-his2 30122 ax-his3 30123 ax-his4 30124 ax-hcompl 30241 |
| This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3364 df-reu 3365 df-rab 3419 df-v 3461 df-sbc 3758 df-csb 3874 df-dif 3931 df-un 3933 df-in 3935 df-ss 3945 df-pss 3947 df-nul 4303 df-if 4507 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4886 df-int 4928 df-iun 4976 df-iin 4977 df-br 5126 df-opab 5188 df-mpt 5209 df-tr 5243 df-id 5551 df-eprel 5557 df-po 5565 df-so 5566 df-fr 5608 df-se 5609 df-we 5610 df-xp 5659 df-rel 5660 df-cnv 5661 df-co 5662 df-dm 5663 df-rn 5664 df-res 5665 df-ima 5666 df-pred 6273 df-ord 6340 df-on 6341 df-lim 6342 df-suc 6343 df-iota 6468 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7333 df-ov 7380 df-oprab 7381 df-mpo 7382 df-of 7637 df-om 7823 df-1st 7941 df-2nd 7942 df-supp 8113 df-frecs 8232 df-wrecs 8263 df-recs 8337 df-rdg 8376 df-1o 8432 df-2o 8433 df-er 8670 df-map 8789 df-pm 8790 df-ixp 8858 df-en 8906 df-dom 8907 df-sdom 8908 df-fin 8909 df-fsupp 9328 df-fi 9371 df-sup 9402 df-inf 9403 df-oi 9470 df-card 9899 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11411 df-neg 11412 df-div 11837 df-nn 12178 df-2 12240
df-3 12241 df-4 12242
df-5 12243 df-6 12244
df-7 12245 df-8 12246
df-9 12247 df-n0 12438 df-z 12524
df-dec 12643 df-uz 12788 df-q 12898
df-rp 12940 df-xneg 13057 df-xadd 13058 df-xmul 13059 df-ioo 13293 df-icc 13296 df-fz 13450 df-fzo 13593 df-seq 13932 df-exp 13993 df-hash 14256 df-cj 15011 df-re 15012 df-im 15013 df-sqrt 15147 df-abs 15148 df-clim 15397 df-sum 15598 df-struct 17045 df-sets 17062 df-slot 17080 df-ndx 17092 df-base 17110 df-ress 17139 df-plusg 17175 df-mulr 17176 df-starv 17177 df-sca 17178 df-vsca 17179 df-ip 17180 df-tset 17181 df-ple 17182 df-ds 17184 df-unif 17185 df-hom 17186 df-cco 17187 df-rest 17333 df-topn 17334 df-0g 17352 df-gsum 17353 df-topgen 17354 df-pt 17355 df-prds 17358 df-xrs 17413 df-qtop 17418 df-imas 17419 df-xps 17421 df-mre 17495 df-mrc 17496 df-acs 17498 df-mgm 18526 df-sgrp 18575 df-mnd 18586 df-submnd 18631 df-mulg 18902 df-cntz 19126 df-cmn 19593 df-psmet 20840 df-xmet 20841 df-met 20842 df-bl 20843 df-mopn 20844 df-cnfld 20849 df-top 22295 df-topon 22312 df-topsp 22334 df-bases 22348 df-cn 22630 df-cnp 22631 df-lm 22632 df-haus 22718 df-tx 22965 df-hmeo 23158 df-xms 23725 df-ms 23726 df-tms 23727 df-cau 24672 df-grpo 29532 df-gid 29533 df-ginv 29534 df-gdiv 29535 df-ablo 29584 df-vc 29598 df-nv 29631 df-va 29634 df-ba 29635 df-sm 29636 df-0v 29637 df-vs 29638 df-nmcv 29639 df-ims 29640 df-dip 29740 df-hnorm 30007 df-hvsub 30010 df-hlim 30011 df-hcau 30012 df-sh 30246 df-ch 30260 df-oc 30291 df-shs 30347 df-chj 30349 |
| This theorem is referenced by: chlejb1i
30515 chdmm1i
30516 chj00i
30526 chj1i
30528 lejdii
30577 cmcmlem
30630 cmbr4i
30640 cmj2i
30644 qlaxr3i
30675 osumcori
30682 mayetes3i
30768 pjclem1
31234 pjci
31239 mdslj1i
31358 mdslj2i
31359 mdsl1i
31360 mdsl2i
31361 cvmdi
31363 mdslmd1lem1
31364 mdslmd1lem2
31365 mdslmd2i
31369 mdexchi
31374 sumdmdlem2
31458 dmdbr5ati
31461 |
