| Colors of
variables: wff
setvar class |
| Syntax hints:
∈ wcel 2107 {csn 4627
0ℎc0v 30155
Cℋ cch 30160
0ℋc0h 30166 |
| This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7720 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184 ax-addf 11185 ax-mulf 11186 ax-hilex 30230 ax-hfvadd 30231 ax-hvcom 30232 ax-hvass 30233 ax-hv0cl 30234 ax-hvaddid 30235 ax-hfvmul 30236 ax-hvmulid 30237 ax-hvmulass 30238 ax-hvdistr1 30239 ax-hvdistr2 30240 ax-hvmul0 30241 ax-hfi 30310 ax-his1 30313 ax-his2 30314 ax-his3 30315 ax-his4 30316 |
| This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7360 df-ov 7407 df-oprab 7408 df-mpo 7409 df-om 7851 df-1st 7970 df-2nd 7971 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-er 8699 df-map 8818 df-pm 8819 df-en 8936 df-dom 8937 df-sdom 8938 df-sup 9433 df-inf 9434 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271
df-3 12272 df-4 12273
df-n0 12469 df-z 12555
df-uz 12819 df-q 12929
df-rp 12971 df-xneg 13088 df-xadd 13089 df-xmul 13090 df-icc 13327 df-seq 13963 df-exp 14024 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-topgen 17385 df-psmet 20921 df-xmet 20922 df-met 20923 df-bl 20924 df-mopn 20925 df-top 22378 df-topon 22395 df-bases 22431 df-lm 22715 df-haus 22801 df-grpo 29724 df-gid 29725 df-ginv 29726 df-gdiv 29727 df-ablo 29776 df-vc 29790 df-nv 29823 df-va 29826 df-ba 29827 df-sm 29828 df-0v 29829 df-vs 29830 df-nmcv 29831 df-ims 29832 df-hnorm 30199 df-hvsub 30202 df-hlim 30203 df-sh 30438 df-ch 30452 df-ch0 30484 |
| This theorem is referenced by: h0elsh
30487 chintcl
30563 omlsi
30635 pjoml
30667 pjoc2
30670 chj0i
30686 chj00i
30718 chm0
30722 chne0
30725 chocin
30726 chj0
30728 chlejb1
30743 chnle
30745 ledi
30771 chsup0
30779 h1datom
30813 cmbr3
30839 cm0
30840 pjoml2
30842 cmcm
30845 cmcm3
30846 lecm
30848 qlaxr3i
30867 nonbooli
30882 pjige0
30922 pjhfo
30937 pj11
30945 ho0f
30982 pjhmop
31381 pjidmco
31412 hst0
31464 largei
31498 mdslmd1lem3
31558 mdslmd1lem4
31559 csmdsymi
31565 elat2
31571 atcveq0
31579 hatomic
31591 atcv0eq
31610 atoml2i
31614 atordi
31615 atord
31619 atcvat2
31620 chirred
31626 |
