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 104wff (𝜑𝜓)
wb 105wff (𝜑𝜓)
ax-ia1 106((𝜑𝜓) → 𝜑)
ax-ia2 107((𝜑𝜓) → 𝜓)
ax-ia3 108(𝜑 → (𝜓 → (𝜑𝜓)))
df-bi 117(((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
ax-in1 614((𝜑 → ¬ 𝜑) → ¬ 𝜑)
ax-in2 615𝜑 → (𝜑𝜓))
wo 708wff (𝜑𝜓)
ax-io 709(((𝜑𝜒) → 𝜓) ↔ ((𝜑𝜓) ∧ (𝜒𝜓)))
wstab 830wff STAB 𝜑
df-stab 831(STAB 𝜑 ↔ (¬ ¬ 𝜑𝜑))
wdc 834wff DECID 𝜑
df-dc 835(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
w3o 977wff (𝜑𝜓𝜒)
w3a 978wff (𝜑𝜓𝜒)
df-3or 979((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
df-3an 980((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
wal 1351wff 𝑥𝜑
cv 1352class 𝑥
wceq 1353wff 𝐴 = 𝐵
wtru 1354wff
df-tru 1356(⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
wfal 1358wff
df-fal 1359(⊥ ↔ ¬ ⊤)
wxo 1375wff (𝜑𝜓)
df-xor 1376((𝜑𝜓) ↔ ((𝜑𝜓) ∧ ¬ (𝜑𝜓)))
ax-5 1447(∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
ax-7 1448(∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
ax-gen 1449𝜑       𝑥𝜑
wnf 1460wff 𝑥𝜑
df-nf 1461(Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
wex 1492wff 𝑥𝜑
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 1762wff [𝑦 / 𝑥]𝜑
df-sb 1763([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦𝜑) ∧ ∃𝑥(𝑥 = 𝑦𝜑)))
ax-16 1814(∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
ax-11o 1823(¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
weu 2026wff ∃!𝑥𝜑
wmo 2027wff ∃*𝑥𝜑
df-eu 2029(∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
df-mo 2030(∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
wcel 2148wff 𝐴𝐵
ax-13 2150(𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
ax-14 2151(𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
ax-ext 2159(∀𝑧(𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
cab 2163class {𝑥𝜑}
df-clab 2164(𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
df-cleq 2170(∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)       (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
df-clel 2173(𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
wnfc 2306wff 𝑥𝐴
df-nfc 2308(𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
wne 2347wff 𝐴𝐵
df-ne 2348(𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
wnel 2442wff 𝐴𝐵
df-nel 2443(𝐴𝐵 ↔ ¬ 𝐴𝐵)
wral 2455wff 𝑥𝐴 𝜑
wrex 2456wff 𝑥𝐴 𝜑
wreu 2457wff ∃!𝑥𝐴 𝜑
wrmo 2458wff ∃*𝑥𝐴 𝜑
crab 2459class {𝑥𝐴𝜑}
df-ral 2460(∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
df-rex 2461(∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
df-reu 2462(∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
df-rmo 2463(∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
df-rab 2464{𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
cvv 2737class V
df-v 2739V = {𝑥𝑥 = 𝑥}
wcdeq 2945wff CondEq(𝑥 = 𝑦𝜑)
df-cdeq 2946(CondEq(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜑))
wsbc 2962wff [𝐴 / 𝑥]𝜑
df-sbc 2963([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
csb 3057class 𝐴 / 𝑥𝐵
df-csb 3058𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
cdif 3126class (𝐴𝐵)
cun 3127class (𝐴𝐵)
cin 3128class (𝐴𝐵)
wss 3129wff 𝐴𝐵
df-dif 3131(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴 ∧ ¬ 𝑥𝐵)}
df-un 3133(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
df-in 3135(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
df-ss 3142(𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
c0 3422class
df-nul 3423∅ = (V ∖ V)
cif 3534class if(𝜑, 𝐴, 𝐵)
df-if 3535if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
cpw 3574class 𝒫 𝐴
df-pw 3576𝒫 𝐴 = {𝑥𝑥𝐴}
csn 3591class {𝐴}
cpr 3592class {𝐴, 𝐵}
ctp 3593class {𝐴, 𝐵, 𝐶}
cop 3594class 𝐴, 𝐵
cotp 3595class 𝐴, 𝐵, 𝐶
df-sn 3597{𝐴} = {𝑥𝑥 = 𝐴}
df-pr 3598{𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
df-tp 3599{𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
df-op 3600𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
df-ot 3601𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
cuni 3807class 𝐴
df-uni 3808 𝐴 = {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦𝐴)}
cint 3842class 𝐴
df-int 3843 𝐴 = {𝑥 ∣ ∀𝑦(𝑦𝐴𝑥𝑦)}
ciun 3884class 𝑥𝐴 𝐵
ciin 3885class 𝑥𝐴 𝐵
df-iun 3886 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
df-iin 3887 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
wdisj 3977wff Disj 𝑥𝐴 𝐵
df-disj 3978(Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)
wbr 4000wff 𝐴𝑅𝐵
df-br 4001(𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
copab 4060class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
cmpt 4061class (𝑥𝐴𝐵)
df-opab 4062{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
df-mpt 4063(𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
wtr 4098wff Tr 𝐴
df-tr 4099(Tr 𝐴 𝐴𝐴)
ax-coll 4115𝑏𝜑       (∀𝑥𝑎𝑦𝜑 → ∃𝑏𝑥𝑎𝑦𝑏 𝜑)
ax-sep 4118𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))
ax-nul 4126𝑥𝑦 ¬ 𝑦𝑥
ax-pow 4171𝑦𝑧(∀𝑤(𝑤𝑧𝑤𝑥) → 𝑧𝑦)
wem 4191wff EXMID
df-exmid 4192(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥))
ax-pr 4206𝑧𝑤((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧)
cep 4284class E
cid 4285class I
df-eprel 4286 E = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}
df-id 4290 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
wpo 4291wff 𝑅 Po 𝐴
wor 4292wff 𝑅 Or 𝐴
df-po 4293(𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
df-iso 4294(𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))))
wfrfor 4324wff FrFor 𝑅𝐴𝑆
wfr 4325wff 𝑅 Fr 𝐴
wse 4326wff 𝑅 Se 𝐴
wwe 4327wff 𝑅 We 𝐴
df-frfor 4328( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆))
df-frind 4329(𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)
df-se 4330(𝑅 Se 𝐴 ↔ ∀𝑥𝐴 {𝑦𝐴𝑦𝑅𝑥} ∈ V)
df-wetr 4331(𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
word 4359wff Ord 𝐴
con0 4360class On
wlim 4361wff Lim 𝐴
csuc 4362class suc 𝐴
df-iord 4363(Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 Tr 𝑥))
df-on 4365On = {𝑥 ∣ Ord 𝑥}
df-ilim 4366(Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴))
df-suc 4368suc 𝐴 = (𝐴 ∪ {𝐴})
ax-un 4430𝑦𝑧(∃𝑤(𝑧𝑤𝑤𝑥) → 𝑧𝑦)
ax-setind 4533(∀𝑎(∀𝑦𝑎 [𝑦 / 𝑎]𝜑𝜑) → ∀𝑎𝜑)
ax-iinf 4584𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦𝑥 → suc 𝑦𝑥))
com 4586class ω
df-iom 4587ω = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
cxp 4621class (𝐴 × 𝐵)
ccnv 4622class 𝐴
cdm 4623class dom 𝐴
crn 4624class ran 𝐴
cres 4625class (𝐴𝐵)
cima 4626class (𝐴𝐵)
ccom 4627class (𝐴𝐵)
wrel 4628wff Rel 𝐴
df-xp 4629(𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
df-rel 4630(Rel 𝐴𝐴 ⊆ (V × V))
df-cnv 4631𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
df-co 4632(𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
df-dm 4633dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
df-rn 4634ran 𝐴 = dom 𝐴
df-res 4635(𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
df-ima 4636(𝐴𝐵) = ran (𝐴𝐵)
cio 5172class (℩𝑥𝜑)
df-iota 5174(℩𝑥𝜑) = {𝑦 ∣ {𝑥𝜑} = {𝑦}}
wfun 5206wff Fun 𝐴
wfn 5207wff 𝐴 Fn 𝐵
wf 5208wff 𝐹:𝐴𝐵
wf1 5209wff 𝐹:𝐴1-1𝐵
wfo 5210wff 𝐹:𝐴onto𝐵
wf1o 5211wff 𝐹:𝐴1-1-onto𝐵
cfv 5212class (𝐹𝐴)
wiso 5213wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
df-fun 5214(Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
df-fn 5215(𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
df-f 5216(𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
df-f1 5217(𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
df-fo 5218(𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
df-f1o 5219(𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
df-fv 5220(𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
df-isom 5221(𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
crio 5824class (𝑥𝐴 𝜑)
df-riota 5825(𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
co 5869class (𝐴𝐹𝐵)
coprab 5870class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
cmpo 5871class (𝑥𝐴, 𝑦𝐵𝐶)
df-ov 5872(𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
df-oprab 5873{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
df-mpo 5874(𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
cof 6075class 𝑓 𝑅
cofr 6076class 𝑟 𝑅
df-of 6077𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓𝑥)𝑅(𝑔𝑥))))
df-ofr 6078𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
c1st 6133class 1st
c2nd 6134class 2nd
df-1st 61351st = (𝑥 ∈ V ↦ dom {𝑥})
df-2nd 61362nd = (𝑥 ∈ V ↦ ran {𝑥})
ctpos 6239class tpos 𝐹
df-tpos 6240tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (dom 𝐹 ∪ {∅}) ↦ {𝑥}))
wsmo 6280wff Smo 𝐴
df-smo 6281(Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴𝑦 ∈ dom 𝐴(𝑥𝑦 → (𝐴𝑥) ∈ (𝐴𝑦))))
crecs 6299class recs(𝐹)
df-recs 6300recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
crdg 6364class rec(𝐹, 𝐼)
df-irdg 6365rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))))
cfrec 6385class frec(𝐹, 𝐼)
df-frec 6386frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐼))})) ↾ ω)
c1o 6404class 1o
c2o 6405class 2o
c3o 6406class 3o
c4o 6407class 4o
coa 6408class +o
comu 6409class ·o
coei 6410class o
df-1o 64111o = suc ∅
df-2o 64122o = suc 1o
df-3o 64133o = suc 2o
df-4o 64144o = suc 3o
df-oadd 6415 +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦))
df-omul 6416 ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦))
df-oexpi 6417o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦))
wer 6526wff 𝑅 Er 𝐴
cec 6527class [𝐴]𝑅
cqs 6528class (𝐴 / 𝑅)
df-er 6529(𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
df-ec 6531[𝐴]𝑅 = (𝑅 “ {𝐴})
df-qs 6535(𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
cmap 6642class 𝑚
cpm 6643class pm
df-map 6644𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓𝑓:𝑦𝑥})
df-pm 6645pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓})
cixp 6692class X𝑥𝐴 𝐵
df-ixp 6693X𝑥𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)}
cen 6732class
cdom 6733class
cfn 6734class Fin
df-en 6735 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
df-dom 6736 ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1𝑦}
df-fin 6737Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥𝑦}
cfi 6961class fi
df-fi 6962fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = 𝑦})
csup 6975class sup(𝐴, 𝐵, 𝑅)
cinf 6976class inf(𝐴, 𝐵, 𝑅)
df-sup 6977sup(𝐴, 𝐵, 𝑅) = {𝑥𝐵 ∣ (∀𝑦𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐴 𝑦𝑅𝑧))}
df-inf 6978inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑅)
cdju 7030class (𝐴𝐵)
df-dju 7031(𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
cinl 7038class inl
cinr 7039class inr
df-inl 7040inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩)
df-inr 7041inr = (𝑥 ∈ V ↦ ⟨1o, 𝑥⟩)
cdjucase 7076class case(𝑅, 𝑆)
df-case 7077case(𝑅, 𝑆) = ((𝑅inl) ∪ (𝑆inr))
cdjud 7095class (𝑅d 𝑆)
df-djud 7096(𝑅d 𝑆) = ((𝑅(inl ↾ dom 𝑅)) ∪ (𝑆(inr ↾ dom 𝑆)))
xnninf 7112class
df-nninf 7113 = {𝑓 ∈ (2o𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓𝑖)}
comni 7126class Omni
df-omni 7127Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥𝑦 (𝑓𝑥) = ∅ ∨ ∀𝑥𝑦 (𝑓𝑥) = 1o))}
cmarkov 7143class Markov
df-markov 7144Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))}
cwomni 7155class WOmni
df-womni 7156WOmni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2oDECID𝑥𝑦 (𝑓𝑥) = 1o)}
ccrd 7172class card
df-card 7173card = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
wac 7198wff CHOICE
df-ac 7199(CHOICE ↔ ∀𝑥𝑓(𝑓𝑥𝑓 Fn dom 𝑥))
wtap 7240wff 𝑅 TAp 𝐴
df-tap 7241(𝑅 TAp 𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦))))
wacc 7252wff CCHOICE
df-cc 7253(CCHOICE ↔ ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓𝑥𝑓 Fn dom 𝑥)))
cnpi 7262class N
cpli 7263class +N
cmi 7264class ·N
clti 7265class <N
cplpq 7266class +pQ
cmpq 7267class ·pQ
cltpq 7268class <pQ
ceq 7269class ~Q
cnq 7270class Q
c1q 7271class 1Q
cplq 7272class +Q
cmq 7273class ·Q
crq 7274class *Q
cltq 7275class <Q
ceq0 7276class ~Q0
cnq0 7277class Q0
c0q0 7278class 0Q0
cplq0 7279class +Q0
cmq0 7280class ·Q0
cnp 7281class P
c1p 7282class 1P
cpp 7283class +P
cmp 7284class ·P
cltp 7285class <P
cer 7286class ~R
cnr 7287class R
c0r 7288class 0R
c1r 7289class 1R
cm1r 7290class -1R
cplr 7291class +R
cmr 7292class ·R
cltr 7293class <R
df-ni 7294N = (ω ∖ {∅})
df-pli 7295 +N = ( +o ↾ (N × N))
df-mi 7296 ·N = ( ·o ↾ (N × N))
df-lti 7297 <N = ( E ∩ (N × N))
df-plpq 7334 +pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨(((1st𝑥) ·N (2nd𝑦)) +N ((1st𝑦) ·N (2nd𝑥))), ((2nd𝑥) ·N (2nd𝑦))⟩)
df-mpq 7335 ·pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨((1st𝑥) ·N (1st𝑦)), ((2nd𝑥) ·N (2nd𝑦))⟩)
df-ltpq 7336 <pQ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ((1st𝑥) ·N (2nd𝑦)) <N ((1st𝑦) ·N (2nd𝑥)))}
df-enq 7337 ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}
df-nqqs 7338Q = ((N × N) / ~Q )
df-plqqs 7339 +Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ +pQ𝑢, 𝑓⟩)] ~Q ))}
df-mqqs 7340 ·Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ𝑢, 𝑓⟩)] ~Q ))}
df-1nqqs 73411Q = [⟨1o, 1o⟩] ~Q
df-rq 7342*Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥Q𝑦Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
df-ltnqqs 7343 <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
df-enq0 7414 ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))}
df-nq0 7415Q0 = ((ω × N) / ~Q0 )
df-0nq0 74160Q0 = [⟨∅, 1o⟩] ~Q0
df-plq0 7417 +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q0𝑦Q0) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
df-mq0 7418 ·Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q0𝑦Q0) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨(𝑤 ·o 𝑢), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
df-inp 7456P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)) ∧ ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))))}
df-i1p 74571P = ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
df-iplp 7458 +P = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
df-imp 7459 ·P = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
df-iltp 7460<P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
df-enr 7716 ~R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (P × P) ∧ 𝑦 ∈ (P × P)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 +P 𝑢) = (𝑤 +P 𝑣)))}
df-nr 7717R = ((P × P) / ~R )
df-plr 7718 +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}
df-mr 7719 ·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑓)), ((𝑤 ·P 𝑓) +P (𝑣 ·P 𝑢))⟩] ~R ))}
df-ltr 7720 <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
df-0r 77210R = [⟨1P, 1P⟩] ~R
df-1r 77221R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 7723-1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 7800class
cr 7801class
cc0 7802class 0
c1 7803class 1
ci 7804class i
caddc 7805class +
cltrr 7806class <
cmul 7807class ·
df-c 7808ℂ = (R × R)
df-0 78090 = ⟨0R, 0R
df-1 78101 = ⟨1R, 0R
df-i 7811i = ⟨0R, 1R
df-r 7812ℝ = (R × {0R})
df-add 7813 + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
df-mul 7814 · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
df-lt 7815 < = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
ax-cnex 7893ℂ ∈ V
ax-resscn 7894ℝ ⊆ ℂ
ax-1cn 78951 ∈ ℂ
ax-1re 78961 ∈ ℝ
ax-icn 7897i ∈ ℂ
ax-addcl 7898((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
ax-addrcl 7899((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
ax-mulcl 7900((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
ax-mulrcl 7901((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
ax-addcom 7902((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
ax-mulcom 7903((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
ax-addass 7904((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
ax-mulass 7905((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
ax-distr 7906((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
ax-i2m1 7907((i · i) + 1) = 0
ax-0lt1 79080 < 1
ax-1rid 7909(𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
ax-0id 7910(𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
ax-rnegex 7911(𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
ax-precex 7912((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ (𝐴 · 𝑥) = 1))
ax-cnre 7913(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
ax-pre-ltirr 7914(𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
ax-pre-ltwlin 7915((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶𝐶 < 𝐵)))
ax-pre-lttrn 7916((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
ax-pre-apti 7917((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)
ax-pre-ltadd 7918((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
ax-pre-mulgt0 7919((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))
ax-pre-mulext 7920((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) < (𝐵 · 𝐶) → (𝐴 < 𝐵𝐵 < 𝐴)))
ax-arch 7921(𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
ax-caucvg 7922𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))
ax-pre-suploc 7923(((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
ax-addf 7924 + :(ℂ × ℂ)⟶ℂ
ax-mulf 7925 · :(ℂ × ℂ)⟶ℂ
cpnf 7979class +∞
cmnf 7980class -∞
cxr 7981class *
clt 7982class <
cle 7983class
df-pnf 7984+∞ = 𝒫
df-mnf 7985-∞ = 𝒫 +∞
df-xr 7986* = (ℝ ∪ {+∞, -∞})
df-ltxr 7987 < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
df-le 7988 ≤ = ((ℝ* × ℝ*) ∖ < )
cmin 8118class
cneg 8119class -𝐴
df-sub 8120 − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
df-neg 8121-𝐴 = (0 − 𝐴)
creap 8521class #
df-reap 8522 # = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
cap 8528class #
df-ap 8529 # = {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))}
cdiv 8618class /
df-div 8619 / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
cn 8908class
df-inn 8909ℕ = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
c2 8959class 2
c3 8960class 3
c4 8961class 4
c5 8962class 5
c6 8963class 6
c7 8964class 7
c8 8965class 8
c9 8966class 9
df-2 89672 = (1 + 1)
df-3 89683 = (2 + 1)
df-4 89694 = (3 + 1)
df-5 89705 = (4 + 1)
df-6 89716 = (5 + 1)
df-7 89727 = (6 + 1)
df-8 89738 = (7 + 1)
df-9 89749 = (8 + 1)
cn0 9165class 0
df-n0 91660 = (ℕ ∪ {0})
cxnn0 9228class 0*
df-xnn0 92290* = (ℕ0 ∪ {+∞})
cz 9242class
df-z 9243ℤ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ -𝑛 ∈ ℕ)}
cdc 9373class 𝐴𝐵
df-dec 9374𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
cuz 9517class
df-uz 9518 = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗𝑘})
cq 9608class
df-q 9609ℚ = ( / “ (ℤ × ℕ))
crp 9640class +
df-rp 9641+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
cxne 9756class -𝑒𝐴
cxad 9757class +𝑒
cxmu 9758class ·e
df-xneg 9759-𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
df-xadd 9760 +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
df-xmul 9761 ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
cioo 9875class (,)
cioc 9876class (,]
cico 9877class [,)
cicc 9878class [,]
df-ioo 9879(,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
df-ioc 9880(,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
df-ico 9881[,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
df-icc 9882[,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
cfz 9995class ...
df-fz 9996... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚𝑘𝑘𝑛)})
cfzo 10128class ..^
df-fzo 10129..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
cfl 10254class
cceil 10255class
df-fl 10256⌊ = (𝑥 ∈ ℝ ↦ (𝑦 ∈ ℤ (𝑦𝑥𝑥 < (𝑦 + 1))))
df-ceil 10257⌈ = (𝑥 ∈ ℝ ↦ -(⌊‘-𝑥))
cmo 10308class mod
df-mod 10309 mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
cseq 10431class seq𝑀( + , 𝐹)
df-seqfrec 10432seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹𝑀)⟩)
cexp 10505class
df-exp 10506↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}))‘-𝑦)))))
cfa 10689class !
df-fac 10690! = ({⟨0, 1⟩} ∪ seq1( · , I ))
cbc 10711class C
df-bc 10712C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
chash 10739class
df-ihash 10740♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))
cshi 10807class shift
df-shft 10808 shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦𝑥)𝑓𝑧)})
ccj 10832class
cre 10833class
cim 10834class
df-cj 10835∗ = (𝑥 ∈ ℂ ↦ (𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥𝑦)) ∈ ℝ)))
df-re 10836ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2))
df-im 10837ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i)))
csqrt 10989class
cabs 10990class abs
df-rsqrt 10991√ = (𝑥 ∈ ℝ ↦ (𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
df-abs 10992abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
cli 11270class
df-clim 11271 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
csu 11345class Σ𝑘𝐴 𝐵
df-sumdc 11346Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚))))
cprod 11542class 𝑘𝐴 𝐵
df-proddc 11543𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))))
ce 11634class exp
ceu 11635class e
csin 11636class sin
ccos 11637class cos
ctan 11638class tan
cpi 11639class π
df-ef 11640exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥𝑘) / (!‘𝑘)))
df-e 11641e = (exp‘1)
df-sin 11642sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
df-cos 11643cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2))
df-tan 11644tan = (𝑥 ∈ (cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥)))
df-pi 11645π = inf((ℝ+ ∩ (sin “ {0})), ℝ, < )
ctau 11766class τ
df-tau 11767τ = inf((ℝ+ ∩ (cos “ {1})), ℝ, < )
cdvds 11778class
df-dvds 11779 ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
cgcd 11926class gcd
df-gcd 11927 gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑥𝑛𝑦)}, ℝ, < )))
clcm 12043class lcm
df-lcm 12044 lcm = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥𝑛𝑦𝑛)}, ℝ, < )))
cprime 12090class
df-prm 12091ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2o}
cnumer 12164class numer
cdenom 12165class denom
df-numer 12166numer = (𝑦 ∈ ℚ ↦ (1st ‘(𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥))))))
df-denom 12167denom = (𝑦 ∈ ℚ ↦ (2nd ‘(𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥))))))
codz 12191class od
cphi 12192class ϕ
df-odz 12193od = (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥𝑚) − 1)}, ℝ, < )))
df-phi 12194ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
cpc 12267class pCnt
df-pc 12268 pCnt = (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))))
cgz 12350class ℤ[i]
df-gz 12351ℤ[i] = {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)}
cstr 12441class Struct
cnx 12442class ndx
csts 12443class sSet
cslot 12444class Slot 𝐴
cbs 12445class Base
cress 12446class s
df-struct 12447 Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
df-ndx 12448ndx = ( I ↾ ℕ)
df-slot 12449Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥𝐴))
df-base 12451Base = Slot 1
df-sets 12452 sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))
df-iress 12453s = (𝑤 ∈ V, 𝑥 ∈ V ↦ (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
cplusg 12518class +g
cmulr 12519class .r
cstv 12520class *𝑟
csca 12521class Scalar
cvsca 12522class ·𝑠
cip 12523class ·𝑖
cts 12524class TopSet
cple 12525class le
coc 12526class oc
cds 12527class dist
cunif 12528class UnifSet
chom 12529class Hom
cco 12530class comp
df-plusg 12531+g = Slot 2
df-mulr 12532.r = Slot 3
df-starv 12533*𝑟 = Slot 4
df-sca 12534Scalar = Slot 5
df-vsca 12535 ·𝑠 = Slot 6
df-ip 12536·𝑖 = Slot 8
df-tset 12537TopSet = Slot 9
df-ple 12538le = Slot 10
df-ocomp 12539oc = Slot 11
df-ds 12540dist = Slot 12
df-unif 12541UnifSet = Slot 13
df-hom 12542Hom = Slot 14
df-cco 12543comp = Slot 15
crest 12636class t
ctopn 12637class TopOpen
df-rest 12638t = (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦𝑗 ↦ (𝑦𝑥)))
df-topn 12639TopOpen = (𝑤 ∈ V ↦ ((TopSet‘𝑤) ↾t (Base‘𝑤)))
ctg 12651class topGen
cpt 12652class t
c0g 12653class 0g
cgsu 12654class Σg
df-0g 126550g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g𝑔)𝑥) = 𝑥 ∧ (𝑥(+g𝑔)𝑒) = 𝑥))))
df-gsum 12656 Σ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 12657topGen = (𝑥 ∈ V ↦ {𝑦𝑦 (𝑥 ∩ 𝒫 𝑦)})
df-pt 12658t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}))
cprds 12659class Xs
cpws 12660class s
df-prds 12661Xs = (𝑠 ∈ 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 12663s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
cplusf 12664class +𝑓
cmgm 12665class Mgm
df-plusf 12666+𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)𝑦)))
df-mgm 12667Mgm = {𝑔[(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏 (𝑥𝑜𝑦) ∈ 𝑏}
csgrp 12699class Smgrp
df-sgrp 12700Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
cmnd 12709class Mnd
df-mnd 12710Mnd = {𝑔 ∈ Smgrp ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑝]𝑒𝑏𝑥𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}
cmhm 12739class MndHom
csubmnd 12740class SubMnd
df-mhm 12741 MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))})
df-submnd 12742SubMnd = (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g𝑠) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑠)𝑦) ∈ 𝑡)})
cgrp 12767class Grp
cminusg 12768class invg
csg 12769class -g
df-grp 12770Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g𝑔)𝑎) = (0g𝑔)}
df-minusg 12771invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))))
df-sbg 12772-g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g𝑔)((invg𝑔)‘𝑦))))
cmg 12872class .g
df-mulg 12873.g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g𝑔), seq1((+g𝑔), (ℕ × {𝑥})) / 𝑠if(0 < 𝑛, (𝑠𝑛), ((invg𝑔)‘(𝑠‘-𝑛))))))
ccmn 12915class CMnd
cabl 12916class Abel
df-cmn 12917CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g𝑔)𝑏) = (𝑏(+g𝑔)𝑎)}
df-abl 12918Abel = (Grp ∩ CMnd)
cmgp 12957class mulGrp
df-mgp 12958mulGrp = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(+g‘ndx), (.r𝑤)⟩))
cur 12968class 1r
df-ur 129691r = (0g ∘ mulGrp)
csrg 12972class SRing
df-srg 12973SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
crg 13005class Ring
ccrg 13006class CRing
df-ring 13007Ring = {𝑓 ∈ Grp ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑟𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
df-cring 13008CRing = {𝑓 ∈ Ring ∣ (mulGrp‘𝑓) ∈ CMnd}
coppr 13064class oppr
df-oppr 13065oppr = (𝑓 ∈ V ↦ (𝑓 sSet ⟨(.r‘ndx), tpos (.r𝑓)⟩))
cdsr 13080class r
cui 13081class Unit
cir 13082class Irred
df-dvdsr 13083r = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑤) ∧ ∃𝑧 ∈ (Base‘𝑤)(𝑧(.r𝑤)𝑥) = 𝑦)})
df-unit 13084Unit = (𝑤 ∈ V ↦ (((∥r𝑤) ∩ (∥r‘(oppr𝑤))) “ {(1r𝑤)}))
df-irred 13085Irred = (𝑤 ∈ V ↦ ((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏{𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑤)𝑦) ≠ 𝑧})
cinvr 13114class invr
df-invr 13115invr = (𝑟 ∈ V ↦ (invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟))))
cdvr 13125class /r
df-dvr 13126/r = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r𝑟)((invr𝑟)‘𝑦))))
crh 13142class RingHom
crs 13143class RingIso
df-rnghom 13144 RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ((𝑓‘(1r𝑟)) = (1r𝑠) ∧ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))))})
df-rngiso 13145 RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ 𝑓 ∈ (𝑠 RingHom 𝑟)})
cpsmet 13146class PsMet
cxmet 13147class ∞Met
cmet 13148class Met
cbl 13149class ball
cfbas 13150class fBas
cfg 13151class filGen
cmopn 13152class MetOpen
cmetu 13153class metUnif
df-psmet 13154PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧𝑥𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
df-xmet 13155∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥𝑧𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
df-met 13156Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥𝑧𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})
df-bl 13157ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))
df-mopn 13158MetOpen = (𝑑 ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))
df-fbas 13159fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑥 ∩ 𝒫 (𝑦𝑧)) ≠ ∅)})
df-fg 13160filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
df-metu 13161metUnif = (𝑑 ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (𝑑 “ (0[,)𝑎)))))
ctop 13162class Top
df-top 13163Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥 𝑦𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ∈ 𝑥)}
ctopon 13175class TopOn
df-topon 13176TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = 𝑗})
ctps 13195class TopSp
df-topsp 13196TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
ctb 13207class TopBases
df-bases 13208TopBases = {𝑥 ∣ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ⊆ (𝑥 ∩ 𝒫 (𝑦𝑧))}
ccld 13259class Clsd
cnt 13260class int
ccl 13261class cls
df-cld 13262Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗})
df-ntr 13263int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 (𝑗 ∩ 𝒫 𝑥)))
df-cls 13264cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥𝑦}))
cnei 13305class nei
df-nei 13306nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 ↦ {𝑦 ∈ 𝒫 𝑗 ∣ ∃𝑔𝑗 (𝑥𝑔𝑔𝑦)}))
ccn 13352class Cn
ccnp 13353class CnP
clm 13354class 𝑡
df-cn 13355 Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 (𝑓𝑦) ∈ 𝑗})
df-cnp 13356 CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
df-lm 13357𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
ctx 13419class ×t
df-tx 13420 ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))))
chmeo 13467class Homeo
df-hmeo 13468Homeo = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ 𝑓 ∈ (𝑘 Cn 𝑗)})
cxms 13503class ∞MetSp
cms 13504class MetSp
ctms 13505class toMetSp
df-xms 13506∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpen‘𝑓) = (MetOpen‘((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))))}
df-ms 13507MetSp = {𝑓 ∈ ∞MetSp ∣ ((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))) ∈ (Met‘(Base‘𝑓))}
df-tms 13508toMetSp = (𝑑 ran ∞Met ↦ ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩))
ccncf 13724class cn
df-cncf 13725cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
climc 13790class lim
cdv 13791class D
df-limced 13792 lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)))})
df-dvap 13793 D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ {𝑤 ∈ dom 𝑓𝑤 # 𝑥} ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)))
clog 13944class log
ccxp 13945class 𝑐
df-relog 13946log = (exp ↾ ℝ)
df-rpcxp 13947𝑐 = (𝑥 ∈ ℝ+, 𝑦 ∈ ℂ ↦ (exp‘(𝑦 · (log‘𝑥))))
clogb 14028class logb
df-logb 14029 logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥)))
clgs 14065class /L
df-lgs 14066 /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 14201wff 𝐴 DECIDin 𝐵
df-dcin 14202(𝐴 DECIDin 𝐵 ↔ ∀𝑥𝐵 DECID 𝑥𝐴)
wbd 14220wff BOUNDED 𝜑
ax-bd0 14221(𝜑𝜓)       (BOUNDED 𝜑BOUNDED 𝜓)
ax-bdim 14222BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdan 14223BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdor 14224BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdn 14225BOUNDED 𝜑       BOUNDED ¬ 𝜑
ax-bdal 14226BOUNDED 𝜑       BOUNDED𝑥𝑦 𝜑
ax-bdex 14227BOUNDED 𝜑       BOUNDED𝑥𝑦 𝜑
ax-bdeq 14228BOUNDED 𝑥 = 𝑦
ax-bdel 14229BOUNDED 𝑥𝑦
ax-bdsb 14230BOUNDED 𝜑       BOUNDED [𝑦 / 𝑥]𝜑
wbdc 14248wff BOUNDED 𝐴
df-bdc 14249(BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥𝐴)
ax-bdsep 14292BOUNDED 𝜑       𝑎𝑏𝑥(𝑥𝑏 ↔ (𝑥𝑎𝜑))
ax-bj-d0cl 14332BOUNDED 𝜑       DECID 𝜑
wind 14334wff Ind 𝐴
df-bj-ind 14335(Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴))
ax-infvn 14349𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦𝑥𝑦))
ax-bdsetind 14376BOUNDED 𝜑       (∀𝑎(∀𝑦𝑎 [𝑦 / 𝑎]𝜑𝜑) → ∀𝑎𝜑)
ax-inf2 14384𝑎𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
ax-strcoll 14390𝑎(∀𝑥𝑎𝑦𝜑 → ∃𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑))
ax-sscoll 14395𝑎𝑏𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐 (∀𝑥𝑎𝑦𝑑 𝜑 ∧ ∀𝑦𝑑𝑥𝑎 𝜑))
ax-ddkcomp 14397(((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 𝑦𝑥 ∧ ((𝐵𝑅 ∧ ∀𝑦𝐴 𝑦𝐵) → 𝑥𝐵)))
walsi 14477wff ∀!𝑥(𝜑𝜓)
walsc 14478wff ∀!𝑥𝐴𝜑
df-alsi 14479(∀!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃𝑥𝜑))
df-alsc 14480(∀!𝑥𝐴𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∃𝑥 𝑥𝐴))
  Copyright terms: Public domain W3C validator