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