Ref | Expression (see link for any distinct variable requirements)
|
wn 3 | wff Β¬ π |
wi 4 | wff (π β π) |
ax-mp 5 | β’ π
& β’ (π β π) β β’ π |
ax-1 6 | β’ (π β (π β π)) |
ax-2 7 | β’ ((π β (π β π)) β ((π β π) β (π β π))) |
wa 104 | wff (π β§ π) |
wb 105 | wff (π β π) |
ax-ia1 106 | β’ ((π β§ π) β π) |
ax-ia2 107 | β’ ((π β§ π) β π) |
ax-ia3 108 | β’ (π β (π β (π β§ π))) |
df-bi 117 | β’ (((π β π) β ((π β π) β§ (π β π))) β§ (((π β π) β§ (π β π)) β (π β π))) |
ax-in1 614 | β’ ((π β Β¬ π) β Β¬ π) |
ax-in2 615 | β’ (Β¬ π β (π β π)) |
wo 708 | wff (π β¨ π) |
ax-io 709 | β’ (((π β¨ π) β π) β ((π β π) β§ (π β π))) |
wstab 830 | wff STAB π |
df-stab 831 | β’ (STAB π β (Β¬ Β¬ π β π)) |
wdc 834 | wff DECID π |
df-dc 835 | β’ (DECID π β (π β¨ Β¬ π)) |
w3o 977 | wff (π β¨ π β¨ π) |
w3a 978 | wff (π β§ π β§ π) |
df-3or 979 | β’ ((π β¨ π β¨ π) β ((π β¨ π) β¨ π)) |
df-3an 980 | β’ ((π β§ π β§ π) β ((π β§ π) β§ π)) |
wal 1351 | wff βπ₯π |
cv 1352 | class π₯ |
wceq 1353 | wff π΄ = π΅ |
wtru 1354 | wff β€ |
df-tru 1356 | β’ (β€ β (βπ₯ π₯ = π₯ β βπ₯ π₯ = π₯)) |
wfal 1358 | wff β₯ |
df-fal 1359 | β’ (β₯ β Β¬
β€) |
wxo 1375 | wff (π β» π) |
df-xor 1376 | β’ ((π β» π) β ((π β¨ π) β§ Β¬ (π β§ π))) |
ax-5 1447 | β’ (βπ₯(π β π) β (βπ₯π β βπ₯π)) |
ax-7 1448 | β’ (βπ₯βπ¦π β βπ¦βπ₯π) |
ax-gen 1449 | β’ π β β’ βπ₯π |
wnf 1460 | wff β²π₯π |
df-nf 1461 | β’ (β²π₯π β βπ₯(π β βπ₯π)) |
wex 1492 | wff βπ₯π |
ax-ie1 1493 | β’ (βπ₯π β βπ₯βπ₯π) |
ax-ie2 1494 | β’ (βπ₯(π β βπ₯π) β (βπ₯(π β π) β (βπ₯π β π))) |
ax-8 1504 | β’ (π₯ = π¦ β (π₯ = π§ β π¦ = π§)) |
ax-10 1505 | β’ (βπ₯ π₯ = π¦ β βπ¦ π¦ = π₯) |
ax-11 1506 | β’ (π₯ = π¦ β (βπ¦π β βπ₯(π₯ = π¦ β π))) |
ax-i12 1507 | β’ (βπ§ π§ = π₯ β¨ (βπ§ π§ = π¦ β¨ βπ§(π₯ = π¦ β βπ§ π₯ = π¦))) |
ax-bndl 1509 | β’ (βπ§ π§ = π₯ β¨ (βπ§ π§ = π¦ β¨ βπ₯βπ§(π₯ = π¦ β βπ§ π₯ = π¦))) |
ax-4 1510 | β’ (βπ₯π β π) |
ax-17 1526 | β’ (π β βπ₯π) |
ax-i9 1530 | β’ βπ₯ π₯ = π¦ |
ax-ial 1534 | β’ (βπ₯π β βπ₯βπ₯π) |
ax-i5r 1535 | β’ ((βπ₯π β βπ₯π) β βπ₯(βπ₯π β π)) |
ax-10o 1716 | β’ (βπ₯ π₯ = π¦ β (βπ₯π β βπ¦π)) |
wsb 1762 | wff [π¦ / π₯]π |
df-sb 1763 | β’ ([π¦ / π₯]π β ((π₯ = π¦ β π) β§ βπ₯(π₯ = π¦ β§ π))) |
ax-16 1814 | β’ (βπ₯ π₯ = π¦ β (π β βπ₯π)) |
ax-11o 1823 | β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) |
weu 2026 | wff β!π₯π |
wmo 2027 | wff β*π₯π |
df-eu 2029 | β’ (β!π₯π β βπ¦βπ₯(π β π₯ = π¦)) |
df-mo 2030 | β’ (β*π₯π β (βπ₯π β β!π₯π)) |
wcel 2148 | wff π΄ β π΅ |
ax-13 2150 | β’ (π₯ = π¦ β (π₯ β π§ β π¦ β π§)) |
ax-14 2151 | β’ (π₯ = π¦ β (π§ β π₯ β π§ β π¦)) |
ax-ext 2159 | β’ (βπ§(π§ β π₯ β π§ β π¦) β π₯ = π¦) |
cab 2163 | class {π₯ β£ π} |
df-clab 2164 | β’ (π₯ β {π¦ β£ π} β [π₯ / π¦]π) |
df-cleq 2170 | β’ (βπ₯(π₯ β π¦ β π₯ β π§) β π¦ = π§) β β’ (π΄ = π΅ β βπ₯(π₯ β π΄ β π₯ β π΅)) |
df-clel 2173 | β’ (π΄ β π΅ β βπ₯(π₯ = π΄ β§ π₯ β π΅)) |
wnfc 2306 | wff β²π₯π΄ |
df-nfc 2308 | β’ (β²π₯π΄ β βπ¦β²π₯ π¦ β π΄) |
wne 2347 | wff π΄ β π΅ |
df-ne 2348 | β’ (π΄ β π΅ β Β¬ π΄ = π΅) |
wnel 2442 | wff π΄ β π΅ |
df-nel 2443 | β’ (π΄ β π΅ β Β¬ π΄ β π΅) |
wral 2455 | wff βπ₯ β π΄ π |
wrex 2456 | wff βπ₯ β π΄ π |
wreu 2457 | wff β!π₯ β π΄ π |
wrmo 2458 | wff β*π₯ β π΄ π |
crab 2459 | class {π₯ β π΄ β£ π} |
df-ral 2460 | β’ (βπ₯ β π΄ π β βπ₯(π₯ β π΄ β π)) |
df-rex 2461 | β’ (βπ₯ β π΄ π β βπ₯(π₯ β π΄ β§ π)) |
df-reu 2462 | β’ (β!π₯ β π΄ π β β!π₯(π₯ β π΄ β§ π)) |
df-rmo 2463 | β’ (β*π₯ β π΄ π β β*π₯(π₯ β π΄ β§ π)) |
df-rab 2464 | β’ {π₯ β π΄ β£ π} = {π₯ β£ (π₯ β π΄ β§ π)} |
cvv 2737 | class V |
df-v 2739 | β’ V = {π₯ β£ π₯ = π₯} |
wcdeq 2945 | wff CondEq(π₯ = π¦ β π) |
df-cdeq 2946 | β’ (CondEq(π₯ = π¦ β π) β (π₯ = π¦ β π)) |
wsbc 2962 | wff [π΄ / π₯]π |
df-sbc 2963 | β’ ([π΄ / π₯]π β π΄ β {π₯ β£ π}) |
csb 3057 | class β¦π΄ / π₯β¦π΅ |
df-csb 3058 | β’ β¦π΄ / π₯β¦π΅ = {π¦ β£ [π΄ / π₯]π¦ β π΅} |
cdif 3126 | class (π΄ β π΅) |
cun 3127 | class (π΄ βͺ π΅) |
cin 3128 | class (π΄ β© π΅) |
wss 3129 | wff π΄ β π΅ |
df-dif 3131 | β’ (π΄ β π΅) = {π₯ β£ (π₯ β π΄ β§ Β¬ π₯ β π΅)} |
df-un 3133 | β’ (π΄ βͺ π΅) = {π₯ β£ (π₯ β π΄ β¨ π₯ β π΅)} |
df-in 3135 | β’ (π΄ β© π΅) = {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} |
df-ss 3142 | β’ (π΄ β π΅ β (π΄ β© π΅) = π΄) |
c0 3422 | class β
|
df-nul 3423 | β’ β
= (V β V) |
cif 3534 | class if(π, π΄, π΅) |
df-if 3535 | β’ if(π, π΄, π΅) = {π₯ β£ ((π₯ β π΄ β§ π) β¨ (π₯ β π΅ β§ Β¬ π))} |
cpw 3575 | class π« π΄ |
df-pw 3577 | β’ π« π΄ = {π₯ β£ π₯ β π΄} |
csn 3592 | class {π΄} |
cpr 3593 | class {π΄, π΅} |
ctp 3594 | class {π΄, π΅, πΆ} |
cop 3595 | class β¨π΄, π΅β© |
cotp 3596 | class β¨π΄, π΅, πΆβ© |
df-sn 3598 | β’ {π΄} = {π₯ β£ π₯ = π΄} |
df-pr 3599 | β’ {π΄, π΅} = ({π΄} βͺ {π΅}) |
df-tp 3600 | β’ {π΄, π΅, πΆ} = ({π΄, π΅} βͺ {πΆ}) |
df-op 3601 | β’ β¨π΄, π΅β© = {π₯ β£ (π΄ β V β§ π΅ β V β§ π₯ β {{π΄}, {π΄, π΅}})} |
df-ot 3602 | β’ β¨π΄, π΅, πΆβ© = β¨β¨π΄, π΅β©, πΆβ© |
cuni 3809 | class βͺ
π΄ |
df-uni 3810 | β’ βͺ π΄ = {π₯ β£ βπ¦(π₯ β π¦ β§ π¦ β π΄)} |
cint 3844 | class β©
π΄ |
df-int 3845 | β’ β© π΄ = {π₯ β£ βπ¦(π¦ β π΄ β π₯ β π¦)} |
ciun 3886 | class βͺ π₯ β π΄ π΅ |
ciin 3887 | class β© π₯ β π΄ π΅ |
df-iun 3888 | β’ βͺ π₯ β π΄ π΅ = {π¦ β£ βπ₯ β π΄ π¦ β π΅} |
df-iin 3889 | β’ β© π₯ β π΄ π΅ = {π¦ β£ βπ₯ β π΄ π¦ β π΅} |
wdisj 3980 | wff Disj π₯ β π΄ π΅ |
df-disj 3981 | β’ (Disj π₯ β π΄ π΅ β βπ¦β*π₯ β π΄ π¦ β π΅) |
wbr 4003 | wff π΄π
π΅ |
df-br 4004 | β’ (π΄π
π΅ β β¨π΄, π΅β© β π
) |
copab 4063 | class {β¨π₯, π¦β© β£ π} |
cmpt 4064 | class (π₯ β π΄ β¦ π΅) |
df-opab 4065 | β’ {β¨π₯, π¦β© β£ π} = {π§ β£ βπ₯βπ¦(π§ = β¨π₯, π¦β© β§ π)} |
df-mpt 4066 | β’ (π₯ β π΄ β¦ π΅) = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = π΅)} |
wtr 4101 | wff Tr π΄ |
df-tr 4102 | β’ (Tr π΄ β βͺ π΄ β π΄) |
ax-coll 4118 | β’ β²ππ β β’ (βπ₯ β π βπ¦π β βπβπ₯ β π βπ¦ β π π) |
ax-sep 4121 | β’ βπ¦βπ₯(π₯ β π¦ β (π₯ β π§ β§ π)) |
ax-nul 4129 | β’ βπ₯βπ¦ Β¬ π¦ β π₯ |
ax-pow 4174 | β’ βπ¦βπ§(βπ€(π€ β π§ β π€ β π₯) β π§ β π¦) |
wem 4194 | wff
EXMID |
df-exmid 4195 | β’ (EXMID β βπ₯(π₯ β {β
} β
DECID β
β π₯)) |
ax-pr 4209 | β’ βπ§βπ€((π€ = π₯ β¨ π€ = π¦) β π€ β π§) |
cep 4287 | class E |
cid 4288 | class I |
df-eprel 4289 | β’ E = {β¨π₯, π¦β© β£ π₯ β π¦} |
df-id 4293 | β’ I = {β¨π₯, π¦β© β£ π₯ = π¦} |
wpo 4294 | wff π
Po π΄ |
wor 4295 | wff π
Or π΄ |
df-po 4296 | β’ (π
Po π΄ β βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (Β¬ π₯π
π₯ β§ ((π₯π
π¦ β§ π¦π
π§) β π₯π
π§))) |
df-iso 4297 | β’ (π
Or π΄ β (π
Po π΄ β§ βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯π
π¦ β (π₯π
π§ β¨ π§π
π¦)))) |
wfrfor 4327 | wff FrFor π
π΄π |
wfr 4328 | wff π
Fr π΄ |
wse 4329 | wff π
Se π΄ |
wwe 4330 | wff π
We π΄ |
df-frfor 4331 | β’ ( FrFor π
π΄π β (βπ₯ β π΄ (βπ¦ β π΄ (π¦π
π₯ β π¦ β π) β π₯ β π) β π΄ β π)) |
df-frind 4332 | β’ (π
Fr π΄ β βπ FrFor π
π΄π ) |
df-se 4333 | β’ (π
Se π΄ β βπ₯ β π΄ {π¦ β π΄ β£ π¦π
π₯} β V) |
df-wetr 4334 | β’ (π
We π΄ β (π
Fr π΄ β§ βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ ((π₯π
π¦ β§ π¦π
π§) β π₯π
π§))) |
word 4362 | wff Ord π΄ |
con0 4363 | class On |
wlim 4364 | wff Lim π΄ |
csuc 4365 | class suc π΄ |
df-iord 4366 | β’ (Ord π΄ β (Tr π΄ β§ βπ₯ β π΄ Tr π₯)) |
df-on 4368 | β’ On = {π₯ β£ Ord π₯} |
df-ilim 4369 | β’ (Lim π΄ β (Ord π΄ β§ β
β π΄ β§ π΄ = βͺ π΄)) |
df-suc 4371 | β’ suc π΄ = (π΄ βͺ {π΄}) |
ax-un 4433 | β’ βπ¦βπ§(βπ€(π§ β π€ β§ π€ β π₯) β π§ β π¦) |
ax-setind 4536 | β’ (βπ(βπ¦ β π [π¦ / π]π β π) β βππ) |
ax-iinf 4587 | β’ βπ₯(β
β π₯ β§ βπ¦(π¦ β π₯ β suc π¦ β π₯)) |
com 4589 | class Ο |
df-iom 4590 | β’ Ο = β© {π₯ β£ (β
β π₯ β§ βπ¦ β π₯ suc π¦ β π₯)} |
cxp 4624 | class (π΄ Γ π΅) |
ccnv 4625 | class β‘π΄ |
cdm 4626 | class dom π΄ |
crn 4627 | class ran π΄ |
cres 4628 | class (π΄ βΎ π΅) |
cima 4629 | class (π΄ β π΅) |
ccom 4630 | class (π΄ β π΅) |
wrel 4631 | wff Rel π΄ |
df-xp 4632 | β’ (π΄ Γ π΅) = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β π΅)} |
df-rel 4633 | β’ (Rel π΄ β π΄ β (V Γ V)) |
df-cnv 4634 | β’ β‘π΄ = {β¨π₯, π¦β© β£ π¦π΄π₯} |
df-co 4635 | β’ (π΄ β π΅) = {β¨π₯, π¦β© β£ βπ§(π₯π΅π§ β§ π§π΄π¦)} |
df-dm 4636 | β’ dom π΄ = {π₯ β£ βπ¦ π₯π΄π¦} |
df-rn 4637 | β’ ran π΄ = dom β‘π΄ |
df-res 4638 | β’ (π΄ βΎ π΅) = (π΄ β© (π΅ Γ V)) |
df-ima 4639 | β’ (π΄ β π΅) = ran (π΄ βΎ π΅) |
cio 5176 | class (β©π₯π) |
df-iota 5178 | β’ (β©π₯π) = βͺ {π¦ β£ {π₯ β£ π} = {π¦}} |
wfun 5210 | wff Fun π΄ |
wfn 5211 | wff π΄ Fn π΅ |
wf 5212 | wff πΉ:π΄βΆπ΅ |
wf1 5213 | wff πΉ:π΄β1-1βπ΅ |
wfo 5214 | wff πΉ:π΄βontoβπ΅ |
wf1o 5215 | wff πΉ:π΄β1-1-ontoβπ΅ |
cfv 5216 | class (πΉβπ΄) |
wiso 5217 | wff π» Isom π
, π (π΄, π΅) |
df-fun 5218 | β’ (Fun π΄ β (Rel π΄ β§ (π΄ β β‘π΄) β I )) |
df-fn 5219 | β’ (π΄ Fn π΅ β (Fun π΄ β§ dom π΄ = π΅)) |
df-f 5220 | β’ (πΉ:π΄βΆπ΅ β (πΉ Fn π΄ β§ ran πΉ β π΅)) |
df-f1 5221 | β’ (πΉ:π΄β1-1βπ΅ β (πΉ:π΄βΆπ΅ β§ Fun β‘πΉ)) |
df-fo 5222 | β’ (πΉ:π΄βontoβπ΅ β (πΉ Fn π΄ β§ ran πΉ = π΅)) |
df-f1o 5223 | β’ (πΉ:π΄β1-1-ontoβπ΅ β (πΉ:π΄β1-1βπ΅ β§ πΉ:π΄βontoβπ΅)) |
df-fv 5224 | β’ (πΉβπ΄) = (β©π₯π΄πΉπ₯) |
df-isom 5225 | β’ (π» Isom π
, π (π΄, π΅) β (π»:π΄β1-1-ontoβπ΅ β§ βπ₯ β π΄ βπ¦ β π΄ (π₯π
π¦ β (π»βπ₯)π(π»βπ¦)))) |
crio 5829 | class (β©π₯ β π΄ π) |
df-riota 5830 | β’ (β©π₯ β π΄ π) = (β©π₯(π₯ β π΄ β§ π)) |
co 5874 | class (π΄πΉπ΅) |
coprab 5875 | class {β¨β¨π₯, π¦β©, π§β© β£ π} |
cmpo 5876 | class (π₯ β π΄, π¦ β π΅ β¦ πΆ) |
df-ov 5877 | β’ (π΄πΉπ΅) = (πΉββ¨π΄, π΅β©) |
df-oprab 5878 | β’ {β¨β¨π₯, π¦β©, π§β© β£ π} = {π€ β£ βπ₯βπ¦βπ§(π€ = β¨β¨π₯, π¦β©, π§β© β§ π)} |
df-mpo 5879 | β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) = {β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β π΄ β§ π¦ β π΅) β§ π§ = πΆ)} |
cof 6080 | class βπ
π
|
cofr 6081 | class βπ
π
|
df-of 6082 | β’ βπ
π
= (π β V, π β V β¦ (π₯ β (dom π β© dom π) β¦ ((πβπ₯)π
(πβπ₯)))) |
df-ofr 6083 | β’ βπ π
= {β¨π, πβ© β£ βπ₯ β (dom π β© dom π)(πβπ₯)π
(πβπ₯)} |
c1st 6138 | class 1st |
c2nd 6139 | class 2nd |
df-1st 6140 | β’ 1st = (π₯ β V β¦ βͺ dom {π₯}) |
df-2nd 6141 | β’ 2nd = (π₯ β V β¦ βͺ ran {π₯}) |
ctpos 6244 | class tpos πΉ |
df-tpos 6245 | β’ tpos πΉ = (πΉ β (π₯ β (β‘dom πΉ βͺ {β
}) β¦ βͺ β‘{π₯})) |
wsmo 6285 | wff Smo π΄ |
df-smo 6286 | β’ (Smo π΄ β (π΄:dom π΄βΆOn β§ Ord dom π΄ β§ βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)))) |
crecs 6304 | class recs(πΉ) |
df-recs 6305 | β’ recs(πΉ) = βͺ {π β£ βπ₯ β On (π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦)))} |
crdg 6369 | class rec(πΉ, πΌ) |
df-irdg 6370 | β’ rec(πΉ, πΌ) = recs((π β V β¦ (πΌ βͺ βͺ
π₯ β dom π(πΉβ(πβπ₯))))) |
cfrec 6390 | class frec(πΉ, πΌ) |
df-frec 6391 | β’ frec(πΉ, πΌ) = (recs((π β V β¦ {π₯ β£ (βπ β Ο (dom π = suc π β§ π₯ β (πΉβ(πβπ))) β¨ (dom π = β
β§ π₯ β πΌ))})) βΎ Ο) |
c1o 6409 | class 1o |
c2o 6410 | class 2o |
c3o 6411 | class 3o |
c4o 6412 | class 4o |
coa 6413 | class +o |
comu 6414 | class
Β·o |
coei 6415 | class
βo |
df-1o 6416 | β’ 1o = suc
β
|
df-2o 6417 | β’ 2o = suc
1o |
df-3o 6418 | β’ 3o = suc
2o |
df-4o 6419 | β’ 4o = suc
3o |
df-oadd 6420 | β’ +o = (π₯ β On, π¦ β On β¦ (rec((π§ β V β¦ suc π§), π₯)βπ¦)) |
df-omul 6421 | β’ Β·o = (π₯ β On, π¦ β On β¦ (rec((π§ β V β¦ (π§ +o π₯)), β
)βπ¦)) |
df-oexpi 6422 | β’ βo = (π₯ β On, π¦ β On β¦ (rec((π§ β V β¦ (π§ Β·o π₯)), 1o)βπ¦)) |
wer 6531 | wff π
Er π΄ |
cec 6532 | class [π΄]π
|
cqs 6533 | class (π΄ / π
) |
df-er 6534 | β’ (π
Er π΄ β (Rel π
β§ dom π
= π΄ β§ (β‘π
βͺ (π
β π
)) β π
)) |
df-ec 6536 | β’ [π΄]π
= (π
β {π΄}) |
df-qs 6540 | β’ (π΄ / π
) = {π¦ β£ βπ₯ β π΄ π¦ = [π₯]π
} |
cmap 6647 | class
βπ |
cpm 6648 | class
βpm |
df-map 6649 | β’ βπ = (π₯ β V, π¦ β V β¦ {π β£ π:π¦βΆπ₯}) |
df-pm 6650 | β’ βpm =
(π₯ β V, π¦ β V β¦ {π β π« (π¦ Γ π₯) β£ Fun π}) |
cixp 6697 | class Xπ₯ β π΄ π΅ |
df-ixp 6698 | β’ Xπ₯ β π΄ π΅ = {π β£ (π Fn {π₯ β£ π₯ β π΄} β§ βπ₯ β π΄ (πβπ₯) β π΅)} |
cen 6737 | class β |
cdom 6738 | class βΌ |
cfn 6739 | class Fin |
df-en 6740 | β’ β = {β¨π₯, π¦β© β£ βπ π:π₯β1-1-ontoβπ¦} |
df-dom 6741 | β’ βΌ = {β¨π₯, π¦β© β£ βπ π:π₯β1-1βπ¦} |
df-fin 6742 | β’ Fin = {π₯ β£ βπ¦ β Ο π₯ β π¦} |
cfi 6966 | class fi |
df-fi 6967 | β’ fi = (π₯ β V β¦ {π§ β£ βπ¦ β (π« π₯ β© Fin)π§ = β© π¦}) |
csup 6980 | class sup(π΄, π΅, π
) |
cinf 6981 | class inf(π΄, π΅, π
) |
df-sup 6982 | β’ sup(π΄, π΅, π
) = βͺ {π₯ β π΅ β£ (βπ¦ β π΄ Β¬ π₯π
π¦ β§ βπ¦ β π΅ (π¦π
π₯ β βπ§ β π΄ π¦π
π§))} |
df-inf 6983 | β’ inf(π΄, π΅, π
) = sup(π΄, π΅, β‘π
) |
cdju 7035 | class (π΄ β π΅) |
df-dju 7036 | β’ (π΄ β π΅) = (({β
} Γ π΄) βͺ ({1o} Γ π΅)) |
cinl 7043 | class inl |
cinr 7044 | class inr |
df-inl 7045 | β’ inl = (π₯ β V β¦ β¨β
, π₯β©) |
df-inr 7046 | β’ inr = (π₯ β V β¦ β¨1o, π₯β©) |
cdjucase 7081 | class case(π
, π) |
df-case 7082 | β’ case(π
, π) = ((π
β β‘inl) βͺ (π β β‘inr)) |
cdjud 7100 | class (π
βd π) |
df-djud 7101 | β’ (π
βd π) = ((π
β β‘(inl βΎ dom π
)) βͺ (π β β‘(inr βΎ dom π))) |
xnninf 7117 | class ββ |
df-nninf 7118 | β’ ββ = {π β (2o
βπ Ο) β£ βπ β Ο (πβsuc π) β (πβπ)} |
comni 7131 | class Omni |
df-omni 7132 | β’ Omni = {π¦ β£ βπ(π:π¦βΆ2o β (βπ₯ β π¦ (πβπ₯) = β
β¨ βπ₯ β π¦ (πβπ₯) = 1o))} |
cmarkov 7148 | class Markov |
df-markov 7149 | β’ Markov = {π¦ β£ βπ(π:π¦βΆ2o β (Β¬
βπ₯ β π¦ (πβπ₯) = 1o β βπ₯ β π¦ (πβπ₯) = β
))} |
cwomni 7160 | class WOmni |
df-womni 7161 | β’ WOmni = {π¦ β£ βπ(π:π¦βΆ2o β
DECID βπ₯ β π¦ (πβπ₯) = 1o)} |
ccrd 7177 | class card |
df-card 7178 | β’ card = (π₯ β V β¦ β© {π¦
β On β£ π¦ β
π₯}) |
wac 7203 | wff
CHOICE |
df-ac 7204 | β’ (CHOICE β
βπ₯βπ(π β π₯ β§ π Fn dom π₯)) |
wap 7245 | wff π
Ap π΄ |
df-pap 7246 | β’ (π
Ap π΄ β ((π
β (π΄ Γ π΄) β§ βπ₯ β π΄ Β¬ π₯π
π₯) β§ (βπ₯ β π΄ βπ¦ β π΄ (π₯π
π¦ β π¦π
π₯) β§ βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯π
π¦ β (π₯π
π§ β¨ π¦π
π§))))) |
wtap 7247 | wff π
TAp π΄ |
df-tap 7248 | β’ (π
TAp π΄ β (π
Ap π΄ β§ βπ₯ β π΄ βπ¦ β π΄ (Β¬ π₯π
π¦ β π₯ = π¦))) |
wacc 7260 | wff
CCHOICE |
df-cc 7261 | β’ (CCHOICE β
βπ₯(dom π₯ β Ο β
βπ(π β π₯ β§ π Fn dom π₯))) |
cnpi 7270 | class N |
cpli 7271 | class
+N |
cmi 7272 | class
Β·N |
clti 7273 | class
<N |
cplpq 7274 | class
+pQ |
cmpq 7275 | class
Β·pQ |
cltpq 7276 | class
<pQ |
ceq 7277 | class
~Q |
cnq 7278 | class Q |
c1q 7279 | class
1Q |
cplq 7280 | class
+Q |
cmq 7281 | class
Β·Q |
crq 7282 | class
*Q |
cltq 7283 | class
<Q |
ceq0 7284 | class
~Q0 |
cnq0 7285 | class
Q0 |
c0q0 7286 | class
0Q0 |
cplq0 7287 | class
+Q0 |
cmq0 7288 | class
Β·Q0 |
cnp 7289 | class P |
c1p 7290 | class
1P |
cpp 7291 | class
+P |
cmp 7292 | class
Β·P |
cltp 7293 | class
<P |
cer 7294 | class
~R |
cnr 7295 | class R |
c0r 7296 | class
0R |
c1r 7297 | class
1R |
cm1r 7298 | class
-1R |
cplr 7299 | class
+R |
cmr 7300 | class
Β·R |
cltr 7301 | class
<R |
df-ni 7302 | β’ N = (Ο
β {β
}) |
df-pli 7303 | β’ +N = (
+o βΎ (N Γ
N)) |
df-mi 7304 | β’
Β·N = ( Β·o βΎ
(N Γ N)) |
df-lti 7305 | β’ <N = ( E β©
(N Γ N)) |
df-plpq 7342 | β’ +pQ = (π₯ β (N Γ
N), π¦ β
(N Γ N) β¦ β¨(((1st
βπ₯)
Β·N (2nd βπ¦)) +N
((1st βπ¦)
Β·N (2nd βπ₯))), ((2nd βπ₯)
Β·N (2nd βπ¦))β©) |
df-mpq 7343 | β’ Β·pQ = (π₯ β (N Γ
N), π¦ β
(N Γ N) β¦ β¨((1st
βπ₯)
Β·N (1st βπ¦)), ((2nd βπ₯)
Β·N (2nd βπ¦))β©) |
df-ltpq 7344 | β’ <pQ =
{β¨π₯, π¦β© β£ ((π₯ β (N Γ
N) β§ π¦
β (N Γ N)) β§ ((1st
βπ₯)
Β·N (2nd βπ¦)) <N
((1st βπ¦)
Β·N (2nd βπ₯)))} |
df-enq 7345 | β’ ~Q = {β¨π₯, π¦β© β£ ((π₯ β (N Γ
N) β§ π¦
β (N Γ N)) β§ βπ§βπ€βπ£βπ’((π₯ = β¨π§, π€β© β§ π¦ = β¨π£, π’β©) β§ (π§ Β·N π’) = (π€ Β·N π£)))} |
df-nqqs 7346 | β’ Q = ((N Γ
N) / ~Q ) |
df-plqqs 7347 | β’ +Q =
{β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β Q β§ π¦ β Q) β§
βπ€βπ£βπ’βπ((π₯ = [β¨π€, π£β©] ~Q β§
π¦ = [β¨π’, πβ©] ~Q ) β§
π§ = [(β¨π€, π£β© +pQ
β¨π’, πβ©)] ~Q
))} |
df-mqqs 7348 | β’ Β·Q =
{β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β Q β§ π¦ β Q) β§
βπ€βπ£βπ’βπ((π₯ = [β¨π€, π£β©] ~Q β§
π¦ = [β¨π’, πβ©] ~Q ) β§
π§ = [(β¨π€, π£β© Β·pQ
β¨π’, πβ©)] ~Q
))} |
df-1nqqs 7349 | β’ 1Q =
[β¨1o, 1oβ©]
~Q |
df-rq 7350 | β’ *Q =
{β¨π₯, π¦β© β£ (π₯ β Q β§
π¦ β Q
β§ (π₯
Β·Q π¦) =
1Q)} |
df-ltnqqs 7351 | β’ <Q =
{β¨π₯, π¦β© β£ ((π₯ β Q β§
π¦ β Q)
β§ βπ§βπ€βπ£βπ’((π₯ = [β¨π§, π€β©] ~Q β§
π¦ = [β¨π£, π’β©] ~Q ) β§
(π§
Β·N π’) <N (π€
Β·N π£)))} |
df-enq0 7422 | β’ ~Q0 = {β¨π₯, π¦β© β£ ((π₯ β (Ο Γ N)
β§ π¦ β (Ο
Γ N)) β§ βπ§βπ€βπ£βπ’((π₯ = β¨π§, π€β© β§ π¦ = β¨π£, π’β©) β§ (π§ Β·o π’) = (π€ Β·o π£)))} |
df-nq0 7423 | β’ Q0 = ((Ο
Γ N) / ~Q0
) |
df-0nq0 7424 | β’ 0Q0 =
[β¨β
, 1oβ©]
~Q0 |
df-plq0 7425 | β’ +Q0 =
{β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β Q0 β§
π¦ β
Q0) β§ βπ€βπ£βπ’βπ((π₯ = [β¨π€, π£β©] ~Q0 β§
π¦ = [β¨π’, πβ©] ~Q0 ) β§
π§ = [β¨((π€ Β·o π) +o (π£ Β·o π’)), (π£ Β·o π)β©] ~Q0
))} |
df-mq0 7426 | β’ Β·Q0 =
{β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β Q0 β§
π¦ β
Q0) β§ βπ€βπ£βπ’βπ((π₯ = [β¨π€, π£β©] ~Q0 β§
π¦ = [β¨π’, πβ©] ~Q0 ) β§
π§ = [β¨(π€ Β·o π’), (π£ Β·o π)β©] ~Q0
))} |
df-inp 7464 | β’ P = {β¨π, π’β© β£ (((π β Q β§ π’ β Q) β§
(βπ β
Q π β
π β§ βπ β Q π β π’)) β§ ((βπ β Q (π β π β βπ β Q (π <Q π β§ π β π)) β§ βπ β Q (π β π’ β βπ β Q (π <Q π β§ π β π’))) β§ βπ β Q Β¬ (π β π β§ π β π’) β§ βπ β Q βπ β Q (π <Q
π β (π β π β¨ π β π’))))} |
df-i1p 7465 | β’ 1P = β¨{π β£ π <Q
1Q}, {π’ β£ 1Q
<Q π’}β© |
df-iplp 7466 | β’ +P = (π₯ β P, π¦ β P β¦
β¨{π β
Q β£ βπ β Q βπ β Q (π β (1st
βπ₯) β§ π β (1st
βπ¦) β§ π = (π +Q π ))}, {π β Q β£ βπ β Q
βπ β
Q (π β
(2nd βπ₯)
β§ π β
(2nd βπ¦)
β§ π = (π +Q
π ))}β©) |
df-imp 7467 | β’ Β·P = (π₯ β P, π¦ β P β¦
β¨{π β
Q β£ βπ β Q βπ β Q (π β (1st
βπ₯) β§ π β (1st
βπ¦) β§ π = (π Β·Q π ))}, {π β Q β£ βπ β Q
βπ β
Q (π β
(2nd βπ₯)
β§ π β
(2nd βπ¦)
β§ π = (π
Β·Q π ))}β©) |
df-iltp 7468 | β’ <P = {β¨π₯, π¦β© β£ ((π₯ β P β§ π¦ β P) β§
βπ β
Q (π β
(2nd βπ₯)
β§ π β
(1st βπ¦)))} |
df-enr 7724 | β’ ~R = {β¨π₯, π¦β© β£ ((π₯ β (P Γ
P) β§ π¦
β (P Γ P)) β§ βπ§βπ€βπ£βπ’((π₯ = β¨π§, π€β© β§ π¦ = β¨π£, π’β©) β§ (π§ +P π’) = (π€ +P π£)))} |
df-nr 7725 | β’ R =
((P Γ P) / ~R
) |
df-plr 7726 | β’ +R =
{β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β R β§ π¦ β R) β§
βπ€βπ£βπ’βπ((π₯ = [β¨π€, π£β©] ~R β§
π¦ = [β¨π’, πβ©] ~R ) β§
π§ = [β¨(π€ +P
π’), (π£ +P π)β©]
~R ))} |
df-mr 7727 | β’
Β·R = {β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β R β§ π¦ β R) β§
βπ€βπ£βπ’βπ((π₯ = [β¨π€, π£β©] ~R β§
π¦ = [β¨π’, πβ©] ~R ) β§
π§ = [β¨((π€
Β·P π’) +P (π£
Β·P π)), ((π€ Β·P π) +P
(π£
Β·P π’))β©] ~R
))} |
df-ltr 7728 | β’ <R =
{β¨π₯, π¦β© β£ ((π₯ β R β§
π¦ β R)
β§ βπ§βπ€βπ£βπ’((π₯ = [β¨π§, π€β©] ~R β§
π¦ = [β¨π£, π’β©] ~R ) β§
(π§
+P π’)<P (π€ +P
π£)))} |
df-0r 7729 | β’ 0R =
[β¨1P, 1Pβ©]
~R |
df-1r 7730 | β’ 1R =
[β¨(1P +P
1P), 1Pβ©]
~R |
df-m1r 7731 | β’ -1R =
[β¨1P, (1P
+P 1P)β©]
~R |
cc 7808 | class β |
cr 7809 | class β |
cc0 7810 | class 0 |
c1 7811 | class 1 |
ci 7812 | class i |
caddc 7813 | class + |
cltrr 7814 | class
<β |
cmul 7815 | class Β· |
df-c 7816 | β’ β = (R
Γ R) |
df-0 7817 | β’ 0 =
β¨0R,
0Rβ© |
df-1 7818 | β’ 1 =
β¨1R,
0Rβ© |
df-i 7819 | β’ i =
β¨0R,
1Rβ© |
df-r 7820 | β’ β = (R
Γ {0R}) |
df-add 7821 | β’ + = {β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β β β§ π¦ β β) β§ βπ€βπ£βπ’βπ((π₯ = β¨π€, π£β© β§ π¦ = β¨π’, πβ©) β§ π§ = β¨(π€ +R π’), (π£ +R π)β©))} |
df-mul 7822 | β’ Β· = {β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β β β§ π¦ β β) β§ βπ€βπ£βπ’βπ((π₯ = β¨π€, π£β© β§ π¦ = β¨π’, πβ©) β§ π§ = β¨((π€ Β·R π’) +R
(-1R Β·R (π£
Β·R π))), ((π£ Β·R π’) +R
(π€
Β·R π))β©))} |
df-lt 7823 | β’ <β =
{β¨π₯, π¦β© β£ ((π₯ β β β§ π¦ β β) β§
βπ§βπ€((π₯ = β¨π§, 0Rβ© β§
π¦ = β¨π€,
0Rβ©) β§ π§ <R π€))} |
ax-cnex 7901 | β’ β β V |
ax-resscn 7902 | β’ β β β |
ax-1cn 7903 | β’ 1 β β |
ax-1re 7904 | β’ 1 β β |
ax-icn 7905 | β’ i β β |
ax-addcl 7906 | β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) β β) |
ax-addrcl 7907 | β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) β β) |
ax-mulcl 7908 | β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) β β) |
ax-mulrcl 7909 | β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) β β) |
ax-addcom 7910 | β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) = (π΅ + π΄)) |
ax-mulcom 7911 | β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) = (π΅ Β· π΄)) |
ax-addass 7912 | β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ))) |
ax-mulass 7913 | β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ))) |
ax-distr 7914 | β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β· (π΅ + πΆ)) = ((π΄ Β· π΅) + (π΄ Β· πΆ))) |
ax-i2m1 7915 | β’ ((i Β· i) + 1) = 0 |
ax-0lt1 7916 | β’ 0 <β 1 |
ax-1rid 7917 | β’ (π΄ β β β (π΄ Β· 1) = π΄) |
ax-0id 7918 | β’ (π΄ β β β (π΄ + 0) = π΄) |
ax-rnegex 7919 | β’ (π΄ β β β βπ₯ β β (π΄ + π₯) = 0) |
ax-precex 7920 | β’ ((π΄ β β β§ 0
<β π΄)
β βπ₯ β
β (0 <β π₯ β§ (π΄ Β· π₯) = 1)) |
ax-cnre 7921 | β’ (π΄ β β β βπ₯ β β βπ¦ β β π΄ = (π₯ + (i Β· π¦))) |
ax-pre-ltirr 7922 | β’ (π΄ β β β Β¬ π΄ <β π΄) |
ax-pre-ltwlin 7923 | β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ <β π΅ β (π΄ <β πΆ β¨ πΆ <β π΅))) |
ax-pre-lttrn 7924 | β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ <β π΅ β§ π΅ <β πΆ) β π΄ <β πΆ)) |
ax-pre-apti 7925 | β’ ((π΄ β β β§ π΅ β β β§ Β¬ (π΄ <β π΅ β¨ π΅ <β π΄)) β π΄ = π΅) |
ax-pre-ltadd 7926 | β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ <β π΅ β (πΆ + π΄) <β (πΆ + π΅))) |
ax-pre-mulgt0 7927 | β’ ((π΄ β β β§ π΅ β β) β ((0
<β π΄
β§ 0 <β π΅) β 0 <β (π΄ Β· π΅))) |
ax-pre-mulext 7928 | β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· πΆ) <β (π΅ Β· πΆ) β (π΄ <β π΅ β¨ π΅ <β π΄))) |
ax-arch 7929 | β’ (π΄ β β β βπ β β© {π₯
β£ (1 β π₯ β§
βπ¦ β π₯ (π¦ + 1) β π₯)}π΄ <β π) |
ax-caucvg 7930 | β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)}
& β’ (π β πΉ:πβΆβ) & β’ (π β βπ β π βπ β π (π <β π β ((πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1)) β§ (πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1))))) β β’ (π β βπ¦ β β βπ₯ β β (0 <β
π₯ β βπ β π βπ β π (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯))))) |
ax-pre-suploc 7931 | β’ (((π΄ β β β§ βπ₯ π₯ β π΄) β§ (βπ₯ β β βπ¦ β π΄ π¦ <β π₯ β§ βπ₯ β β βπ¦ β β (π₯ <β π¦ β (βπ§ β π΄ π₯ <β π§ β¨ βπ§ β π΄ π§ <β π¦)))) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§))) |
ax-addf 7932 | β’ + :(β Γ
β)βΆβ |
ax-mulf 7933 | β’ Β· :(β Γ
β)βΆβ |
cpnf 7988 | class +β |
cmnf 7989 | class -β |
cxr 7990 | class
β* |
clt 7991 | class < |
cle 7992 | class β€ |
df-pnf 7993 | β’ +β = π« βͺ β |
df-mnf 7994 | β’ -β = π«
+β |
df-xr 7995 | β’ β* = (β
βͺ {+β, -β}) |
df-ltxr 7996 | β’ < = ({β¨π₯, π¦β© β£ (π₯ β β β§ π¦ β β β§ π₯ <β π¦)} βͺ (((β βͺ {-β}) Γ
{+β}) βͺ ({-β} Γ β))) |
df-le 7997 | β’ β€ = ((β*
Γ β*) β β‘
< ) |
cmin 8127 | class β |
cneg 8128 | class -π΄ |
df-sub 8129 | β’ β = (π₯ β β, π¦ β β β¦ (β©π§ β β (π¦ + π§) = π₯)) |
df-neg 8130 | β’ -π΄ = (0 β π΄) |
creap 8530 | class
#β |
df-reap 8531 | β’ #β = {β¨π₯, π¦β© β£ ((π₯ β β β§ π¦ β β) β§ (π₯ < π¦ β¨ π¦ < π₯))} |
cap 8537 | class # |
df-ap 8538 | β’ # = {β¨π₯, π¦β© β£ βπ β β βπ β β βπ‘ β β βπ’ β β ((π₯ = (π + (i Β· π )) β§ π¦ = (π‘ + (i Β· π’))) β§ (π #β π‘ β¨ π #β π’))} |
cdiv 8628 | class / |
df-div 8629 | β’ / = (π₯ β β, π¦ β (β β {0}) β¦
(β©π§ β
β (π¦ Β· π§) = π₯)) |
cn 8918 | class β |
df-inn 8919 | β’ β = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} |
c2 8969 | class 2 |
c3 8970 | class 3 |
c4 8971 | class 4 |
c5 8972 | class 5 |
c6 8973 | class 6 |
c7 8974 | class 7 |
c8 8975 | class 8 |
c9 8976 | class 9 |
df-2 8977 | β’ 2 = (1 + 1) |
df-3 8978 | β’ 3 = (2 + 1) |
df-4 8979 | β’ 4 = (3 + 1) |
df-5 8980 | β’ 5 = (4 + 1) |
df-6 8981 | β’ 6 = (5 + 1) |
df-7 8982 | β’ 7 = (6 + 1) |
df-8 8983 | β’ 8 = (7 + 1) |
df-9 8984 | β’ 9 = (8 + 1) |
cn0 9175 | class
β0 |
df-n0 9176 | β’ β0 = (β
βͺ {0}) |
cxnn0 9238 | class
β0* |
df-xnn0 9239 | β’ β0* =
(β0 βͺ {+β}) |
cz 9252 | class β€ |
df-z 9253 | β’ β€ = {π β β β£ (π = 0 β¨ π β β β¨ -π β β)} |
cdc 9383 | class ;π΄π΅ |
df-dec 9384 | β’ ;π΄π΅ = (((9 + 1) Β· π΄) + π΅) |
cuz 9527 | class
β€β₯ |
df-uz 9528 | β’ β€β₯ = (π β β€ β¦ {π β β€ β£ π β€ π}) |
cq 9618 | class β |
df-q 9619 | β’ β = ( / β (β€
Γ β)) |
crp 9652 | class
β+ |
df-rp 9653 | β’ β+ = {π₯ β β β£ 0 <
π₯} |
cxne 9768 | class -ππ΄ |
cxad 9769 | class
+π |
cxmu 9770 | class
Β·e |
df-xneg 9771 | β’ -ππ΄ = if(π΄ = +β, -β, if(π΄ = -β, +β, -π΄)) |
df-xadd 9772 | β’ +π = (π₯ β β*, π¦ β β*
β¦ if(π₯ = +β,
if(π¦ = -β, 0,
+β), if(π₯ = -β,
if(π¦ = +β, 0,
-β), if(π¦ = +β,
+β, if(π¦ = -β,
-β, (π₯ + π¦)))))) |
df-xmul 9773 | β’ Β·e = (π₯ β β*, π¦ β β*
β¦ if((π₯ = 0 β¨
π¦ = 0), 0, if((((0 <
π¦ β§ π₯ = +β) β¨ (π¦ < 0 β§ π₯ = -β)) β¨ ((0 < π₯ β§ π¦ = +β) β¨ (π₯ < 0 β§ π¦ = -β))), +β, if((((0 < π¦ β§ π₯ = -β) β¨ (π¦ < 0 β§ π₯ = +β)) β¨ ((0 < π₯ β§ π¦ = -β) β¨ (π₯ < 0 β§ π¦ = +β))), -β, (π₯ Β· π¦))))) |
cioo 9887 | class (,) |
cioc 9888 | class (,] |
cico 9889 | class [,) |
cicc 9890 | class [,] |
df-ioo 9891 | β’ (,) = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ < π§ β§ π§ < π¦)}) |
df-ioc 9892 | β’ (,] = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ < π§ β§ π§ β€ π¦)}) |
df-ico 9893 | β’ [,) = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ β€ π§ β§ π§ < π¦)}) |
df-icc 9894 | β’ [,] = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ β€ π§ β§ π§ β€ π¦)}) |
cfz 10007 | class ... |
df-fz 10008 | β’ ... = (π β β€, π β β€ β¦ {π β β€ β£ (π β€ π β§ π β€ π)}) |
cfzo 10141 | class ..^ |
df-fzo 10142 | β’ ..^ = (π β β€, π β β€ β¦ (π...(π β 1))) |
cfl 10267 | class β |
cceil 10268 | class β |
df-fl 10269 | β’ β = (π₯ β β β¦ (β©π¦ β β€ (π¦ β€ π₯ β§ π₯ < (π¦ + 1)))) |
df-ceil 10270 | β’ β = (π₯ β β β¦
-(ββ-π₯)) |
cmo 10321 | class mod |
df-mod 10322 | β’ mod = (π₯ β β, π¦ β β+ β¦ (π₯ β (π¦ Β· (ββ(π₯ / π¦))))) |
cseq 10444 | class seqπ( + , πΉ) |
df-seqfrec 10445 | β’ seqπ( + , πΉ) = ran frec((π₯ β (β€β₯βπ), π¦ β V β¦ β¨(π₯ + 1), (π¦ + (πΉβ(π₯ + 1)))β©), β¨π, (πΉβπ)β©) |
cexp 10518 | class β |
df-exp 10519 | β’ β = (π₯ β β, π¦ β β€ β¦ if(π¦ = 0, 1, if(0 < π¦, (seq1( Β· , (β Γ {π₯}))βπ¦), (1 / (seq1( Β· , (β Γ
{π₯}))β-π¦))))) |
cfa 10704 | class ! |
df-fac 10705 | β’ ! = ({β¨0, 1β©} βͺ seq1( Β·
, I )) |
cbc 10726 | class C |
df-bc 10727 | β’ C = (π β β0, π β β€ β¦ if(π β (0...π), ((!βπ) / ((!β(π β π)) Β· (!βπ))), 0)) |
chash 10754 | class β― |
df-ihash 10755 | β’ β― = ((frec((π₯ β β€ β¦ (π₯ + 1)), 0) βͺ {β¨Ο,
+ββ©}) β (π₯
β V β¦ βͺ {π¦ β (Ο βͺ {Ο}) β£
π¦ βΌ π₯})) |
cshi 10822 | class shift |
df-shft 10823 | β’ shift = (π β V, π₯ β β β¦ {β¨π¦, π§β© β£ (π¦ β β β§ (π¦ β π₯)ππ§)}) |
ccj 10847 | class β |
cre 10848 | class β |
cim 10849 | class β |
df-cj 10850 | β’ β = (π₯ β β β¦ (β©π¦ β β ((π₯ + π¦) β β β§ (i Β· (π₯ β π¦)) β β))) |
df-re 10851 | β’ β = (π₯ β β β¦ ((π₯ + (ββπ₯)) / 2)) |
df-im 10852 | β’ β = (π₯ β β β¦ (ββ(π₯ / i))) |
csqrt 11004 | class β |
cabs 11005 | class abs |
df-rsqrt 11006 | β’ β = (π₯ β β β¦ (β©π¦ β β ((π¦β2) = π₯ β§ 0 β€ π¦))) |
df-abs 11007 | β’ abs = (π₯ β β β¦ (ββ(π₯ Β· (ββπ₯)))) |
cli 11285 | class β |
df-clim 11286 | β’ β = {β¨π, π¦β© β£ (π¦ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β π¦)) < π₯))} |
csu 11360 | class Ξ£π β π΄ π΅ |
df-sumdc 11361 | β’ Ξ£π β π΄ π΅ = (β©π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
cprod 11557 | class βπ β π΄ π΅ |
df-proddc 11558 | β’ βπ β π΄ π΅ = (β©π₯(βπ β β€ ((π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄) β§ (βπ β (β€β₯βπ)βπ¦(π¦ # 0 β§ seqπ( Β· , (π β β€ β¦ if(π β π΄, π΅, 1))) β π¦) β§ seqπ( Β· , (π β β€ β¦ if(π β π΄, π΅, 1))) β π₯)) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( Β· , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 1)))βπ)))) |
ce 11649 | class exp |
ceu 11650 | class e |
csin 11651 | class sin |
ccos 11652 | class cos |
ctan 11653 | class tan |
cpi 11654 | class Ο |
df-ef 11655 | β’ exp = (π₯ β β β¦ Ξ£π β β0
((π₯βπ) / (!βπ))) |
df-e 11656 | β’ e =
(expβ1) |
df-sin 11657 | β’ sin = (π₯ β β β¦ (((expβ(i
Β· π₯)) β
(expβ(-i Β· π₯))) / (2 Β· i))) |
df-cos 11658 | β’ cos = (π₯ β β β¦ (((expβ(i
Β· π₯)) +
(expβ(-i Β· π₯))) / 2)) |
df-tan 11659 | β’ tan = (π₯ β (β‘cos β (β β {0})) β¦
((sinβπ₯) /
(cosβπ₯))) |
df-pi 11660 | β’ Ο = inf((β+
β© (β‘sin β {0})), β,
< ) |
ctau 11781 | class Ο |
df-tau 11782 | β’ Ο = inf((β+ β©
(β‘cos β {1})), β, <
) |
cdvds 11793 | class β₯ |
df-dvds 11794 | β’ β₯ = {β¨π₯, π¦β© β£ ((π₯ β β€ β§ π¦ β β€) β§ βπ β β€ (π Β· π₯) = π¦)} |
cgcd 11942 | class gcd |
df-gcd 11943 | β’ gcd = (π₯ β β€, π¦ β β€ β¦ if((π₯ = 0 β§ π¦ = 0), 0, sup({π β β€ β£ (π β₯ π₯ β§ π β₯ π¦)}, β, < ))) |
clcm 12059 | class lcm |
df-lcm 12060 | β’ lcm = (π₯ β β€, π¦ β β€ β¦ if((π₯ = 0 β¨ π¦ = 0), 0, inf({π β β β£ (π₯ β₯ π β§ π¦ β₯ π)}, β, < ))) |
cprime 12106 | class β |
df-prm 12107 | β’ β = {π β β β£ {π β β β£ π β₯ π} β 2o} |
cnumer 12180 | class numer |
cdenom 12181 | class denom |
df-numer 12182 | β’ numer = (π¦ β β β¦ (1st
β(β©π₯
β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π¦ = ((1st βπ₯) / (2nd βπ₯)))))) |
df-denom 12183 | β’ denom = (π¦ β β β¦ (2nd
β(β©π₯
β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π¦ = ((1st βπ₯) / (2nd βπ₯)))))) |
codz 12207 | class
odβ€ |
cphi 12208 | class Ο |
df-odz 12209 | β’ odβ€ = (π β β β¦ (π₯ β {π₯ β β€ β£ (π₯ gcd π) = 1} β¦ inf({π β β β£ π β₯ ((π₯βπ) β 1)}, β, <
))) |
df-phi 12210 | β’ Ο = (π β β β¦ (β―β{π₯ β (1...π) β£ (π₯ gcd π) = 1})) |
cpc 12283 | class pCnt |
df-pc 12284 | β’ pCnt = (π β β, π β β β¦ if(π = 0, +β, (β©π§βπ₯ β β€ βπ¦ β β (π = (π₯ / π¦) β§ π§ = (sup({π β β0 β£ (πβπ) β₯ π₯}, β, < ) β sup({π β β0
β£ (πβπ) β₯ π¦}, β, < )))))) |
cgz 12366 | class β€[i] |
df-gz 12367 | β’ β€[i] = {π₯ β β β£ ((ββπ₯) β β€ β§
(ββπ₯) β
β€)} |
cstr 12457 | class Struct |
cnx 12458 | class ndx |
csts 12459 | class sSet |
cslot 12460 | class Slot π΄ |
cbs 12461 | class Base |
cress 12462 | class
βΎs |
df-struct 12463 | β’ Struct = {β¨π, π₯β© β£ (π₯ β ( β€ β© (β Γ
β)) β§ Fun (π
β {β
}) β§ dom π β (...βπ₯))} |
df-ndx 12464 | β’ ndx = ( I βΎ β) |
df-slot 12465 | β’ Slot π΄ = (π₯ β V β¦ (π₯βπ΄)) |
df-base 12467 | β’ Base = Slot 1 |
df-sets 12468 | β’ sSet = (π β V, π β V β¦ ((π βΎ (V β dom {π})) βͺ {π})) |
df-iress 12469 | β’ βΎs = (π€ β V, π₯ β V β¦ (π€ sSet β¨(Baseβndx), (π₯ β© (Baseβπ€))β©)) |
cplusg 12535 | class +g |
cmulr 12536 | class .r |
cstv 12537 | class
*π |
csca 12538 | class Scalar |
cvsca 12539 | class
Β·π |
cip 12540 | class
Β·π |
cts 12541 | class TopSet |
cple 12542 | class le |
coc 12543 | class oc |
cds 12544 | class dist |
cunif 12545 | class UnifSet |
chom 12546 | class Hom |
cco 12547 | class comp |
df-plusg 12548 | β’ +g = Slot 2 |
df-mulr 12549 | β’ .r = Slot 3 |
df-starv 12550 | β’ *π = Slot
4 |
df-sca 12551 | β’ Scalar = Slot 5 |
df-vsca 12552 | β’ Β·π = Slot
6 |
df-ip 12553 | β’
Β·π = Slot 8 |
df-tset 12554 | β’ TopSet = Slot 9 |
df-ple 12555 | β’ le = Slot ;10 |
df-ocomp 12556 | β’ oc = Slot ;11 |
df-ds 12557 | β’ dist = Slot ;12 |
df-unif 12558 | β’ UnifSet = Slot ;13 |
df-hom 12559 | β’ Hom = Slot ;14 |
df-cco 12560 | β’ comp = Slot ;15 |
crest 12687 | class
βΎt |
ctopn 12688 | class TopOpen |
df-rest 12689 | β’ βΎt = (π β V, π₯ β V β¦ ran (π¦ β π β¦ (π¦ β© π₯))) |
df-topn 12690 | β’ TopOpen = (π€ β V β¦ ((TopSetβπ€) βΎt
(Baseβπ€))) |
ctg 12702 | class topGen |
cpt 12703 | class
βt |
c0g 12704 | class 0g |
cgsu 12705 | class
Ξ£g |
df-0g 12706 | β’ 0g = (π β V β¦ (β©π(π β (Baseβπ) β§ βπ₯ β (Baseβπ)((π(+gβπ)π₯) = π₯ β§ (π₯(+gβπ)π) = π₯)))) |
df-gsum 12707 | β’ Ξ£g = (π€ β V, π β V β¦ β¦{π₯ β (Baseβπ€) β£ βπ¦ β (Baseβπ€)((π₯(+gβπ€)π¦) = π¦ β§ (π¦(+gβπ€)π₯) = π¦)} / πβ¦if(ran π β π, (0gβπ€), if(dom π β ran ..., (β©π₯βπβπ β (β€β₯βπ)(dom π = (π...π) β§ π₯ = (seqπ((+gβπ€), π)βπ))), (β©π₯βπ[(β‘π β (V β π)) / π¦](π:(1...(β―βπ¦))β1-1-ontoβπ¦ β§ π₯ = (seq1((+gβπ€), (π β π))β(β―βπ¦))))))) |
df-topgen 12708 | β’ topGen = (π₯ β V β¦ {π¦ β£ π¦ β βͺ (π₯ β© π« π¦)}) |
df-pt 12709 | β’ βt = (π β V β¦
(topGenβ{π₯ β£
βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦))})) |
cprds 12713 | class Xs |
cpws 12714 | class
βs |
df-prds 12715 | β’ Xs = (π β V, π β V β¦ β¦Xπ₯ β
dom π(Baseβ(πβπ₯)) / π£β¦β¦(π β π£, π β π£ β¦ Xπ₯ β dom π((πβπ₯)(Hom β(πβπ₯))(πβπ₯))) / ββ¦(({β¨(Baseβndx),
π£β©,
β¨(+gβndx), (π β π£, π β π£ β¦ (π₯ β dom π β¦ ((πβπ₯)(+gβ(πβπ₯))(πβπ₯))))β©, β¨(.rβndx),
(π β π£, π β π£ β¦ (π₯ β dom π β¦ ((πβπ₯)(.rβ(πβπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
π β©, β¨(
Β·π βndx), (π β (Baseβπ ), π β π£ β¦ (π₯ β dom π β¦ (π( Β·π
β(πβπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β π£, π β π£ β¦ (π Ξ£g (π₯ β dom π β¦ ((πβπ₯)(Β·πβ(πβπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(βtβ(TopOpen β π))β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π£ β§ βπ₯ β dom π(πβπ₯)(leβ(πβπ₯))(πβπ₯))}β©, β¨(distβndx), (π β π£, π β π£ β¦ sup((ran (π₯ β dom π β¦ ((πβπ₯)(distβ(πβπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), ββ©, β¨(compβndx), (π β (π£ Γ π£), π β π£ β¦ (π β (πβ(2nd βπ)), π β (ββπ) β¦ (π₯ β dom π β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(πβπ₯))(πβπ₯))(πβπ₯)))))β©}))) |
df-pws 12718 | β’ βs = (π β V, π β V β¦ ((Scalarβπ)Xs(π Γ {π}))) |
cimas 12719 | class
βs |
cqus 12720 | class
/s |
cxps 12721 | class
Γs |
df-iimas 12722 | β’ βs = (π β V, π β V β¦
β¦(Baseβπ) / π£β¦{β¨(Baseβndx), ran
πβ©,
β¨(+gβndx), βͺ π β π£ βͺ π β π£ {β¨β¨(πβπ), (πβπ)β©, (πβ(π(+gβπ)π))β©}β©,
β¨(.rβndx), βͺ π β π£ βͺ π β π£ {β¨β¨(πβπ), (πβπ)β©, (πβ(π(.rβπ)π))β©}β©}) |
df-qus 12723 | β’ /s = (π β V, π β V β¦ ((π₯ β (Baseβπ) β¦ [π₯]π) βs π)) |
df-xps 12724 | β’ Γs = (π β V, π β V β¦ (β‘(π₯ β (Baseβπ), π¦ β (Baseβπ ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs ((Scalarβπ)Xs{β¨β
, πβ©, β¨1o, π β©}))) |
cplusf 12771 | class
+π |
cmgm 12772 | class Mgm |
df-plusf 12773 | β’ +π = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(+gβπ)π¦))) |
df-mgm 12774 | β’ Mgm = {π β£ [(Baseβπ) / π][(+gβπ) / π]βπ₯ β π βπ¦ β π (π₯ππ¦) β π} |
csgrp 12806 | class Smgrp |
df-sgrp 12807 | β’ Smgrp = {π β Mgm β£ [(Baseβπ) / π][(+gβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π ((π₯ππ¦)ππ§) = (π₯π(π¦ππ§))} |
cmnd 12816 | class Mnd |
df-mnd 12817 | β’ Mnd = {π β Smgrp β£
[(Baseβπ) /
π][(+gβπ) / π]βπ β π βπ₯ β π ((πππ₯) = π₯ β§ (π₯ππ) = π₯)} |
cmhm 12848 | class MndHom |
csubmnd 12849 | class SubMnd |
df-mhm 12850 | β’ MndHom = (π β Mnd, π‘ β Mnd β¦ {π β ((Baseβπ‘) βπ
(Baseβπ )) β£
(βπ₯ β
(Baseβπ )βπ¦ β (Baseβπ )(πβ(π₯(+gβπ )π¦)) = ((πβπ₯)(+gβπ‘)(πβπ¦)) β§ (πβ(0gβπ )) = (0gβπ‘))}) |
df-submnd 12851 | β’ SubMnd = (π β Mnd β¦ {π‘ β π« (Baseβπ ) β£
((0gβπ )
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ )π¦) β π‘)}) |
cgrp 12876 | class Grp |
cminusg 12877 | class invg |
csg 12878 | class -g |
df-grp 12879 | β’ Grp = {π β Mnd β£ βπ β (Baseβπ)βπ β (Baseβπ)(π(+gβπ)π) = (0gβπ)} |
df-minusg 12880 | β’ invg = (π β V β¦ (π₯ β (Baseβπ) β¦ (β©π€ β (Baseβπ)(π€(+gβπ)π₯) = (0gβπ)))) |
df-sbg 12881 | β’ -g = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(+gβπ)((invgβπ)βπ¦)))) |
cmg 12982 | class .g |
df-mulg 12983 | β’ .g = (π β V β¦ (π β β€, π₯ β (Baseβπ) β¦ if(π = 0, (0gβπ),
β¦seq1((+gβπ), (β Γ {π₯})) / π β¦if(0 < π, (π βπ), ((invgβπ)β(π β-π)))))) |
csubg 13025 | class SubGrp |
cnsg 13026 | class NrmSGrp |
cqg 13027 | class
~QG |
df-subg 13028 | β’ SubGrp = (π€ β Grp β¦ {π β π« (Baseβπ€) β£ (π€ βΎs π ) β Grp}) |
df-nsg 13029 | β’ NrmSGrp = (π€ β Grp β¦ {π β (SubGrpβπ€) β£ [(Baseβπ€) / π][(+gβπ€) / π]βπ₯ β π βπ¦ β π ((π₯ππ¦) β π β (π¦ππ₯) β π )}) |
df-eqg 13030 | β’ ~QG = (π β V, π β V β¦ {β¨π₯, π¦β© β£ ({π₯, π¦} β (Baseβπ) β§ (((invgβπ)βπ₯)(+gβπ)π¦) β π)}) |
ccmn 13086 | class CMnd |
cabl 13087 | class Abel |
df-cmn 13088 | β’ CMnd = {π β Mnd β£ βπ β (Baseβπ)βπ β (Baseβπ)(π(+gβπ)π) = (π(+gβπ)π)} |
df-abl 13089 | β’ Abel = (Grp β© CMnd) |
cmgp 13128 | class mulGrp |
df-mgp 13129 | β’ mulGrp = (π€ β V β¦ (π€ sSet β¨(+gβndx),
(.rβπ€)β©)) |
cur 13140 | class 1r |
df-ur 13141 | β’ 1r = (0g
β mulGrp) |
csrg 13144 | class SRing |
df-srg 13145 | β’ SRing = {π β CMnd β£ ((mulGrpβπ) β Mnd β§
[(Baseβπ) /
π][(+gβπ) / π][(.rβπ) / π‘][(0gβπ) / π]βπ₯ β π (βπ¦ β π βπ§ β π ((π₯π‘(π¦ππ§)) = ((π₯π‘π¦)π(π₯π‘π§)) β§ ((π₯ππ¦)π‘π§) = ((π₯π‘π§)π(π¦π‘π§))) β§ ((ππ‘π₯) = π β§ (π₯π‘π) = π)))} |
crg 13177 | class Ring |
ccrg 13178 | class CRing |
df-ring 13179 | β’ Ring = {π β Grp β£ ((mulGrpβπ) β Mnd β§
[(Baseβπ) /
π][(+gβπ) / π][(.rβπ) / π‘]βπ₯ β π βπ¦ β π βπ§ β π ((π₯π‘(π¦ππ§)) = ((π₯π‘π¦)π(π₯π‘π§)) β§ ((π₯ππ¦)π‘π§) = ((π₯π‘π§)π(π¦π‘π§))))} |
df-cring 13180 | β’ CRing = {π β Ring β£ (mulGrpβπ) β CMnd} |
coppr 13237 | class
oppr |
df-oppr 13238 | β’ oppr = (π β V β¦ (π sSet β¨(.rβndx), tpos
(.rβπ)β©)) |
cdsr 13253 | class
β₯r |
cui 13254 | class Unit |
cir 13255 | class Irred |
df-dvdsr 13256 | β’ β₯r = (π€ β V β¦ {β¨π₯, π¦β© β£ (π₯ β (Baseβπ€) β§ βπ§ β (Baseβπ€)(π§(.rβπ€)π₯) = π¦)}) |
df-unit 13257 | β’ Unit = (π€ β V β¦ (β‘((β₯rβπ€) β©
(β₯rβ(opprβπ€))) β {(1rβπ€)})) |
df-irred 13258 | β’ Irred = (π€ β V β¦
β¦((Baseβπ€) β (Unitβπ€)) / πβ¦{π§ β π β£ βπ₯ β π βπ¦ β π (π₯(.rβπ€)π¦) β π§}) |
cinvr 13287 | class invr |
df-invr 13288 | β’ invr = (π β V β¦
(invgβ((mulGrpβπ) βΎs (Unitβπ)))) |
cdvr 13298 | class /r |
df-dvr 13299 | β’ /r = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Unitβπ) β¦ (π₯(.rβπ)((invrβπ)βπ¦)))) |
crh 13317 | class RingHom |
crs 13318 | class RingIso |
df-rnghom 13319 | β’ RingHom = (π β Ring, π β Ring β¦
β¦(Baseβπ) / π£β¦β¦(Baseβπ ) / π€β¦{π β (π€ βπ π£) β£ ((πβ(1rβπ)) = (1rβπ ) β§ βπ₯ β π£ βπ¦ β π£ ((πβ(π₯(+gβπ)π¦)) = ((πβπ₯)(+gβπ )(πβπ¦)) β§ (πβ(π₯(.rβπ)π¦)) = ((πβπ₯)(.rβπ )(πβπ¦))))}) |
df-rngiso 13320 | β’ RingIso = (π β V, π β V β¦ {π β (π RingHom π ) β£ β‘π β (π RingHom π)}) |
cnzr 13321 | class NzRing |
df-nzr 13322 | β’ NzRing = {π β Ring β£
(1rβπ)
β (0gβπ)} |
clring 13329 | class LRing |
df-lring 13330 | β’ LRing = {π β NzRing β£ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((π₯(+gβπ)π¦) = (1rβπ) β (π₯ β (Unitβπ) β¨ π¦ β (Unitβπ)))} |
csubrg 13336 | class SubRing |
crgspn 13337 | class RingSpan |
df-subrg 13338 | β’ SubRing = (π€ β Ring β¦ {π β π« (Baseβπ€) β£ ((π€ βΎs π ) β Ring β§
(1rβπ€)
β π )}) |
df-rgspn 13339 | β’ RingSpan = (π€ β V β¦ (π β π« (Baseβπ€) β¦ β© {π‘
β (SubRingβπ€)
β£ π β π‘})) |
capr 13368 | class #r |
df-apr 13369 | β’ #r = (π€ β V β¦ {β¨π₯, π¦β© β£ ((π₯ β (Baseβπ€) β§ π¦ β (Baseβπ€)) β§ (π₯(-gβπ€)π¦) β (Unitβπ€))}) |
cpsmet 13375 | class PsMet |
cxmet 13376 | class βMet |
cmet 13377 | class Met |
cbl 13378 | class ball |
cfbas 13379 | class fBas |
cfg 13380 | class filGen |
cmopn 13381 | class MetOpen |
cmetu 13382 | class metUnif |
df-psmet 13383 | β’ PsMet = (π₯ β V β¦ {π β (β*
βπ (π₯ Γ π₯)) β£ βπ¦ β π₯ ((π¦ππ¦) = 0 β§ βπ§ β π₯ βπ€ β π₯ (π¦ππ§) β€ ((π€ππ¦) +π (π€ππ§)))}) |
df-xmet 13384 | β’ βMet = (π₯ β V β¦ {π β (β*
βπ (π₯ Γ π₯)) β£ βπ¦ β π₯ βπ§ β π₯ (((π¦ππ§) = 0 β π¦ = π§) β§ βπ€ β π₯ (π¦ππ§) β€ ((π€ππ¦) +π (π€ππ§)))}) |
df-met 13385 | β’ Met = (π₯ β V β¦ {π β (β βπ
(π₯ Γ π₯)) β£ βπ¦ β π₯ βπ§ β π₯ (((π¦ππ§) = 0 β π¦ = π§) β§ βπ€ β π₯ (π¦ππ§) β€ ((π€ππ¦) + (π€ππ§)))}) |
df-bl 13386 | β’ ball = (π β V β¦ (π₯ β dom dom π, π§ β β* β¦ {π¦ β dom dom π β£ (π₯ππ¦) < π§})) |
df-mopn 13387 | β’ MetOpen = (π β βͺ ran
βMet β¦ (topGenβran (ballβπ))) |
df-fbas 13388 | β’ fBas = (π€ β V β¦ {π₯ β π« π« π€ β£ (π₯ β β
β§ β
β π₯ β§ βπ¦ β π₯ βπ§ β π₯ (π₯ β© π« (π¦ β© π§)) β β
)}) |
df-fg 13389 | β’ filGen = (π€ β V, π₯ β (fBasβπ€) β¦ {π¦ β π« π€ β£ (π₯ β© π« π¦) β β
}) |
df-metu 13390 | β’ metUnif = (π β βͺ ran
PsMet β¦ ((dom dom π
Γ dom dom π)filGenran
(π β
β+ β¦ (β‘π β (0[,)π))))) |
ccnfld 13391 | class
βfld |
df-icnfld 13392 | β’ βfld =
({β¨(Baseβndx), ββ©, β¨(+gβndx), +
β©, β¨(.rβndx), Β· β©} βͺ
{β¨(*πβndx), ββ©}) |
czring 13416 | class
β€ring |
df-zring 13417 | β’ β€ring =
(βfld βΎs β€) |
ctop 13433 | class Top |
df-top 13434 | β’ Top = {π₯ β£ (βπ¦ β π« π₯βͺ π¦ β π₯ β§ βπ¦ β π₯ βπ§ β π₯ (π¦ β© π§) β π₯)} |
ctopon 13446 | class TopOn |
df-topon 13447 | β’ TopOn = (π β V β¦ {π β Top β£ π = βͺ π}) |
ctps 13466 | class TopSp |
df-topsp 13467 | β’ TopSp = {π β£ (TopOpenβπ) β (TopOnβ(Baseβπ))} |
ctb 13478 | class TopBases |
df-bases 13479 | β’ TopBases = {π₯ β£ βπ¦ β π₯ βπ§ β π₯ (π¦ β© π§) β βͺ (π₯ β© π« (π¦ β© π§))} |
ccld 13528 | class Clsd |
cnt 13529 | class int |
ccl 13530 | class cls |
df-cld 13531 | β’ Clsd = (π β Top β¦ {π₯ β π« βͺ π
β£ (βͺ π β π₯) β π}) |
df-ntr 13532 | β’ int = (π β Top β¦ (π₯ β π« βͺ π
β¦ βͺ (π β© π« π₯))) |
df-cls 13533 | β’ cls = (π β Top β¦ (π₯ β π« βͺ π
β¦ β© {π¦ β (Clsdβπ) β£ π₯ β π¦})) |
cnei 13574 | class nei |
df-nei 13575 | β’ nei = (π β Top β¦ (π₯ β π« βͺ π
β¦ {π¦ β π«
βͺ π β£ βπ β π (π₯ β π β§ π β π¦)})) |
ccn 13621 | class Cn |
ccnp 13622 | class CnP |
clm 13623 | class
βπ‘ |
df-cn 13624 | β’ Cn = (π β Top, π β Top β¦ {π β (βͺ π βπ
βͺ π) β£ βπ¦ β π (β‘π β π¦) β π}) |
df-cnp 13625 | β’ CnP = (π β Top, π β Top β¦ (π₯ β βͺ π β¦ {π β (βͺ π βπ
βͺ π) β£ βπ¦ β π ((πβπ₯) β π¦ β βπ β π (π₯ β π β§ (π β π) β π¦))})) |
df-lm 13626 | β’ βπ‘ =
(π β Top β¦
{β¨π, π₯β© β£ (π β (βͺ π
βpm β) β§ π₯ β βͺ π β§ βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) |
ctx 13688 | class
Γt |
df-tx 13689 | β’ Γt = (π β V, π β V β¦ (topGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
chmeo 13736 | class Homeo |
df-hmeo 13737 | β’ Homeo = (π β Top, π β Top β¦ {π β (π Cn π) β£ β‘π β (π Cn π)}) |
cxms 13772 | class βMetSp |
cms 13773 | class MetSp |
ctms 13774 | class toMetSp |
df-xms 13775 | β’ βMetSp = {π β TopSp β£ (TopOpenβπ) =
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))} |
df-ms 13776 | β’ MetSp = {π β βMetSp β£
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) β
(Metβ(Baseβπ))} |
df-tms 13777 | β’ toMetSp = (π β βͺ ran
βMet β¦ ({β¨(Baseβndx), dom dom πβ©, β¨(distβndx), πβ©} sSet
β¨(TopSetβndx), (MetOpenβπ)β©)) |
ccncf 13993 | class βcnβ |
df-cncf 13994 | β’ βcnβ = (π β π« β, π β π« β β¦ {π β (π βπ π) β£ βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((absβ(π₯ β π¦)) < π β (absβ((πβπ₯) β (πβπ¦))) < π)}) |
climc 14059 | class
limβ |
cdv 14060 | class D |
df-limced 14061 | β’ limβ = (π β (β βpm
β), π₯ β β
β¦ {π¦ β β
β£ ((π:dom πβΆβ β§ dom π β β) β§ (π₯ β β β§
βπ β
β+ βπ β β+ βπ§ β dom π((π§ # π₯ β§ (absβ(π§ β π₯)) < π) β (absβ((πβπ§) β π¦)) < π)))}) |
df-dvap 14062 | β’ D = (π β π« β, π β (β βpm
π ) β¦ βͺ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π ))βdom π)({π₯} Γ ((π§ β {π€ β dom π β£ π€ # π₯} β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯))) |
clog 14213 | class log |
ccxp 14214 | class
βπ |
df-relog 14215 | β’ log = β‘(exp βΎ β) |
df-rpcxp 14216 | β’ βπ = (π₯ β β+,
π¦ β β β¦
(expβ(π¦ Β·
(logβπ₯)))) |
clogb 14297 | class
logb |
df-logb 14298 | β’ logb = (π₯ β (β β {0, 1}), π¦ β (β β {0})
β¦ ((logβπ¦) /
(logβπ₯))) |
clgs 14334 | class
/L |
df-lgs 14335 | β’ /L = (π β β€, π β β€ β¦ if(π = 0, if((πβ2) = 1, 1, 0), (if((π < 0 β§ π < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
(if(π = 2, if(2 β₯
π, 0, if((π mod 8) β {1, 7}, 1, -1)),
((((πβ((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)))β(absβπ))))) |
The
list of syntax, axioms (ax-) and definitions (df-) for the starts here |
wdcin 14481 | wff π΄ DECIDin
π΅ |
df-dcin 14482 | β’ (π΄ DECIDin
π΅ β βπ₯ β π΅ DECID π₯ β π΄) |
wbd 14500 | wff BOUNDED π |
ax-bd0 14501 | β’ (π β π) β β’ (BOUNDED π β BOUNDED
π) |
ax-bdim 14502 | β’ BOUNDED π
& β’ BOUNDED π β β’ BOUNDED (π β π) |
ax-bdan 14503 | β’ BOUNDED π
& β’ BOUNDED π β β’ BOUNDED (π β§ π) |
ax-bdor 14504 | β’ BOUNDED π
& β’ BOUNDED π β β’ BOUNDED (π β¨ π) |
ax-bdn 14505 | β’ BOUNDED π β β’ BOUNDED Β¬
π |
ax-bdal 14506 | β’ BOUNDED π β β’ BOUNDED
βπ₯ β π¦ π |
ax-bdex 14507 | β’ BOUNDED π β β’ BOUNDED
βπ₯ β π¦ π |
ax-bdeq 14508 | β’ BOUNDED π₯ = π¦ |
ax-bdel 14509 | β’ BOUNDED π₯ β π¦ |
ax-bdsb 14510 | β’ BOUNDED π β β’ BOUNDED [π¦ / π₯]π |
wbdc 14528 | wff BOUNDED
π΄ |
df-bdc 14529 | β’ (BOUNDED π΄ β βπ₯BOUNDED π₯ β π΄) |
ax-bdsep 14572 | β’ BOUNDED π β β’ βπβπβπ₯(π₯ β π β (π₯ β π β§ π)) |
ax-bj-d0cl 14612 | β’ BOUNDED π β β’ DECID π |
wind 14614 | wff Ind π΄ |
df-bj-ind 14615 | β’ (Ind π΄ β (β
β π΄ β§ βπ₯ β π΄ suc π₯ β π΄)) |
ax-infvn 14629 | β’ βπ₯(Ind π₯ β§ βπ¦(Ind π¦ β π₯ β π¦)) |
ax-bdsetind 14656 | β’ BOUNDED π β β’ (βπ(βπ¦ β π [π¦ / π]π β π) β βππ) |
ax-inf2 14664 | β’ βπβπ₯(π₯ β π β (π₯ = β
β¨ βπ¦ β π π₯ = suc π¦)) |
ax-strcoll 14670 | β’ βπ(βπ₯ β π βπ¦π β βπ(βπ₯ β π βπ¦ β π π β§ βπ¦ β π βπ₯ β π π)) |
ax-sscoll 14675 | β’ βπβπβπβπ§(βπ₯ β π βπ¦ β π π β βπ β π (βπ₯ β π βπ¦ β π π β§ βπ¦ β π βπ₯ β π π)) |
ax-ddkcomp 14677 | β’ (((π΄ β β β§ βπ₯ π₯ β π΄) β§ βπ₯ β β βπ¦ β π΄ π¦ < π₯ β§ βπ₯ β β βπ¦ β β (π₯ < π¦ β (βπ§ β π΄ π₯ < π§ β¨ βπ§ β π΄ π§ < π¦))) β βπ₯ β β (βπ¦ β π΄ π¦ β€ π₯ β§ ((π΅ β π
β§ βπ¦ β π΄ π¦ β€ π΅) β π₯ β€ π΅))) |
walsi 14759 | wff β!π₯(π β π) |
walsc 14760 | wff β!π₯ β π΄π |
df-alsi 14761 | β’ (β!π₯(π β π) β (βπ₯(π β π) β§ βπ₯π)) |
df-alsc 14762 | β’ (β!π₯ β π΄π β (βπ₯ β π΄ π β§ βπ₯ π₯ β π΄)) |