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 102wff (𝜑𝜓)
wb 103wff (𝜑𝜓)
ax-ia1 104((𝜑𝜓) → 𝜑)
ax-ia2 105((𝜑𝜓) → 𝜓)
ax-ia3 106(𝜑 → (𝜓 → (𝜑𝜓)))
df-bi 115(((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
ax-in1 577((𝜑 → ¬ 𝜑) → ¬ 𝜑)
ax-in2 578𝜑 → (𝜑𝜓))
wo 662wff (𝜑𝜓)
ax-io 663(((𝜑𝜒) → 𝜓) ↔ ((𝜑𝜓) ∧ (𝜒𝜓)))
wstab 773wff STAB 𝜑
df-stab 774(STAB 𝜑 ↔ (¬ ¬ 𝜑𝜑))
wdc 776wff DECID 𝜑
df-dc 777(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
w3o 919wff (𝜑𝜓𝜒)
w3a 920wff (𝜑𝜓𝜒)
df-3or 921((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
df-3an 922((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
wal 1283wff 𝑥𝜑
cv 1284class 𝑥
wceq 1285wff 𝐴 = 𝐵
wtru 1286wff
df-tru 1288(⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
wfal 1290wff
df-fal 1291(⊥ ↔ ¬ ⊤)
wxo 1307wff (𝜑𝜓)
df-xor 1308((𝜑𝜓) ↔ ((𝜑𝜓) ∧ ¬ (𝜑𝜓)))
ax-5 1377(∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
ax-7 1378(∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
ax-gen 1379𝜑       𝑥𝜑
wnf 1390wff 𝑥𝜑
df-nf 1391(Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
wex 1422wff 𝑥𝜑
ax-ie1 1423(∃𝑥𝜑 → ∀𝑥𝑥𝜑)
ax-ie2 1424(∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓)))
wcel 1434wff 𝐴𝐵
ax-8 1436(𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
ax-10 1437(∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
ax-11 1438(𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
ax-i12 1439(∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
ax-bndl 1440(∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
ax-4 1441(∀𝑥𝜑𝜑)
ax-13 1445(𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
ax-14 1446(𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
ax-17 1460(𝜑 → ∀𝑥𝜑)
ax-i9 1464𝑥 𝑥 = 𝑦
ax-ial 1468(∀𝑥𝜑 → ∀𝑥𝑥𝜑)
ax-i5r 1469((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑𝜓))
ax-10o 1646(∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
wsb 1687wff [𝑦 / 𝑥]𝜑
df-sb 1688([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦𝜑) ∧ ∃𝑥(𝑥 = 𝑦𝜑)))
ax-16 1737(∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
ax-11o 1746(¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
weu 1943wff ∃!𝑥𝜑
wmo 1944wff ∃*𝑥𝜑
df-eu 1946(∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
df-mo 1947(∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
ax-ext 2065(∀𝑧(𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
cab 2069class {𝑥𝜑}
df-clab 2070(𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
df-cleq 2076(∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)       (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
df-clel 2079(𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
wnfc 2210wff 𝑥𝐴
df-nfc 2212(𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
wne 2249wff 𝐴𝐵
df-ne 2250(𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
wnel 2344wff 𝐴𝐵
df-nel 2345(𝐴𝐵 ↔ ¬ 𝐴𝐵)
wral 2353wff 𝑥𝐴 𝜑
wrex 2354wff 𝑥𝐴 𝜑
wreu 2355wff ∃!𝑥𝐴 𝜑
wrmo 2356wff ∃*𝑥𝐴 𝜑
crab 2357class {𝑥𝐴𝜑}
df-ral 2358(∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
df-rex 2359(∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
df-reu 2360(∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
df-rmo 2361(∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
df-rab 2362{𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
cvv 2612class V
df-v 2614V = {𝑥𝑥 = 𝑥}
wcdeq 2809wff CondEq(𝑥 = 𝑦𝜑)
df-cdeq 2810(CondEq(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜑))
wsbc 2826wff [𝐴 / 𝑥]𝜑
df-sbc 2827([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
csb 2919class 𝐴 / 𝑥𝐵
df-csb 2920𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
cdif 2981class (𝐴𝐵)
cun 2982class (𝐴𝐵)
cin 2983class (𝐴𝐵)
wss 2984wff 𝐴𝐵
df-dif 2986(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴 ∧ ¬ 𝑥𝐵)}
df-un 2988(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
df-in 2990(𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
df-ss 2997(𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
c0 3269class
df-nul 3270∅ = (V ∖ V)
cif 3373class if(𝜑, 𝐴, 𝐵)
df-if 3374if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
cpw 3406class 𝒫 𝐴
df-pw 3408𝒫 𝐴 = {𝑥𝑥𝐴}
csn 3422class {𝐴}
cpr 3423class {𝐴, 𝐵}
ctp 3424class {𝐴, 𝐵, 𝐶}
cop 3425class 𝐴, 𝐵
cotp 3426class 𝐴, 𝐵, 𝐶
df-sn 3428{𝐴} = {𝑥𝑥 = 𝐴}
df-pr 3429{𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
df-tp 3430{𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
df-op 3431𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
df-ot 3432𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
cuni 3627class 𝐴
df-uni 3628 𝐴 = {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦𝐴)}
cint 3662class 𝐴
df-int 3663 𝐴 = {𝑥 ∣ ∀𝑦(𝑦𝐴𝑥𝑦)}
ciun 3704class 𝑥𝐴 𝐵
ciin 3705class 𝑥𝐴 𝐵
df-iun 3706 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
df-iin 3707 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
wdisj 3792wff Disj 𝑥𝐴 𝐵
df-disj 3793(Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)
wbr 3811wff 𝐴𝑅𝐵
df-br 3812(𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
copab 3864class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
cmpt 3865class (𝑥𝐴𝐵)
df-opab 3866{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
df-mpt 3867(𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
wtr 3901wff Tr 𝐴
df-tr 3902(Tr 𝐴 𝐴𝐴)
ax-coll 3919𝑏𝜑       (∀𝑥𝑎𝑦𝜑 → ∃𝑏𝑥𝑎𝑦𝑏 𝜑)
ax-sep 3922𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))
ax-nul 3930𝑥𝑦 ¬ 𝑦𝑥
ax-pow 3974𝑦𝑧(∀𝑤(𝑤𝑧𝑤𝑥) → 𝑧𝑦)
wem 3993wff EXMID
df-exmid 3994(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥))
ax-pr 4000𝑧𝑤((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧)
cep 4078class E
cid 4079class I
df-eprel 4080 E = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}
df-id 4084 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
wpo 4085wff 𝑅 Po 𝐴
wor 4086wff 𝑅 Or 𝐴
df-po 4087(𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
df-iso 4088(𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))))
wfrfor 4118wff FrFor 𝑅𝐴𝑆
wfr 4119wff 𝑅 Fr 𝐴
wse 4120wff 𝑅 Se 𝐴
wwe 4121wff 𝑅 We 𝐴
df-frfor 4122( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆))
df-frind 4123(𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)
df-se 4124(𝑅 Se 𝐴 ↔ ∀𝑥𝐴 {𝑦𝐴𝑦𝑅𝑥} ∈ V)
df-wetr 4125(𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
word 4153wff Ord 𝐴
con0 4154class On
wlim 4155wff Lim 𝐴
csuc 4156class suc 𝐴
df-iord 4157(Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 Tr 𝑥))
df-on 4159On = {𝑥 ∣ Ord 𝑥}
df-ilim 4160(Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴))
df-suc 4162suc 𝐴 = (𝐴 ∪ {𝐴})
ax-un 4224𝑦𝑧(∃𝑤(𝑧𝑤𝑤𝑥) → 𝑧𝑦)
ax-setind 4316(∀𝑎(∀𝑦𝑎 [𝑦 / 𝑎]𝜑𝜑) → ∀𝑎𝜑)
ax-iinf 4366𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦𝑥 → suc 𝑦𝑥))
com 4368class ω
df-iom 4369ω = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
cxp 4399class (𝐴 × 𝐵)
ccnv 4400class 𝐴
cdm 4401class dom 𝐴
crn 4402class ran 𝐴
cres 4403class (𝐴𝐵)
cima 4404class (𝐴𝐵)
ccom 4405class (𝐴𝐵)
wrel 4406wff Rel 𝐴
df-xp 4407(𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
df-rel 4408(Rel 𝐴𝐴 ⊆ (V × V))
df-cnv 4409𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
df-co 4410(𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
df-dm 4411dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
df-rn 4412ran 𝐴 = dom 𝐴
df-res 4413(𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
df-ima 4414(𝐴𝐵) = ran (𝐴𝐵)
cio 4932class (℩𝑥𝜑)
df-iota 4934(℩𝑥𝜑) = {𝑦 ∣ {𝑥𝜑} = {𝑦}}
wfun 4963wff Fun 𝐴
wfn 4964wff 𝐴 Fn 𝐵
wf 4965wff 𝐹:𝐴𝐵
wf1 4966wff 𝐹:𝐴1-1𝐵
wfo 4967wff 𝐹:𝐴onto𝐵
wf1o 4968wff 𝐹:𝐴1-1-onto𝐵
cfv 4969class (𝐹𝐴)
wiso 4970wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
df-fun 4971(Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
df-fn 4972(𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
df-f 4973(𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
df-f1 4974(𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
df-fo 4975(𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
df-f1o 4976(𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
df-fv 4977(𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
df-isom 4978(𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
crio 5546class (𝑥𝐴 𝜑)
df-riota 5547(𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
co 5591class (𝐴𝐹𝐵)
coprab 5592class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
cmpt2 5593class (𝑥𝐴, 𝑦𝐵𝐶)
df-ov 5594(𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
df-oprab 5595{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
df-mpt2 5596(𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
cof 5789class 𝑓 𝑅
cofr 5790class 𝑟 𝑅
df-of 5791𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓𝑥)𝑅(𝑔𝑥))))
df-ofr 5792𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
c1st 5844class 1st
c2nd 5845class 2nd
df-1st 58461st = (𝑥 ∈ V ↦ dom {𝑥})
df-2nd 58472nd = (𝑥 ∈ V ↦ ran {𝑥})
ctpos 5941class tpos 𝐹
df-tpos 5942tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (dom 𝐹 ∪ {∅}) ↦ {𝑥}))
wsmo 5982wff Smo 𝐴
df-smo 5983(Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴𝑦 ∈ dom 𝐴(𝑥𝑦 → (𝐴𝑥) ∈ (𝐴𝑦))))
crecs 6001class recs(𝐹)
df-recs 6002recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
crdg 6066class rec(𝐹, 𝐼)
df-irdg 6067rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))))
cfrec 6087class frec(𝐹, 𝐼)
df-frec 6088frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐼))})) ↾ ω)
c1o 6106class 1𝑜
c2o 6107class 2𝑜
c3o 6108class 3𝑜
c4o 6109class 4𝑜
coa 6110class +𝑜
comu 6111class ·𝑜
coei 6112class 𝑜
df-1o 61131𝑜 = suc ∅
df-2o 61142𝑜 = suc 1𝑜
df-3o 61153𝑜 = suc 2𝑜
df-4o 61164𝑜 = suc 3𝑜
df-oadd 6117 +𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦))
df-omul 6118 ·𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +𝑜 𝑥)), ∅)‘𝑦))
df-oexpi 6119𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)‘𝑦))
wer 6219wff 𝑅 Er 𝐴
cec 6220class [𝐴]𝑅
cqs 6221class (𝐴 / 𝑅)
df-er 6222(𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
df-ec 6224[𝐴]𝑅 = (𝑅 “ {𝐴})
df-qs 6228(𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
cmap 6335class 𝑚
cpm 6336class pm
df-map 6337𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓𝑓:𝑦𝑥})
df-pm 6338pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓})
cen 6385class
cdom 6386class
cfn 6387class Fin
df-en 6388 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
df-dom 6389 ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1𝑦}
df-fin 6390Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥𝑦}
csup 6584class sup(𝐴, 𝐵, 𝑅)
cinf 6585class inf(𝐴, 𝐵, 𝑅)
df-sup 6586sup(𝐴, 𝐵, 𝑅) = {𝑥𝐵 ∣ (∀𝑦𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐴 𝑦𝑅𝑧))}
df-inf 6587inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑅)
cdju 6637class (𝐴𝐵)
df-dju 6638(𝐴𝐵) = (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵))
cinl 6644class inl
cinr 6645class inr
df-inl 6646inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩)
df-inr 6647inr = (𝑥 ∈ V ↦ ⟨1𝑜, 𝑥⟩)
cdjucase 6681class case(𝑅, 𝑆)
df-case 6682case(𝑅, 𝑆) = ((𝑅inl) ∪ (𝑆inr))
cdjud 6689class (𝑅d 𝑆)
df-djud 6690(𝑅d 𝑆) = ((𝑅(inl ↾ dom 𝑅)) ∪ (𝑆(inr ↾ dom 𝑆)))
comni 6695class Omni
df-omni 6696Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2𝑜 → (∃𝑥𝑦 (𝑓𝑥) = ∅ ∨ ∀𝑥𝑦 (𝑓𝑥) = 1𝑜))}
ccrd 6710class card
df-card 6711card = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
cnpi 6734class N
cpli 6735class +N
cmi 6736class ·N
clti 6737class <N
cplpq 6738class +pQ
cmpq 6739class ·pQ
cltpq 6740class <pQ
ceq 6741class ~Q
cnq 6742class Q
c1q 6743class 1Q
cplq 6744class +Q
cmq 6745class ·Q
crq 6746class *Q
cltq 6747class <Q
ceq0 6748class ~Q0
cnq0 6749class Q0
c0q0 6750class 0Q0
cplq0 6751class +Q0
cmq0 6752class ·Q0
cnp 6753class P
c1p 6754class 1P
cpp 6755class +P
cmp 6756class ·P
cltp 6757class <P
cer 6758class ~R
cnr 6759class R
c0r 6760class 0R
c1r 6761class 1R
cm1r 6762class -1R
cplr 6763class +R
cmr 6764class ·R
cltr 6765class <R
df-ni 6766N = (ω ∖ {∅})
df-pli 6767 +N = ( +𝑜 ↾ (N × N))
df-mi 6768 ·N = ( ·𝑜 ↾ (N × N))
df-lti 6769 <N = ( E ∩ (N × N))
df-plpq 6806 +pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨(((1st𝑥) ·N (2nd𝑦)) +N ((1st𝑦) ·N (2nd𝑥))), ((2nd𝑥) ·N (2nd𝑦))⟩)
df-mpq 6807 ·pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨((1st𝑥) ·N (1st𝑦)), ((2nd𝑥) ·N (2nd𝑦))⟩)
df-ltpq 6808 <pQ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ((1st𝑥) ·N (2nd𝑦)) <N ((1st𝑦) ·N (2nd𝑥)))}
df-enq 6809 ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}
df-nqqs 6810Q = ((N × N) / ~Q )
df-plqqs 6811 +Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ +pQ𝑢, 𝑓⟩)] ~Q ))}
df-mqqs 6812 ·Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ𝑢, 𝑓⟩)] ~Q ))}
df-1nqqs 68131Q = [⟨1𝑜, 1𝑜⟩] ~Q
df-rq 6814*Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥Q𝑦Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
df-ltnqqs 6815 <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
df-enq0 6886 ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)))}
df-nq0 6887Q0 = ((ω × N) / ~Q0 )
df-0nq0 68880Q0 = [⟨∅, 1𝑜⟩] ~Q0
df-plq0 6889 +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q0𝑦Q0) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·𝑜 𝑓) +𝑜 (𝑣 ·𝑜 𝑢)), (𝑣 ·𝑜 𝑓)⟩] ~Q0 ))}
df-mq0 6890 ·Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥Q0𝑦Q0) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨(𝑤 ·𝑜 𝑢), (𝑣 ·𝑜 𝑓)⟩] ~Q0 ))}
df-inp 6928P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)) ∧ ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))))}
df-i1p 69291P = ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
df-iplp 6930 +P = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
df-imp 6931 ·P = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
df-iltp 6932<P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
df-enr 7175 ~R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (P × P) ∧ 𝑦 ∈ (P × P)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 +P 𝑢) = (𝑤 +P 𝑣)))}
df-nr 7176R = ((P × P) / ~R )
df-plr 7177 +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}
df-mr 7178 ·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑓)), ((𝑤 ·P 𝑓) +P (𝑣 ·P 𝑢))⟩] ~R ))}
df-ltr 7179 <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
df-0r 71800R = [⟨1P, 1P⟩] ~R
df-1r 71811R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 7182-1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 7251class
cr 7252class
cc0 7253class 0
c1 7254class 1
ci 7255class i
caddc 7256class +
cltrr 7257class <
cmul 7258class ·
df-c 7259ℂ = (R × R)
df-0 72600 = ⟨0R, 0R
df-1 72611 = ⟨1R, 0R
df-i 7262i = ⟨0R, 1R
df-r 7263ℝ = (R × {0R})
df-add 7264 + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
df-mul 7265 · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
df-lt 7266 < = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
ax-cnex 7339ℂ ∈ V
ax-resscn 7340ℝ ⊆ ℂ
ax-1cn 73411 ∈ ℂ
ax-1re 73421 ∈ ℝ
ax-icn 7343i ∈ ℂ
ax-addcl 7344((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
ax-addrcl 7345((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
ax-mulcl 7346((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
ax-mulrcl 7347((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
ax-addcom 7348((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
ax-mulcom 7349((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
ax-addass 7350((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
ax-mulass 7351((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
ax-distr 7352((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
ax-i2m1 7353((i · i) + 1) = 0
ax-0lt1 73540 < 1
ax-1rid 7355(𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
ax-0id 7356(𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
ax-rnegex 7357(𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
ax-precex 7358((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ (𝐴 · 𝑥) = 1))
ax-cnre 7359(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
ax-pre-ltirr 7360(𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
ax-pre-ltwlin 7361((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶𝐶 < 𝐵)))
ax-pre-lttrn 7362((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
ax-pre-apti 7363((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)
ax-pre-ltadd 7364((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
ax-pre-mulgt0 7365((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))
ax-pre-mulext 7366((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) < (𝐵 · 𝐶) → (𝐴 < 𝐵𝐵 < 𝐴)))
ax-arch 7367(𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
ax-caucvg 7368𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))
cpnf 7422class +∞
cmnf 7423class -∞
cxr 7424class *
clt 7425class <
cle 7426class
df-pnf 7427+∞ = 𝒫
df-mnf 7428-∞ = 𝒫 +∞
df-xr 7429* = (ℝ ∪ {+∞, -∞})
df-ltxr 7430 < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
df-le 7431 ≤ = ((ℝ* × ℝ*) ∖ < )
cmin 7556class
cneg 7557class -𝐴
df-sub 7558 − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
df-neg 7559-𝐴 = (0 − 𝐴)
creap 7951class #
df-reap 7952 # = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
cap 7958class #
df-ap 7959 # = {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))}
cdiv 8037class /
df-div 8038 / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
cn 8316class
df-inn 8317ℕ = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
c2 8366class 2
c3 8367class 3
c4 8368class 4
c5 8369class 5
c6 8370class 6
c7 8371class 7
c8 8372class 8
c9 8373class 9
c10 8374class 10
df-2 83752 = (1 + 1)
df-3 83763 = (2 + 1)
df-4 83774 = (3 + 1)
df-5 83785 = (4 + 1)
df-6 83796 = (5 + 1)
df-7 83807 = (6 + 1)
df-8 83818 = (7 + 1)
df-9 83829 = (8 + 1)
cn0 8565class 0
df-n0 85660 = (ℕ ∪ {0})
cxnn0 8628class 0*
xnninf 8629class
df-xnn0 86300* = (ℕ0 ∪ {+∞})
df-nninf 8631 = {𝑓 ∈ (2𝑜𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓𝑖)}
cz 8646class
df-z 8647ℤ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ -𝑛 ∈ ℕ)}
cdc 8772class 𝐴𝐵
df-dec 8773𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
cuz 8914class
df-uz 8915 = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗𝑘})
cq 8999class
df-q 9000ℚ = ( / “ (ℤ × ℕ))
crp 9029class +
df-rp 9030+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
cxne 9135class -𝑒𝐴
cxad 9136class +𝑒
cxmu 9137class ·e
df-xneg 9138-𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
df-xadd 9139 +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
df-xmul 9140 ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
cioo 9201class (,)
cioc 9202class (,]
cico 9203class [,)
cicc 9204class [,]
df-ioo 9205(,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
df-ioc 9206(,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
df-ico 9207[,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
df-icc 9208[,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
cfz 9319class ...
df-fz 9320... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚𝑘𝑘𝑛)})
cfzo 9443class ..^
df-fzo 9444..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
cfl 9564class
cceil 9565class
df-fl 9566⌊ = (𝑥 ∈ ℝ ↦ (𝑦 ∈ ℤ (𝑦𝑥𝑥 < (𝑦 + 1))))
df-ceil 9567⌈ = (𝑥 ∈ ℝ ↦ -(⌊‘-𝑥))
cmo 9618class mod
df-mod 9619 mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
cseq 9740class seq𝑀( + , 𝐹, 𝑆)
df-iseq 9741seq𝑀( + , 𝐹, 𝑆) = ran frec((𝑥 ∈ (ℤ𝑀), 𝑦𝑆 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹𝑀)⟩)
cexp 9791class
df-iexp 9792↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦)))))
cfa 9968class !
df-fac 9969! = ({⟨0, 1⟩} ∪ seq1( · , I , ℂ))
cbc 9990class C
df-bc 9991C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
chash 10018class
df-ihash 10019♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))
cshi 10076class shift
df-shft 10077 shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦𝑥)𝑓𝑧)})
ccj 10100class
cre 10101class
cim 10102class
df-cj 10103∗ = (𝑥 ∈ ℂ ↦ (𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥𝑦)) ∈ ℝ)))
df-re 10104ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2))
df-im 10105ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i)))
csqrt 10256class
cabs 10257class abs
df-rsqrt 10258√ = (𝑥 ∈ ℝ ↦ (𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
df-abs 10259abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
cli 10491class
df-clim 10492 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
csu 10564class Σ𝑘𝐴 𝐵
df-isum 10565Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚))))
cdvds 10576class
df-dvds 10577 ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
cgcd 10718class gcd
df-gcd 10719 gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑥𝑛𝑦)}, ℝ, < )))
clcm 10822class lcm
df-lcm 10823 lcm = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥𝑛𝑦𝑛)}, ℝ, < )))
cprime 10869class
df-prm 10870ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜}
cnumer 10939class numer
cdenom 10940class denom
df-numer 10941numer = (𝑦 ∈ ℚ ↦ (1st ‘(𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥))))))
df-denom 10942denom = (𝑦 ∈ ℚ ↦ (2nd ‘(𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥))))))
cphi 10966class ϕ
df-phi 10967ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 11036wff 𝐴 DECIDin 𝐵
df-dcin 11037(𝐴 DECIDin 𝐵 ↔ ∀𝑥𝐵 DECID 𝑥𝐴)
wbd 11046wff BOUNDED 𝜑
ax-bd0 11047(𝜑𝜓)       (BOUNDED 𝜑BOUNDED 𝜓)
ax-bdim 11048BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdan 11049BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdor 11050BOUNDED 𝜑    &   BOUNDED 𝜓       BOUNDED (𝜑𝜓)
ax-bdn 11051BOUNDED 𝜑       BOUNDED ¬ 𝜑
ax-bdal 11052BOUNDED 𝜑       BOUNDED𝑥𝑦 𝜑
ax-bdex 11053BOUNDED 𝜑       BOUNDED𝑥𝑦 𝜑
ax-bdeq 11054BOUNDED 𝑥 = 𝑦
ax-bdel 11055BOUNDED 𝑥𝑦
ax-bdsb 11056BOUNDED 𝜑       BOUNDED [𝑦 / 𝑥]𝜑
wbdc 11074wff BOUNDED 𝐴
df-bdc 11075(BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥𝐴)
ax-bdsep 11118BOUNDED 𝜑       𝑎𝑏𝑥(𝑥𝑏 ↔ (𝑥𝑎𝜑))
ax-bj-d0cl 11158BOUNDED 𝜑       DECID 𝜑
wind 11164wff Ind 𝐴
df-bj-ind 11165(Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴))
ax-infvn 11179𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦𝑥𝑦))
ax-bdsetind 11206BOUNDED 𝜑       (∀𝑎(∀𝑦𝑎 [𝑦 / 𝑎]𝜑𝜑) → ∀𝑎𝜑)
ax-inf2 11214𝑎𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
ax-strcoll 11220𝑎(∀𝑥𝑎𝑦𝜑 → ∃𝑏𝑦(𝑦𝑏 ↔ ∃𝑥𝑎 𝜑))
ax-sscoll 11225𝑎𝑏𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑))
ax-ddkcomp 11227(((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 𝑦𝑥 ∧ ((𝐵𝑅 ∧ ∀𝑦𝐴 𝑦𝐵) → 𝑥𝐵)))
walsi 11230wff ∀!𝑥(𝜑𝜓)
walsc 11231wff ∀!𝑥𝐴𝜑
df-alsi 11232(∀!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃𝑥𝜑))
df-alsc 11233(∀!𝑥𝐴𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∃𝑥 𝑥𝐴))
  Copyright terms: Public domain W3C validator