Intuitionistic Logic Explorer |
This is the GIF version. Change to Unicode version |
Ref | Expression (see link for any distinct variable requirements) |
wn 3 | |
wi 4 | |
ax-mp 5 | |
ax-1 6 | |
ax-2 7 | |
wa 103 | |
wb 104 | |
ax-ia1 105 | |
ax-ia2 106 | |
ax-ia3 107 | |
df-bi 116 | |
ax-in1 588 | |
ax-in2 589 | |
wo 682 | |
ax-io 683 | |
wstab 800 | STAB |
df-stab 801 | STAB |
wdc 804 | DECID |
df-dc 805 | DECID |
w3o 946 | |
w3a 947 | |
df-3or 948 | |
df-3an 949 | |
wal 1314 | |
cv 1315 | |
wceq 1316 | |
wtru 1317 | |
df-tru 1319 | |
wfal 1321 | |
df-fal 1322 | |
wxo 1338 | |
df-xor 1339 | |
ax-5 1408 | |
ax-7 1409 | |
ax-gen 1410 | |
wnf 1421 | |
df-nf 1422 | |
wex 1453 | |
ax-ie1 1454 | |
ax-ie2 1455 | |
wcel 1465 | |
ax-8 1467 | |
ax-10 1468 | |
ax-11 1469 | |
ax-i12 1470 | |
ax-bndl 1471 | |
ax-4 1472 | |
ax-13 1476 | |
ax-14 1477 | |
ax-17 1491 | |
ax-i9 1495 | |
ax-ial 1499 | |
ax-i5r 1500 | |
ax-10o 1679 | |
wsb 1720 | |
df-sb 1721 | |
ax-16 1770 | |
ax-11o 1779 | |
weu 1977 | |
wmo 1978 | |
df-eu 1980 | |
df-mo 1981 | |
ax-ext 2099 | |
cab 2103 | |
df-clab 2104 | |
df-cleq 2110 | |
df-clel 2113 | |
wnfc 2245 | |
df-nfc 2247 | |
wne 2285 | |
df-ne 2286 | |
wnel 2380 | |
df-nel 2381 | |
wral 2393 | |
wrex 2394 | |
wreu 2395 | |
wrmo 2396 | |
crab 2397 | |
df-ral 2398 | |
df-rex 2399 | |
df-reu 2400 | |
df-rmo 2401 | |
df-rab 2402 | |
cvv 2660 | |
df-v 2662 | |
wcdeq 2865 | CondEq |
df-cdeq 2866 | CondEq |
wsbc 2882 | |
df-sbc 2883 | |
csb 2975 | |
df-csb 2976 | |
cdif 3038 | |
cun 3039 | |
cin 3040 | |
wss 3041 | |
df-dif 3043 | |
df-un 3045 | |
df-in 3047 | |
df-ss 3054 | |
c0 3333 | |
df-nul 3334 | |
cif 3444 | |
df-if 3445 | |
cpw 3480 | |
df-pw 3482 | |
csn 3497 | |
cpr 3498 | |
ctp 3499 | |
cop 3500 | |
cotp 3501 | |
df-sn 3503 | |
df-pr 3504 | |
df-tp 3505 | |
df-op 3506 | |
df-ot 3507 | |
cuni 3706 | |
df-uni 3707 | |
cint 3741 | |
df-int 3742 | |
ciun 3783 | |
ciin 3784 | |
df-iun 3785 | |
df-iin 3786 | |
wdisj 3876 | Disj |
df-disj 3877 | Disj |
wbr 3899 | |
df-br 3900 | |
copab 3958 | |
cmpt 3959 | |
df-opab 3960 | |
df-mpt 3961 | |
wtr 3996 | |
df-tr 3997 | |
ax-coll 4013 | |
ax-sep 4016 | |
ax-nul 4024 | |
ax-pow 4068 | |
wem 4088 | EXMID |
df-exmid 4089 | EXMID DECID |
ax-pr 4101 | |
cep 4179 | |
cid 4180 | |
df-eprel 4181 | |
df-id 4185 | |
wpo 4186 | |
wor 4187 | |
df-po 4188 | |
df-iso 4189 | |
wfrfor 4219 | FrFor |
wfr 4220 | |
wse 4221 | Se |
wwe 4222 | |
df-frfor 4223 | FrFor |
df-frind 4224 | FrFor |
df-se 4225 | Se |
df-wetr 4226 | |
word 4254 | |
con0 4255 | |
wlim 4256 | |
csuc 4257 | |
df-iord 4258 | |
df-on 4260 | |
df-ilim 4261 | |
df-suc 4263 | |
ax-un 4325 | |
ax-setind 4422 | |
ax-iinf 4472 | |
com 4474 | |
df-iom 4475 | |
cxp 4507 | |
ccnv 4508 | |
cdm 4509 | |
crn 4510 | |
cres 4511 | |
cima 4512 | |
ccom 4513 | |
wrel 4514 | |
df-xp 4515 | |
df-rel 4516 | |
df-cnv 4517 | |
df-co 4518 | |
df-dm 4519 | |
df-rn 4520 | |
df-res 4521 | |
df-ima 4522 | |
cio 5056 | |
df-iota 5058 | |
wfun 5087 | |
wfn 5088 | |
wf 5089 | |
wf1 5090 | |
wfo 5091 | |
wf1o 5092 | |
cfv 5093 | |
wiso 5094 | |
df-fun 5095 | |
df-fn 5096 | |
df-f 5097 | |
df-f1 5098 | |
df-fo 5099 | |
df-f1o 5100 | |
df-fv 5101 | |
df-isom 5102 | |
crio 5697 | |
df-riota 5698 | |
co 5742 | |
coprab 5743 | |
cmpo 5744 | |
df-ov 5745 | |
df-oprab 5746 | |
df-mpo 5747 | |
cof 5948 | |
cofr 5949 | |
df-of 5950 | |
df-ofr 5951 | |
c1st 6004 | |
c2nd 6005 | |
df-1st 6006 | |
df-2nd 6007 | |
ctpos 6109 | tpos |
df-tpos 6110 | tpos |
wsmo 6150 | |
df-smo 6151 | |
crecs 6169 | recs |
df-recs 6170 | recs |
crdg 6234 | |
df-irdg 6235 | recs |
cfrec 6255 | frec |
df-frec 6256 | frec recs |
c1o 6274 | |
c2o 6275 | |
c3o 6276 | |
c4o 6277 | |
coa 6278 | |
comu 6279 | |
coei 6280 | ↑o |
df-1o 6281 | |
df-2o 6282 | |
df-3o 6283 | |
df-4o 6284 | |
df-oadd 6285 | |
df-omul 6286 | |
df-oexpi 6287 | ↑o |
wer 6394 | |
cec 6395 | |
cqs 6396 | |
df-er 6397 | |
df-ec 6399 | |
df-qs 6403 | |
cmap 6510 | |
cpm 6511 | |
df-map 6512 | |
df-pm 6513 | |
cixp 6560 | |
df-ixp 6561 | |
cen 6600 | |
cdom 6601 | |
cfn 6602 | |
df-en 6603 | |
df-dom 6604 | |
df-fin 6605 | |
cfi 6824 | |
df-fi 6825 | |
csup 6837 | |
cinf 6838 | inf |
df-sup 6839 | |
df-inf 6840 | inf |
cdju 6890 | ⊔ |
df-dju 6891 | ⊔ |
cinl 6898 | inl |
cinr 6899 | inr |
df-inl 6900 | inl |
df-inr 6901 | inr |
cdjucase 6936 | case |
df-case 6937 | case inl inr |
cdjud 6955 | ⊔d |
df-djud 6956 | ⊔d inl inr |
comni 6972 | Omni |
xnninf 6973 | ℕ∞ |
df-omni 6974 | Omni |
df-nninf 6975 | ℕ∞ |
cmarkov 6993 | Markov |
df-markov 6994 | Markov |
ccrd 7003 | |
df-card 7004 | |
wac 7029 | CHOICE |
df-ac 7030 | CHOICE |
wacc 7045 | CCHOICE |
df-cc 7046 | CCHOICE |
cnpi 7048 | |
cpli 7049 | |
cmi 7050 | |
clti 7051 | |
cplpq 7052 | |
cmpq 7053 | |
cltpq 7054 | |
ceq 7055 | |
cnq 7056 | |
c1q 7057 | |
cplq 7058 | |
cmq 7059 | |
crq 7060 | |
cltq 7061 | |
ceq0 7062 | ~Q0 |
cnq0 7063 | Q0 |
c0q0 7064 | 0Q0 |
cplq0 7065 | +Q0 |
cmq0 7066 | ·Q0 |
cnp 7067 | |
c1p 7068 | |
cpp 7069 | |
cmp 7070 | |
cltp 7071 | |
cer 7072 | |
cnr 7073 | |
c0r 7074 | |
c1r 7075 | |
cm1r 7076 | |
cplr 7077 | |
cmr 7078 | |
cltr 7079 | |
df-ni 7080 | |
df-pli 7081 | |
df-mi 7082 | |
df-lti 7083 | |
df-plpq 7120 | |
df-mpq 7121 | |
df-ltpq 7122 | |
df-enq 7123 | |
df-nqqs 7124 | |
df-plqqs 7125 | |
df-mqqs 7126 | |
df-1nqqs 7127 | |
df-rq 7128 | |
df-ltnqqs 7129 | |
df-enq0 7200 | ~Q0 |
df-nq0 7201 | Q0 ~Q0 |
df-0nq0 7202 | 0Q0 ~Q0 |
df-plq0 7203 | +Q0 Q0 Q0 ~Q0 ~Q0 ~Q0 |
df-mq0 7204 | ·Q0 Q0 Q0 ~Q0 ~Q0 ~Q0 |
df-inp 7242 | |
df-i1p 7243 | |
df-iplp 7244 | |
df-imp 7245 | |
df-iltp 7246 | |
df-enr 7502 | |
df-nr 7503 | |
df-plr 7504 | |
df-mr 7505 | |
df-ltr 7506 | |
df-0r 7507 | |
df-1r 7508 | |
df-m1r 7509 | |
cc 7586 | |
cr 7587 | |
cc0 7588 | |
c1 7589 | |
ci 7590 | |
caddc 7591 | |
cltrr 7592 | |
cmul 7593 | |
df-c 7594 | |
df-0 7595 | |
df-1 7596 | |
df-i 7597 | |
df-r 7598 | |
df-add 7599 | |
df-mul 7600 | |
df-lt 7601 | |
ax-cnex 7679 | |
ax-resscn 7680 | |
ax-1cn 7681 | |
ax-1re 7682 | |
ax-icn 7683 | |
ax-addcl 7684 | |
ax-addrcl 7685 | |
ax-mulcl 7686 | |
ax-mulrcl 7687 | |
ax-addcom 7688 | |
ax-mulcom 7689 | |
ax-addass 7690 | |
ax-mulass 7691 | |
ax-distr 7692 | |
ax-i2m1 7693 | |
ax-0lt1 7694 | |
ax-1rid 7695 | |
ax-0id 7696 | |
ax-rnegex 7697 | |
ax-precex 7698 | |
ax-cnre 7699 | |
ax-pre-ltirr 7700 | |
ax-pre-ltwlin 7701 | |
ax-pre-lttrn 7702 | |
ax-pre-apti 7703 | |
ax-pre-ltadd 7704 | |
ax-pre-mulgt0 7705 | |
ax-pre-mulext 7706 | |
ax-arch 7707 | |
ax-caucvg 7708 | |
ax-pre-suploc 7709 | |
ax-addf 7710 | |
ax-mulf 7711 | |
cpnf 7765 | |
cmnf 7766 | |
cxr 7767 | |
clt 7768 | |
cle 7769 | |
df-pnf 7770 | |
df-mnf 7771 | |
df-xr 7772 | |
df-ltxr 7773 | |
df-le 7774 | |
cmin 7901 | |
cneg 7902 | |
df-sub 7903 | |
df-neg 7904 | |
creap 8304 | #ℝ |
df-reap 8305 | #ℝ |
cap 8311 | # |
df-ap 8312 | # #ℝ #ℝ |
cdiv 8400 | |
df-div 8401 | |
cn 8688 | |
df-inn 8689 | |
c2 8739 | |
c3 8740 | |
c4 8741 | |
c5 8742 | |
c6 8743 | |
c7 8744 | |
c8 8745 | |
c9 8746 | |
df-2 8747 | |
df-3 8748 | |
df-4 8749 | |
df-5 8750 | |
df-6 8751 | |
df-7 8752 | |
df-8 8753 | |
df-9 8754 | |
cn0 8945 | |
df-n0 8946 | |
cxnn0 9008 | NN0* |
df-xnn0 9009 | NN0* |
cz 9022 | |
df-z 9023 | |
cdc 9150 | ; |
df-dec 9151 | ; |
cuz 9294 | |
df-uz 9295 | |
cq 9379 | |
df-q 9380 | |
crp 9409 | |
df-rp 9410 | |
cxne 9524 | |
cxad 9525 | |
cxmu 9526 | |
df-xneg 9527 | |
df-xadd 9528 | |
df-xmul 9529 | |
cioo 9639 | |
cioc 9640 | |
cico 9641 | |
cicc 9642 | |
df-ioo 9643 | |
df-ioc 9644 | |
df-ico 9645 | |
df-icc 9646 | |
cfz 9758 | |
df-fz 9759 | |
cfzo 9887 | ..^ |
df-fzo 9888 | ..^ |
cfl 10009 | |
cceil 10010 | ⌈ |
df-fl 10011 | |
df-ceil 10012 | ⌈ |
cmo 10063 | |
df-mod 10064 | |
cseq 10186 | |
df-seqfrec 10187 | frec |
cexp 10260 | |
df-exp 10261 | |
cfa 10439 | |
df-fac 10440 | |
cbc 10461 | |
df-bc 10462 | |
chash 10489 | ♯ |
df-ihash 10490 | ♯ frec |
cshi 10554 | |
df-shft 10555 | |
ccj 10579 | |
cre 10580 | |
cim 10581 | |
df-cj 10582 | |
df-re 10583 | |
df-im 10584 | |
csqrt 10736 | |
cabs 10737 | |
df-rsqrt 10738 | |
df-abs 10739 | |
cli 11015 | |
df-clim 11016 | |
csu 11090 | |
df-sumdc 11091 | DECID |
ce 11275 | |
ceu 11276 | |
csin 11277 | |
ccos 11278 | |
ctan 11279 | |
cpi 11280 | |
df-ef 11281 | |
df-e 11282 | |
df-sin 11283 | |
df-cos 11284 | |
df-tan 11285 | |
df-pi 11286 | inf |
ctau 11408 | |
df-tau 11409 | inf |
cdvds 11420 | |
df-dvds 11421 | |
cgcd 11562 | |
df-gcd 11563 | |
clcm 11668 | lcm |
df-lcm 11669 | lcm inf |
cprime 11715 | |
df-prm 11716 | |
cnumer 11786 | numer |
cdenom 11787 | denom |
df-numer 11788 | numer |
df-denom 11789 | denom |
cphi 11813 | |
df-phi 11814 | ♯ |
cstr 11882 | Struct |
cnx 11883 | |
csts 11884 | sSet |
cslot 11885 | Slot |
cbs 11886 | |
cress 11887 | ↾s |
df-struct 11888 | Struct |
df-ndx 11889 | |
df-slot 11890 | Slot |
df-base 11892 | Slot |
df-sets 11893 | sSet |
df-ress 11894 | ↾s sSet |
cplusg 11948 | |
cmulr 11949 | |
cstv 11950 | |
csca 11951 | Scalar |
cvsca 11952 | |
cip 11953 | |
cts 11954 | TopSet |
cple 11955 | |
coc 11956 | |
cds 11957 | |
cunif 11958 | |
chom 11959 | |
cco 11960 | comp |
df-plusg 11961 | Slot |
df-mulr 11962 | Slot |
df-starv 11963 | Slot |
df-sca 11964 | Scalar Slot |
df-vsca 11965 | Slot |
df-ip 11966 | Slot |
df-tset 11967 | TopSet Slot |
df-ple 11968 | Slot ; |
df-ocomp 11969 | Slot ; |
df-ds 11970 | Slot ; |
df-unif 11971 | Slot ; |
df-hom 11972 | Slot ; |
df-cco 11973 | comp Slot ; |
crest 12047 | ↾t |
ctopn 12048 | |
df-rest 12049 | ↾t |
df-topn 12050 | TopSet ↾t |
ctg 12062 | |
cpt 12063 | |
c0g 12064 | |
cgsu 12065 | g |
df-0g 12066 | |
df-gsum 12067 | g ♯ ♯ |
df-topgen 12068 | |
df-pt 12069 | |
cprds 12070 | s |
cpws 12071 | s |
df-prds 12072 | s Scalar g TopSet comp comp |
df-pws 12074 | s Scalars |
cpsmet 12075 | PsMet |
cxmet 12076 | |
cmet 12077 | |
cbl 12078 | |
cfbas 12079 | |
cfg 12080 | |
cmopn 12081 | |
cmetu 12082 | metUnif |
df-psmet 12083 | PsMet |
df-xmet 12084 | |
df-met 12085 | |
df-bl 12086 | |
df-mopn 12087 | |
df-fbas 12088 | |
df-fg 12089 | |
df-metu 12090 | metUnif PsMet |
ctop 12091 | |
df-top 12092 | |
ctopon 12104 | TopOn |
df-topon 12105 | TopOn |
ctps 12124 | |
df-topsp 12125 | TopOn |
ctb 12136 | |
df-bases 12137 | |
ccld 12188 | |
cnt 12189 | |
ccl 12190 | |
df-cld 12191 | |
df-ntr 12192 | |
df-cls 12193 | |
cnei 12234 | |
df-nei 12235 | |
ccn 12281 | |
ccnp 12282 | |
clm 12283 | |
df-cn 12284 | |
df-cnp 12285 | |
df-lm 12286 | |
ctx 12348 | |
df-tx 12349 | |
chmeo 12396 | |
df-hmeo 12397 | |
cxms 12432 | |
cms 12433 | |
ctms 12434 | toMetSp |
df-xms 12435 | |
df-ms 12436 | |
df-tms 12437 | toMetSp sSet TopSet |
ccncf 12653 | |
df-cncf 12654 | |
climc 12719 | lim |
cdv 12720 | |
df-limced 12721 | lim # |
df-dvap 12722 | ↾t # lim |
The list of syntax, axioms (ax-) and definitions (df-) for the starts here | |
wdcin 12927 | DECIDin |
df-dcin 12928 | DECIDin DECID |
wbd 12937 | BOUNDED |
ax-bd0 12938 | BOUNDED BOUNDED |
ax-bdim 12939 | BOUNDED BOUNDED BOUNDED |
ax-bdan 12940 | BOUNDED BOUNDED BOUNDED |
ax-bdor 12941 | BOUNDED BOUNDED BOUNDED |
ax-bdn 12942 | BOUNDED BOUNDED |
ax-bdal 12943 | BOUNDED BOUNDED |
ax-bdex 12944 | BOUNDED BOUNDED |
ax-bdeq 12945 | BOUNDED |
ax-bdel 12946 | BOUNDED |
ax-bdsb 12947 | BOUNDED BOUNDED |
wbdc 12965 | BOUNDED |
df-bdc 12966 | BOUNDED BOUNDED |
ax-bdsep 13009 | BOUNDED |
ax-bj-d0cl 13049 | BOUNDED DECID |
wind 13051 | Ind |
df-bj-ind 13052 | Ind |
ax-infvn 13066 | Ind Ind |
ax-bdsetind 13093 | BOUNDED |
ax-inf2 13101 | |
ax-strcoll 13107 | |
ax-sscoll 13112 | |
ax-ddkcomp 13114 | |
walsi 13169 | ! |
walsc 13170 | ! |
df-alsi 13171 | ! |
df-alsc 13172 | ! |
Copyright terms: Public domain | W3C validator |