mmdefinitions - Intuitionistic Logic Explorer

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 104	wff (𝜑 ∧ 𝜓)
wb 105	wff (𝜑 ↔ 𝜓)
ax-ia1 106	⊢ ((𝜑 ∧ 𝜓) → 𝜑)
ax-ia2 107	⊢ ((𝜑 ∧ 𝜓) → 𝜓)
ax-ia3 108	⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
df-bi 117	⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
ax-in1 614	⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)
ax-in2 615	⊢ (¬ 𝜑 → (𝜑 → 𝜓))
wo 708	wff (𝜑 ∨ 𝜓)
ax-io 709	⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓)))
wstab 830	wff STAB 𝜑
df-stab 831	⊢ (STAB 𝜑 ↔ (¬ ¬ 𝜑 → 𝜑))
wdc 834	wff DECID 𝜑
df-dc 835	⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
w3o 977	wff (𝜑 ∨ 𝜓 ∨ 𝜒)
w3a 978	wff (𝜑 ∧ 𝜓 ∧ 𝜒)
df-3or 979	⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
df-3an 980	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
wal 1351	wff ∀𝑥𝜑
cv 1352	class 𝑥
wceq 1353	wff 𝐴 = 𝐵
wtru 1354	wff ⊤
df-tru 1356	⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
wfal 1358	wff ⊥
df-fal 1359	⊢ (⊥ ↔ ¬ ⊤)
wxo 1375	wff (𝜑 ⊻ 𝜓)
df-xor 1376	⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)))
ax-5 1447	⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
ax-7 1448	⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
ax-gen 1449	⊢ 𝜑    ⇒   ⊢ ∀𝑥𝜑
wnf 1460	wff Ⅎ𝑥𝜑
df-nf 1461	⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
wex 1492	wff ∃𝑥𝜑
ax-ie1 1493	⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
ax-ie2 1494	⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
ax-8 1504	⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
ax-10 1505	⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
ax-11 1506	⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
ax-i12 1507	⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
ax-bndl 1509	⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
ax-4 1510	⊢ (∀𝑥𝜑 → 𝜑)
ax-17 1526	⊢ (𝜑 → ∀𝑥𝜑)
ax-i9 1530	⊢ ∃𝑥 𝑥 = 𝑦
ax-ial 1534	⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
ax-i5r 1535	⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑 → 𝜓))
ax-10o 1716	⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
wsb 1762	wff [𝑦 / 𝑥]𝜑
df-sb 1763	⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
ax-16 1814	⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
ax-11o 1823	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
weu 2026	wff ∃!𝑥𝜑
wmo 2027	wff ∃*𝑥𝜑
df-eu 2029	⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
df-mo 2030	⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
wcel 2148	wff 𝐴 ∈ 𝐵
ax-13 2150	⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
ax-14 2151	⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
ax-ext 2159	⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
cab 2163	class {𝑥 ∣ 𝜑}
df-clab 2164	⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
df-cleq 2170	⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
df-clel 2173	⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
wnfc 2306	wff Ⅎ𝑥𝐴
df-nfc 2308	⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
wne 2347	wff 𝐴 ≠ 𝐵
df-ne 2348	⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
wnel 2442	wff 𝐴 ∉ 𝐵
df-nel 2443	⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
wral 2455	wff ∀𝑥 ∈ 𝐴 𝜑
wrex 2456	wff ∃𝑥 ∈ 𝐴 𝜑
wreu 2457	wff ∃!𝑥 ∈ 𝐴 𝜑
wrmo 2458	wff ∃*𝑥 ∈ 𝐴 𝜑
crab 2459	class {𝑥 ∈ 𝐴 ∣ 𝜑}
df-ral 2460	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
df-rex 2461	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
df-reu 2462	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
df-rmo 2463	⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
df-rab 2464	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
cvv 2739	class V
df-v 2741	⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
wcdeq 2947	wff CondEq(𝑥 = 𝑦 → 𝜑)
df-cdeq 2948	⊢ (CondEq(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑))
wsbc 2964	wff [𝐴 / 𝑥]𝜑
df-sbc 2965	⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
csb 3059	class ⦋𝐴 / 𝑥⦌𝐵
df-csb 3060	⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
cdif 3128	class (𝐴 ∖ 𝐵)
cun 3129	class (𝐴 ∪ 𝐵)
cin 3130	class (𝐴 ∩ 𝐵)
wss 3131	wff 𝐴 ⊆ 𝐵
df-dif 3133	⊢ (𝐴 ∖ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)}
df-un 3135	⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
df-in 3137	⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
df-ss 3144	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
c0 3424	class ∅
df-nul 3425	⊢ ∅ = (V ∖ V)
cif 3536	class if(𝜑, 𝐴, 𝐵)
df-if 3537	⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
cpw 3577	class 𝒫 𝐴
df-pw 3579	⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}
csn 3594	class {𝐴}
cpr 3595	class {𝐴, 𝐵}
ctp 3596	class {𝐴, 𝐵, 𝐶}
cop 3597	class ⟨𝐴, 𝐵⟩
cotp 3598	class ⟨𝐴, 𝐵, 𝐶⟩
df-sn 3600	⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
df-pr 3601	⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
df-tp 3602	⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
df-op 3603	⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
df-ot 3604	⊢ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩
cuni 3811	class ∪ 𝐴
df-uni 3812	⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)}
cint 3846	class ∩ 𝐴
df-int 3847	⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)}
ciun 3888	class ∪ 𝑥 ∈ 𝐴 𝐵
ciin 3889	class ∩ 𝑥 ∈ 𝐴 𝐵
df-iun 3890	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
df-iin 3891	⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
wdisj 3982	wff Disj 𝑥 ∈ 𝐴 𝐵
df-disj 3983	⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
wbr 4005	wff 𝐴𝑅𝐵
df-br 4006	⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
copab 4065	class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
cmpt 4066	class (𝑥 ∈ 𝐴 ↦ 𝐵)
df-opab 4067	⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
df-mpt 4068	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
wtr 4103	wff Tr 𝐴
df-tr 4104	⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
ax-coll 4120	⊢ Ⅎ𝑏𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)
ax-sep 4123	⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
ax-nul 4131	⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
ax-pow 4176	⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
wem 4196	wff EXMID
df-exmid 4197	⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥))
ax-pr 4211	⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
cep 4289	class E
cid 4290	class I
df-eprel 4291	⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
df-id 4295	⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
wpo 4296	wff 𝑅 Po 𝐴
wor 4297	wff 𝑅 Or 𝐴
df-po 4298	⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
df-iso 4299	⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))))
wfrfor 4329	wff FrFor 𝑅𝐴𝑆
wfr 4330	wff 𝑅 Fr 𝐴
wse 4331	wff 𝑅 Se 𝐴
wwe 4332	wff 𝑅 We 𝐴
df-frfor 4333	⊢ ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆))
df-frind 4334	⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)
df-se 4335	⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V)
df-wetr 4336	⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
word 4364	wff Ord 𝐴
con0 4365	class On
wlim 4366	wff Lim 𝐴
csuc 4367	class suc 𝐴
df-iord 4368	⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))
df-on 4370	⊢ On = {𝑥 ∣ Ord 𝑥}
df-ilim 4371	⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))
df-suc 4373	⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
ax-un 4435	⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
ax-setind 4538	⊢ (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑)
ax-iinf 4589	⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
com 4591	class ω
df-iom 4592	⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
cxp 4626	class (𝐴 × 𝐵)
ccnv 4627	class ◡𝐴
cdm 4628	class dom 𝐴
crn 4629	class ran 𝐴
cres 4630	class (𝐴 ↾ 𝐵)
cima 4631	class (𝐴 “ 𝐵)
ccom 4632	class (𝐴 ∘ 𝐵)
wrel 4633	wff Rel 𝐴
df-xp 4634	⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
df-rel 4635	⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
df-cnv 4636	⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
df-co 4637	⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
df-dm 4638	⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
df-rn 4639	⊢ ran 𝐴 = dom ◡𝐴
df-res 4640	⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
df-ima 4641	⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
cio 5178	class (℩𝑥𝜑)
df-iota 5180	⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
wfun 5212	wff Fun 𝐴
wfn 5213	wff 𝐴 Fn 𝐵
wf 5214	wff 𝐹:𝐴⟶𝐵
wf1 5215	wff 𝐹:𝐴–1-1→𝐵
wfo 5216	wff 𝐹:𝐴–onto→𝐵
wf1o 5217	wff 𝐹:𝐴–1-1-onto→𝐵
cfv 5218	class (𝐹‘𝐴)
wiso 5219	wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
df-fun 5220	⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
df-fn 5221	⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
df-f 5222	⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
df-f1 5223	⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
df-fo 5224	⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
df-f1o 5225	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
df-fv 5226	⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
df-isom 5227	⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
crio 5832	class (℩𝑥 ∈ 𝐴 𝜑)
df-riota 5833	⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
co 5877	class (𝐴𝐹𝐵)
coprab 5878	class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
cmpo 5879	class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
df-ov 5880	⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
df-oprab 5881	⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
df-mpo 5882	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
cof 6083	class ∘𝑓 𝑅
cofr 6084	class ∘𝑟 𝑅
df-of 6085	⊢ ∘𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥))))
df-ofr 6086	⊢ ∘𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)}
c1st 6141	class 1st
c2nd 6142	class 2nd
df-1st 6143	⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
df-2nd 6144	⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥})
ctpos 6247	class tpos 𝐹
df-tpos 6248	⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
wsmo 6288	wff Smo 𝐴
df-smo 6289	⊢ (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))))
crecs 6307	class recs(𝐹)
df-recs 6308	⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
crdg 6372	class rec(𝐹, 𝐼)
df-irdg 6373	⊢ rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))))
cfrec 6393	class frec(𝐹, 𝐼)
df-frec 6394	⊢ frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐼))})) ↾ ω)
c1o 6412	class 1o
c2o 6413	class 2o
c3o 6414	class 3o
c4o 6415	class 4o
coa 6416	class +o
comu 6417	class ·o
coei 6418	class ↑o
df-1o 6419	⊢ 1o = suc ∅
df-2o 6420	⊢ 2o = suc 1o
df-3o 6421	⊢ 3o = suc 2o
df-4o 6422	⊢ 4o = suc 3o
df-oadd 6423	⊢ +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦))
df-omul 6424	⊢ ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦))
df-oexpi 6425	⊢ ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦))
wer 6534	wff 𝑅 Er 𝐴
cec 6535	class [𝐴]𝑅
cqs 6536	class (𝐴 / 𝑅)
df-er 6537	⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
df-ec 6539	⊢ [𝐴]𝑅 = (𝑅 “ {𝐴})
df-qs 6543	⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
cmap 6650	class ↑𝑚
cpm 6651	class ↑pm
df-map 6652	⊢ ↑𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥})
df-pm 6653	⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓})
cixp 6700	class X𝑥 ∈ 𝐴 𝐵
df-ixp 6701	⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}
cen 6740	class ≈
cdom 6741	class ≼
cfn 6742	class Fin
df-en 6743	⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
df-dom 6744	⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦}
df-fin 6745	⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦}
cfi 6969	class fi
df-fi 6970	⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦})
csup 6983	class sup(𝐴, 𝐵, 𝑅)
cinf 6984	class inf(𝐴, 𝐵, 𝑅)
df-sup 6985	⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))}
df-inf 6986	⊢ inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)
cdju 7038	class (𝐴 ⊔ 𝐵)
df-dju 7039	⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
cinl 7046	class inl
cinr 7047	class inr
df-inl 7048	⊢ inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩)
df-inr 7049	⊢ inr = (𝑥 ∈ V ↦ ⟨1o, 𝑥⟩)
cdjucase 7084	class case(𝑅, 𝑆)
df-case 7085	⊢ case(𝑅, 𝑆) = ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr))
cdjud 7103	class (𝑅 ⊔d 𝑆)
df-djud 7104	⊢ (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆)))
xnninf 7120	class ℕ∞
df-nninf 7121	⊢ ℕ∞ = {𝑓 ∈ (2o ↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)}
comni 7134	class Omni
df-omni 7135	⊢ Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))}
cmarkov 7151	class Markov
df-markov 7152	⊢ Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅))}
cwomni 7163	class WOmni
df-womni 7164	⊢ WOmni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)}
ccrd 7180	class card
df-card 7181	⊢ card = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝑥})
wac 7206	wff CHOICE
df-ac 7207	⊢ (CHOICE ↔ ∀𝑥∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥))
wap 7248	wff 𝑅 Ap 𝐴
df-pap 7249	⊢ (𝑅 Ap 𝐴 ↔ ((𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)))))
wtap 7250	wff 𝑅 TAp 𝐴
df-tap 7251	⊢ (𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)))
wacc 7263	wff CCHOICE
df-cc 7264	⊢ (CCHOICE ↔ ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥)))
cnpi 7273	class N
cpli 7274	class +N
cmi 7275	class ·N
clti 7276	class <N
cplpq 7277	class +pQ
cmpq 7278	class ·pQ
cltpq 7279	class <pQ
ceq 7280	class ~Q
cnq 7281	class Q
c1q 7282	class 1Q
cplq 7283	class +Q
cmq 7284	class ·Q
crq 7285	class *Q
cltq 7286	class <Q
ceq0 7287	class ~Q0
cnq0 7288	class Q0
c0q0 7289	class 0Q0
cplq0 7290	class +Q0
cmq0 7291	class ·Q0
cnp 7292	class P
c1p 7293	class 1P
cpp 7294	class +P
cmp 7295	class ·P
cltp 7296	class <P
cer 7297	class ~R
cnr 7298	class R
c0r 7299	class 0R
c1r 7300	class 1R
cm1r 7301	class -1R
cplr 7302	class +R
cmr 7303	class ·R
cltr 7304	class <R
df-ni 7305	⊢ N = (ω ∖ {∅})
df-pli 7306	⊢ +N = ( +o ↾ (N × N))
df-mi 7307	⊢ ·N = ( ·o ↾ (N × N))
df-lti 7308	⊢ <N = ( E ∩ (N × N))
df-plpq 7345	⊢ +pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨(((1st ‘𝑥) ·N (2nd ‘𝑦)) +N ((1st ‘𝑦) ·N (2nd ‘𝑥))), ((2nd ‘𝑥) ·N (2nd ‘𝑦))⟩)
df-mpq 7346	⊢ ·pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨((1st ‘𝑥) ·N (1st ‘𝑦)), ((2nd ‘𝑥) ·N (2nd ‘𝑦))⟩)
df-ltpq 7347	⊢ <pQ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ((1st ‘𝑥) ·N (2nd ‘𝑦)) <N ((1st ‘𝑦) ·N (2nd ‘𝑥)))}
df-enq 7348	⊢ ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}
df-nqqs 7349	⊢ Q = ((N × N) / ~Q )
df-plqqs 7350	⊢ +Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ +pQ ⟨𝑢, 𝑓⟩)] ~Q ))}
df-mqqs 7351	⊢ ·Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q ))}
df-1nqqs 7352	⊢ 1Q = [⟨1o, 1o⟩] ~Q
df-rq 7353	⊢ *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
df-ltnqqs 7354	⊢ <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
df-enq0 7425	⊢ ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))}
df-nq0 7426	⊢ Q0 = ((ω × N) / ~Q0 )
df-0nq0 7427	⊢ 0Q0 = [⟨∅, 1o⟩] ~Q0
df-plq0 7428	⊢ +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
df-mq0 7429	⊢ ·Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨(𝑤 ·o 𝑢), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
df-inp 7467	⊢ P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙 ⊆ Q ∧ 𝑢 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))))}
df-i1p 7468	⊢ 1P = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
df-iplp 7469	⊢ +P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
df-imp 7470	⊢ ·P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
df-iltp 7471	⊢ <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))}
df-enr 7727	⊢ ~R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (P × P) ∧ 𝑦 ∈ (P × P)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 +P 𝑢) = (𝑤 +P 𝑣)))}
df-nr 7728	⊢ R = ((P × P) / ~R )
df-plr 7729	⊢ +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}
df-mr 7730	⊢ ·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑓)), ((𝑤 ·P 𝑓) +P (𝑣 ·P 𝑢))⟩] ~R ))}
df-ltr 7731	⊢ <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
df-0r 7732	⊢ 0R = [⟨1P, 1P⟩] ~R
df-1r 7733	⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 7734	⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 7811	class ℂ
cr 7812	class ℝ
cc0 7813	class 0
c1 7814	class 1
ci 7815	class i
caddc 7816	class +
cltrr 7817	class <ℝ
cmul 7818	class ·
df-c 7819	⊢ ℂ = (R × R)
df-0 7820	⊢ 0 = ⟨0R, 0R⟩
df-1 7821	⊢ 1 = ⟨1R, 0R⟩
df-i 7822	⊢ i = ⟨0R, 1R⟩
df-r 7823	⊢ ℝ = (R × {0R})
df-add 7824	⊢ + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
df-mul 7825	⊢ · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
df-lt 7826	⊢ <ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
ax-cnex 7904	⊢ ℂ ∈ V
ax-resscn 7905	⊢ ℝ ⊆ ℂ
ax-1cn 7906	⊢ 1 ∈ ℂ
ax-1re 7907	⊢ 1 ∈ ℝ
ax-icn 7908	⊢ i ∈ ℂ
ax-addcl 7909	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
ax-addrcl 7910	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
ax-mulcl 7911	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
ax-mulrcl 7912	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
ax-addcom 7913	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
ax-mulcom 7914	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
ax-addass 7915	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
ax-mulass 7916	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
ax-distr 7917	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
ax-i2m1 7918	⊢ ((i · i) + 1) = 0
ax-0lt1 7919	⊢ 0 <ℝ 1
ax-1rid 7920	⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
ax-0id 7921	⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
ax-rnegex 7922	⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
ax-precex 7923	⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃𝑥 ∈ ℝ (0 <ℝ 𝑥 ∧ (𝐴 · 𝑥) = 1))
ax-cnre 7924	⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
ax-pre-ltirr 7925	⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴)
ax-pre-ltwlin 7926	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵)))
ax-pre-lttrn 7927	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
ax-pre-apti 7928	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵)
ax-pre-ltadd 7929	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
ax-pre-mulgt0 7930	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
ax-pre-mulext 7931	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)))
ax-arch 7932	⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛)
ax-caucvg 7933	⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))))
ax-pre-suploc 7934	⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
ax-addf 7935	⊢ + :(ℂ × ℂ)⟶ℂ
ax-mulf 7936	⊢ · :(ℂ × ℂ)⟶ℂ
cpnf 7991	class +∞
cmnf 7992	class -∞
cxr 7993	class ℝ*
clt 7994	class <
cle 7995	class ≤
df-pnf 7996	⊢ +∞ = 𝒫 ∪ ℂ
df-mnf 7997	⊢ -∞ = 𝒫 +∞
df-xr 7998	⊢ ℝ* = (ℝ ∪ {+∞, -∞})
df-ltxr 7999	⊢ < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
df-le 8000	⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
cmin 8130	class −
cneg 8131	class -𝐴
df-sub 8132	⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
df-neg 8133	⊢ -𝐴 = (0 − 𝐴)
creap 8533	class #ℝ
df-reap 8534	⊢ #ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))}
cap 8540	class #
df-ap 8541	⊢ # = {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢))}
cdiv 8631	class /
df-div 8632	⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
cn 8921	class ℕ
df-inn 8922	⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
c2 8972	class 2
c3 8973	class 3
c4 8974	class 4
c5 8975	class 5
c6 8976	class 6
c7 8977	class 7
c8 8978	class 8
c9 8979	class 9
df-2 8980	⊢ 2 = (1 + 1)
df-3 8981	⊢ 3 = (2 + 1)
df-4 8982	⊢ 4 = (3 + 1)
df-5 8983	⊢ 5 = (4 + 1)
df-6 8984	⊢ 6 = (5 + 1)
df-7 8985	⊢ 7 = (6 + 1)
df-8 8986	⊢ 8 = (7 + 1)
df-9 8987	⊢ 9 = (8 + 1)
cn0 9178	class ℕ0
df-n0 9179	⊢ ℕ0 = (ℕ ∪ {0})
cxnn0 9241	class ℕ0*
df-xnn0 9242	⊢ ℕ0* = (ℕ0 ∪ {+∞})
cz 9255	class ℤ
df-z 9256	⊢ ℤ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ -𝑛 ∈ ℕ)}
cdc 9386	class ;𝐴𝐵
df-dec 9387	⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
cuz 9530	class ℤ≥
df-uz 9531	⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
cq 9621	class ℚ
df-q 9622	⊢ ℚ = ( / “ (ℤ × ℕ))
crp 9655	class ℝ+
df-rp 9656	⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
cxne 9771	class -𝑒𝐴
cxad 9772	class +𝑒
cxmu 9773	class ·e
df-xneg 9774	⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
df-xadd 9775	⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
df-xmul 9776	⊢ ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
cioo 9890	class (,)
cioc 9891	class (,]
cico 9892	class [,)
cicc 9893	class [,]
df-ioo 9894	⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
df-ioc 9895	⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
df-ico 9896	⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
df-icc 9897	⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
cfz 10010	class ...
df-fz 10011	⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)})
cfzo 10144	class ..^
df-fzo 10145	⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
cfl 10270	class ⌊
cceil 10271	class ⌈
df-fl 10272	⊢ ⌊ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1))))
df-ceil 10273	⊢ ⌈ = (𝑥 ∈ ℝ ↦ -(⌊‘-𝑥))
cmo 10324	class mod
df-mod 10325	⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
cseq 10447	class seq𝑀( + , 𝐹)
df-seqfrec 10448	⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
cexp 10521	class ↑
df-exp 10522	⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}))‘-𝑦)))))
cfa 10707	class !
df-fac 10708	⊢ ! = ({⟨0, 1⟩} ∪ seq1( · , I ))
cbc 10729	class C
df-bc 10730	⊢ C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
chash 10757	class ♯
df-ihash 10758	⊢ ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))
cshi 10825	class shift
df-shft 10826	⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)})
ccj 10850	class ∗
cre 10851	class ℜ
cim 10852	class ℑ
df-cj 10853	⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ)))
df-re 10854	⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2))
df-im 10855	⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i)))
csqrt 11007	class √
cabs 11008	class abs
df-rsqrt 11009	⊢ √ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
df-abs 11010	⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
cli 11288	class ⇝
df-clim 11289	⊢ ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}
csu 11363	class Σ𝑘 ∈ 𝐴 𝐵
df-sumdc 11364	⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
cprod 11560	class ∏𝑘 ∈ 𝐴 𝐵
df-proddc 11561	⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
ce 11652	class exp
ceu 11653	class e
csin 11654	class sin
ccos 11655	class cos
ctan 11656	class tan
cpi 11657	class π
df-ef 11658	⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘)))
df-e 11659	⊢ e = (exp‘1)
df-sin 11660	⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
df-cos 11661	⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2))
df-tan 11662	⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥)))
df-pi 11663	⊢ π = inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < )
ctau 11784	class τ
df-tau 11785	⊢ τ = inf((ℝ+ ∩ (◡cos “ {1})), ℝ, < )
cdvds 11796	class ∥
df-dvds 11797	⊢ ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
cgcd 11945	class gcd
df-gcd 11946	⊢ gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦)}, ℝ, < )))
clcm 12062	class lcm
df-lcm 12063	⊢ lcm = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛)}, ℝ, < )))
cprime 12109	class ℙ
df-prm 12110	⊢ ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2o}
cnumer 12183	class numer
cdenom 12184	class denom
df-numer 12185	⊢ numer = (𝑦 ∈ ℚ ↦ (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
df-denom 12186	⊢ denom = (𝑦 ∈ ℚ ↦ (2nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
codz 12210	class odℤ
cphi 12211	class ϕ
df-odz 12212	⊢ odℤ = (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, < )))
df-phi 12213	⊢ ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
cpc 12286	class pCnt
df-pc 12287	⊢ pCnt = (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < ))))))
cgz 12369	class ℤ[i]
df-gz 12370	⊢ ℤ[i] = {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)}
cstr 12460	class Struct
cnx 12461	class ndx
csts 12462	class sSet
cslot 12463	class Slot 𝐴
cbs 12464	class Base
cress 12465	class ↾s
df-struct 12466	⊢ Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
df-ndx 12467	⊢ ndx = ( I ↾ ℕ)
df-slot 12468	⊢ Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴))
df-base 12470	⊢ Base = Slot 1
df-sets 12471	⊢ sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))
df-iress 12472	⊢ ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
cplusg 12538	class +g
cmulr 12539	class .r
cstv 12540	class *𝑟
csca 12541	class Scalar
cvsca 12542	class ·𝑠
cip 12543	class ·𝑖
cts 12544	class TopSet
cple 12545	class le
coc 12546	class oc
cds 12547	class dist
cunif 12548	class UnifSet
chom 12549	class Hom
cco 12550	class comp
df-plusg 12551	⊢ +g = Slot 2
df-mulr 12552	⊢ .r = Slot 3
df-starv 12553	⊢ *𝑟 = Slot 4
df-sca 12554	⊢ Scalar = Slot 5
df-vsca 12555	⊢ ·𝑠 = Slot 6
df-ip 12556	⊢ ·𝑖 = Slot 8
df-tset 12557	⊢ TopSet = Slot 9
df-ple 12558	⊢ le = Slot ;10
df-ocomp 12559	⊢ oc = Slot ;11
df-ds 12560	⊢ dist = Slot ;12
df-unif 12561	⊢ UnifSet = Slot ;13
df-hom 12562	⊢ Hom = Slot ;14
df-cco 12563	⊢ comp = Slot ;15
crest 12693	class ↾t
ctopn 12694	class TopOpen
df-rest 12695	⊢ ↾t = (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥)))
df-topn 12696	⊢ TopOpen = (𝑤 ∈ V ↦ ((TopSet‘𝑤) ↾t (Base‘𝑤)))
ctg 12708	class topGen
cpt 12709	class ∏t
c0g 12710	class 0g
cgsu 12711	class Σg
df-0g 12712	⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥))))
df-gsum 12713	⊢ Σ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 12714	⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)})
df-pt 12715	⊢ ∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}))
cprds 12719	class Xs
cpws 12720	class ↑s
df-prds 12721	⊢ 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 12724	⊢ ↑s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
cimas 12725	class “s
cqus 12726	class /s
cxps 12727	class ×s
df-iimas 12728	⊢ “s = (𝑓 ∈ V, 𝑟 ∈ V ↦ ⦋(Base‘𝑟) / 𝑣⦌{⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩})
df-qus 12729	⊢ /s = (𝑟 ∈ V, 𝑒 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟))
df-xps 12730	⊢ ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
cplusf 12777	class +𝑓
cmgm 12778	class Mgm
df-plusf 12779	⊢ +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)𝑦)))
df-mgm 12780	⊢ Mgm = {𝑔 ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏}
csgrp 12812	class Smgrp
df-sgrp 12813	⊢ Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
cmnd 12822	class Mnd
df-mnd 12823	⊢ Mnd = {𝑔 ∈ Smgrp ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}
cmhm 12854	class MndHom
csubmnd 12855	class SubMnd
df-mhm 12856	⊢ MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})
df-submnd 12857	⊢ SubMnd = (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g‘𝑠) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡)})
cgrp 12882	class Grp
cminusg 12883	class invg
csg 12884	class -g
df-grp 12885	⊢ Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}
df-minusg 12886	⊢ invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))
df-sbg 12887	⊢ -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))
cmg 12988	class .g
df-mulg 12989	⊢ .g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))))
csubg 13032	class SubGrp
cnsg 13033	class NrmSGrp
cqg 13034	class ~QG
df-subg 13035	⊢ SubGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp})
df-nsg 13036	⊢ NrmSGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})
df-eqg 13037	⊢ ~QG = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)})
ccmn 13093	class CMnd
cabl 13094	class Abel
df-cmn 13095	⊢ CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)}
df-abl 13096	⊢ Abel = (Grp ∩ CMnd)
cmgp 13135	class mulGrp
df-mgp 13136	⊢ mulGrp = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(+g‘ndx), (.r‘𝑤)⟩))
cur 13147	class 1r
df-ur 13148	⊢ 1r = (0g ∘ mulGrp)
csrg 13151	class SRing
df-srg 13152	⊢ SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
crg 13184	class Ring
ccrg 13185	class CRing
df-ring 13186	⊢ Ring = {𝑓 ∈ Grp ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
df-cring 13187	⊢ CRing = {𝑓 ∈ Ring ∣ (mulGrp‘𝑓) ∈ CMnd}
coppr 13244	class oppr
df-oppr 13245	⊢ oppr = (𝑓 ∈ V ↦ (𝑓 sSet ⟨(.r‘ndx), tpos (.r‘𝑓)⟩))
cdsr 13260	class ∥r
cui 13261	class Unit
cir 13262	class Irred
df-dvdsr 13263	⊢ ∥r = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑤) ∧ ∃𝑧 ∈ (Base‘𝑤)(𝑧(.r‘𝑤)𝑥) = 𝑦)})
df-unit 13264	⊢ Unit = (𝑤 ∈ V ↦ (◡((∥r‘𝑤) ∩ (∥r‘(oppr‘𝑤))) “ {(1r‘𝑤)}))
df-irred 13265	⊢ Irred = (𝑤 ∈ V ↦ ⦋((Base‘𝑤) ∖ (Unit‘𝑤)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑤)𝑦) ≠ 𝑧})
cinvr 13294	class invr
df-invr 13295	⊢ invr = (𝑟 ∈ V ↦ (invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟))))
cdvr 13305	class /r
df-dvr 13306	⊢ /r = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦))))
crh 13324	class RingHom
crs 13325	class RingIso
df-rnghom 13326	⊢ RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))})
df-rngiso 13327	⊢ RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)})
cnzr 13328	class NzRing
df-nzr 13329	⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)}
clring 13336	class LRing
df-lring 13337	⊢ LRing = {𝑟 ∈ NzRing ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑥(+g‘𝑟)𝑦) = (1r‘𝑟) → (𝑥 ∈ (Unit‘𝑟) ∨ 𝑦 ∈ (Unit‘𝑟)))}
csubrg 13343	class SubRing
crgspn 13344	class RingSpan
df-subrg 13345	⊢ SubRing = (𝑤 ∈ Ring ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ((𝑤 ↾s 𝑠) ∈ Ring ∧ (1r‘𝑤) ∈ 𝑠)})
df-rgspn 13346	⊢ RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}))
capr 13375	class #r
df-apr 13376	⊢ #r = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))})
clmod 13382	class LMod
cscaf 13383	class ·sf
df-lmod 13384	⊢ LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))}
df-scaf 13385	⊢ ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦)))
clss 13447	class LSubSp
df-lssm 13448	⊢ LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (∃𝑗 𝑗 ∈ 𝑠 ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠)})
clspn 13478	class LSpan
df-lsp 13479	⊢ LSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (LSubSp‘𝑤) ∣ 𝑠 ⊆ 𝑡}))
cpsmet 13524	class PsMet
cxmet 13525	class ∞Met
cmet 13526	class Met
cbl 13527	class ball
cfbas 13528	class fBas
cfg 13529	class filGen
cmopn 13530	class MetOpen
cmetu 13531	class metUnif
df-psmet 13532	⊢ PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
df-xmet 13533	⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
df-met 13534	⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})
df-bl 13535	⊢ ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))
df-mopn 13536	⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))
df-fbas 13537	⊢ fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)})
df-fg 13538	⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
df-metu 13539	⊢ metUnif = (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))))
ccnfld 13540	class ℂfld
df-icnfld 13541	⊢ ℂfld = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
czring 13565	class ℤring
df-zring 13566	⊢ ℤring = (ℂfld ↾s ℤ)
ctop 13582	class Top
df-top 13583	⊢ Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)}
ctopon 13595	class TopOn
df-topon 13596	⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗})
ctps 13615	class TopSp
df-topsp 13616	⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
ctb 13627	class TopBases
df-bases 13628	⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))}
ccld 13677	class Clsd
cnt 13678	class int
ccl 13679	class cls
df-cld 13680	⊢ Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗})
df-ntr 13681	⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))
df-cls 13682	⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}))
cnei 13723	class nei
df-nei 13724	⊢ nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)}))
ccn 13770	class Cn
ccnp 13771	class CnP
clm 13772	class ⇝𝑡
df-cn 13773	⊢ Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗})
df-cnp 13774	⊢ CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}))
df-lm 13775	⊢ ⇝𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})
ctx 13837	class ×t
df-tx 13838	⊢ ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))))
chmeo 13885	class Homeo
df-hmeo 13886	⊢ Homeo = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ ◡𝑓 ∈ (𝑘 Cn 𝑗)})
cxms 13921	class ∞MetSp
cms 13922	class MetSp
ctms 13923	class toMetSp
df-xms 13924	⊢ ∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpen‘𝑓) = (MetOpen‘((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))))}
df-ms 13925	⊢ MetSp = {𝑓 ∈ ∞MetSp ∣ ((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))) ∈ (Met‘(Base‘𝑓))}
df-tms 13926	⊢ toMetSp = (𝑑 ∈ ∪ ran ∞Met ↦ ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩))
ccncf 14142	class –cn→
df-cncf 14143	⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑𝑚 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)})
climc 14208	class limℂ
cdv 14209	class D
df-limced 14210	⊢ limℂ = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)))})
df-dvap 14211	⊢ D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ ∪ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))
clog 14362	class log
ccxp 14363	class ↑𝑐
df-relog 14364	⊢ log = ◡(exp ↾ ℝ)
df-rpcxp 14365	⊢ ↑𝑐 = (𝑥 ∈ ℝ+, 𝑦 ∈ ℂ ↦ (exp‘(𝑦 · (log‘𝑥))))
clogb 14446	class logb
df-logb 14447	⊢ logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥)))
clgs 14483	class /L
df-lgs 14484	⊢ /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 14630	wff 𝐴 DECIDin 𝐵
df-dcin 14631	⊢ (𝐴 DECIDin 𝐵 ↔ ∀𝑥 ∈ 𝐵 DECID 𝑥 ∈ 𝐴)
wbd 14649	wff BOUNDED 𝜑
ax-bd0 14650	⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (BOUNDED 𝜑 → BOUNDED 𝜓)
ax-bdim 14651	⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝜓    ⇒   ⊢ BOUNDED (𝜑 → 𝜓)
ax-bdan 14652	⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝜓    ⇒   ⊢ BOUNDED (𝜑 ∧ 𝜓)
ax-bdor 14653	⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝜓    ⇒   ⊢ BOUNDED (𝜑 ∨ 𝜓)
ax-bdn 14654	⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED ¬ 𝜑
ax-bdal 14655	⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED ∀𝑥 ∈ 𝑦 𝜑
ax-bdex 14656	⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED ∃𝑥 ∈ 𝑦 𝜑
ax-bdeq 14657	⊢ BOUNDED 𝑥 = 𝑦
ax-bdel 14658	⊢ BOUNDED 𝑥 ∈ 𝑦
ax-bdsb 14659	⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED [𝑦 / 𝑥]𝜑
wbdc 14677	wff BOUNDED 𝐴
df-bdc 14678	⊢ (BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥 ∈ 𝐴)
ax-bdsep 14721	⊢ BOUNDED 𝜑    ⇒   ⊢ ∀𝑎∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
ax-bj-d0cl 14761	⊢ BOUNDED 𝜑    ⇒   ⊢ DECID 𝜑
wind 14763	wff Ind 𝐴
df-bj-ind 14764	⊢ (Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
ax-infvn 14778	⊢ ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦))
ax-bdsetind 14805	⊢ BOUNDED 𝜑    ⇒   ⊢ (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑)
ax-inf2 14813	⊢ ∃𝑎∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦))
ax-strcoll 14819	⊢ ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))
ax-sscoll 14824	⊢ ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑))
ax-ddkcomp 14826	⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵)))
walsi 14909	wff ∀!𝑥(𝜑 → 𝜓)
walsc 14910	wff ∀!𝑥 ∈ 𝐴𝜑
df-alsi 14911	⊢ (∀!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑))
df-alsc 14912	⊢ (∀!𝑥 ∈ 𝐴𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴))