ILE Home Intuitionistic Logic Explorer This is the Unicode version.
Change to GIF version

List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 3wff ¬ 𝜑
wi 4wff (𝜑𝜓)
ax-1 5(𝜑 → (𝜓𝜑))
ax-2 6((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
ax-mp 7𝜑    &   (𝜑𝜓)       𝜓
wa 97wff (𝜑𝜓)
wb 98wff (𝜑𝜓)
ax-ia1 99((𝜑𝜓) → 𝜑)
ax-ia2 100((𝜑𝜓) → 𝜓)
ax-ia3 101(𝜑 → (𝜓 → (𝜑𝜓)))
df-bi 110(((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
ax-in1 544((𝜑 → ¬ 𝜑) → ¬ 𝜑)
ax-in2 545𝜑 → (𝜑𝜓))
wo 629wff (𝜑𝜓)
ax-io 630(((𝜑𝜒) → 𝜓) ↔ ((𝜑𝜓) ∧ (𝜒𝜓)))
wstab 739wff STAB 𝜑
df-stab 740(STAB 𝜑 ↔ (¬ ¬ 𝜑𝜑))
wdc 742wff DECID 𝜑
df-dc 743(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
w3o 884wff (𝜑𝜓𝜒)
w3a 885wff (𝜑𝜓𝜒)
df-3or 886((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
df-3an 887((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
wal 1241wff 𝑥𝜑
cv 1242class 𝑥
wceq 1243wff 𝐴 = 𝐵
wtru 1244wff
df-tru 1246(⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
wfal 1248wff
df-fal 1249(⊥ ↔ ¬ ⊤)
wxo 1266wff (𝜑𝜓)
df-xor 1267((𝜑𝜓) ↔ ((𝜑𝜓) ∧ ¬ (𝜑𝜓)))
ax-5 1336(∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
ax-7 1337(∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
ax-gen 1338𝜑       𝑥𝜑
wnf 1349wff 𝑥𝜑
df-nf 1350(Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
wex 1381wff 𝑥𝜑
ax-ie1 1382(∃𝑥𝜑 → ∀𝑥𝑥𝜑)
ax-ie2 1383(∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓)))
wcel 1393wff 𝐴𝐵
ax-8 1395(𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
ax-10 1396(∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
ax-11 1397(𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
ax-i12 1398(∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
ax-bndl 1399(∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
ax-4 1400(∀𝑥𝜑𝜑)
ax-13 1404(𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
ax-14 1405(𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
ax-17 1419(𝜑 → ∀𝑥𝜑)
ax-i9 1423𝑥 𝑥 = 𝑦
ax-ial 1427(∀𝑥𝜑 → ∀𝑥𝑥𝜑)
ax-i5r 1428((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑𝜓))
ax-10o 1604(∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
wsb 1645wff [𝑦 / 𝑥]𝜑
df-sb 1646([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦𝜑) ∧ ∃𝑥(𝑥 = 𝑦𝜑)))
ax-16 1695(∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
ax-11o 1704(¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
weu 1900wff ∃!𝑥𝜑
wmo 1901wff ∃*𝑥𝜑
df-eu 1903(∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
df-mo 1904(∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
ax-ext 2022(∀𝑧(𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
cab 2026class {𝑥𝜑}
df-clab 2027(𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
df-cleq 2033(∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)       (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
df-clel 2036(𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
wnfc 2165wff 𝑥𝐴
df-nfc 2167(𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
wne 2204wff 𝐴𝐵
wnel 2205wff 𝐴𝐵
df-ne 2206(𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
df-nel 2207(𝐴𝐵 ↔ ¬ 𝐴𝐵)
wral 2303wff 𝑥𝐴 𝜑
wrex 2304wff 𝑥𝐴 𝜑
wreu 2305wff ∃!𝑥𝐴 𝜑
wrmo 2306wff ∃*𝑥𝐴 𝜑
crab 2307class {𝑥𝐴𝜑}
df-ral 2308(∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
df-rex 2309(∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
df-reu 2310(∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
df-rmo 2311(∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
df-rab 2312{𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
cvv 2554class V
df-v 2556V = {𝑥𝑥 = 𝑥}
wcdeq 2744wff CondEq(𝑥 = 𝑦𝜑)
df-cdeq 2745(CondEq(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜑))
wsbc 2761wff [𝐴 / 𝑥]𝜑
df-sbc 2762([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
csb 2849class 𝐴 / 𝑥𝐵
df-csb 2850𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
cdif 2911class (𝐴𝐵)
cun 2912class (𝐴𝐵)
cin 2913class (𝐴𝐵)
wss 2914wff 𝐴𝐵
wpss 2915wff 𝐴𝐵
df-dif 2917(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴 ∧ ¬ 𝑥𝐵)}
df-un 2919(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
df-in 2921(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
df-ss 2928(𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
df-pss 2930(𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
c0 3221class
df-nul 3222∅ = (V ∖ V)
cif 3328class if(𝜑, 𝐴, 𝐵)
df-if 3329if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
cpw 3356class 𝒫 𝐴
df-pw 3358𝒫 𝐴 = {𝑥𝑥𝐴}
csn 3372class {𝐴}
cpr 3373class {𝐴, 𝐵}
ctp 3374class {𝐴, 𝐵, 𝐶}
cop 3375class 𝐴, 𝐵
cotp 3376class 𝐴, 𝐵, 𝐶
df-sn 3378{𝐴} = {𝑥𝑥 = 𝐴}
df-pr 3379{𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
df-tp 3380{𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
df-op 3381𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
df-ot 3382𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
cuni 3577class 𝐴
df-uni 3578 𝐴 = {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦𝐴)}
cint 3612class 𝐴
df-int 3613 𝐴 = {𝑥 ∣ ∀𝑦(𝑦𝐴𝑥𝑦)}
ciun 3654class 𝑥𝐴 𝐵
ciin 3655class 𝑥𝐴 𝐵
df-iun 3656 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
df-iin 3657 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
wdisj 3742wff Disj 𝑥𝐴 𝐵
df-disj 3743(Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)
wbr 3761wff 𝐴𝑅𝐵
df-br 3762(𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
copab 3814class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
cmpt 3815class (𝑥𝐴𝐵)
df-opab 3816{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
df-mpt 3817(𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
wtr 3851wff Tr 𝐴
df-tr 3852(Tr 𝐴 𝐴𝐴)
ax-coll 3869𝑏𝜑       (∀𝑥𝑎𝑦𝜑 → ∃𝑏𝑥𝑎𝑦𝑏 𝜑)
ax-sep 3872𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))
ax-nul 3880𝑥𝑦 ¬ 𝑦𝑥
ax-pow 3924𝑦𝑧(∀𝑤(𝑤𝑧𝑤𝑥) → 𝑧𝑦)
ax-pr 3941𝑧𝑤((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧)
cep 4021class E
cid 4022class I
df-eprel 4023 E = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}
df-id 4027 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
wpo 4028wff 𝑅 Po 𝐴
wor 4029wff 𝑅 Or 𝐴
df-po 4030(𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
df-iso 4031(𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))))
wse 4061wff 𝑅 Se 𝐴
df-se 4062(𝑅 Se 𝐴 ↔ ∀𝑥𝐴 {𝑦𝐴𝑦𝑅𝑥} ∈ V)
word 4071wff Ord 𝐴
con0 4072class On
wlim 4073wff Lim 𝐴
csuc 4074class suc 𝐴
df-iord 4075(Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 Tr 𝑥))
df-on 4077On = {𝑥 ∣ Ord 𝑥}
df-ilim 4078(Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴))
df-suc 4080suc 𝐴 = (𝐴 ∪ {𝐴})
ax-un 4142𝑦𝑧(∃𝑤(𝑧𝑤𝑤𝑥) → 𝑧𝑦)
ax-setind 4232(∀𝑎(∀𝑦𝑎 [𝑦 / 𝑎]𝜑𝜑) → ∀𝑎𝜑)
ax-iinf 4274𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦𝑥 → suc 𝑦𝑥))
com 4276class ω
df-iom 4277ω = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
cxp 4306class (𝐴 × 𝐵)
ccnv 4307class 𝐴
cdm 4308class dom 𝐴
crn 4309class ran 𝐴
cres 4310class (𝐴𝐵)
cima 4311class (𝐴𝐵)
ccom 4312class (𝐴𝐵)
wrel 4313wff Rel 𝐴
df-xp 4314(𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
df-rel 4315(Rel 𝐴𝐴 ⊆ (V × V))
df-cnv 4316𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
df-co 4317(𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
df-dm 4318dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
df-rn 4319ran 𝐴 = dom 𝐴
df-res 4320(𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
df-ima 4321(𝐴𝐵) = ran (𝐴𝐵)
cio 4828class (℩𝑥𝜑)
df-iota 4830(℩𝑥𝜑) = {𝑦 ∣ {𝑥𝜑} = {𝑦}}
wfun 4859wff Fun 𝐴
wfn 4860wff 𝐴 Fn 𝐵
wf 4861wff 𝐹:𝐴𝐵
wf1 4862wff 𝐹:𝐴1-1𝐵
wfo 4863wff 𝐹:𝐴onto𝐵
wf1o 4864wff 𝐹:𝐴1-1-onto𝐵
cfv 4865class (𝐹𝐴)
wiso 4866wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
df-fun 4867(Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
df-fn 4868(𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
df-f 4869(𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
df-f1 4870(𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
df-fo 4871(𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
df-f1o 4872(𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
df-fv 4873(𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
df-isom 4874(𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
crio 5430class (𝑥𝐴 𝜑)
df-riota 5431(𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
co 5475class (𝐴𝐹𝐵)
coprab 5476class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
cmpt2 5477class (𝑥𝐴, 𝑦𝐵𝐶)
df-ov 5478(𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
df-oprab 5479{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
df-mpt2 5480(𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
cof 5673class 𝑓 𝑅
cofr 5674class 𝑟 𝑅
df-of 5675𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓𝑥)𝑅(𝑔𝑥))))
df-ofr 5676𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
c1st 5728class 1st
c2nd 5729class 2nd
df-1st 57301st = (𝑥 ∈ V ↦ dom {𝑥})
df-2nd 57312nd = (𝑥 ∈ V ↦ ran {𝑥})
ctpos 5822class tpos 𝐹
df-tpos 5823tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (dom 𝐹 ∪ {∅}) ↦ {𝑥}))
wsmo 5863wff Smo 𝐴
df-smo 5864(Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴𝑦 ∈ dom 𝐴(𝑥𝑦 → (𝐴𝑥) ∈ (𝐴𝑦))))
crecs 5882class recs(𝐹)
df-recs 5883recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
crdg 5919class rec(𝐹, 𝐼)
df-irdg 5920rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))))
cfrec 5940class frec(𝐹, 𝐼)
df-frec 5941frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐼))})) ↾ ω)
c1o 5957class 1𝑜
c2o 5958class 2𝑜
c3o 5959class 3𝑜
c4o 5960class 4𝑜
coa 5961class +𝑜
comu 5962class ·𝑜
coei 5963class 𝑜
df-1o 59641𝑜 = suc ∅
df-2o 59652𝑜 = suc 1𝑜
df-3o 59663𝑜 = suc 2𝑜
df-4o 59674𝑜 = suc 3𝑜
df-oadd 5968 +𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦))
df-omul 5969 ·𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +𝑜 𝑥)), ∅)‘𝑦))
df-oexpi 5970𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)‘𝑦))
wer 6066wff 𝑅 Er 𝐴
cec 6067class [𝐴]𝑅
cqs 6068class (𝐴 / 𝑅)
df-er 6069(𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
df-ec 6071[𝐴]𝑅 = (𝑅 “ {𝐴})
df-qs 6075(𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
cen 6182class
cdom 6183class
cfn 6184class Fin
df-en 6185 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
df-dom 6186 ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1𝑦}
df-fin 6187Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥𝑦}
ccrd 6316class card
df-card 6317card = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
cnpi 6327class N
cpli 6328class +N
cmi 6329class ·N
clti 6330class <N
cplpq 6331class +pQ
cmpq 6332class ·pQ
cltpq 6333class <pQ
ceq 6334class ~Q
cnq 6335class Q
c1q 6336class 1Q
cplq 6337class +Q
cmq 6338class ·Q
crq 6339class *Q
cltq 6340class <Q
ceq0 6341class ~Q0
cnq0 6342class Q0
c0q0 6343class 0Q0
cplq0 6344class +Q0
cmq0 6345class ·Q0
cnp 6346class P
c1p 6347class 1P
cpp 6348class +P
cmp 6349class ·P
cltp 6350class <P
cer 6351class ~R
cnr 6352class R
c0r 6353class 0R
c1r 6354class 1R
cm1r 6355class -1R
cplr 6356class +R
cmr 6357class ·R
cltr 6358class <R
df-ni 6359N = (ω ∖ {∅})
df-pli 6360 +N = ( +𝑜 ↾ (N × N))
df-mi 6361 ·N = ( ·𝑜 ↾ (N × N))
df-lti 6362 <N = ( E ∩ (N × N))
df-plpq 6399 +pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨(((1st𝑥) ·N (2nd𝑦)) +N ((1st𝑦) ·N (2nd𝑥))), ((2nd𝑥) ·N (2nd𝑦))⟩)
df-mpq 6400 ·pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨((1st𝑥) ·N (1st𝑦)), ((2nd𝑥) ·N (2nd𝑦))⟩)
df-ltpq 6401 <pQ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ((1st𝑥) ·N (2nd𝑦)) <N ((1st𝑦) ·N (2nd𝑥)))}
df-enq 6402 ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}
df-nqqs 6403Q = ((N × N) / ~Q )
df-plqqs 6404 +Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ +pQ𝑢, 𝑓⟩)] ~Q ))}
df-mqqs 6405 ·Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ𝑢, 𝑓⟩)] ~Q ))}
df-1nqqs 64061Q = [⟨1𝑜, 1𝑜⟩] ~Q
df-rq 6407*Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥Q𝑦Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
df-ltnqqs 6408 <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
df-enq0 6479 ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)))}
df-nq0 6480Q0 = ((ω × N) / ~Q0 )
df-0nq0 64810Q0 = [⟨∅, 1𝑜⟩] ~Q0
df-plq0 6482 +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q0𝑦Q0) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·𝑜 𝑓) +𝑜 (𝑣 ·𝑜 𝑢)), (𝑣 ·𝑜 𝑓)⟩] ~Q0 ))}
df-mq0 6483 ·Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q0𝑦Q0) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨(𝑤 ·𝑜 𝑢), (𝑣 ·𝑜 𝑓)⟩] ~Q0 ))}
df-inp 6521P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)) ∧ ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))))}
df-i1p 65221P = ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
df-iplp 6523 +P = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
df-imp 6524 ·P = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
df-iltp 6525<P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
df-enr 6768 ~R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (P × P) ∧ 𝑦 ∈ (P × P)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 +P 𝑢) = (𝑤 +P 𝑣)))}
df-nr 6769R = ((P × P) / ~R )
df-plr 6770 +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}
df-mr 6771 ·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑓)), ((𝑤 ·P 𝑓) +P (𝑣 ·P 𝑢))⟩] ~R ))}
df-ltr 6772 <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
df-0r 67730R = [⟨1P, 1P⟩] ~R
df-1r 67741R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 6775-1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 6844class
cr 6845class
cc0 6846class 0
c1 6847class 1
ci 6848class i
caddc 6849class +
cltrr 6850class <
cmul 6851class ·
df-c 6852ℂ = (R × R)
df-0 68530 = ⟨0R, 0R
df-1 68541 = ⟨1R, 0R
df-i 6855i = ⟨0R, 1R
df-r 6856ℝ = (R × {0R})
df-add 6857 + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
df-mul 6858 · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
df-lt 6859 < = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
ax-cnex 6932ℂ ∈ V
ax-resscn 6933ℝ ⊆ ℂ
ax-1cn 69341 ∈ ℂ
ax-1re 69351 ∈ ℝ
ax-icn 6936i ∈ ℂ
ax-addcl 6937((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
ax-addrcl 6938((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
ax-mulcl 6939((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
ax-mulrcl 6940((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
ax-addcom 6941((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
ax-mulcom 6942((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
ax-addass 6943((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
ax-mulass 6944((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
ax-distr 6945((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
ax-i2m1 6946((i · i) + 1) = 0
ax-1rid 6948(𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
ax-0id 6949(𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
ax-rnegex 6950(𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
ax-precex 6951((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ (𝐴 · 𝑥) = 1))
ax-cnre 6952(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
ax-pre-ltirr 6953(𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
ax-pre-ltwlin 6954((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶𝐶 < 𝐵)))
ax-pre-lttrn 6955((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
ax-pre-apti 6956((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)
ax-pre-ltadd 6957((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
ax-pre-mulgt0 6958((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))
ax-pre-mulext 6959((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) < (𝐵 · 𝐶) → (𝐴 < 𝐵𝐵 < 𝐴)))
ax-arch 6960(𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
ax-caucvg 6961𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))
cpnf 7013class +∞
cmnf 7014class -∞
cxr 7015class *
clt 7016class <
cle 7017class
df-pnf 7018+∞ = 𝒫
df-mnf 7019-∞ = 𝒫 +∞
df-xr 7020* = (ℝ ∪ {+∞, -∞})
df-ltxr 7021 < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
df-le 7022 ≤ = ((ℝ* × ℝ*) ∖ < )
cmin 7138class
cneg 7139class -𝐴
df-sub 7140 − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
df-neg 7141-𝐴 = (0 − 𝐴)
creap 7517class #
df-reap 7518 # = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
cap 7524class #
df-ap 7525 # = {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))}
cdiv 7603class /
df-div 7604 / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
cn 7866class
df-inn 7867ℕ = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
c2 7916class 2
c3 7917class 3
c4 7918class 4
c5 7919class 5
c6 7920class 6
c7 7921class 7
c8 7922class 8
c9 7923class 9
c10 7924class 10
df-2 79252 = (1 + 1)
df-3 79263 = (2 + 1)
df-4 79274 = (3 + 1)
df-5 79285 = (4 + 1)
df-6 79296 = (5 + 1)
df-7 79307 = (6 + 1)
df-8 79318 = (7 + 1)
df-9 79329 = (8 + 1)
df-10 793310 = (9 + 1)
cn0 8129class 0
df-n0 81300 = (ℕ ∪ {0})
cz 8193class
df-z 8194ℤ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ -𝑛 ∈ ℕ)}
cdc 8316class 𝐴𝐵
df-dec 8317𝐴𝐵 = ((10 · 𝐴) + 𝐵)
cuz 8421class
df-uz 8422 = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗𝑘})
cq 8502class
df-q 8503ℚ = ( / “ (ℤ × ℕ))
crp 8530class +
df-rp 8531+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
cxne 8629class -𝑒𝐴
cxad 8630class +𝑒
cxmu 8631class ·e
df-xneg 8632-𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
df-xadd 8633 +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
df-xmul 8634 ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
cioo 8700class (,)
cioc 8701class (,]
cico 8702class [,)
cicc 8703class [,]
df-ioo 8704(,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
df-ioc 8705(,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
df-ico 8706[,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
df-icc 8707[,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
cfz 8817class ...
df-fz 8818... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚𝑘𝑘𝑛)})
cfzo 8942class ..^
df-fzo 8943..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
cseq 9065class seq𝑀( + , 𝐹, 𝑆)
df-iseq 9066seq𝑀( + , 𝐹, 𝑆) = ran frec((𝑥 ∈ (ℤ𝑀), 𝑦𝑆 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹𝑀)⟩)
cexp 9108class
df-iexp 9109↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦)))))
cshi 9269class shift
df-shft 9270 shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦𝑥)𝑓𝑧)})
ccj 9293class
cre 9294class
cim 9295class
df-cj 9296∗ = (𝑥 ∈ ℂ ↦ (𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥𝑦)) ∈ ℝ)))
df-re 9297ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2))
df-im 9298ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i)))
csqrt 9448class
cabs 9449class abs
df-rsqrt 9450√ = (𝑥 ∈ ℝ ↦ (𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
df-abs 9451abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
cli 9652class
df-clim 9653 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
csu 9725class Σ𝑘𝐴 𝐵
df-sum 9726Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵), ℂ)‘𝑚))))
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wbd 9781wff BOUNDED 𝜑
ax-bd0 9782(𝜑𝜓)       (BOUNDED 𝜑BOUNDED 𝜓)
ax-bdim 9783BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdan 9784BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdor 9785BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdn 9786BOUNDED 𝜑       BOUNDED ¬ 𝜑
ax-bdal 9787BOUNDED 𝜑       BOUNDED𝑥𝑦 𝜑
ax-bdex 9788BOUNDED 𝜑       BOUNDED𝑥𝑦 𝜑
ax-bdeq 9789BOUNDED 𝑥 = 𝑦
ax-bdel 9790BOUNDED 𝑥𝑦
ax-bdsb 9791BOUNDED 𝜑       BOUNDED [𝑦 / 𝑥]𝜑
wbdc 9809wff BOUNDED 𝐴
df-bdc 9810(BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥𝐴)
ax-bdsep 9853BOUNDED 𝜑       𝑎𝑏𝑥(𝑥𝑏 ↔ (𝑥𝑎𝜑))
ax-bj-d0cl 9893BOUNDED 𝜑       DECID 𝜑
wind 9899wff Ind 𝐴
df-bj-ind 9900(Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴))
ax-infvn 9915𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦𝑥𝑦))
ax-bdsetind 9942BOUNDED 𝜑       (∀𝑎(∀𝑦𝑎 [𝑦 / 𝑎]𝜑𝜑) → ∀𝑎𝜑)
ax-inf2 9950𝑎𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
ax-strcoll 9956𝑎(∀𝑥𝑎𝑦𝜑 → ∃𝑏𝑦(𝑦𝑏 ↔ ∃𝑥𝑎 𝜑))
ax-sscoll 9961𝑎𝑏𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑))
walsi 9963wff ∀!𝑥(𝜑𝜓)
walsc 9964wff ∀!𝑥𝐴𝜑
df-alsi 9965(∀!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃𝑥𝜑))
df-alsc 9966(∀!𝑥𝐴𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∃𝑥 𝑥𝐴))
  Copyright terms: Public domain W3C validator