| Colors of
variables: wff
setvar class |
Syntax hints: -.wn 3 ->wi 4
<->wb 184 /\wa 369 /\w3a 965
=wceq 1370 e.wcel 1757 C_wss 3410
class class class wbr 4374 `cfv 5500
cbs 14260 cple 14331 chlt 33276 clh 33909 cdih 35154 |
| This theorem is referenced by: dih11
35191 dihcnvord
35200 dihmeetlem1N
35216 dihglblem5apreN
35217 dihglblem5aN
35218 dihglblem4
35223 dihmeetlem9N
35241 dihmeetlem11N
35243 dihlspsnat
35259 dihglblem6
35266 dochvalr
35283 dochss
35291 dvh4dimat
35364 |
| This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671
ax-6 1709 ax-7 1729 ax-8 1759
ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2429 ax-rep 4485 ax-sep 4495 ax-nul 4503 ax-pow 4552 ax-pr 4613 ax-un 6456 ax-cnex 9423 ax-resscn 9424 ax-1cn 9425 ax-icn 9426 ax-addcl 9427 ax-addrcl 9428 ax-mulcl 9429 ax-mulrcl 9430 ax-mulcom 9431 ax-addass 9432 ax-mulass 9433 ax-distr 9434 ax-i2m1 9435 ax-1ne0 9436 ax-1rid 9437 ax-rnegex 9438 ax-rrecex 9439 ax-cnre 9440 ax-pre-lttri 9441 ax-pre-lttrn 9442 ax-pre-ltadd 9443 ax-pre-mulgt0 9444 ax-riotaBAD 32885 |
| This theorem depends on definitions:
df-bi 185 df-or 370
df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1702 df-eu 2263 df-mo 2264 df-clab 2436 df-cleq 2442 df-clel 2445 df-nfc 2598 df-ne 2643 df-nel 2644 df-ral 2797 df-rex 2798 df-reu 2799 df-rmo 2800 df-rab 2801 df-v 3054 df-sbc 3269 df-csb 3371 df-dif 3413 df-un 3415 df-in 3417 df-ss 3424 df-pss 3426 df-nul 3720 df-if 3874 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4174 df-int 4211 df-iun 4255 df-iin 4256 df-br 4375 df-opab 4433 df-mpt 4434 df-tr 4468 df-eprel 4714 df-id 4718 df-po 4723 df-so 4724 df-fr 4761 df-we 4763 df-ord 4804 df-on 4805 df-lim 4806 df-suc 4807 df-xp 4928 df-rel 4929 df-cnv 4930 df-co 4931 df-dm 4932 df-rn 4933 df-res 4934 df-ima 4935 df-iota 5463 df-fun 5502 df-fn 5503 df-f 5504 df-f1 5505 df-fo 5506 df-f1o 5507 df-fv 5508 df-riota 6135 df-ov 6177 df-oprab 6178 df-mpt2 6179 df-om 6561 df-1st 6661 df-2nd 6662 df-tpos 6829 df-undef 6876 df-recs 6916 df-rdg 6950 df-1o 7004 df-oadd 7008 df-er 7185 df-map 7300 df-en 7395 df-dom 7396 df-sdom 7397 df-fin 7398 df-pnf 9505 df-mnf 9506 df-xr 9507 df-ltxr 9508 df-le 9509 df-sub 9682 df-neg 9683 df-nn 10408 df-2 10465
df-3 10466 df-4 10467
df-5 10468 df-6 10469
df-n0 10665 df-z 10732
df-uz 10947 df-fz 11523 df-struct 14262 df-ndx 14263 df-slot 14264 df-base 14265 df-sets 14266 df-ress 14267 df-plusg 14337 df-mulr 14338 df-sca 14340 df-vsca 14341 df-0g 14466 df-poset 15202 df-plt 15214 df-lub 15230 df-glb 15231 df-join 15232 df-meet 15233 df-p0 15295 df-p1 15296 df-lat 15302 df-clat 15364 df-mnd 15501 df-submnd 15551 df-grp 15631 df-minusg 15632 df-sbg 15633 df-subg 15764 df-cntz 15921 df-lsm 16223 df-cmn 16367 df-abl 16368 df-mgp 16681 df-ur 16693 df-rng 16737 df-oppr 16805 df-dvdsr 16823 df-unit 16824 df-invr 16854 df-dvr 16865 df-drng 16924 df-lmod 17040 df-lss 17104 df-lsp 17143 df-lvec 17274 df-oposet 33102 df-ol 33104 df-oml 33105 df-covers 33192 df-ats 33193 df-atl 33224 df-cvlat 33248 df-hlat 33277 df-llines 33423 df-lplanes 33424 df-lvols 33425 df-lines 33426 df-psubsp 33428 df-pmap 33429 df-padd 33721 df-lhyp 33913 df-laut 33914 df-ldil 34029 df-ltrn 34030 df-trl 34084 df-tendo 34680 df-edring 34682 df-disoa 34955 df-dvech 35005 df-dib 35065 df-dic 35099 df-dih 35155 |
