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 103wff (𝜑𝜓)
wb 104wff (𝜑𝜓)
ax-ia1 105((𝜑𝜓) → 𝜑)
ax-ia2 106((𝜑𝜓) → 𝜓)
ax-ia3 107(𝜑 → (𝜓 → (𝜑𝜓)))
df-bi 116(((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
ax-in1 582((𝜑 → ¬ 𝜑) → ¬ 𝜑)
ax-in2 583𝜑 → (𝜑𝜓))
wo 667wff (𝜑𝜓)
ax-io 668(((𝜑𝜒) → 𝜓) ↔ ((𝜑𝜓) ∧ (𝜒𝜓)))
wstab 778wff STAB 𝜑
df-stab 779(STAB 𝜑 ↔ (¬ ¬ 𝜑𝜑))
wdc 783wff DECID 𝜑
df-dc 784(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
w3o 926wff (𝜑𝜓𝜒)
w3a 927wff (𝜑𝜓𝜒)
df-3or 928((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
df-3an 929((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
wal 1294wff 𝑥𝜑
cv 1295class 𝑥
wceq 1296wff 𝐴 = 𝐵
wtru 1297wff
df-tru 1299(⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
wfal 1301wff
df-fal 1302(⊥ ↔ ¬ ⊤)
wxo 1318wff (𝜑𝜓)
df-xor 1319((𝜑𝜓) ↔ ((𝜑𝜓) ∧ ¬ (𝜑𝜓)))
ax-5 1388(∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
ax-7 1389(∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
ax-gen 1390𝜑       𝑥𝜑
wnf 1401wff 𝑥𝜑
df-nf 1402(Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
wex 1433wff 𝑥𝜑
ax-ie1 1434(∃𝑥𝜑 → ∀𝑥𝑥𝜑)
ax-ie2 1435(∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓)))
wcel 1445wff 𝐴𝐵
ax-8 1447(𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
ax-10 1448(∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
ax-11 1449(𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
ax-i12 1450(∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
ax-bndl 1451(∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
ax-4 1452(∀𝑥𝜑𝜑)
ax-13 1456(𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
ax-14 1457(𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
ax-17 1471(𝜑 → ∀𝑥𝜑)
ax-i9 1475𝑥 𝑥 = 𝑦
ax-ial 1479(∀𝑥𝜑 → ∀𝑥𝑥𝜑)
ax-i5r 1480((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑𝜓))
ax-10o 1658(∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
wsb 1699wff [𝑦 / 𝑥]𝜑
df-sb 1700([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦𝜑) ∧ ∃𝑥(𝑥 = 𝑦𝜑)))
ax-16 1749(∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
ax-11o 1758(¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
weu 1955wff ∃!𝑥𝜑
wmo 1956wff ∃*𝑥𝜑
df-eu 1958(∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
df-mo 1959(∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
ax-ext 2077(∀𝑧(𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
cab 2081class {𝑥𝜑}
df-clab 2082(𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
df-cleq 2088(∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)       (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
df-clel 2091(𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
wnfc 2222wff 𝑥𝐴
df-nfc 2224(𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
wne 2262wff 𝐴𝐵
df-ne 2263(𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
wnel 2357wff 𝐴𝐵
df-nel 2358(𝐴𝐵 ↔ ¬ 𝐴𝐵)
wral 2370wff 𝑥𝐴 𝜑
wrex 2371wff 𝑥𝐴 𝜑
wreu 2372wff ∃!𝑥𝐴 𝜑
wrmo 2373wff ∃*𝑥𝐴 𝜑
crab 2374class {𝑥𝐴𝜑}
df-ral 2375(∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
df-rex 2376(∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
df-reu 2377(∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
df-rmo 2378(∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
df-rab 2379{𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
cvv 2633class V
df-v 2635V = {𝑥𝑥 = 𝑥}
wcdeq 2837wff CondEq(𝑥 = 𝑦𝜑)
df-cdeq 2838(CondEq(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜑))
wsbc 2854wff [𝐴 / 𝑥]𝜑
df-sbc 2855([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
csb 2947class 𝐴 / 𝑥𝐵
df-csb 2948𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
cdif 3010class (𝐴𝐵)
cun 3011class (𝐴𝐵)
cin 3012class (𝐴𝐵)
wss 3013wff 𝐴𝐵
df-dif 3015(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴 ∧ ¬ 𝑥𝐵)}
df-un 3017(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
df-in 3019(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
df-ss 3026(𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
c0 3302class
df-nul 3303∅ = (V ∖ V)
cif 3413class if(𝜑, 𝐴, 𝐵)
df-if 3414if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
cpw 3449class 𝒫 𝐴
df-pw 3451𝒫 𝐴 = {𝑥𝑥𝐴}
csn 3466class {𝐴}
cpr 3467class {𝐴, 𝐵}
ctp 3468class {𝐴, 𝐵, 𝐶}
cop 3469class 𝐴, 𝐵
cotp 3470class 𝐴, 𝐵, 𝐶
df-sn 3472{𝐴} = {𝑥𝑥 = 𝐴}
df-pr 3473{𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
df-tp 3474{𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
df-op 3475𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
df-ot 3476𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
cuni 3675class 𝐴
df-uni 3676 𝐴 = {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦𝐴)}
cint 3710class 𝐴
df-int 3711 𝐴 = {𝑥 ∣ ∀𝑦(𝑦𝐴𝑥𝑦)}
ciun 3752class 𝑥𝐴 𝐵
ciin 3753class 𝑥𝐴 𝐵
df-iun 3754 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
df-iin 3755 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
wdisj 3844wff Disj 𝑥𝐴 𝐵
df-disj 3845(Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)
wbr 3867wff 𝐴𝑅𝐵
df-br 3868(𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
copab 3920class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
cmpt 3921class (𝑥𝐴𝐵)
df-opab 3922{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
df-mpt 3923(𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
wtr 3958wff Tr 𝐴
df-tr 3959(Tr 𝐴 𝐴𝐴)
ax-coll 3975𝑏𝜑       (∀𝑥𝑎𝑦𝜑 → ∃𝑏𝑥𝑎𝑦𝑏 𝜑)
ax-sep 3978𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))
ax-nul 3986𝑥𝑦 ¬ 𝑦𝑥
ax-pow 4030𝑦𝑧(∀𝑤(𝑤𝑧𝑤𝑥) → 𝑧𝑦)
wem 4050wff EXMID
df-exmid 4051(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥))
ax-pr 4060𝑧𝑤((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧)
cep 4138class E
cid 4139class I
df-eprel 4140 E = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}
df-id 4144 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
wpo 4145wff 𝑅 Po 𝐴
wor 4146wff 𝑅 Or 𝐴
df-po 4147(𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
df-iso 4148(𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))))
wfrfor 4178wff FrFor 𝑅𝐴𝑆
wfr 4179wff 𝑅 Fr 𝐴
wse 4180wff 𝑅 Se 𝐴
wwe 4181wff 𝑅 We 𝐴
df-frfor 4182( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆))
df-frind 4183(𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)
df-se 4184(𝑅 Se 𝐴 ↔ ∀𝑥𝐴 {𝑦𝐴𝑦𝑅𝑥} ∈ V)
df-wetr 4185(𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
word 4213wff Ord 𝐴
con0 4214class On
wlim 4215wff Lim 𝐴
csuc 4216class suc 𝐴
df-iord 4217(Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 Tr 𝑥))
df-on 4219On = {𝑥 ∣ Ord 𝑥}
df-ilim 4220(Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴))
df-suc 4222suc 𝐴 = (𝐴 ∪ {𝐴})
ax-un 4284𝑦𝑧(∃𝑤(𝑧𝑤𝑤𝑥) → 𝑧𝑦)
ax-setind 4381(∀𝑎(∀𝑦𝑎 [𝑦 / 𝑎]𝜑𝜑) → ∀𝑎𝜑)
ax-iinf 4431𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦𝑥 → suc 𝑦𝑥))
com 4433class ω
df-iom 4434ω = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
cxp 4465class (𝐴 × 𝐵)
ccnv 4466class 𝐴
cdm 4467class dom 𝐴
crn 4468class ran 𝐴
cres 4469class (𝐴𝐵)
cima 4470class (𝐴𝐵)
ccom 4471class (𝐴𝐵)
wrel 4472wff Rel 𝐴
df-xp 4473(𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
df-rel 4474(Rel 𝐴𝐴 ⊆ (V × V))
df-cnv 4475𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
df-co 4476(𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
df-dm 4477dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
df-rn 4478ran 𝐴 = dom 𝐴
df-res 4479(𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
df-ima 4480(𝐴𝐵) = ran (𝐴𝐵)
cio 5012class (℩𝑥𝜑)
df-iota 5014(℩𝑥𝜑) = {𝑦 ∣ {𝑥𝜑} = {𝑦}}
wfun 5043wff Fun 𝐴
wfn 5044wff 𝐴 Fn 𝐵
wf 5045wff 𝐹:𝐴𝐵
wf1 5046wff 𝐹:𝐴1-1𝐵
wfo 5047wff 𝐹:𝐴onto𝐵
wf1o 5048wff 𝐹:𝐴1-1-onto𝐵
cfv 5049class (𝐹𝐴)
wiso 5050wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
df-fun 5051(Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
df-fn 5052(𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
df-f 5053(𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
df-f1 5054(𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
df-fo 5055(𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
df-f1o 5056(𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
df-fv 5057(𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
df-isom 5058(𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
crio 5645class (𝑥𝐴 𝜑)
df-riota 5646(𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
co 5690class (𝐴𝐹𝐵)
coprab 5691class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
cmpt2 5692class (𝑥𝐴, 𝑦𝐵𝐶)
df-ov 5693(𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
df-oprab 5694{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
df-mpt2 5695(𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
cof 5892class 𝑓 𝑅
cofr 5893class 𝑟 𝑅
df-of 5894𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓𝑥)𝑅(𝑔𝑥))))
df-ofr 5895𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
c1st 5947class 1st
c2nd 5948class 2nd
df-1st 59491st = (𝑥 ∈ V ↦ dom {𝑥})
df-2nd 59502nd = (𝑥 ∈ V ↦ ran {𝑥})
ctpos 6047class tpos 𝐹
df-tpos 6048tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (dom 𝐹 ∪ {∅}) ↦ {𝑥}))
wsmo 6088wff Smo 𝐴
df-smo 6089(Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴𝑦 ∈ dom 𝐴(𝑥𝑦 → (𝐴𝑥) ∈ (𝐴𝑦))))
crecs 6107class recs(𝐹)
df-recs 6108recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
crdg 6172class rec(𝐹, 𝐼)
df-irdg 6173rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))))
cfrec 6193class frec(𝐹, 𝐼)
df-frec 6194frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐼))})) ↾ ω)
c1o 6212class 1o
c2o 6213class 2o
c3o 6214class 3o
c4o 6215class 4o
coa 6216class +o
comu 6217class ·o
coei 6218class o
df-1o 62191o = suc ∅
df-2o 62202o = suc 1o
df-3o 62213o = suc 2o
df-4o 62224o = suc 3o
df-oadd 6223 +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦))
df-omul 6224 ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦))
df-oexpi 6225o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦))
wer 6329wff 𝑅 Er 𝐴
cec 6330class [𝐴]𝑅
cqs 6331class (𝐴 / 𝑅)
df-er 6332(𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
df-ec 6334[𝐴]𝑅 = (𝑅 “ {𝐴})
df-qs 6338(𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
cmap 6445class 𝑚
cpm 6446class pm
df-map 6447𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓𝑓:𝑦𝑥})
df-pm 6448pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓})
cixp 6495class X𝑥𝐴 𝐵
df-ixp 6496X𝑥𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)}
cen 6535class
cdom 6536class
cfn 6537class Fin
df-en 6538 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
df-dom 6539 ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1𝑦}
df-fin 6540Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥𝑦}
csup 6757class sup(𝐴, 𝐵, 𝑅)
cinf 6758class inf(𝐴, 𝐵, 𝑅)
df-sup 6759sup(𝐴, 𝐵, 𝑅) = {𝑥𝐵 ∣ (∀𝑦𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐴 𝑦𝑅𝑧))}
df-inf 6760inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑅)
cdju 6810class (𝐴𝐵)
df-dju 6811(𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
cinl 6817class inl
cinr 6818class inr
df-inl 6819inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩)
df-inr 6820inr = (𝑥 ∈ V ↦ ⟨1o, 𝑥⟩)
cdjucase 6854class case(𝑅, 𝑆)
df-case 6855case(𝑅, 𝑆) = ((𝑅inl) ∪ (𝑆inr))
cdjud 6864class (𝑅d 𝑆)
df-djud 6865(𝑅d 𝑆) = ((𝑅(inl ↾ dom 𝑅)) ∪ (𝑆(inr ↾ dom 𝑆)))
comni 6875class Omni
xnninf 6876class
df-omni 6877Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥𝑦 (𝑓𝑥) = ∅ ∨ ∀𝑥𝑦 (𝑓𝑥) = 1o))}
df-nninf 6878 = {𝑓 ∈ (2o𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓𝑖)}
cmarkov 6895class Markov
df-markov 6896Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))}
ccrd 6904class card
df-card 6905card = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
cnpi 6928class N
cpli 6929class +N
cmi 6930class ·N
clti 6931class <N
cplpq 6932class +pQ
cmpq 6933class ·pQ
cltpq 6934class <pQ
ceq 6935class ~Q
cnq 6936class Q
c1q 6937class 1Q
cplq 6938class +Q
cmq 6939class ·Q
crq 6940class *Q
cltq 6941class <Q
ceq0 6942class ~Q0
cnq0 6943class Q0
c0q0 6944class 0Q0
cplq0 6945class +Q0
cmq0 6946class ·Q0
cnp 6947class P
c1p 6948class 1P
cpp 6949class +P
cmp 6950class ·P
cltp 6951class <P
cer 6952class ~R
cnr 6953class R
c0r 6954class 0R
c1r 6955class 1R
cm1r 6956class -1R
cplr 6957class +R
cmr 6958class ·R
cltr 6959class <R
df-ni 6960N = (ω ∖ {∅})
df-pli 6961 +N = ( +o ↾ (N × N))
df-mi 6962 ·N = ( ·o ↾ (N × N))
df-lti 6963 <N = ( E ∩ (N × N))
df-plpq 7000 +pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨(((1st𝑥) ·N (2nd𝑦)) +N ((1st𝑦) ·N (2nd𝑥))), ((2nd𝑥) ·N (2nd𝑦))⟩)
df-mpq 7001 ·pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨((1st𝑥) ·N (1st𝑦)), ((2nd𝑥) ·N (2nd𝑦))⟩)
df-ltpq 7002 <pQ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ((1st𝑥) ·N (2nd𝑦)) <N ((1st𝑦) ·N (2nd𝑥)))}
df-enq 7003 ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}
df-nqqs 7004Q = ((N × N) / ~Q )
df-plqqs 7005 +Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ +pQ𝑢, 𝑓⟩)] ~Q ))}
df-mqqs 7006 ·Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ𝑢, 𝑓⟩)] ~Q ))}
df-1nqqs 70071Q = [⟨1o, 1o⟩] ~Q
df-rq 7008*Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥Q𝑦Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
df-ltnqqs 7009 <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
df-enq0 7080 ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))}
df-nq0 7081Q0 = ((ω × N) / ~Q0 )
df-0nq0 70820Q0 = [⟨∅, 1o⟩] ~Q0
df-plq0 7083 +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q0𝑦Q0) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
df-mq0 7084 ·Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q0𝑦Q0) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨(𝑤 ·o 𝑢), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
df-inp 7122P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)) ∧ ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))))}
df-i1p 71231P = ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
df-iplp 7124 +P = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
df-imp 7125 ·P = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
df-iltp 7126<P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
df-enr 7369 ~R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (P × P) ∧ 𝑦 ∈ (P × P)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 +P 𝑢) = (𝑤 +P 𝑣)))}
df-nr 7370R = ((P × P) / ~R )
df-plr 7371 +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}
df-mr 7372 ·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑓)), ((𝑤 ·P 𝑓) +P (𝑣 ·P 𝑢))⟩] ~R ))}
df-ltr 7373 <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
df-0r 73740R = [⟨1P, 1P⟩] ~R
df-1r 73751R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 7376-1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 7445class
cr 7446class
cc0 7447class 0
c1 7448class 1
ci 7449class i
caddc 7450class +
cltrr 7451class <
cmul 7452class ·
df-c 7453ℂ = (R × R)
df-0 74540 = ⟨0R, 0R
df-1 74551 = ⟨1R, 0R
df-i 7456i = ⟨0R, 1R
df-r 7457ℝ = (R × {0R})
df-add 7458 + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
df-mul 7459 · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
df-lt 7460 < = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
ax-cnex 7533ℂ ∈ V
ax-resscn 7534ℝ ⊆ ℂ
ax-1cn 75351 ∈ ℂ
ax-1re 75361 ∈ ℝ
ax-icn 7537i ∈ ℂ
ax-addcl 7538((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
ax-addrcl 7539((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
ax-mulcl 7540((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
ax-mulrcl 7541((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
ax-addcom 7542((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
ax-mulcom 7543((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
ax-addass 7544((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
ax-mulass 7545((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
ax-distr 7546((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
ax-i2m1 7547((i · i) + 1) = 0
ax-0lt1 75480 < 1
ax-1rid 7549(𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
ax-0id 7550(𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
ax-rnegex 7551(𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
ax-precex 7552((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ (𝐴 · 𝑥) = 1))
ax-cnre 7553(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
ax-pre-ltirr 7554(𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
ax-pre-ltwlin 7555((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶𝐶 < 𝐵)))
ax-pre-lttrn 7556((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
ax-pre-apti 7557((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)
ax-pre-ltadd 7558((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
ax-pre-mulgt0 7559((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))
ax-pre-mulext 7560((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) < (𝐵 · 𝐶) → (𝐴 < 𝐵𝐵 < 𝐴)))
ax-arch 7561(𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
ax-caucvg 7562𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))
cpnf 7616class +∞
cmnf 7617class -∞
cxr 7618class *
clt 7619class <
cle 7620class
df-pnf 7621+∞ = 𝒫
df-mnf 7622-∞ = 𝒫 +∞
df-xr 7623* = (ℝ ∪ {+∞, -∞})
df-ltxr 7624 < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
df-le 7625 ≤ = ((ℝ* × ℝ*) ∖ < )
cmin 7750class
cneg 7751class -𝐴
df-sub 7752 − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
df-neg 7753-𝐴 = (0 − 𝐴)
creap 8148class #
df-reap 8149 # = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
cap 8155class #
df-ap 8156 # = {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))}
cdiv 8236class /
df-div 8237 / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
cn 8520class
df-inn 8521ℕ = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
c2 8571class 2
c3 8572class 3
c4 8573class 4
c5 8574class 5
c6 8575class 6
c7 8576class 7
c8 8577class 8
c9 8578class 9
df-2 85792 = (1 + 1)
df-3 85803 = (2 + 1)
df-4 85814 = (3 + 1)
df-5 85825 = (4 + 1)
df-6 85836 = (5 + 1)
df-7 85847 = (6 + 1)
df-8 85858 = (7 + 1)
df-9 85869 = (8 + 1)
cn0 8771class 0
df-n0 87720 = (ℕ ∪ {0})
cxnn0 8834class 0*
df-xnn0 88350* = (ℕ0 ∪ {+∞})
cz 8848class
df-z 8849ℤ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ -𝑛 ∈ ℕ)}
cdc 8976class 𝐴𝐵
df-dec 8977𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
cuz 9118class
df-uz 9119 = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗𝑘})
cq 9203class
df-q 9204ℚ = ( / “ (ℤ × ℕ))
crp 9233class +
df-rp 9234+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
cxne 9339class -𝑒𝐴
cxad 9340class +𝑒
cxmu 9341class ·e
df-xneg 9342-𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
df-xadd 9343 +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
df-xmul 9344 ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
cioo 9454class (,)
cioc 9455class (,]
cico 9456class [,)
cicc 9457class [,]
df-ioo 9458(,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
df-ioc 9459(,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
df-ico 9460[,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
df-icc 9461[,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
cfz 9573class ...
df-fz 9574... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚𝑘𝑘𝑛)})
cfzo 9702class ..^
df-fzo 9703..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
cfl 9824class
cceil 9825class
df-fl 9826⌊ = (𝑥 ∈ ℝ ↦ (𝑦 ∈ ℤ (𝑦𝑥𝑥 < (𝑦 + 1))))
df-ceil 9827⌈ = (𝑥 ∈ ℝ ↦ -(⌊‘-𝑥))
cmo 9878class mod
df-mod 9879 mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
cseq 10000class seq𝑀( + , 𝐹)
df-seqfrec 10001seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹𝑀)⟩)
cexp 10069class
df-exp 10070↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}))‘-𝑦)))))
cfa 10248class !
df-fac 10249! = ({⟨0, 1⟩} ∪ seq1( · , I ))
cbc 10270class C
df-bc 10271C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
chash 10298class
df-ihash 10299♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))
cshi 10363class shift
df-shft 10364 shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦𝑥)𝑓𝑧)})
ccj 10388class
cre 10389class
cim 10390class
df-cj 10391∗ = (𝑥 ∈ ℂ ↦ (𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥𝑦)) ∈ ℝ)))
df-re 10392ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2))
df-im 10393ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i)))
csqrt 10544class
cabs 10545class abs
df-rsqrt 10546√ = (𝑥 ∈ ℝ ↦ (𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
df-abs 10547abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
cli 10821class
df-clim 10822 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
csu 10896class Σ𝑘𝐴 𝐵
df-sumdc 10897Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)))‘𝑚))))
ce 11081class exp
ceu 11082class e
csin 11083class sin
ccos 11084class cos
ctan 11085class tan
cpi 11086class π
df-ef 11087exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥𝑘) / (!‘𝑘)))
df-e 11088e = (exp‘1)
df-sin 11089sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
df-cos 11090cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2))
df-tan 11091tan = (𝑥 ∈ (cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥)))
df-pi 11092π = inf((ℝ+ ∩ (sin “ {0})), ℝ, < )
cdvds 11223class
df-dvds 11224 ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
cgcd 11365class gcd
df-gcd 11366 gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑥𝑛𝑦)}, ℝ, < )))
clcm 11469class lcm
df-lcm 11470 lcm = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥𝑛𝑦𝑛)}, ℝ, < )))
cprime 11516class
df-prm 11517ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2o}
cnumer 11586class numer
cdenom 11587class denom
df-numer 11588numer = (𝑦 ∈ ℚ ↦ (1st ‘(𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥))))))
df-denom 11589denom = (𝑦 ∈ ℚ ↦ (2nd ‘(𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥))))))
cphi 11613class ϕ
df-phi 11614ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
cstr 11639class Struct
cnx 11640class ndx
csts 11641class sSet
cslot 11642class Slot 𝐴
cbs 11643class Base
cress 11644class s
df-struct 11645 Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
df-ndx 11646ndx = ( I ↾ ℕ)
df-slot 11647Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥𝐴))
df-base 11649Base = Slot 1
df-sets 11650 sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))
df-ress 11651s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
cplusg 11705class +g
cmulr 11706class .r
cstv 11707class *𝑟
csca 11708class Scalar
cvsca 11709class ·𝑠
cip 11710class ·𝑖
cts 11711class TopSet
cple 11712class le
coc 11713class oc
cds 11714class dist
cunif 11715class UnifSet
chom 11716class Hom
cco 11717class comp
df-plusg 11718+g = Slot 2
df-mulr 11719.r = Slot 3
df-starv 11720*𝑟 = Slot 4
df-sca 11721Scalar = Slot 5
df-vsca 11722 ·𝑠 = Slot 6
df-ip 11723·𝑖 = Slot 8
df-tset 11724TopSet = Slot 9
df-ple 11725le = Slot 10
df-ocomp 11726oc = Slot 11
df-ds 11727dist = Slot 12
df-unif 11728UnifSet = Slot 13
df-hom 11729Hom = Slot 14
df-cco 11730comp = Slot 15
crest 11804class t
ctopn 11805class TopOpen
df-rest 11806t = (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦𝑗 ↦ (𝑦𝑥)))
df-topn 11807TopOpen = (𝑤 ∈ V ↦ ((TopSet‘𝑤) ↾t (Base‘𝑤)))
ctg 11819class topGen
cpt 11820class t
c0g 11821class 0g
cgsu 11822class Σg
df-0g 118230g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g𝑔)𝑥) = 𝑥 ∧ (𝑥(+g𝑔)𝑒) = 𝑥))))
df-gsum 11824 Σ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 11825topGen = (𝑥 ∈ V ↦ {𝑦𝑦 (𝑥 ∩ 𝒫 𝑦)})
df-pt 11826t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}))
cprds 11827class Xs
cpws 11828class s
df-prds 11829Xs = (𝑠 ∈ 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 11831s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
cpsmet 11832class PsMet
cxmet 11833class ∞Met
cmet 11834class Met
cbl 11835class ball
cfbas 11836class fBas
cfg 11837class filGen
cmopn 11838class MetOpen
cmetu 11839class metUnif
df-psmet 11840PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧𝑥𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
df-xmet 11841∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥𝑧𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
df-met 11842Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥𝑧𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})
df-bl 11843ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))
df-mopn 11844MetOpen = (𝑑 ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))
df-fbas 11845fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑥 ∩ 𝒫 (𝑦𝑧)) ≠ ∅)})
df-fg 11846filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
df-metu 11847metUnif = (𝑑 ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (𝑑 “ (0[,)𝑎)))))
ctop 11848class Top
df-top 11849Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥 𝑦𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ∈ 𝑥)}
ctopon 11861class TopOn
df-topon 11862TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = 𝑗})
ctps 11880class TopSp
df-topsp 11881TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
ctb 11892class TopBases
df-bases 11893TopBases = {𝑥 ∣ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ⊆ (𝑥 ∩ 𝒫 (𝑦𝑧))}
ccld 11944class Clsd
cnt 11945class int
ccl 11946class cls
df-cld 11947Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗})
df-ntr 11948int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 (𝑗 ∩ 𝒫 𝑥)))
df-cls 11949cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥𝑦}))
cnei 11990class nei
df-nei 11991nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 ↦ {𝑦 ∈ 𝒫 𝑗 ∣ ∃𝑔𝑗 (𝑥𝑔𝑔𝑦)}))
ccn 12037class Cn
ccnp 12038class CnP
clm 12039class 𝑡
df-cn 12040 Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 (𝑓𝑦) ∈ 𝑗})
df-cnp 12041 CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
df-lm 12042𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
cxms 12122class ∞MetSp
cms 12123class MetSp
ctms 12124class toMetSp
df-xms 12125∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpen‘𝑓) = (MetOpen‘((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))))}
df-ms 12126MetSp = {𝑓 ∈ ∞MetSp ∣ ((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))) ∈ (Met‘(Base‘𝑓))}
df-tms 12127toMetSp = (𝑑 ran ∞Met ↦ ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩))
ccncf 12325class cn
df-cncf 12326cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
climc 12358class lim
df-limced 12359 lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)))})
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 12410wff 𝐴 DECIDin 𝐵
df-dcin 12411(𝐴 DECIDin 𝐵 ↔ ∀𝑥𝐵 DECID 𝑥𝐴)
wbd 12420wff BOUNDED 𝜑
ax-bd0 12421(𝜑𝜓)       (BOUNDED 𝜑BOUNDED 𝜓)
ax-bdim 12422BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdan 12423BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdor 12424BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdn 12425BOUNDED 𝜑       BOUNDED ¬ 𝜑
ax-bdal 12426BOUNDED 𝜑       BOUNDED𝑥𝑦 𝜑
ax-bdex 12427BOUNDED 𝜑       BOUNDED𝑥𝑦 𝜑
ax-bdeq 12428BOUNDED 𝑥 = 𝑦
ax-bdel 12429BOUNDED 𝑥𝑦
ax-bdsb 12430BOUNDED 𝜑       BOUNDED [𝑦 / 𝑥]𝜑
wbdc 12448wff BOUNDED 𝐴
df-bdc 12449(BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥𝐴)
ax-bdsep 12492BOUNDED 𝜑       𝑎𝑏𝑥(𝑥𝑏 ↔ (𝑥𝑎𝜑))
ax-bj-d0cl 12532BOUNDED 𝜑       DECID 𝜑
wind 12538wff Ind 𝐴
df-bj-ind 12539(Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴))
ax-infvn 12553𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦𝑥𝑦))
ax-bdsetind 12580BOUNDED 𝜑       (∀𝑎(∀𝑦𝑎 [𝑦 / 𝑎]𝜑𝜑) → ∀𝑎𝜑)
ax-inf2 12588𝑎𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
ax-strcoll 12594𝑎(∀𝑥𝑎𝑦𝜑 → ∃𝑏𝑦(𝑦𝑏 ↔ ∃𝑥𝑎 𝜑))
ax-sscoll 12599𝑎𝑏𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑))
ax-ddkcomp 12601(((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 𝑦𝑥 ∧ ((𝐵𝑅 ∧ ∀𝑦𝐴 𝑦𝐵) → 𝑥𝐵)))
walsi 12633wff ∀!𝑥(𝜑𝜓)
walsc 12634wff ∀!𝑥𝐴𝜑
df-alsi 12635(∀!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃𝑥𝜑))
df-alsc 12636(∀!𝑥𝐴𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∃𝑥 𝑥𝐴))
  Copyright terms: Public domain W3C validator