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