Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2104 class class class wbr 5081
(class class class)co 7307 ℝcr 10916
0cc0 10917 1c1 10918
≤ cle 11056 [,]cicc 13128 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7620 ax-cnex 10973 ax-resscn 10974 ax-1cn 10975 ax-icn 10976 ax-addcl 10977 ax-addrcl 10978 ax-mulcl 10979 ax-mulrcl 10980 ax-mulcom 10981 ax-addass 10982 ax-mulass 10983 ax-distr 10984 ax-i2m1 10985 ax-1ne0 10986 ax-1rid 10987 ax-rnegex 10988 ax-rrecex 10989 ax-cnre 10990 ax-pre-lttri 10991 ax-pre-lttrn 10992 ax-pre-ltadd 10993 ax-pre-mulgt0 10994 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3286 df-rab 3287 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-br 5082 df-opab 5144 df-mpt 5165 df-id 5500 df-po 5514 df-so 5515 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-riota 7264 df-ov 7310 df-oprab 7311 df-mpo 7312 df-er 8529 df-en 8765 df-dom 8766 df-sdom 8767 df-pnf 11057 df-mnf 11058 df-xr 11059 df-ltxr 11060 df-le 11061 df-sub 11253 df-neg 11254 df-icc 13132 |
This theorem is referenced by: iccpnfcnv
24152 htpycom
24184 htpyid
24185 htpyco1
24186 htpyco2
24187 htpycc
24188 phtpy01
24193 phtpycom
24196 phtpyid
24197 phtpyco2
24198 phtpycc
24199 reparphti
24205 pco1
24223 pcohtpylem
24227 pcoptcl
24229 pcopt
24230 pcopt2
24231 pcoass
24232 pcorevcl
24233 pcorevlem
24234 pi1xfrf
24261 pi1xfr
24263 pi1xfrcnvlem
24264 pi1xfrcnv
24265 pi1cof
24267 pi1coghm
24269 dvlipcn
25203 leibpi
26137 lgamgulmlem2
26224 ttgcontlem1
27297 axpaschlem
27353 iistmd
31897 xrge0iif1
31933 xrge0iifmhm
31934 cnpconn
33237 pconnconn
33238 txpconn
33239 ptpconn
33240 indispconn
33241 connpconn
33242 txsconnlem
33247 txsconn
33248 cvxpconn
33249 cvxsconn
33250 cvmliftphtlem
33324 cvmlift3lem2
33327 cvmlift3lem4
33329 cvmlift3lem5
33330 cvmlift3lem6
33331 cvmlift3lem9
33334 lcmineqlem12
40090 k0004val0
41802 |