List of Syntax, Axioms (ax-) and
Definitions (df-)|
Ref | Expression (see link for any distinct variable requirements)
|
| wn 3 | wff ¬ 𝜑 |
| wi 4 | wff (𝜑 → 𝜓) |
| ax-mp 5 | ⊢ 𝜑
& ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 |
| ax-1 6 | ⊢ (𝜑 → (𝜓 → 𝜑)) |
| ax-2 7 | ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) |
| wa 103 | wff (𝜑 ∧ 𝜓) |
| wb 104 | wff (𝜑 ↔ 𝜓) |
| ax-ia1 105 | ⊢ ((𝜑 ∧ 𝜓) → 𝜑) |
| ax-ia2 106 | ⊢ ((𝜑 ∧ 𝜓) → 𝜓) |
| ax-ia3 107 | ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
| df-bi 116 | ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) |
| ax-in1 609 | ⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑) |
| ax-in2 610 | ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) |
| wo 703 | wff (𝜑 ∨ 𝜓) |
| ax-io 704 | ⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓))) |
| wstab 825 | wff STAB 𝜑 |
| df-stab 826 | ⊢ (STAB 𝜑 ↔ (¬ ¬ 𝜑 → 𝜑)) |
| wdc 829 | wff DECID 𝜑 |
| df-dc 830 | ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
| w3o 972 | wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
| w3a 973 | wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
| df-3or 974 | ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
| df-3an 975 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
| wal 1346 | wff ∀𝑥𝜑 |
| cv 1347 | class 𝑥 |
| wceq 1348 | wff 𝐴 = 𝐵 |
| wtru 1349 | wff ⊤ |
| df-tru 1351 | ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) |
| wfal 1353 | wff ⊥ |
| df-fal 1354 | ⊢ (⊥ ↔ ¬
⊤) |
| wxo 1370 | wff (𝜑 ⊻ 𝜓) |
| df-xor 1371 | ⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) |
| ax-5 1440 | ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) |
| ax-7 1441 | ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
| ax-gen 1442 | ⊢ 𝜑 ⇒ ⊢ ∀𝑥𝜑 |
| wnf 1453 | wff Ⅎ𝑥𝜑 |
| df-nf 1454 | ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) |
| wex 1485 | wff ∃𝑥𝜑 |
| ax-ie1 1486 | ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) |
| ax-ie2 1487 | ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))) |
| ax-8 1497 | ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) |
| ax-10 1498 | ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) |
| ax-11 1499 | ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
| ax-i12 1500 | ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
| ax-bndl 1502 | ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
| ax-4 1503 | ⊢ (∀𝑥𝜑 → 𝜑) |
| ax-17 1519 | ⊢ (𝜑 → ∀𝑥𝜑) |
| ax-i9 1523 | ⊢ ∃𝑥 𝑥 = 𝑦 |
| ax-ial 1527 | ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) |
| ax-i5r 1528 | ⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑 → 𝜓)) |
| ax-10o 1709 | ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) |
| wsb 1755 | wff [𝑦 / 𝑥]𝜑 |
| df-sb 1756 | ⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
| ax-16 1807 | ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) |
| ax-11o 1816 | ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) |
| weu 2019 | wff ∃!𝑥𝜑 |
| wmo 2020 | wff ∃*𝑥𝜑 |
| df-eu 2022 | ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
| df-mo 2023 | ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
| wcel 2141 | wff 𝐴 ∈ 𝐵 |
| ax-13 2143 | ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) |
| ax-14 2144 | ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) |
| ax-ext 2152 | ⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) |
| cab 2156 | class {𝑥 ∣ 𝜑} |
| df-clab 2157 | ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) |
| df-cleq 2163 | ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧) ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
| df-clel 2166 | ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
| wnfc 2299 | wff Ⅎ𝑥𝐴 |
| df-nfc 2301 | ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) |
| wne 2340 | wff 𝐴 ≠ 𝐵 |
| df-ne 2341 | ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) |
| wnel 2435 | wff 𝐴 ∉ 𝐵 |
| df-nel 2436 | ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) |
| wral 2448 | wff ∀𝑥 ∈ 𝐴 𝜑 |
| wrex 2449 | wff ∃𝑥 ∈ 𝐴 𝜑 |
| wreu 2450 | wff ∃!𝑥 ∈ 𝐴 𝜑 |
| wrmo 2451 | wff ∃*𝑥 ∈ 𝐴 𝜑 |
| crab 2452 | class {𝑥 ∈ 𝐴 ∣ 𝜑} |
| df-ral 2453 | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
| df-rex 2454 | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| df-reu 2455 | ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| df-rmo 2456 | ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| df-rab 2457 | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
| cvv 2730 | class V |
| df-v 2732 | ⊢ V = {𝑥 ∣ 𝑥 = 𝑥} |
| wcdeq 2938 | wff CondEq(𝑥 = 𝑦 → 𝜑) |
| df-cdeq 2939 | ⊢ (CondEq(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑)) |
| wsbc 2955 | wff [𝐴 / 𝑥]𝜑 |
| df-sbc 2956 | ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
| csb 3049 | class ⦋𝐴 / 𝑥⦌𝐵 |
| df-csb 3050 | ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
| cdif 3118 | class (𝐴 ∖ 𝐵) |
| cun 3119 | class (𝐴 ∪ 𝐵) |
| cin 3120 | class (𝐴 ∩ 𝐵) |
| wss 3121 | wff 𝐴 ⊆ 𝐵 |
| df-dif 3123 | ⊢ (𝐴 ∖ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} |
| df-un 3125 | ⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} |
| df-in 3127 | ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
| df-ss 3134 | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) |
| c0 3414 | class ∅ |
| df-nul 3415 | ⊢ ∅ = (V ∖ V) |
| cif 3526 | class if(𝜑, 𝐴, 𝐵) |
| df-if 3527 | ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} |
| cpw 3566 | class 𝒫 𝐴 |
| df-pw 3568 | ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
| csn 3583 | class {𝐴} |
| cpr 3584 | class {𝐴, 𝐵} |
| ctp 3585 | class {𝐴, 𝐵, 𝐶} |
| cop 3586 | class ⟨𝐴, 𝐵⟩ |
| cotp 3587 | class ⟨𝐴, 𝐵, 𝐶⟩ |
| df-sn 3589 | ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
| df-pr 3590 | ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
| df-tp 3591 | ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
| df-op 3592 | ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} |
| df-ot 3593 | ⊢ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ |
| cuni 3796 | class ∪
𝐴 |
| df-uni 3797 | ⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)} |
| cint 3831 | class ∩
𝐴 |
| df-int 3832 | ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)} |
| ciun 3873 | class ∪ 𝑥 ∈ 𝐴 𝐵 |
| ciin 3874 | class ∩ 𝑥 ∈ 𝐴 𝐵 |
| df-iun 3875 | ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
| df-iin 3876 | ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
| wdisj 3966 | wff Disj 𝑥 ∈ 𝐴 𝐵 |
| df-disj 3967 | ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
| wbr 3989 | wff 𝐴𝑅𝐵 |
| df-br 3990 | ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅) |
| copab 4049 | class {⟨𝑥, 𝑦⟩ ∣ 𝜑} |
| cmpt 4050 | class (𝑥 ∈ 𝐴 ↦ 𝐵) |
| df-opab 4051 | ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} |
| df-mpt 4052 | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
| wtr 4087 | wff Tr 𝐴 |
| df-tr 4088 | ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) |
| ax-coll 4104 | ⊢ Ⅎ𝑏𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑) |
| ax-sep 4107 | ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
| ax-nul 4115 | ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 |
| ax-pow 4160 | ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) |
| wem 4180 | wff
EXMID |
| df-exmid 4181 | ⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} →
DECID ∅ ∈ 𝑥)) |
| ax-pr 4194 | ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) |
| cep 4272 | class E |
| cid 4273 | class I |
| df-eprel 4274 | ⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦} |
| df-id 4278 | ⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} |
| wpo 4279 | wff 𝑅 Po 𝐴 |
| wor 4280 | wff 𝑅 Or 𝐴 |
| df-po 4281 | ⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
| df-iso 4282 | ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))) |
| wfrfor 4312 | wff FrFor 𝑅𝐴𝑆 |
| wfr 4313 | wff 𝑅 Fr 𝐴 |
| wse 4314 | wff 𝑅 Se 𝐴 |
| wwe 4315 | wff 𝑅 We 𝐴 |
| df-frfor 4316 | ⊢ ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆)) |
| df-frind 4317 | ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠) |
| df-se 4318 | ⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) |
| df-wetr 4319 | ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
| word 4347 | wff Ord 𝐴 |
| con0 4348 | class On |
| wlim 4349 | wff Lim 𝐴 |
| csuc 4350 | class suc 𝐴 |
| df-iord 4351 | ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) |
| df-on 4353 | ⊢ On = {𝑥 ∣ Ord 𝑥} |
| df-ilim 4354 | ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) |
| df-suc 4356 | ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
| ax-un 4418 | ⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) |
| ax-setind 4521 | ⊢ (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑) |
| ax-iinf 4572 | ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) |
| com 4574 | class ω |
| df-iom 4575 | ⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} |
| cxp 4609 | class (𝐴 × 𝐵) |
| ccnv 4610 | class ◡𝐴 |
| cdm 4611 | class dom 𝐴 |
| crn 4612 | class ran 𝐴 |
| cres 4613 | class (𝐴 ↾ 𝐵) |
| cima 4614 | class (𝐴 “ 𝐵) |
| ccom 4615 | class (𝐴 ∘ 𝐵) |
| wrel 4616 | wff Rel 𝐴 |
| df-xp 4617 | ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
| df-rel 4618 | ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
| df-cnv 4619 | ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} |
| df-co 4620 | ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
| df-dm 4621 | ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} |
| df-rn 4622 | ⊢ ran 𝐴 = dom ◡𝐴 |
| df-res 4623 | ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) |
| df-ima 4624 | ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) |
| cio 5158 | class (℩𝑥𝜑) |
| df-iota 5160 | ⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} |
| wfun 5192 | wff Fun 𝐴 |
| wfn 5193 | wff 𝐴 Fn 𝐵 |
| wf 5194 | wff 𝐹:𝐴⟶𝐵 |
| wf1 5195 | wff 𝐹:𝐴–1-1→𝐵 |
| wfo 5196 | wff 𝐹:𝐴–onto→𝐵 |
| wf1o 5197 | wff 𝐹:𝐴–1-1-onto→𝐵 |
| cfv 5198 | class (𝐹‘𝐴) |
| wiso 5199 | wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) |
| df-fun 5200 | ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) |
| df-fn 5201 | ⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) |
| df-f 5202 | ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
| df-f1 5203 | ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) |
| df-fo 5204 | ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) |
| df-f1o 5205 | ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) |
| df-fv 5206 | ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥) |
| df-isom 5207 | ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) |
| crio 5808 | class (℩𝑥 ∈ 𝐴 𝜑) |
| df-riota 5809 | ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| co 5853 | class (𝐴𝐹𝐵) |
| coprab 5854 | class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} |
| cmpo 5855 | class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
| df-ov 5856 | ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩) |
| df-oprab 5857 | ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)} |
| df-mpo 5858 | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
| cof 6059 | class ∘𝑓
𝑅 |
| cofr 6060 | class ∘𝑟
𝑅 |
| df-of 6061 | ⊢ ∘𝑓
𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥)))) |
| df-ofr 6062 | ⊢ ∘𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)} |
| c1st 6117 | class 1st |
| c2nd 6118 | class 2nd |
| df-1st 6119 | ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) |
| df-2nd 6120 | ⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) |
| ctpos 6223 | class tpos 𝐹 |
| df-tpos 6224 | ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) |
| wsmo 6264 | wff Smo 𝐴 |
| df-smo 6265 | ⊢ (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
| crecs 6283 | class recs(𝐹) |
| df-recs 6284 | ⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
| crdg 6348 | class rec(𝐹, 𝐼) |
| df-irdg 6349 | ⊢ rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))) |
| cfrec 6369 | class frec(𝐹, 𝐼) |
| df-frec 6370 | ⊢ frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐼))})) ↾ ω) |
| c1o 6388 | class 1o |
| c2o 6389 | class 2o |
| c3o 6390 | class 3o |
| c4o 6391 | class 4o |
| coa 6392 | class +o |
| comu 6393 | class
·o |
| coei 6394 | class
↑o |
| df-1o 6395 | ⊢ 1o = suc
∅ |
| df-2o 6396 | ⊢ 2o = suc
1o |
| df-3o 6397 | ⊢ 3o = suc
2o |
| df-4o 6398 | ⊢ 4o = suc
3o |
| df-oadd 6399 | ⊢ +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) |
| df-omul 6400 | ⊢ ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦)) |
| df-oexpi 6401 | ⊢ ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)) |
| wer 6510 | wff 𝑅 Er 𝐴 |
| cec 6511 | class [𝐴]𝑅 |
| cqs 6512 | class (𝐴 / 𝑅) |
| df-er 6513 | ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) |
| df-ec 6515 | ⊢ [𝐴]𝑅 = (𝑅 “ {𝐴}) |
| df-qs 6519 | ⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
| cmap 6626 | class
↑𝑚 |
| cpm 6627 | class
↑pm |
| df-map 6628 | ⊢ ↑𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) |
| df-pm 6629 | ⊢ ↑pm =
(𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓}) |
| cixp 6676 | class X𝑥 ∈ 𝐴 𝐵 |
| df-ixp 6677 | ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} |
| cen 6716 | class ≈ |
| cdom 6717 | class ≼ |
| cfn 6718 | class Fin |
| df-en 6719 | ⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} |
| df-dom 6720 | ⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} |
| df-fin 6721 | ⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦} |
| cfi 6945 | class fi |
| df-fi 6946 | ⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦}) |
| csup 6959 | class sup(𝐴, 𝐵, 𝑅) |
| cinf 6960 | class inf(𝐴, 𝐵, 𝑅) |
| df-sup 6961 | ⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} |
| df-inf 6962 | ⊢ inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅) |
| cdju 7014 | class (𝐴 ⊔ 𝐵) |
| df-dju 7015 | ⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
| cinl 7022 | class inl |
| cinr 7023 | class inr |
| df-inl 7024 | ⊢ inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩) |
| df-inr 7025 | ⊢ inr = (𝑥 ∈ V ↦ ⟨1o, 𝑥⟩) |
| cdjucase 7060 | class case(𝑅, 𝑆) |
| df-case 7061 | ⊢ case(𝑅, 𝑆) = ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr)) |
| cdjud 7079 | class (𝑅 ⊔d 𝑆) |
| df-djud 7080 | ⊢ (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆))) |
| xnninf 7096 | class ℕ∞ |
| df-nninf 7097 | ⊢ ℕ∞ = {𝑓 ∈ (2o
↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)} |
| comni 7110 | class Omni |
| df-omni 7111 | ⊢ Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))} |
| cmarkov 7127 | class Markov |
| df-markov 7128 | ⊢ Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬
∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅))} |
| cwomni 7139 | class WOmni |
| df-womni 7140 | ⊢ WOmni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o →
DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)} |
| ccrd 7156 | class card |
| df-card 7157 | ⊢ card = (𝑥 ∈ V ↦ ∩ {𝑦
∈ On ∣ 𝑦 ≈
𝑥}) |
| wac 7182 | wff
CHOICE |
| df-ac 7183 | ⊢ (CHOICE ↔
∀𝑥∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥)) |
| wacc 7224 | wff
CCHOICE |
| df-cc 7225 | ⊢ (CCHOICE ↔
∀𝑥(dom 𝑥 ≈ ω →
∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥))) |
| cnpi 7234 | class N |
| cpli 7235 | class
+N |
| cmi 7236 | class
·N |
| clti 7237 | class
<N |
| cplpq 7238 | class
+pQ |
| cmpq 7239 | class
·pQ |
| cltpq 7240 | class
<pQ |
| ceq 7241 | class
~Q |
| cnq 7242 | class Q |
| c1q 7243 | class
1Q |
| cplq 7244 | class
+Q |
| cmq 7245 | class
·Q |
| crq 7246 | class
*Q |
| cltq 7247 | class
<Q |
| ceq0 7248 | class
~Q0 |
| cnq0 7249 | class
Q0 |
| c0q0 7250 | class
0Q0 |
| cplq0 7251 | class
+Q0 |
| cmq0 7252 | class
·Q0 |
| cnp 7253 | class P |
| c1p 7254 | class
1P |
| cpp 7255 | class
+P |
| cmp 7256 | class
·P |
| cltp 7257 | class
<P |
| cer 7258 | class
~R |
| cnr 7259 | class R |
| c0r 7260 | class
0R |
| c1r 7261 | class
1R |
| cm1r 7262 | class
-1R |
| cplr 7263 | class
+R |
| cmr 7264 | class
·R |
| cltr 7265 | class
<R |
| df-ni 7266 | ⊢ N = (ω
∖ {∅}) |
| df-pli 7267 | ⊢ +N = (
+o ↾ (N ×
N)) |
| df-mi 7268 | ⊢
·N = ( ·o ↾
(N × N)) |
| df-lti 7269 | ⊢ <N = ( E ∩
(N × N)) |
| df-plpq 7306 | ⊢ +pQ = (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ ⟨(((1st
‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))⟩) |
| df-mpq 7307 | ⊢ ·pQ = (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ ⟨((1st
‘𝑥)
·N (1st ‘𝑦)), ((2nd ‘𝑥)
·N (2nd ‘𝑦))⟩) |
| df-ltpq 7308 | ⊢ <pQ =
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((1st
‘𝑥)
·N (2nd ‘𝑦)) <N
((1st ‘𝑦)
·N (2nd ‘𝑥)))} |
| df-enq 7309 | ⊢ ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))} |
| df-nqqs 7310 | ⊢ Q = ((N ×
N) / ~Q ) |
| df-plqqs 7311 | ⊢ +Q =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
))} |
| df-mqqs 7312 | ⊢ ·Q =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ
⟨𝑢, 𝑓⟩)] ~Q
))} |
| df-1nqqs 7313 | ⊢ 1Q =
[⟨1o, 1o⟩]
~Q |
| df-rq 7314 | ⊢ *Q =
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ (𝑥
·Q 𝑦) =
1Q)} |
| df-ltnqqs 7315 | ⊢ <Q =
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧
𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧
(𝑧
·N 𝑢) <N (𝑤
·N 𝑣)))} |
| df-enq0 7386 | ⊢ ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))} |
| df-nq0 7387 | ⊢ Q0 = ((ω
× N) / ~Q0
) |
| df-0nq0 7388 | ⊢ 0Q0 =
[⟨∅, 1o⟩]
~Q0 |
| df-plq0 7389 | ⊢ +Q0 =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧
𝑦 ∈
Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧
𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0
))} |
| df-mq0 7390 | ⊢ ·Q0 =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧
𝑦 ∈
Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧
𝑧 = [⟨(𝑤 ·o 𝑢), (𝑣 ·o 𝑓)⟩] ~Q0
))} |
| df-inp 7428 | ⊢ P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙 ⊆ Q ∧ 𝑢 ⊆ Q) ∧
(∃𝑞 ∈
Q 𝑞 ∈
𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q
𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))))} |
| df-i1p 7429 | ⊢ 1P = ⟨{𝑙 ∣ 𝑙 <Q
1Q}, {𝑢 ∣ 1Q
<Q 𝑢}⟩ |
| df-iplp 7430 | ⊢ +P = (𝑥 ∈ P, 𝑦 ∈ P ↦
⟨{𝑞 ∈
Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st
‘𝑥) ∧ 𝑠 ∈ (1st
‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q
∃𝑠 ∈
Q (𝑟 ∈
(2nd ‘𝑥)
∧ 𝑠 ∈
(2nd ‘𝑦)
∧ 𝑞 = (𝑟 +Q
𝑠))}⟩) |
| df-imp 7431 | ⊢ ·P = (𝑥 ∈ P, 𝑦 ∈ P ↦
⟨{𝑞 ∈
Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st
‘𝑥) ∧ 𝑠 ∈ (1st
‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q
∃𝑠 ∈
Q (𝑟 ∈
(2nd ‘𝑥)
∧ 𝑠 ∈
(2nd ‘𝑦)
∧ 𝑞 = (𝑟
·Q 𝑠))}⟩) |
| df-iltp 7432 | ⊢ <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧
∃𝑞 ∈
Q (𝑞 ∈
(2nd ‘𝑥)
∧ 𝑞 ∈
(1st ‘𝑦)))} |
| df-enr 7688 | ⊢ ~R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (P ×
P) ∧ 𝑦
∈ (P × P)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 +P 𝑢) = (𝑤 +P 𝑣)))} |
| df-nr 7689 | ⊢ R =
((P × P) / ~R
) |
| df-plr 7690 | ⊢ +R =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧
𝑧 = [⟨(𝑤 +P
𝑢), (𝑣 +P 𝑓)⟩]
~R ))} |
| df-mr 7691 | ⊢
·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧
𝑧 = [⟨((𝑤
·P 𝑢) +P (𝑣
·P 𝑓)), ((𝑤 ·P 𝑓) +P
(𝑣
·P 𝑢))⟩] ~R
))} |
| df-ltr 7692 | ⊢ <R =
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R ∧
𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)))} |
| df-0r 7693 | ⊢ 0R =
[⟨1P, 1P⟩]
~R |
| df-1r 7694 | ⊢ 1R =
[⟨(1P +P
1P), 1P⟩]
~R |
| df-m1r 7695 | ⊢ -1R =
[⟨1P, (1P
+P 1P)⟩]
~R |
| cc 7772 | class ℂ |
| cr 7773 | class ℝ |
| cc0 7774 | class 0 |
| c1 7775 | class 1 |
| ci 7776 | class i |
| caddc 7777 | class + |
| cltrr 7778 | class
<ℝ |
| cmul 7779 | class · |
| df-c 7780 | ⊢ ℂ = (R
× R) |
| df-0 7781 | ⊢ 0 =
⟨0R,
0R⟩ |
| df-1 7782 | ⊢ 1 =
⟨1R,
0R⟩ |
| df-i 7783 | ⊢ i =
⟨0R,
1R⟩ |
| df-r 7784 | ⊢ ℝ = (R
× {0R}) |
| df-add 7785 | ⊢ + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))} |
| df-mul 7786 | ⊢ · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R
(-1R ·R (𝑣
·R 𝑓))), ((𝑣 ·R 𝑢) +R
(𝑤
·R 𝑓))⟩))} |
| df-lt 7787 | ⊢ <ℝ =
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧
∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤))} |
| ax-cnex 7865 | ⊢ ℂ ∈ V |
| ax-resscn 7866 | ⊢ ℝ ⊆ ℂ |
| ax-1cn 7867 | ⊢ 1 ∈ ℂ |
| ax-1re 7868 | ⊢ 1 ∈ ℝ |
| ax-icn 7869 | ⊢ i ∈ ℂ |
| ax-addcl 7870 | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
| ax-addrcl 7871 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) |
| ax-mulcl 7872 | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) |
| ax-mulrcl 7873 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
| ax-addcom 7874 | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
| ax-mulcom 7875 | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
| ax-addass 7876 | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
| ax-mulass 7877 | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
| ax-distr 7878 | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
| ax-i2m1 7879 | ⊢ ((i · i) + 1) = 0 |
| ax-0lt1 7880 | ⊢ 0 <ℝ 1 |
| ax-1rid 7881 | ⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) |
| ax-0id 7882 | ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) |
| ax-rnegex 7883 | ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) |
| ax-precex 7884 | ⊢ ((𝐴 ∈ ℝ ∧ 0
<ℝ 𝐴)
→ ∃𝑥 ∈
ℝ (0 <ℝ 𝑥 ∧ (𝐴 · 𝑥) = 1)) |
| ax-cnre 7885 | ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) |
| ax-pre-ltirr 7886 | ⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴) |
| ax-pre-ltwlin 7887 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵))) |
| ax-pre-lttrn 7888 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) |
| ax-pre-apti 7889 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵) |
| ax-pre-ltadd 7890 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) |
| ax-pre-mulgt0 7891 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0
<ℝ 𝐴
∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵))) |
| ax-pre-mulext 7892 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴))) |
| ax-arch 7893 | ⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥
∣ (1 ∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛) |
| ax-caucvg 7894 | ⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
& ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ
𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))) |
| ax-pre-suploc 7895 | ⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
| ax-addf 7896 | ⊢ + :(ℂ ×
ℂ)⟶ℂ |
| ax-mulf 7897 | ⊢ · :(ℂ ×
ℂ)⟶ℂ |
| cpnf 7951 | class +∞ |
| cmnf 7952 | class -∞ |
| cxr 7953 | class
ℝ* |
| clt 7954 | class < |
| cle 7955 | class ≤ |
| df-pnf 7956 | ⊢ +∞ = 𝒫 ∪ ℂ |
| df-mnf 7957 | ⊢ -∞ = 𝒫
+∞ |
| df-xr 7958 | ⊢ ℝ* = (ℝ
∪ {+∞, -∞}) |
| df-ltxr 7959 | ⊢ < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))) |
| df-le 7960 | ⊢ ≤ = ((ℝ*
× ℝ*) ∖ ◡
< ) |
| cmin 8090 | class − |
| cneg 8091 | class -𝐴 |
| df-sub 8092 | ⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
| df-neg 8093 | ⊢ -𝐴 = (0 − 𝐴) |
| creap 8493 | class
#ℝ |
| df-reap 8494 | ⊢ #ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))} |
| cap 8500 | class # |
| df-ap 8501 | ⊢ # = {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢))} |
| cdiv 8589 | class / |
| df-div 8590 | ⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦
(℩𝑧 ∈
ℂ (𝑦 · 𝑧) = 𝑥)) |
| cn 8878 | class ℕ |
| df-inn 8879 | ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} |
| c2 8929 | class 2 |
| c3 8930 | class 3 |
| c4 8931 | class 4 |
| c5 8932 | class 5 |
| c6 8933 | class 6 |
| c7 8934 | class 7 |
| c8 8935 | class 8 |
| c9 8936 | class 9 |
| df-2 8937 | ⊢ 2 = (1 + 1) |
| df-3 8938 | ⊢ 3 = (2 + 1) |
| df-4 8939 | ⊢ 4 = (3 + 1) |
| df-5 8940 | ⊢ 5 = (4 + 1) |
| df-6 8941 | ⊢ 6 = (5 + 1) |
| df-7 8942 | ⊢ 7 = (6 + 1) |
| df-8 8943 | ⊢ 8 = (7 + 1) |
| df-9 8944 | ⊢ 9 = (8 + 1) |
| cn0 9135 | class
ℕ0 |
| df-n0 9136 | ⊢ ℕ0 = (ℕ
∪ {0}) |
| cxnn0 9198 | class
ℕ0* |
| df-xnn0 9199 | ⊢ ℕ0* =
(ℕ0 ∪ {+∞}) |
| cz 9212 | class ℤ |
| df-z 9213 | ⊢ ℤ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ -𝑛 ∈ ℕ)} |
| cdc 9343 | class ;𝐴𝐵 |
| df-dec 9344 | ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵) |
| cuz 9487 | class
ℤ≥ |
| df-uz 9488 | ⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) |
| cq 9578 | class ℚ |
| df-q 9579 | ⊢ ℚ = ( / “ (ℤ
× ℕ)) |
| crp 9610 | class
ℝ+ |
| df-rp 9611 | ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 <
𝑥} |
| cxne 9726 | class -𝑒𝐴 |
| cxad 9727 | class
+𝑒 |
| cxmu 9728 | class
·e |
| df-xneg 9729 | ⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) |
| df-xadd 9730 | ⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ if(𝑥 = +∞,
if(𝑦 = -∞, 0,
+∞), if(𝑥 = -∞,
if(𝑦 = +∞, 0,
-∞), if(𝑦 = +∞,
+∞, if(𝑦 = -∞,
-∞, (𝑥 + 𝑦)))))) |
| df-xmul 9731 | ⊢ ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ if((𝑥 = 0 ∨
𝑦 = 0), 0, if((((0 <
𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))))) |
| cioo 9845 | class (,) |
| cioc 9846 | class (,] |
| cico 9847 | class [,) |
| cicc 9848 | class [,] |
| df-ioo 9849 | ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
| df-ioc 9850 | ⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
| df-ico 9851 | ⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| df-icc 9852 | ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
| cfz 9965 | class ... |
| df-fz 9966 | ⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)}) |
| cfzo 10098 | class ..^ |
| df-fzo 10099 | ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1))) |
| cfl 10224 | class ⌊ |
| cceil 10225 | class ⌈ |
| df-fl 10226 | ⊢ ⌊ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1)))) |
| df-ceil 10227 | ⊢ ⌈ = (𝑥 ∈ ℝ ↦
-(⌊‘-𝑥)) |
| cmo 10278 | class mod |
| df-mod 10279 | ⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))) |
| cseq 10401 | class seq𝑀( + , 𝐹) |
| df-seqfrec 10402 | ⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) |
| cexp 10475 | class ↑ |
| df-exp 10476 | ⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ ×
{𝑥}))‘-𝑦))))) |
| cfa 10659 | class ! |
| df-fac 10660 | ⊢ ! = ({⟨0, 1⟩} ∪ seq1( ·
, I )) |
| cbc 10681 | class C |
| df-bc 10682 | ⊢ C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
| chash 10709 | class ♯ |
| df-ihash 10710 | ⊢ ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω,
+∞⟩}) ∘ (𝑥
∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝑥})) |
| cshi 10778 | class shift |
| df-shft 10779 | ⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) |
| ccj 10803 | class ∗ |
| cre 10804 | class ℜ |
| cim 10805 | class ℑ |
| df-cj 10806 | ⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ))) |
| df-re 10807 | ⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2)) |
| df-im 10808 | ⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i))) |
| csqrt 10960 | class √ |
| cabs 10961 | class abs |
| df-rsqrt 10962 | ⊢ √ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦))) |
| df-abs 10963 | ⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥)))) |
| cli 11241 | class ⇝ |
| df-clim 11242 | ⊢ ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))} |
| csu 11316 | class Σ𝑘 ∈ 𝐴 𝐵 |
| df-sumdc 11317 | ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈
(ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) |
| cprod 11513 | class ∏𝑘 ∈ 𝐴 𝐵 |
| df-proddc 11514 | ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈
(ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) |
| ce 11605 | class exp |
| ceu 11606 | class e |
| csin 11607 | class sin |
| ccos 11608 | class cos |
| ctan 11609 | class tan |
| cpi 11610 | class π |
| df-ef 11611 | ⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0
((𝑥↑𝑘) / (!‘𝑘))) |
| df-e 11612 | ⊢ e =
(exp‘1) |
| df-sin 11613 | ⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i
· 𝑥)) −
(exp‘(-i · 𝑥))) / (2 · i))) |
| df-cos 11614 | ⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i
· 𝑥)) +
(exp‘(-i · 𝑥))) / 2)) |
| df-tan 11615 | ⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) /
(cos‘𝑥))) |
| df-pi 11616 | ⊢ π = inf((ℝ+
∩ (◡sin “ {0})), ℝ,
< ) |
| ctau 11737 | class τ |
| df-tau 11738 | ⊢ τ = inf((ℝ+ ∩
(◡cos “ {1})), ℝ, <
) |
| cdvds 11749 | class ∥ |
| df-dvds 11750 | ⊢ ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)} |
| cgcd 11897 | class gcd |
| df-gcd 11898 | ⊢ gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦)}, ℝ, < ))) |
| clcm 12014 | class lcm |
| df-lcm 12015 | ⊢ lcm = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛)}, ℝ, < ))) |
| cprime 12061 | class ℙ |
| df-prm 12062 | ⊢ ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2o} |
| cnumer 12135 | class numer |
| cdenom 12136 | class denom |
| df-numer 12137 | ⊢ numer = (𝑦 ∈ ℚ ↦ (1st
‘(℩𝑥
∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥)))))) |
| df-denom 12138 | ⊢ denom = (𝑦 ∈ ℚ ↦ (2nd
‘(℩𝑥
∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥)))))) |
| codz 12162 | class
odℤ |
| cphi 12163 | class ϕ |
| df-odz 12164 | ⊢ odℤ = (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, <
))) |
| df-phi 12165 | ⊢ ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1})) |
| cpc 12238 | class pCnt |
| df-pc 12239 | ⊢ pCnt = (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < )))))) |
| cgz 12321 | class ℤ[i] |
| df-gz 12322 | ⊢ ℤ[i] = {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧
(ℑ‘𝑥) ∈
ℤ)} |
| cstr 12412 | class Struct |
| cnx 12413 | class ndx |
| csts 12414 | class sSet |
| cslot 12415 | class Slot 𝐴 |
| cbs 12416 | class Base |
| cress 12417 | class
↾s |
| df-struct 12418 | ⊢ Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝑓
∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))} |
| df-ndx 12419 | ⊢ ndx = ( I ↾ ℕ) |
| df-slot 12420 | ⊢ Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴)) |
| df-base 12422 | ⊢ Base = Slot 1 |
| df-sets 12423 | ⊢ sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒})) |
| df-ress 12424 | ⊢ ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))) |
| cplusg 12480 | class +g |
| cmulr 12481 | class .r |
| cstv 12482 | class
*𝑟 |
| csca 12483 | class Scalar |
| cvsca 12484 | class
·𝑠 |
| cip 12485 | class
·𝑖 |
| cts 12486 | class TopSet |
| cple 12487 | class le |
| coc 12488 | class oc |
| cds 12489 | class dist |
| cunif 12490 | class UnifSet |
| chom 12491 | class Hom |
| cco 12492 | class comp |
| df-plusg 12493 | ⊢ +g = Slot 2 |
| df-mulr 12494 | ⊢ .r = Slot 3 |
| df-starv 12495 | ⊢ *𝑟 = Slot
4 |
| df-sca 12496 | ⊢ Scalar = Slot 5 |
| df-vsca 12497 | ⊢ ·𝑠 = Slot
6 |
| df-ip 12498 | ⊢
·𝑖 = Slot 8 |
| df-tset 12499 | ⊢ TopSet = Slot 9 |
| df-ple 12500 | ⊢ le = Slot ;10 |
| df-ocomp 12501 | ⊢ oc = Slot ;11 |
| df-ds 12502 | ⊢ dist = Slot ;12 |
| df-unif 12503 | ⊢ UnifSet = Slot ;13 |
| df-hom 12504 | ⊢ Hom = Slot ;14 |
| df-cco 12505 | ⊢ comp = Slot ;15 |
| crest 12579 | class
↾t |
| ctopn 12580 | class TopOpen |
| df-rest 12581 | ⊢ ↾t = (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥))) |
| df-topn 12582 | ⊢ TopOpen = (𝑤 ∈ V ↦ ((TopSet‘𝑤) ↾t
(Base‘𝑤))) |
| ctg 12594 | class topGen |
| cpt 12595 | class
∏t |
| c0g 12596 | class 0g |
| cgsu 12597 | class
Σg |
| df-0g 12598 | ⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) |
| df-gsum 12599 | ⊢ Σ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 12600 | ⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)}) |
| df-pt 12601 | ⊢ ∏t = (𝑓 ∈ V ↦
(topGen‘{𝑥 ∣
∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))})) |
| cprds 12602 | class Xs |
| cpws 12603 | class
↑s |
| df-prds 12604 | ⊢ Xs = (𝑠 ∈ 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 12606 | ⊢ ↑s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟}))) |
| cplusf 12607 | class
+𝑓 |
| cmgm 12608 | class Mgm |
| df-plusf 12609 | ⊢ +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)𝑦))) |
| df-mgm 12610 | ⊢ Mgm = {𝑔 ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏} |
| csgrp 12642 | class Smgrp |
| df-sgrp 12643 | ⊢ Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))} |
| cmnd 12652 | class Mnd |
| df-mnd 12653 | ⊢ Mnd = {𝑔 ∈ Smgrp ∣
[(Base‘𝑔) /
𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)} |
| cmhm 12681 | class MndHom |
| csubmnd 12682 | class SubMnd |
| df-mhm 12683 | ⊢ MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚
(Base‘𝑠)) ∣
(∀𝑥 ∈
(Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))}) |
| df-submnd 12684 | ⊢ SubMnd = (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣
((0g‘𝑠)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡)}) |
| cgrp 12708 | class Grp |
| cminusg 12709 | class invg |
| csg 12710 | class -g |
| df-grp 12711 | ⊢ Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)} |
| df-minusg 12712 | ⊢ invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)))) |
| df-sbg 12713 | ⊢ -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)))) |
| cpsmet 12773 | class PsMet |
| cxmet 12774 | class ∞Met |
| cmet 12775 | class Met |
| cbl 12776 | class ball |
| cfbas 12777 | class fBas |
| cfg 12778 | class filGen |
| cmopn 12779 | class MetOpen |
| cmetu 12780 | class metUnif |
| df-psmet 12781 | ⊢ PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*
↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) |
| df-xmet 12782 | ⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*
↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) |
| df-met 12783 | ⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚
(𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) |
| df-bl 12784 | ⊢ ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧})) |
| df-mopn 12785 | ⊢ MetOpen = (𝑑 ∈ ∪ ran
∞Met ↦ (topGen‘ran (ball‘𝑑))) |
| df-fbas 12786 | ⊢ fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)}) |
| df-fg 12787 | ⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅}) |
| df-metu 12788 | ⊢ metUnif = (𝑑 ∈ ∪ ran
PsMet ↦ ((dom dom 𝑑
× dom dom 𝑑)filGenran
(𝑎 ∈
ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))) |
| ctop 12789 | class Top |
| df-top 12790 | ⊢ Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
| ctopon 12802 | class TopOn |
| df-topon 12803 | ⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗}) |
| ctps 12822 | class TopSp |
| df-topsp 12823 | ⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} |
| ctb 12834 | class TopBases |
| df-bases 12835 | ⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))} |
| ccld 12886 | class Clsd |
| cnt 12887 | class int |
| ccl 12888 | class cls |
| df-cld 12889 | ⊢ Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗
∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗}) |
| df-ntr 12890 | ⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∪ (𝑗 ∩ 𝒫 𝑥))) |
| df-cls 12891 | ⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) |
| cnei 12932 | class nei |
| df-nei 12933 | ⊢ nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ {𝑦 ∈ 𝒫
∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)})) |
| ccn 12979 | class Cn |
| ccnp 12980 | class CnP |
| clm 12981 | class
⇝𝑡 |
| df-cn 12982 | ⊢ Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗}) |
| df-cnp 12983 | ⊢ CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))})) |
| df-lm 12984 | ⊢ ⇝𝑡 =
(𝑗 ∈ Top ↦
{⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗
↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) |
| ctx 13046 | class
×t |
| df-tx 13047 | ⊢ ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))) |
| chmeo 13094 | class Homeo |
| df-hmeo 13095 | ⊢ Homeo = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ ◡𝑓 ∈ (𝑘 Cn 𝑗)}) |
| cxms 13130 | class ∞MetSp |
| cms 13131 | class MetSp |
| ctms 13132 | class toMetSp |
| df-xms 13133 | ⊢ ∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpen‘𝑓) =
(MetOpen‘((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))))} |
| df-ms 13134 | ⊢ MetSp = {𝑓 ∈ ∞MetSp ∣
((dist‘𝑓) ↾
((Base‘𝑓) ×
(Base‘𝑓))) ∈
(Met‘(Base‘𝑓))} |
| df-tms 13135 | ⊢ toMetSp = (𝑑 ∈ ∪ ran
∞Met ↦ ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet
⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩)) |
| ccncf 13351 | class –cn→ |
| df-cncf 13352 | ⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑𝑚 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)}) |
| climc 13417 | class
limℂ |
| cdv 13418 | class D |
| df-limced 13419 | ⊢ limℂ = (𝑓 ∈ (ℂ ↑pm
ℂ), 𝑥 ∈ ℂ
↦ {𝑦 ∈ ℂ
∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)))}) |
| df-dvap 13420 | ⊢ D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm
𝑠) ↦ ∪ 𝑥 ∈ ((int‘((MetOpen‘(abs
∘ − )) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) |
| clog 13571 | class log |
| ccxp 13572 | class
↑𝑐 |
| df-relog 13573 | ⊢ log = ◡(exp ↾ ℝ) |
| df-rpcxp 13574 | ⊢ ↑𝑐 = (𝑥 ∈ ℝ+,
𝑦 ∈ ℂ ↦
(exp‘(𝑦 ·
(log‘𝑥)))) |
| clogb 13655 | class
logb |
| df-logb 13656 | ⊢ logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0})
↦ ((log‘𝑦) /
(log‘𝑥))) |
| clgs 13692 | class
/L |
| df-lgs 13693 | ⊢ /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 13828 | wff 𝐴 DECIDin
𝐵 |
| df-dcin 13829 | ⊢ (𝐴 DECIDin
𝐵 ↔ ∀𝑥 ∈ 𝐵 DECID 𝑥 ∈ 𝐴) |
| wbd 13847 | wff BOUNDED 𝜑 |
| ax-bd0 13848 | ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (BOUNDED 𝜑 → BOUNDED
𝜓) |
| ax-bdim 13849 | ⊢ BOUNDED 𝜑
& ⊢ BOUNDED 𝜓 ⇒ ⊢ BOUNDED (𝜑 → 𝜓) |
| ax-bdan 13850 | ⊢ BOUNDED 𝜑
& ⊢ BOUNDED 𝜓 ⇒ ⊢ BOUNDED (𝜑 ∧ 𝜓) |
| ax-bdor 13851 | ⊢ BOUNDED 𝜑
& ⊢ BOUNDED 𝜓 ⇒ ⊢ BOUNDED (𝜑 ∨ 𝜓) |
| ax-bdn 13852 | ⊢ BOUNDED 𝜑 ⇒ ⊢ BOUNDED ¬
𝜑 |
| ax-bdal 13853 | ⊢ BOUNDED 𝜑 ⇒ ⊢ BOUNDED
∀𝑥 ∈ 𝑦 𝜑 |
| ax-bdex 13854 | ⊢ BOUNDED 𝜑 ⇒ ⊢ BOUNDED
∃𝑥 ∈ 𝑦 𝜑 |
| ax-bdeq 13855 | ⊢ BOUNDED 𝑥 = 𝑦 |
| ax-bdel 13856 | ⊢ BOUNDED 𝑥 ∈ 𝑦 |
| ax-bdsb 13857 | ⊢ BOUNDED 𝜑 ⇒ ⊢ BOUNDED [𝑦 / 𝑥]𝜑 |
| wbdc 13875 | wff BOUNDED
𝐴 |
| df-bdc 13876 | ⊢ (BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥 ∈ 𝐴) |
| ax-bdsep 13919 | ⊢ BOUNDED 𝜑 ⇒ ⊢ ∀𝑎∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) |
| ax-bj-d0cl 13959 | ⊢ BOUNDED 𝜑 ⇒ ⊢ DECID 𝜑 |
| wind 13961 | wff Ind 𝐴 |
| df-bj-ind 13962 | ⊢ (Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) |
| ax-infvn 13976 | ⊢ ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦)) |
| ax-bdsetind 14003 | ⊢ BOUNDED 𝜑 ⇒ ⊢ (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑) |
| ax-inf2 14011 | ⊢ ∃𝑎∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦)) |
| ax-strcoll 14017 | ⊢ ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)) |
| ax-sscoll 14022 | ⊢ ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑)) |
| ax-ddkcomp 14024 | ⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵))) |
| walsi 14105 | wff ∀!𝑥(𝜑 → 𝜓) |
| walsc 14106 | wff ∀!𝑥 ∈ 𝐴𝜑 |
| df-alsi 14107 | ⊢ (∀!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑)) |
| df-alsc 14108 | ⊢ (∀!𝑥 ∈ 𝐴𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴)) |
