ILE Home Intuitionistic Logic Explorer This is the Unicode version.
Change to GIF version

List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 3wff Β¬ πœ‘
wi 4wff (πœ‘ β†’ πœ“)
ax-mp 5πœ‘    &   (πœ‘ β†’ πœ“)    β‡’   πœ“
ax-1 6(πœ‘ β†’ (πœ“ β†’ πœ‘))
ax-2 7((πœ‘ β†’ (πœ“ β†’ πœ’)) β†’ ((πœ‘ β†’ πœ“) β†’ (πœ‘ β†’ πœ’)))
wa 104wff (πœ‘ ∧ πœ“)
wb 105wff (πœ‘ ↔ πœ“)
ax-ia1 106((πœ‘ ∧ πœ“) β†’ πœ‘)
ax-ia2 107((πœ‘ ∧ πœ“) β†’ πœ“)
ax-ia3 108(πœ‘ β†’ (πœ“ β†’ (πœ‘ ∧ πœ“)))
df-bi 117(((πœ‘ ↔ πœ“) β†’ ((πœ‘ β†’ πœ“) ∧ (πœ“ β†’ πœ‘))) ∧ (((πœ‘ β†’ πœ“) ∧ (πœ“ β†’ πœ‘)) β†’ (πœ‘ ↔ πœ“)))
ax-in1 614((πœ‘ β†’ Β¬ πœ‘) β†’ Β¬ πœ‘)
ax-in2 615(Β¬ πœ‘ β†’ (πœ‘ β†’ πœ“))
wo 708wff (πœ‘ ∨ πœ“)
ax-io 709(((πœ‘ ∨ πœ’) β†’ πœ“) ↔ ((πœ‘ β†’ πœ“) ∧ (πœ’ β†’ πœ“)))
wstab 830wff STAB πœ‘
df-stab 831(STAB πœ‘ ↔ (Β¬ Β¬ πœ‘ β†’ πœ‘))
wdc 834wff DECID πœ‘
df-dc 835(DECID πœ‘ ↔ (πœ‘ ∨ Β¬ πœ‘))
w3o 977wff (πœ‘ ∨ πœ“ ∨ πœ’)
w3a 978wff (πœ‘ ∧ πœ“ ∧ πœ’)
df-3or 979((πœ‘ ∨ πœ“ ∨ πœ’) ↔ ((πœ‘ ∨ πœ“) ∨ πœ’))
df-3an 980((πœ‘ ∧ πœ“ ∧ πœ’) ↔ ((πœ‘ ∧ πœ“) ∧ πœ’))
wal 1351wff βˆ€π‘₯πœ‘
cv 1352class π‘₯
wceq 1353wff 𝐴 = 𝐡
wtru 1354wff ⊀
df-tru 1356(⊀ ↔ (βˆ€π‘₯ π‘₯ = π‘₯ β†’ βˆ€π‘₯ π‘₯ = π‘₯))
wfal 1358wff βŠ₯
df-fal 1359(βŠ₯ ↔ Β¬ ⊀)
wxo 1375wff (πœ‘ ⊻ πœ“)
df-xor 1376((πœ‘ ⊻ πœ“) ↔ ((πœ‘ ∨ πœ“) ∧ Β¬ (πœ‘ ∧ πœ“)))
ax-5 1447(βˆ€π‘₯(πœ‘ β†’ πœ“) β†’ (βˆ€π‘₯πœ‘ β†’ βˆ€π‘₯πœ“))
ax-7 1448(βˆ€π‘₯βˆ€π‘¦πœ‘ β†’ βˆ€π‘¦βˆ€π‘₯πœ‘)
ax-gen 1449πœ‘    β‡’   βˆ€π‘₯πœ‘
wnf 1460wff β„²π‘₯πœ‘
df-nf 1461(β„²π‘₯πœ‘ ↔ βˆ€π‘₯(πœ‘ β†’ βˆ€π‘₯πœ‘))
wex 1492wff βˆƒπ‘₯πœ‘
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 1762wff [𝑦 / π‘₯]πœ‘
df-sb 1763([𝑦 / π‘₯]πœ‘ ↔ ((π‘₯ = 𝑦 β†’ πœ‘) ∧ βˆƒπ‘₯(π‘₯ = 𝑦 ∧ πœ‘)))
ax-16 1814(βˆ€π‘₯ π‘₯ = 𝑦 β†’ (πœ‘ β†’ βˆ€π‘₯πœ‘))
ax-11o 1823(Β¬ βˆ€π‘₯ π‘₯ = 𝑦 β†’ (π‘₯ = 𝑦 β†’ (πœ‘ β†’ βˆ€π‘₯(π‘₯ = 𝑦 β†’ πœ‘))))
weu 2026wff βˆƒ!π‘₯πœ‘
wmo 2027wff βˆƒ*π‘₯πœ‘
df-eu 2029(βˆƒ!π‘₯πœ‘ ↔ βˆƒπ‘¦βˆ€π‘₯(πœ‘ ↔ π‘₯ = 𝑦))
df-mo 2030(βˆƒ*π‘₯πœ‘ ↔ (βˆƒπ‘₯πœ‘ β†’ βˆƒ!π‘₯πœ‘))
wcel 2148wff 𝐴 ∈ 𝐡
ax-13 2150(π‘₯ = 𝑦 β†’ (π‘₯ ∈ 𝑧 β†’ 𝑦 ∈ 𝑧))
ax-14 2151(π‘₯ = 𝑦 β†’ (𝑧 ∈ π‘₯ β†’ 𝑧 ∈ 𝑦))
ax-ext 2159(βˆ€π‘§(𝑧 ∈ π‘₯ ↔ 𝑧 ∈ 𝑦) β†’ π‘₯ = 𝑦)
cab 2163class {π‘₯ ∣ πœ‘}
df-clab 2164(π‘₯ ∈ {𝑦 ∣ πœ‘} ↔ [π‘₯ / 𝑦]πœ‘)
df-cleq 2170(βˆ€π‘₯(π‘₯ ∈ 𝑦 ↔ π‘₯ ∈ 𝑧) β†’ 𝑦 = 𝑧)    β‡’   (𝐴 = 𝐡 ↔ βˆ€π‘₯(π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ 𝐡))
df-clel 2173(𝐴 ∈ 𝐡 ↔ βˆƒπ‘₯(π‘₯ = 𝐴 ∧ π‘₯ ∈ 𝐡))
wnfc 2306wff β„²π‘₯𝐴
df-nfc 2308(β„²π‘₯𝐴 ↔ βˆ€π‘¦β„²π‘₯ 𝑦 ∈ 𝐴)
wne 2347wff 𝐴 β‰  𝐡
df-ne 2348(𝐴 β‰  𝐡 ↔ Β¬ 𝐴 = 𝐡)
wnel 2442wff 𝐴 βˆ‰ 𝐡
df-nel 2443(𝐴 βˆ‰ 𝐡 ↔ Β¬ 𝐴 ∈ 𝐡)
wral 2455wff βˆ€π‘₯ ∈ 𝐴 πœ‘
wrex 2456wff βˆƒπ‘₯ ∈ 𝐴 πœ‘
wreu 2457wff βˆƒ!π‘₯ ∈ 𝐴 πœ‘
wrmo 2458wff βˆƒ*π‘₯ ∈ 𝐴 πœ‘
crab 2459class {π‘₯ ∈ 𝐴 ∣ πœ‘}
df-ral 2460(βˆ€π‘₯ ∈ 𝐴 πœ‘ ↔ βˆ€π‘₯(π‘₯ ∈ 𝐴 β†’ πœ‘))
df-rex 2461(βˆƒπ‘₯ ∈ 𝐴 πœ‘ ↔ βˆƒπ‘₯(π‘₯ ∈ 𝐴 ∧ πœ‘))
df-reu 2462(βˆƒ!π‘₯ ∈ 𝐴 πœ‘ ↔ βˆƒ!π‘₯(π‘₯ ∈ 𝐴 ∧ πœ‘))
df-rmo 2463(βˆƒ*π‘₯ ∈ 𝐴 πœ‘ ↔ βˆƒ*π‘₯(π‘₯ ∈ 𝐴 ∧ πœ‘))
df-rab 2464{π‘₯ ∈ 𝐴 ∣ πœ‘} = {π‘₯ ∣ (π‘₯ ∈ 𝐴 ∧ πœ‘)}
cvv 2738class V
df-v 2740V = {π‘₯ ∣ π‘₯ = π‘₯}
wcdeq 2946wff CondEq(π‘₯ = 𝑦 β†’ πœ‘)
df-cdeq 2947(CondEq(π‘₯ = 𝑦 β†’ πœ‘) ↔ (π‘₯ = 𝑦 β†’ πœ‘))
wsbc 2963wff [𝐴 / π‘₯]πœ‘
df-sbc 2964([𝐴 / π‘₯]πœ‘ ↔ 𝐴 ∈ {π‘₯ ∣ πœ‘})
csb 3058class ⦋𝐴 / π‘₯⦌𝐡
df-csb 3059⦋𝐴 / π‘₯⦌𝐡 = {𝑦 ∣ [𝐴 / π‘₯]𝑦 ∈ 𝐡}
cdif 3127class (𝐴 βˆ– 𝐡)
cun 3128class (𝐴 βˆͺ 𝐡)
cin 3129class (𝐴 ∩ 𝐡)
wss 3130wff 𝐴 βŠ† 𝐡
df-dif 3132(𝐴 βˆ– 𝐡) = {π‘₯ ∣ (π‘₯ ∈ 𝐴 ∧ Β¬ π‘₯ ∈ 𝐡)}
df-un 3134(𝐴 βˆͺ 𝐡) = {π‘₯ ∣ (π‘₯ ∈ 𝐴 ∨ π‘₯ ∈ 𝐡)}
df-in 3136(𝐴 ∩ 𝐡) = {π‘₯ ∣ (π‘₯ ∈ 𝐴 ∧ π‘₯ ∈ 𝐡)}
df-ss 3143(𝐴 βŠ† 𝐡 ↔ (𝐴 ∩ 𝐡) = 𝐴)
c0 3423class βˆ…
df-nul 3424βˆ… = (V βˆ– V)
cif 3535class if(πœ‘, 𝐴, 𝐡)
df-if 3536if(πœ‘, 𝐴, 𝐡) = {π‘₯ ∣ ((π‘₯ ∈ 𝐴 ∧ πœ‘) ∨ (π‘₯ ∈ 𝐡 ∧ Β¬ πœ‘))}
cpw 3576class 𝒫 𝐴
df-pw 3578𝒫 𝐴 = {π‘₯ ∣ π‘₯ βŠ† 𝐴}
csn 3593class {𝐴}
cpr 3594class {𝐴, 𝐡}
ctp 3595class {𝐴, 𝐡, 𝐢}
cop 3596class ⟨𝐴, 𝐡⟩
cotp 3597class ⟨𝐴, 𝐡, 𝐢⟩
df-sn 3599{𝐴} = {π‘₯ ∣ π‘₯ = 𝐴}
df-pr 3600{𝐴, 𝐡} = ({𝐴} βˆͺ {𝐡})
df-tp 3601{𝐴, 𝐡, 𝐢} = ({𝐴, 𝐡} βˆͺ {𝐢})
df-op 3602⟨𝐴, 𝐡⟩ = {π‘₯ ∣ (𝐴 ∈ V ∧ 𝐡 ∈ V ∧ π‘₯ ∈ {{𝐴}, {𝐴, 𝐡}})}
df-ot 3603⟨𝐴, 𝐡, 𝐢⟩ = ⟨⟨𝐴, 𝐡⟩, 𝐢⟩
cuni 3810class βˆͺ 𝐴
df-uni 3811βˆͺ 𝐴 = {π‘₯ ∣ βˆƒπ‘¦(π‘₯ ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)}
cint 3845class ∩ 𝐴
df-int 3846∩ 𝐴 = {π‘₯ ∣ βˆ€π‘¦(𝑦 ∈ 𝐴 β†’ π‘₯ ∈ 𝑦)}
ciun 3887class βˆͺ π‘₯ ∈ 𝐴 𝐡
ciin 3888class ∩ π‘₯ ∈ 𝐴 𝐡
df-iun 3889βˆͺ π‘₯ ∈ 𝐴 𝐡 = {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 ∈ 𝐡}
df-iin 3890∩ π‘₯ ∈ 𝐴 𝐡 = {𝑦 ∣ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ 𝐡}
wdisj 3981wff Disj π‘₯ ∈ 𝐴 𝐡
df-disj 3982(Disj π‘₯ ∈ 𝐴 𝐡 ↔ βˆ€π‘¦βˆƒ*π‘₯ ∈ 𝐴 𝑦 ∈ 𝐡)
wbr 4004wff 𝐴𝑅𝐡
df-br 4005(𝐴𝑅𝐡 ↔ ⟨𝐴, 𝐡⟩ ∈ 𝑅)
copab 4064class {⟨π‘₯, π‘¦βŸ© ∣ πœ‘}
cmpt 4065class (π‘₯ ∈ 𝐴 ↦ 𝐡)
df-opab 4066{⟨π‘₯, π‘¦βŸ© ∣ πœ‘} = {𝑧 ∣ βˆƒπ‘₯βˆƒπ‘¦(𝑧 = ⟨π‘₯, π‘¦βŸ© ∧ πœ‘)}
df-mpt 4067(π‘₯ ∈ 𝐴 ↦ 𝐡) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐡)}
wtr 4102wff Tr 𝐴
df-tr 4103(Tr 𝐴 ↔ βˆͺ 𝐴 βŠ† 𝐴)
ax-coll 4119β„²π‘πœ‘    β‡’   (βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦πœ‘ β†’ βˆƒπ‘βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦ ∈ 𝑏 πœ‘)
ax-sep 4122βˆƒπ‘¦βˆ€π‘₯(π‘₯ ∈ 𝑦 ↔ (π‘₯ ∈ 𝑧 ∧ πœ‘))
ax-nul 4130βˆƒπ‘₯βˆ€π‘¦ Β¬ 𝑦 ∈ π‘₯
ax-pow 4175βˆƒπ‘¦βˆ€π‘§(βˆ€π‘€(𝑀 ∈ 𝑧 β†’ 𝑀 ∈ π‘₯) β†’ 𝑧 ∈ 𝑦)
wem 4195wff EXMID
df-exmid 4196(EXMID ↔ βˆ€π‘₯(π‘₯ βŠ† {βˆ…} β†’ DECID βˆ… ∈ π‘₯))
ax-pr 4210βˆƒπ‘§βˆ€π‘€((𝑀 = π‘₯ ∨ 𝑀 = 𝑦) β†’ 𝑀 ∈ 𝑧)
cep 4288class E
cid 4289class I
df-eprel 4290 E = {⟨π‘₯, π‘¦βŸ© ∣ π‘₯ ∈ 𝑦}
df-id 4294 I = {⟨π‘₯, π‘¦βŸ© ∣ π‘₯ = 𝑦}
wpo 4295wff 𝑅 Po 𝐴
wor 4296wff 𝑅 Or 𝐴
df-po 4297(𝑅 Po 𝐴 ↔ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘§ ∈ 𝐴 (Β¬ π‘₯𝑅π‘₯ ∧ ((π‘₯𝑅𝑦 ∧ 𝑦𝑅𝑧) β†’ π‘₯𝑅𝑧)))
df-iso 4298(𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘§ ∈ 𝐴 (π‘₯𝑅𝑦 β†’ (π‘₯𝑅𝑧 ∨ 𝑧𝑅𝑦))))
wfrfor 4328wff FrFor 𝑅𝐴𝑆
wfr 4329wff 𝑅 Fr 𝐴
wse 4330wff 𝑅 Se 𝐴
wwe 4331wff 𝑅 We 𝐴
df-frfor 4332( FrFor 𝑅𝐴𝑆 ↔ (βˆ€π‘₯ ∈ 𝐴 (βˆ€π‘¦ ∈ 𝐴 (𝑦𝑅π‘₯ β†’ 𝑦 ∈ 𝑆) β†’ π‘₯ ∈ 𝑆) β†’ 𝐴 βŠ† 𝑆))
df-frind 4333(𝑅 Fr 𝐴 ↔ βˆ€π‘  FrFor 𝑅𝐴𝑠)
df-se 4334(𝑅 Se 𝐴 ↔ βˆ€π‘₯ ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅π‘₯} ∈ V)
df-wetr 4335(𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘§ ∈ 𝐴 ((π‘₯𝑅𝑦 ∧ 𝑦𝑅𝑧) β†’ π‘₯𝑅𝑧)))
word 4363wff Ord 𝐴
con0 4364class On
wlim 4365wff Lim 𝐴
csuc 4366class suc 𝐴
df-iord 4367(Ord 𝐴 ↔ (Tr 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 Tr π‘₯))
df-on 4369On = {π‘₯ ∣ Ord π‘₯}
df-ilim 4370(Lim 𝐴 ↔ (Ord 𝐴 ∧ βˆ… ∈ 𝐴 ∧ 𝐴 = βˆͺ 𝐴))
df-suc 4372suc 𝐴 = (𝐴 βˆͺ {𝐴})
ax-un 4434βˆƒπ‘¦βˆ€π‘§(βˆƒπ‘€(𝑧 ∈ 𝑀 ∧ 𝑀 ∈ π‘₯) β†’ 𝑧 ∈ 𝑦)
ax-setind 4537(βˆ€π‘Ž(βˆ€π‘¦ ∈ π‘Ž [𝑦 / π‘Ž]πœ‘ β†’ πœ‘) β†’ βˆ€π‘Žπœ‘)
ax-iinf 4588βˆƒπ‘₯(βˆ… ∈ π‘₯ ∧ βˆ€π‘¦(𝑦 ∈ π‘₯ β†’ suc 𝑦 ∈ π‘₯))
com 4590class Ο‰
df-iom 4591Ο‰ = ∩ {π‘₯ ∣ (βˆ… ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ suc 𝑦 ∈ π‘₯)}
cxp 4625class (𝐴 Γ— 𝐡)
ccnv 4626class ◑𝐴
cdm 4627class dom 𝐴
crn 4628class ran 𝐴
cres 4629class (𝐴 β†Ύ 𝐡)
cima 4630class (𝐴 β€œ 𝐡)
ccom 4631class (𝐴 ∘ 𝐡)
wrel 4632wff Rel 𝐴
df-xp 4633(𝐴 Γ— 𝐡) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐡)}
df-rel 4634(Rel 𝐴 ↔ 𝐴 βŠ† (V Γ— V))
df-cnv 4635◑𝐴 = {⟨π‘₯, π‘¦βŸ© ∣ 𝑦𝐴π‘₯}
df-co 4636(𝐴 ∘ 𝐡) = {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘§(π‘₯𝐡𝑧 ∧ 𝑧𝐴𝑦)}
df-dm 4637dom 𝐴 = {π‘₯ ∣ βˆƒπ‘¦ π‘₯𝐴𝑦}
df-rn 4638ran 𝐴 = dom ◑𝐴
df-res 4639(𝐴 β†Ύ 𝐡) = (𝐴 ∩ (𝐡 Γ— V))
df-ima 4640(𝐴 β€œ 𝐡) = ran (𝐴 β†Ύ 𝐡)
cio 5177class (β„©π‘₯πœ‘)
df-iota 5179(β„©π‘₯πœ‘) = βˆͺ {𝑦 ∣ {π‘₯ ∣ πœ‘} = {𝑦}}
wfun 5211wff Fun 𝐴
wfn 5212wff 𝐴 Fn 𝐡
wf 5213wff 𝐹:𝐴⟢𝐡
wf1 5214wff 𝐹:𝐴–1-1→𝐡
wfo 5215wff 𝐹:𝐴–onto→𝐡
wf1o 5216wff 𝐹:𝐴–1-1-onto→𝐡
cfv 5217class (πΉβ€˜π΄)
wiso 5218wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐡)
df-fun 5219(Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◑𝐴) βŠ† I ))
df-fn 5220(𝐴 Fn 𝐡 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐡))
df-f 5221(𝐹:𝐴⟢𝐡 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 βŠ† 𝐡))
df-f1 5222(𝐹:𝐴–1-1→𝐡 ↔ (𝐹:𝐴⟢𝐡 ∧ Fun ◑𝐹))
df-fo 5223(𝐹:𝐴–onto→𝐡 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐡))
df-f1o 5224(𝐹:𝐴–1-1-onto→𝐡 ↔ (𝐹:𝐴–1-1→𝐡 ∧ 𝐹:𝐴–onto→𝐡))
df-fv 5225(πΉβ€˜π΄) = (β„©π‘₯𝐴𝐹π‘₯)
df-isom 5226(𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐡) ↔ (𝐻:𝐴–1-1-onto→𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯𝑅𝑦 ↔ (π»β€˜π‘₯)𝑆(π»β€˜π‘¦))))
crio 5830class (β„©π‘₯ ∈ 𝐴 πœ‘)
df-riota 5831(β„©π‘₯ ∈ 𝐴 πœ‘) = (β„©π‘₯(π‘₯ ∈ 𝐴 ∧ πœ‘))
co 5875class (𝐴𝐹𝐡)
coprab 5876class {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ πœ‘}
cmpo 5877class (π‘₯ ∈ 𝐴, 𝑦 ∈ 𝐡 ↦ 𝐢)
df-ov 5878(𝐴𝐹𝐡) = (πΉβ€˜βŸ¨π΄, 𝐡⟩)
df-oprab 5879{⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ πœ‘} = {𝑀 ∣ βˆƒπ‘₯βˆƒπ‘¦βˆƒπ‘§(𝑀 = ⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∧ πœ‘)}
df-mpo 5880(π‘₯ ∈ 𝐴, 𝑦 ∈ 𝐡 ↦ 𝐢) = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 = 𝐢)}
cof 6081class βˆ˜π‘“ 𝑅
cofr 6082class βˆ˜π‘Ÿ 𝑅
df-of 6083 βˆ˜π‘“ 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (π‘₯ ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((π‘“β€˜π‘₯)𝑅(π‘”β€˜π‘₯))))
df-ofr 6084 βˆ˜π‘Ÿ 𝑅 = {βŸ¨π‘“, π‘”βŸ© ∣ βˆ€π‘₯ ∈ (dom 𝑓 ∩ dom 𝑔)(π‘“β€˜π‘₯)𝑅(π‘”β€˜π‘₯)}
c1st 6139class 1st
c2nd 6140class 2nd
df-1st 61411st = (π‘₯ ∈ V ↦ βˆͺ dom {π‘₯})
df-2nd 61422nd = (π‘₯ ∈ V ↦ βˆͺ ran {π‘₯})
ctpos 6245class tpos 𝐹
df-tpos 6246tpos 𝐹 = (𝐹 ∘ (π‘₯ ∈ (β—‘dom 𝐹 βˆͺ {βˆ…}) ↦ βˆͺ β—‘{π‘₯}))
wsmo 6286wff Smo 𝐴
df-smo 6287(Smo 𝐴 ↔ (𝐴:dom 𝐴⟢On ∧ Ord dom 𝐴 ∧ βˆ€π‘₯ ∈ dom π΄βˆ€π‘¦ ∈ dom 𝐴(π‘₯ ∈ 𝑦 β†’ (π΄β€˜π‘₯) ∈ (π΄β€˜π‘¦))))
crecs 6305class recs(𝐹)
df-recs 6306recs(𝐹) = βˆͺ {𝑓 ∣ βˆƒπ‘₯ ∈ On (𝑓 Fn π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (π‘“β€˜π‘¦) = (πΉβ€˜(𝑓 β†Ύ 𝑦)))}
crdg 6370class rec(𝐹, 𝐼)
df-irdg 6371rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 βˆͺ βˆͺ π‘₯ ∈ dom 𝑔(πΉβ€˜(π‘”β€˜π‘₯)))))
cfrec 6391class frec(𝐹, 𝐼)
df-frec 6392frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {π‘₯ ∣ (βˆƒπ‘š ∈ Ο‰ (dom 𝑔 = suc π‘š ∧ π‘₯ ∈ (πΉβ€˜(π‘”β€˜π‘š))) ∨ (dom 𝑔 = βˆ… ∧ π‘₯ ∈ 𝐼))})) β†Ύ Ο‰)
c1o 6410class 1o
c2o 6411class 2o
c3o 6412class 3o
c4o 6413class 4o
coa 6414class +o
comu 6415class Β·o
coei 6416class ↑o
df-1o 64171o = suc βˆ…
df-2o 64182o = suc 1o
df-3o 64193o = suc 2o
df-4o 64204o = suc 3o
df-oadd 6421 +o = (π‘₯ ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), π‘₯)β€˜π‘¦))
df-omul 6422 Β·o = (π‘₯ ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o π‘₯)), βˆ…)β€˜π‘¦))
df-oexpi 6423 ↑o = (π‘₯ ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 Β·o π‘₯)), 1o)β€˜π‘¦))
wer 6532wff 𝑅 Er 𝐴
cec 6533class [𝐴]𝑅
cqs 6534class (𝐴 / 𝑅)
df-er 6535(𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◑𝑅 βˆͺ (𝑅 ∘ 𝑅)) βŠ† 𝑅))
df-ec 6537[𝐴]𝑅 = (𝑅 β€œ {𝐴})
df-qs 6541(𝐴 / 𝑅) = {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = [π‘₯]𝑅}
cmap 6648class β†‘π‘š
cpm 6649class ↑pm
df-map 6650 β†‘π‘š = (π‘₯ ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:π‘¦βŸΆπ‘₯})
df-pm 6651 ↑pm = (π‘₯ ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 Γ— π‘₯) ∣ Fun 𝑓})
cixp 6698class Xπ‘₯ ∈ 𝐴 𝐡
df-ixp 6699Xπ‘₯ ∈ 𝐴 𝐡 = {𝑓 ∣ (𝑓 Fn {π‘₯ ∣ π‘₯ ∈ 𝐴} ∧ βˆ€π‘₯ ∈ 𝐴 (π‘“β€˜π‘₯) ∈ 𝐡)}
cen 6738class β‰ˆ
cdom 6739class β‰Ό
cfn 6740class Fin
df-en 6741 β‰ˆ = {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ 𝑓:π‘₯–1-1-onto→𝑦}
df-dom 6742 β‰Ό = {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ 𝑓:π‘₯–1-1→𝑦}
df-fin 6743Fin = {π‘₯ ∣ βˆƒπ‘¦ ∈ Ο‰ π‘₯ β‰ˆ 𝑦}
cfi 6967class fi
df-fi 6968fi = (π‘₯ ∈ V ↦ {𝑧 ∣ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑧 = ∩ 𝑦})
csup 6981class sup(𝐴, 𝐡, 𝑅)
cinf 6982class inf(𝐴, 𝐡, 𝑅)
df-sup 6983sup(𝐴, 𝐡, 𝑅) = βˆͺ {π‘₯ ∈ 𝐡 ∣ (βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯𝑅𝑦 ∧ βˆ€π‘¦ ∈ 𝐡 (𝑦𝑅π‘₯ β†’ βˆƒπ‘§ ∈ 𝐴 𝑦𝑅𝑧))}
df-inf 6984inf(𝐴, 𝐡, 𝑅) = sup(𝐴, 𝐡, ◑𝑅)
cdju 7036class (𝐴 βŠ” 𝐡)
df-dju 7037(𝐴 βŠ” 𝐡) = (({βˆ…} Γ— 𝐴) βˆͺ ({1o} Γ— 𝐡))
cinl 7044class inl
cinr 7045class inr
df-inl 7046inl = (π‘₯ ∈ V ↦ βŸ¨βˆ…, π‘₯⟩)
df-inr 7047inr = (π‘₯ ∈ V ↦ ⟨1o, π‘₯⟩)
cdjucase 7082class case(𝑅, 𝑆)
df-case 7083case(𝑅, 𝑆) = ((𝑅 ∘ β—‘inl) βˆͺ (𝑆 ∘ β—‘inr))
cdjud 7101class (𝑅 βŠ”d 𝑆)
df-djud 7102(𝑅 βŠ”d 𝑆) = ((𝑅 ∘ β—‘(inl β†Ύ dom 𝑅)) βˆͺ (𝑆 ∘ β—‘(inr β†Ύ dom 𝑆)))
xnninf 7118class β„•βˆž
df-nninf 7119β„•βˆž = {𝑓 ∈ (2o β†‘π‘š Ο‰) ∣ βˆ€π‘– ∈ Ο‰ (π‘“β€˜suc 𝑖) βŠ† (π‘“β€˜π‘–)}
comni 7132class Omni
df-omni 7133Omni = {𝑦 ∣ βˆ€π‘“(𝑓:π‘¦βŸΆ2o β†’ (βˆƒπ‘₯ ∈ 𝑦 (π‘“β€˜π‘₯) = βˆ… ∨ βˆ€π‘₯ ∈ 𝑦 (π‘“β€˜π‘₯) = 1o))}
cmarkov 7149class Markov
df-markov 7150Markov = {𝑦 ∣ βˆ€π‘“(𝑓:π‘¦βŸΆ2o β†’ (Β¬ βˆ€π‘₯ ∈ 𝑦 (π‘“β€˜π‘₯) = 1o β†’ βˆƒπ‘₯ ∈ 𝑦 (π‘“β€˜π‘₯) = βˆ…))}
cwomni 7161class WOmni
df-womni 7162WOmni = {𝑦 ∣ βˆ€π‘“(𝑓:π‘¦βŸΆ2o β†’ DECID βˆ€π‘₯ ∈ 𝑦 (π‘“β€˜π‘₯) = 1o)}
ccrd 7178class card
df-card 7179card = (π‘₯ ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑦 β‰ˆ π‘₯})
wac 7204wff CHOICE
df-ac 7205(CHOICE ↔ βˆ€π‘₯βˆƒπ‘“(𝑓 βŠ† π‘₯ ∧ 𝑓 Fn dom π‘₯))
wap 7246wff 𝑅 Ap 𝐴
df-pap 7247(𝑅 Ap 𝐴 ↔ ((𝑅 βŠ† (𝐴 Γ— 𝐴) ∧ βˆ€π‘₯ ∈ 𝐴 Β¬ π‘₯𝑅π‘₯) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯𝑅𝑦 β†’ 𝑦𝑅π‘₯) ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘§ ∈ 𝐴 (π‘₯𝑅𝑦 β†’ (π‘₯𝑅𝑧 ∨ 𝑦𝑅𝑧)))))
wtap 7248wff 𝑅 TAp 𝐴
df-tap 7249(𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (Β¬ π‘₯𝑅𝑦 β†’ π‘₯ = 𝑦)))
wacc 7261wff CCHOICE
df-cc 7262(CCHOICE ↔ βˆ€π‘₯(dom π‘₯ β‰ˆ Ο‰ β†’ βˆƒπ‘“(𝑓 βŠ† π‘₯ ∧ 𝑓 Fn dom π‘₯)))
cnpi 7271class N
cpli 7272class +N
cmi 7273class Β·N
clti 7274class <N
cplpq 7275class +pQ
cmpq 7276class Β·pQ
cltpq 7277class <pQ
ceq 7278class ~Q
cnq 7279class Q
c1q 7280class 1Q
cplq 7281class +Q
cmq 7282class Β·Q
crq 7283class *Q
cltq 7284class <Q
ceq0 7285class ~Q0
cnq0 7286class Q0
c0q0 7287class 0Q0
cplq0 7288class +Q0
cmq0 7289class Β·Q0
cnp 7290class P
c1p 7291class 1P
cpp 7292class +P
cmp 7293class Β·P
cltp 7294class <P
cer 7295class ~R
cnr 7296class R
c0r 7297class 0R
c1r 7298class 1R
cm1r 7299class -1R
cplr 7300class +R
cmr 7301class Β·R
cltr 7302class <R
df-ni 7303N = (Ο‰ βˆ– {βˆ…})
df-pli 7304 +N = ( +o β†Ύ (N Γ— N))
df-mi 7305 Β·N = ( Β·o β†Ύ (N Γ— N))
df-lti 7306 <N = ( E ∩ (N Γ— N))
df-plpq 7343 +pQ = (π‘₯ ∈ (N Γ— N), 𝑦 ∈ (N Γ— N) ↦ ⟨(((1st β€˜π‘₯) Β·N (2nd β€˜π‘¦)) +N ((1st β€˜π‘¦) Β·N (2nd β€˜π‘₯))), ((2nd β€˜π‘₯) Β·N (2nd β€˜π‘¦))⟩)
df-mpq 7344 Β·pQ = (π‘₯ ∈ (N Γ— N), 𝑦 ∈ (N Γ— N) ↦ ⟨((1st β€˜π‘₯) Β·N (1st β€˜π‘¦)), ((2nd β€˜π‘₯) Β·N (2nd β€˜π‘¦))⟩)
df-ltpq 7345 <pQ = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (N Γ— N) ∧ 𝑦 ∈ (N Γ— N)) ∧ ((1st β€˜π‘₯) Β·N (2nd β€˜π‘¦)) <N ((1st β€˜π‘¦) Β·N (2nd β€˜π‘₯)))}
df-enq 7346 ~Q = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (N Γ— N) ∧ 𝑦 ∈ (N Γ— N)) ∧ βˆƒπ‘§βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’((π‘₯ = βŸ¨π‘§, π‘€βŸ© ∧ 𝑦 = βŸ¨π‘£, π‘’βŸ©) ∧ (𝑧 Β·N 𝑒) = (𝑀 Β·N 𝑣)))}
df-nqqs 7347Q = ((N Γ— N) / ~Q )
df-plqqs 7348 +Q = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ Q ∧ 𝑦 ∈ Q) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~Q ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~Q ) ∧ 𝑧 = [(βŸ¨π‘€, π‘£βŸ© +pQ βŸ¨π‘’, π‘“βŸ©)] ~Q ))}
df-mqqs 7349 Β·Q = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ Q ∧ 𝑦 ∈ Q) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~Q ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~Q ) ∧ 𝑧 = [(βŸ¨π‘€, π‘£βŸ© Β·pQ βŸ¨π‘’, π‘“βŸ©)] ~Q ))}
df-1nqqs 73501Q = [⟨1o, 1o⟩] ~Q
df-rq 7351*Q = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ Q ∧ 𝑦 ∈ Q ∧ (π‘₯ Β·Q 𝑦) = 1Q)}
df-ltnqqs 7352 <Q = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ Q ∧ 𝑦 ∈ Q) ∧ βˆƒπ‘§βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’((π‘₯ = [βŸ¨π‘§, π‘€βŸ©] ~Q ∧ 𝑦 = [βŸ¨π‘£, π‘’βŸ©] ~Q ) ∧ (𝑧 Β·N 𝑒) <N (𝑀 Β·N 𝑣)))}
df-enq0 7423 ~Q0 = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (Ο‰ Γ— N) ∧ 𝑦 ∈ (Ο‰ Γ— N)) ∧ βˆƒπ‘§βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’((π‘₯ = βŸ¨π‘§, π‘€βŸ© ∧ 𝑦 = βŸ¨π‘£, π‘’βŸ©) ∧ (𝑧 Β·o 𝑒) = (𝑀 Β·o 𝑣)))}
df-nq0 7424Q0 = ((Ο‰ Γ— N) / ~Q0 )
df-0nq0 74250Q0 = [βŸ¨βˆ…, 1o⟩] ~Q0
df-plq0 7426 +Q0 = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~Q0 ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~Q0 ) ∧ 𝑧 = [⟨((𝑀 Β·o 𝑓) +o (𝑣 Β·o 𝑒)), (𝑣 Β·o 𝑓)⟩] ~Q0 ))}
df-mq0 7427 Β·Q0 = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~Q0 ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~Q0 ) ∧ 𝑧 = [⟨(𝑀 Β·o 𝑒), (𝑣 Β·o 𝑓)⟩] ~Q0 ))}
df-inp 7465P = {βŸ¨π‘™, π‘’βŸ© ∣ (((𝑙 βŠ† Q ∧ 𝑒 βŠ† Q) ∧ (βˆƒπ‘ž ∈ Q π‘ž ∈ 𝑙 ∧ βˆƒπ‘Ÿ ∈ Q π‘Ÿ ∈ 𝑒)) ∧ ((βˆ€π‘ž ∈ Q (π‘ž ∈ 𝑙 ↔ βˆƒπ‘Ÿ ∈ Q (π‘ž <Q π‘Ÿ ∧ π‘Ÿ ∈ 𝑙)) ∧ βˆ€π‘Ÿ ∈ Q (π‘Ÿ ∈ 𝑒 ↔ βˆƒπ‘ž ∈ Q (π‘ž <Q π‘Ÿ ∧ π‘ž ∈ 𝑒))) ∧ βˆ€π‘ž ∈ Q Β¬ (π‘ž ∈ 𝑙 ∧ π‘ž ∈ 𝑒) ∧ βˆ€π‘ž ∈ Q βˆ€π‘Ÿ ∈ Q (π‘ž <Q π‘Ÿ β†’ (π‘ž ∈ 𝑙 ∨ π‘Ÿ ∈ 𝑒))))}
df-i1p 74661P = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑒 ∣ 1Q <Q 𝑒}⟩
df-iplp 7467 +P = (π‘₯ ∈ P, 𝑦 ∈ P ↦ ⟨{π‘ž ∈ Q ∣ βˆƒπ‘Ÿ ∈ Q βˆƒπ‘  ∈ Q (π‘Ÿ ∈ (1st β€˜π‘₯) ∧ 𝑠 ∈ (1st β€˜π‘¦) ∧ π‘ž = (π‘Ÿ +Q 𝑠))}, {π‘ž ∈ Q ∣ βˆƒπ‘Ÿ ∈ Q βˆƒπ‘  ∈ Q (π‘Ÿ ∈ (2nd β€˜π‘₯) ∧ 𝑠 ∈ (2nd β€˜π‘¦) ∧ π‘ž = (π‘Ÿ +Q 𝑠))}⟩)
df-imp 7468 Β·P = (π‘₯ ∈ P, 𝑦 ∈ P ↦ ⟨{π‘ž ∈ Q ∣ βˆƒπ‘Ÿ ∈ Q βˆƒπ‘  ∈ Q (π‘Ÿ ∈ (1st β€˜π‘₯) ∧ 𝑠 ∈ (1st β€˜π‘¦) ∧ π‘ž = (π‘Ÿ Β·Q 𝑠))}, {π‘ž ∈ Q ∣ βˆƒπ‘Ÿ ∈ Q βˆƒπ‘  ∈ Q (π‘Ÿ ∈ (2nd β€˜π‘₯) ∧ 𝑠 ∈ (2nd β€˜π‘¦) ∧ π‘ž = (π‘Ÿ Β·Q 𝑠))}⟩)
df-iltp 7469<P = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ P ∧ 𝑦 ∈ P) ∧ βˆƒπ‘ž ∈ Q (π‘ž ∈ (2nd β€˜π‘₯) ∧ π‘ž ∈ (1st β€˜π‘¦)))}
df-enr 7725 ~R = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (P Γ— P) ∧ 𝑦 ∈ (P Γ— P)) ∧ βˆƒπ‘§βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’((π‘₯ = βŸ¨π‘§, π‘€βŸ© ∧ 𝑦 = βŸ¨π‘£, π‘’βŸ©) ∧ (𝑧 +P 𝑒) = (𝑀 +P 𝑣)))}
df-nr 7726R = ((P Γ— P) / ~R )
df-plr 7727 +R = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ R ∧ 𝑦 ∈ R) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~R ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~R ) ∧ 𝑧 = [⟨(𝑀 +P 𝑒), (𝑣 +P 𝑓)⟩] ~R ))}
df-mr 7728 Β·R = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ R ∧ 𝑦 ∈ R) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~R ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~R ) ∧ 𝑧 = [⟨((𝑀 Β·P 𝑒) +P (𝑣 Β·P 𝑓)), ((𝑀 Β·P 𝑓) +P (𝑣 Β·P 𝑒))⟩] ~R ))}
df-ltr 7729 <R = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ R ∧ 𝑦 ∈ R) ∧ βˆƒπ‘§βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’((π‘₯ = [βŸ¨π‘§, π‘€βŸ©] ~R ∧ 𝑦 = [βŸ¨π‘£, π‘’βŸ©] ~R ) ∧ (𝑧 +P 𝑒)<P (𝑀 +P 𝑣)))}
df-0r 77300R = [⟨1P, 1P⟩] ~R
df-1r 77311R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 7732-1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 7809class β„‚
cr 7810class ℝ
cc0 7811class 0
c1 7812class 1
ci 7813class i
caddc 7814class +
cltrr 7815class <ℝ
cmul 7816class Β·
df-c 7817β„‚ = (R Γ— R)
df-0 78180 = ⟨0R, 0R⟩
df-1 78191 = ⟨1R, 0R⟩
df-i 7820i = ⟨0R, 1R⟩
df-r 7821ℝ = (R Γ— {0R})
df-add 7822 + = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = βŸ¨π‘€, π‘£βŸ© ∧ 𝑦 = βŸ¨π‘’, π‘“βŸ©) ∧ 𝑧 = ⟨(𝑀 +R 𝑒), (𝑣 +R 𝑓)⟩))}
df-mul 7823 Β· = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = βŸ¨π‘€, π‘£βŸ© ∧ 𝑦 = βŸ¨π‘’, π‘“βŸ©) ∧ 𝑧 = ⟨((𝑀 Β·R 𝑒) +R (-1R Β·R (𝑣 Β·R 𝑓))), ((𝑣 Β·R 𝑒) +R (𝑀 Β·R 𝑓))⟩))}
df-lt 7824 <ℝ = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ βˆƒπ‘§βˆƒπ‘€((π‘₯ = βŸ¨π‘§, 0R⟩ ∧ 𝑦 = βŸ¨π‘€, 0R⟩) ∧ 𝑧 <R 𝑀))}
ax-cnex 7902β„‚ ∈ V
ax-resscn 7903ℝ βŠ† β„‚
ax-1cn 79041 ∈ β„‚
ax-1re 79051 ∈ ℝ
ax-icn 7906i ∈ β„‚
ax-addcl 7907((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 + 𝐡) ∈ β„‚)
ax-addrcl 7908((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴 + 𝐡) ∈ ℝ)
ax-mulcl 7909((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 Β· 𝐡) ∈ β„‚)
ax-mulrcl 7910((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴 Β· 𝐡) ∈ ℝ)
ax-addcom 7911((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 + 𝐡) = (𝐡 + 𝐴))
ax-mulcom 7912((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 Β· 𝐡) = (𝐡 Β· 𝐴))
ax-addass 7913((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐴 + 𝐡) + 𝐢) = (𝐴 + (𝐡 + 𝐢)))
ax-mulass 7914((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐴 Β· 𝐡) Β· 𝐢) = (𝐴 Β· (𝐡 Β· 𝐢)))
ax-distr 7915((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ (𝐴 Β· (𝐡 + 𝐢)) = ((𝐴 Β· 𝐡) + (𝐴 Β· 𝐢)))
ax-i2m1 7916((i Β· i) + 1) = 0
ax-0lt1 79170 <ℝ 1
ax-1rid 7918(𝐴 ∈ ℝ β†’ (𝐴 Β· 1) = 𝐴)
ax-0id 7919(𝐴 ∈ β„‚ β†’ (𝐴 + 0) = 𝐴)
ax-rnegex 7920(𝐴 ∈ ℝ β†’ βˆƒπ‘₯ ∈ ℝ (𝐴 + π‘₯) = 0)
ax-precex 7921((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) β†’ βˆƒπ‘₯ ∈ ℝ (0 <ℝ π‘₯ ∧ (𝐴 Β· π‘₯) = 1))
ax-cnre 7922(𝐴 ∈ β„‚ β†’ βˆƒπ‘₯ ∈ ℝ βˆƒπ‘¦ ∈ ℝ 𝐴 = (π‘₯ + (i Β· 𝑦)))
ax-pre-ltirr 7923(𝐴 ∈ ℝ β†’ Β¬ 𝐴 <ℝ 𝐴)
ax-pre-ltwlin 7924((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ (𝐴 <ℝ 𝐡 β†’ (𝐴 <ℝ 𝐢 ∨ 𝐢 <ℝ 𝐡)))
ax-pre-lttrn 7925((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ ((𝐴 <ℝ 𝐡 ∧ 𝐡 <ℝ 𝐢) β†’ 𝐴 <ℝ 𝐢))
ax-pre-apti 7926((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ Β¬ (𝐴 <ℝ 𝐡 ∨ 𝐡 <ℝ 𝐴)) β†’ 𝐴 = 𝐡)
ax-pre-ltadd 7927((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ (𝐴 <ℝ 𝐡 β†’ (𝐢 + 𝐴) <ℝ (𝐢 + 𝐡)))
ax-pre-mulgt0 7928((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐡) β†’ 0 <ℝ (𝐴 Β· 𝐡)))
ax-pre-mulext 7929((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ ((𝐴 Β· 𝐢) <ℝ (𝐡 Β· 𝐢) β†’ (𝐴 <ℝ 𝐡 ∨ 𝐡 <ℝ 𝐴)))
ax-arch 7930(𝐴 ∈ ℝ β†’ βˆƒπ‘› ∈ ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}𝐴 <ℝ 𝑛)
ax-caucvg 7931𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    &   (πœ‘ β†’ 𝐹:π‘βŸΆβ„)    &   (πœ‘ β†’ βˆ€π‘› ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑛 <ℝ π‘˜ β†’ ((πΉβ€˜π‘›) <ℝ ((πΉβ€˜π‘˜) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)) ∧ (πΉβ€˜π‘˜) <ℝ ((πΉβ€˜π‘›) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)))))    β‡’   (πœ‘ β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘₯ ∈ ℝ (0 <ℝ π‘₯ β†’ βˆƒπ‘— ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯)))))
ax-pre-suploc 7932(((𝐴 βŠ† ℝ ∧ βˆƒπ‘₯ π‘₯ ∈ 𝐴) ∧ (βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ 𝐴 𝑦 <ℝ π‘₯ ∧ βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ <ℝ 𝑦 β†’ (βˆƒπ‘§ ∈ 𝐴 π‘₯ <ℝ 𝑧 ∨ βˆ€π‘§ ∈ 𝐴 𝑧 <ℝ 𝑦)))) β†’ βˆƒπ‘₯ ∈ ℝ (βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <ℝ 𝑦 ∧ βˆ€π‘¦ ∈ ℝ (𝑦 <ℝ π‘₯ β†’ βˆƒπ‘§ ∈ 𝐴 𝑦 <ℝ 𝑧)))
ax-addf 7933 + :(β„‚ Γ— β„‚)βŸΆβ„‚
ax-mulf 7934 Β· :(β„‚ Γ— β„‚)βŸΆβ„‚
cpnf 7989class +∞
cmnf 7990class -∞
cxr 7991class ℝ*
clt 7992class <
cle 7993class ≀
df-pnf 7994+∞ = 𝒫 βˆͺ β„‚
df-mnf 7995-∞ = 𝒫 +∞
df-xr 7996ℝ* = (ℝ βˆͺ {+∞, -∞})
df-ltxr 7997 < = ({⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ π‘₯ <ℝ 𝑦)} βˆͺ (((ℝ βˆͺ {-∞}) Γ— {+∞}) βˆͺ ({-∞} Γ— ℝ)))
df-le 7998 ≀ = ((ℝ* Γ— ℝ*) βˆ– β—‘ < )
cmin 8128class βˆ’
cneg 8129class -𝐴
df-sub 8130 βˆ’ = (π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (℩𝑧 ∈ β„‚ (𝑦 + 𝑧) = π‘₯))
df-neg 8131-𝐴 = (0 βˆ’ 𝐴)
creap 8531class #ℝ
df-reap 8532 #ℝ = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (π‘₯ < 𝑦 ∨ 𝑦 < π‘₯))}
cap 8538class #
df-ap 8539 # = {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘Ÿ ∈ ℝ βˆƒπ‘  ∈ ℝ βˆƒπ‘‘ ∈ ℝ βˆƒπ‘’ ∈ ℝ ((π‘₯ = (π‘Ÿ + (i Β· 𝑠)) ∧ 𝑦 = (𝑑 + (i Β· 𝑒))) ∧ (π‘Ÿ #ℝ 𝑑 ∨ 𝑠 #ℝ 𝑒))}
cdiv 8629class /
df-div 8630 / = (π‘₯ ∈ β„‚, 𝑦 ∈ (β„‚ βˆ– {0}) ↦ (℩𝑧 ∈ β„‚ (𝑦 Β· 𝑧) = π‘₯))
cn 8919class β„•
df-inn 8920β„• = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}
c2 8970class 2
c3 8971class 3
c4 8972class 4
c5 8973class 5
c6 8974class 6
c7 8975class 7
c8 8976class 8
c9 8977class 9
df-2 89782 = (1 + 1)
df-3 89793 = (2 + 1)
df-4 89804 = (3 + 1)
df-5 89815 = (4 + 1)
df-6 89826 = (5 + 1)
df-7 89837 = (6 + 1)
df-8 89848 = (7 + 1)
df-9 89859 = (8 + 1)
cn0 9176class β„•0
df-n0 9177β„•0 = (β„• βˆͺ {0})
cxnn0 9239class β„•0*
df-xnn0 9240β„•0* = (β„•0 βˆͺ {+∞})
cz 9253class β„€
df-z 9254β„€ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ β„• ∨ -𝑛 ∈ β„•)}
cdc 9384class 𝐴𝐡
df-dec 9385𝐴𝐡 = (((9 + 1) Β· 𝐴) + 𝐡)
cuz 9528class β„€β‰₯
df-uz 9529β„€β‰₯ = (𝑗 ∈ β„€ ↦ {π‘˜ ∈ β„€ ∣ 𝑗 ≀ π‘˜})
cq 9619class β„š
df-q 9620β„š = ( / β€œ (β„€ Γ— β„•))
crp 9653class ℝ+
df-rp 9654ℝ+ = {π‘₯ ∈ ℝ ∣ 0 < π‘₯}
cxne 9769class -𝑒𝐴
cxad 9770class +𝑒
cxmu 9771class Β·e
df-xneg 9772-𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
df-xadd 9773 +𝑒 = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(π‘₯ = +∞, if(𝑦 = -∞, 0, +∞), if(π‘₯ = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (π‘₯ + 𝑦))))))
df-xmul 9774 Β·e = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((π‘₯ = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ π‘₯ = +∞) ∨ (𝑦 < 0 ∧ π‘₯ = -∞)) ∨ ((0 < π‘₯ ∧ 𝑦 = +∞) ∨ (π‘₯ < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ π‘₯ = -∞) ∨ (𝑦 < 0 ∧ π‘₯ = +∞)) ∨ ((0 < π‘₯ ∧ 𝑦 = -∞) ∨ (π‘₯ < 0 ∧ 𝑦 = +∞))), -∞, (π‘₯ Β· 𝑦)))))
cioo 9888class (,)
cioc 9889class (,]
cico 9890class [,)
cicc 9891class [,]
df-ioo 9892(,) = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (π‘₯ < 𝑧 ∧ 𝑧 < 𝑦)})
df-ioc 9893(,] = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (π‘₯ < 𝑧 ∧ 𝑧 ≀ 𝑦)})
df-ico 9894[,) = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (π‘₯ ≀ 𝑧 ∧ 𝑧 < 𝑦)})
df-icc 9895[,] = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (π‘₯ ≀ 𝑧 ∧ 𝑧 ≀ 𝑦)})
cfz 10008class ...
df-fz 10009... = (π‘š ∈ β„€, 𝑛 ∈ β„€ ↦ {π‘˜ ∈ β„€ ∣ (π‘š ≀ π‘˜ ∧ π‘˜ ≀ 𝑛)})
cfzo 10142class ..^
df-fzo 10143..^ = (π‘š ∈ β„€, 𝑛 ∈ β„€ ↦ (π‘š...(𝑛 βˆ’ 1)))
cfl 10268class ⌊
cceil 10269class ⌈
df-fl 10270⌊ = (π‘₯ ∈ ℝ ↦ (℩𝑦 ∈ β„€ (𝑦 ≀ π‘₯ ∧ π‘₯ < (𝑦 + 1))))
df-ceil 10271⌈ = (π‘₯ ∈ ℝ ↦ -(βŒŠβ€˜-π‘₯))
cmo 10322class mod
df-mod 10323 mod = (π‘₯ ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (π‘₯ βˆ’ (𝑦 Β· (βŒŠβ€˜(π‘₯ / 𝑦)))))
cseq 10445class seq𝑀( + , 𝐹)
df-seqfrec 10446seq𝑀( + , 𝐹) = ran frec((π‘₯ ∈ (β„€β‰₯β€˜π‘€), 𝑦 ∈ V ↦ ⟨(π‘₯ + 1), (𝑦 + (πΉβ€˜(π‘₯ + 1)))⟩), βŸ¨π‘€, (πΉβ€˜π‘€)⟩)
cexp 10519class ↑
df-exp 10520↑ = (π‘₯ ∈ β„‚, 𝑦 ∈ β„€ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( Β· , (β„• Γ— {π‘₯}))β€˜π‘¦), (1 / (seq1( Β· , (β„• Γ— {π‘₯}))β€˜-𝑦)))))
cfa 10705class !
df-fac 10706! = ({⟨0, 1⟩} βˆͺ seq1( Β· , I ))
cbc 10727class C
df-bc 10728C = (𝑛 ∈ β„•0, π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ (0...𝑛), ((!β€˜π‘›) / ((!β€˜(𝑛 βˆ’ π‘˜)) Β· (!β€˜π‘˜))), 0))
chash 10755class β™―
df-ihash 10756β™― = ((frec((π‘₯ ∈ β„€ ↦ (π‘₯ + 1)), 0) βˆͺ {βŸ¨Ο‰, +∞⟩}) ∘ (π‘₯ ∈ V ↦ βˆͺ {𝑦 ∈ (Ο‰ βˆͺ {Ο‰}) ∣ 𝑦 β‰Ό π‘₯}))
cshi 10823class shift
df-shft 10824 shift = (𝑓 ∈ V, π‘₯ ∈ β„‚ ↦ {βŸ¨π‘¦, π‘§βŸ© ∣ (𝑦 ∈ β„‚ ∧ (𝑦 βˆ’ π‘₯)𝑓𝑧)})
ccj 10848class βˆ—
cre 10849class β„œ
cim 10850class β„‘
df-cj 10851βˆ— = (π‘₯ ∈ β„‚ ↦ (℩𝑦 ∈ β„‚ ((π‘₯ + 𝑦) ∈ ℝ ∧ (i Β· (π‘₯ βˆ’ 𝑦)) ∈ ℝ)))
df-re 10852β„œ = (π‘₯ ∈ β„‚ ↦ ((π‘₯ + (βˆ—β€˜π‘₯)) / 2))
df-im 10853β„‘ = (π‘₯ ∈ β„‚ ↦ (β„œβ€˜(π‘₯ / i)))
csqrt 11005class √
cabs 11006class abs
df-rsqrt 11007√ = (π‘₯ ∈ ℝ ↦ (℩𝑦 ∈ ℝ ((𝑦↑2) = π‘₯ ∧ 0 ≀ 𝑦)))
df-abs 11008abs = (π‘₯ ∈ β„‚ ↦ (βˆšβ€˜(π‘₯ Β· (βˆ—β€˜π‘₯))))
cli 11286class ⇝
df-clim 11287 ⇝ = {βŸ¨π‘“, π‘¦βŸ© ∣ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((π‘“β€˜π‘˜) ∈ β„‚ ∧ (absβ€˜((π‘“β€˜π‘˜) βˆ’ 𝑦)) < π‘₯))}
csu 11361class Ξ£π‘˜ ∈ 𝐴 𝐡
df-sumdc 11362Ξ£π‘˜ ∈ 𝐴 𝐡 = (β„©π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
cprod 11558class βˆπ‘˜ ∈ 𝐴 𝐡
df-proddc 11559βˆπ‘˜ ∈ 𝐴 𝐡 = (β„©π‘₯(βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
ce 11650class exp
ceu 11651class e
csin 11652class sin
ccos 11653class cos
ctan 11654class tan
cpi 11655class Ο€
df-ef 11656exp = (π‘₯ ∈ β„‚ ↦ Ξ£π‘˜ ∈ β„•0 ((π‘₯β†‘π‘˜) / (!β€˜π‘˜)))
df-e 11657e = (expβ€˜1)
df-sin 11658sin = (π‘₯ ∈ β„‚ ↦ (((expβ€˜(i Β· π‘₯)) βˆ’ (expβ€˜(-i Β· π‘₯))) / (2 Β· i)))
df-cos 11659cos = (π‘₯ ∈ β„‚ ↦ (((expβ€˜(i Β· π‘₯)) + (expβ€˜(-i Β· π‘₯))) / 2))
df-tan 11660tan = (π‘₯ ∈ (β—‘cos β€œ (β„‚ βˆ– {0})) ↦ ((sinβ€˜π‘₯) / (cosβ€˜π‘₯)))
df-pi 11661Ο€ = inf((ℝ+ ∩ (β—‘sin β€œ {0})), ℝ, < )
ctau 11782class Ο„
df-tau 11783Ο„ = inf((ℝ+ ∩ (β—‘cos β€œ {1})), ℝ, < )
cdvds 11794class βˆ₯
df-dvds 11795 βˆ₯ = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ β„€ ∧ 𝑦 ∈ β„€) ∧ βˆƒπ‘› ∈ β„€ (𝑛 Β· π‘₯) = 𝑦)}
cgcd 11943class gcd
df-gcd 11944 gcd = (π‘₯ ∈ β„€, 𝑦 ∈ β„€ ↦ if((π‘₯ = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ β„€ ∣ (𝑛 βˆ₯ π‘₯ ∧ 𝑛 βˆ₯ 𝑦)}, ℝ, < )))
clcm 12060class lcm
df-lcm 12061 lcm = (π‘₯ ∈ β„€, 𝑦 ∈ β„€ ↦ if((π‘₯ = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ β„• ∣ (π‘₯ βˆ₯ 𝑛 ∧ 𝑦 βˆ₯ 𝑛)}, ℝ, < )))
cprime 12107class β„™
df-prm 12108β„™ = {𝑝 ∈ β„• ∣ {𝑛 ∈ β„• ∣ 𝑛 βˆ₯ 𝑝} β‰ˆ 2o}
cnumer 12181class numer
cdenom 12182class denom
df-numer 12183numer = (𝑦 ∈ β„š ↦ (1st β€˜(β„©π‘₯ ∈ (β„€ Γ— β„•)(((1st β€˜π‘₯) gcd (2nd β€˜π‘₯)) = 1 ∧ 𝑦 = ((1st β€˜π‘₯) / (2nd β€˜π‘₯))))))
df-denom 12184denom = (𝑦 ∈ β„š ↦ (2nd β€˜(β„©π‘₯ ∈ (β„€ Γ— β„•)(((1st β€˜π‘₯) gcd (2nd β€˜π‘₯)) = 1 ∧ 𝑦 = ((1st β€˜π‘₯) / (2nd β€˜π‘₯))))))
codz 12208class odβ„€
cphi 12209class Ο•
df-odz 12210odβ„€ = (𝑛 ∈ β„• ↦ (π‘₯ ∈ {π‘₯ ∈ β„€ ∣ (π‘₯ gcd 𝑛) = 1} ↦ inf({π‘š ∈ β„• ∣ 𝑛 βˆ₯ ((π‘₯β†‘π‘š) βˆ’ 1)}, ℝ, < )))
df-phi 12211Ο• = (𝑛 ∈ β„• ↦ (β™―β€˜{π‘₯ ∈ (1...𝑛) ∣ (π‘₯ gcd 𝑛) = 1}))
cpc 12284class pCnt
df-pc 12285 pCnt = (𝑝 ∈ β„™, π‘Ÿ ∈ β„š ↦ if(π‘Ÿ = 0, +∞, (β„©π‘§βˆƒπ‘₯ ∈ β„€ βˆƒπ‘¦ ∈ β„• (π‘Ÿ = (π‘₯ / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ β„•0 ∣ (𝑝↑𝑛) βˆ₯ π‘₯}, ℝ, < ) βˆ’ sup({𝑛 ∈ β„•0 ∣ (𝑝↑𝑛) βˆ₯ 𝑦}, ℝ, < ))))))
cgz 12367class β„€[i]
df-gz 12368β„€[i] = {π‘₯ ∈ β„‚ ∣ ((β„œβ€˜π‘₯) ∈ β„€ ∧ (β„‘β€˜π‘₯) ∈ β„€)}
cstr 12458class Struct
cnx 12459class ndx
csts 12460class sSet
cslot 12461class Slot 𝐴
cbs 12462class Base
cress 12463class β†Ύs
df-struct 12464 Struct = {βŸ¨π‘“, π‘₯⟩ ∣ (π‘₯ ∈ ( ≀ ∩ (β„• Γ— β„•)) ∧ Fun (𝑓 βˆ– {βˆ…}) ∧ dom 𝑓 βŠ† (...β€˜π‘₯))}
df-ndx 12465ndx = ( I β†Ύ β„•)
df-slot 12466Slot 𝐴 = (π‘₯ ∈ V ↦ (π‘₯β€˜π΄))
df-base 12468Base = Slot 1
df-sets 12469 sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 β†Ύ (V βˆ– dom {𝑒})) βˆͺ {𝑒}))
df-iress 12470 β†Ύs = (𝑀 ∈ V, π‘₯ ∈ V ↦ (𝑀 sSet ⟨(Baseβ€˜ndx), (π‘₯ ∩ (Baseβ€˜π‘€))⟩))
cplusg 12536class +g
cmulr 12537class .r
cstv 12538class *π‘Ÿ
csca 12539class Scalar
cvsca 12540class ·𝑠
cip 12541class ·𝑖
cts 12542class TopSet
cple 12543class le
coc 12544class oc
cds 12545class dist
cunif 12546class UnifSet
chom 12547class Hom
cco 12548class comp
df-plusg 12549+g = Slot 2
df-mulr 12550.r = Slot 3
df-starv 12551*π‘Ÿ = Slot 4
df-sca 12552Scalar = Slot 5
df-vsca 12553 ·𝑠 = Slot 6
df-ip 12554·𝑖 = Slot 8
df-tset 12555TopSet = Slot 9
df-ple 12556le = Slot 10
df-ocomp 12557oc = Slot 11
df-ds 12558dist = Slot 12
df-unif 12559UnifSet = Slot 13
df-hom 12560Hom = Slot 14
df-cco 12561comp = Slot 15
crest 12688class β†Ύt
ctopn 12689class TopOpen
df-rest 12690 β†Ύt = (𝑗 ∈ V, π‘₯ ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ π‘₯)))
df-topn 12691TopOpen = (𝑀 ∈ V ↦ ((TopSetβ€˜π‘€) β†Ύt (Baseβ€˜π‘€)))
ctg 12703class topGen
cpt 12704class ∏t
c0g 12705class 0g
cgsu 12706class Ξ£g
df-0g 127070g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Baseβ€˜π‘”) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘”)((𝑒(+gβ€˜π‘”)π‘₯) = π‘₯ ∧ (π‘₯(+gβ€˜π‘”)𝑒) = π‘₯))))
df-gsum 12708 Ξ£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 12709topGen = (π‘₯ ∈ V ↦ {𝑦 ∣ 𝑦 βŠ† βˆͺ (π‘₯ ∩ 𝒫 𝑦)})
df-pt 12710∏t = (𝑓 ∈ V ↦ (topGenβ€˜{π‘₯ ∣ βˆƒπ‘”((𝑔 Fn dom 𝑓 ∧ βˆ€π‘¦ ∈ dom 𝑓(π‘”β€˜π‘¦) ∈ (π‘“β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (dom 𝑓 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ (π‘“β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ dom 𝑓(π‘”β€˜π‘¦))}))
cprds 12714class Xs
cpws 12715class ↑s
df-prds 12716Xs = (𝑠 ∈ 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 12719 ↑s = (π‘Ÿ ∈ V, 𝑖 ∈ V ↦ ((Scalarβ€˜π‘Ÿ)Xs(𝑖 Γ— {π‘Ÿ})))
cimas 12720class β€œs
cqus 12721class /s
cxps 12722class Γ—s
df-iimas 12723 β€œs = (𝑓 ∈ V, π‘Ÿ ∈ V ↦ ⦋(Baseβ€˜π‘Ÿ) / π‘£β¦Œ{⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩})
df-qus 12724 /s = (π‘Ÿ ∈ V, 𝑒 ∈ V ↦ ((π‘₯ ∈ (Baseβ€˜π‘Ÿ) ↦ [π‘₯]𝑒) β€œs π‘Ÿ))
df-xps 12725 Γ—s = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ (β—‘(π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑦 ∈ (Baseβ€˜π‘ ) ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) β€œs ((Scalarβ€˜π‘Ÿ)Xs{βŸ¨βˆ…, π‘ŸβŸ©, ⟨1o, π‘ βŸ©})))
cplusf 12772class +𝑓
cmgm 12773class Mgm
df-plusf 12774+𝑓 = (𝑔 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜π‘”), 𝑦 ∈ (Baseβ€˜π‘”) ↦ (π‘₯(+gβ€˜π‘”)𝑦)))
df-mgm 12775Mgm = {𝑔 ∣ [(Baseβ€˜π‘”) / 𝑏][(+gβ€˜π‘”) / π‘œ]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯π‘œπ‘¦) ∈ 𝑏}
csgrp 12807class Smgrp
df-sgrp 12808Smgrp = {𝑔 ∈ Mgm ∣ [(Baseβ€˜π‘”) / 𝑏][(+gβ€˜π‘”) / π‘œ]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 ((π‘₯π‘œπ‘¦)π‘œπ‘§) = (π‘₯π‘œ(π‘¦π‘œπ‘§))}
cmnd 12817class Mnd
df-mnd 12818Mnd = {𝑔 ∈ Smgrp ∣ [(Baseβ€˜π‘”) / 𝑏][(+gβ€˜π‘”) / 𝑝]βˆƒπ‘’ ∈ 𝑏 βˆ€π‘₯ ∈ 𝑏 ((𝑒𝑝π‘₯) = π‘₯ ∧ (π‘₯𝑝𝑒) = π‘₯)}
cmhm 12849class MndHom
csubmnd 12850class SubMnd
df-mhm 12851 MndHom = (𝑠 ∈ Mnd, 𝑑 ∈ Mnd ↦ {𝑓 ∈ ((Baseβ€˜π‘‘) β†‘π‘š (Baseβ€˜π‘ )) ∣ (βˆ€π‘₯ ∈ (Baseβ€˜π‘ )βˆ€π‘¦ ∈ (Baseβ€˜π‘ )(π‘“β€˜(π‘₯(+gβ€˜π‘ )𝑦)) = ((π‘“β€˜π‘₯)(+gβ€˜π‘‘)(π‘“β€˜π‘¦)) ∧ (π‘“β€˜(0gβ€˜π‘ )) = (0gβ€˜π‘‘))})
df-submnd 12852SubMnd = (𝑠 ∈ Mnd ↦ {𝑑 ∈ 𝒫 (Baseβ€˜π‘ ) ∣ ((0gβ€˜π‘ ) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘ )𝑦) ∈ 𝑑)})
cgrp 12877class Grp
cminusg 12878class invg
csg 12879class -g
df-grp 12880Grp = {𝑔 ∈ Mnd ∣ βˆ€π‘Ž ∈ (Baseβ€˜π‘”)βˆƒπ‘š ∈ (Baseβ€˜π‘”)(π‘š(+gβ€˜π‘”)π‘Ž) = (0gβ€˜π‘”)}
df-minusg 12881invg = (𝑔 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜π‘”) ↦ (℩𝑀 ∈ (Baseβ€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯) = (0gβ€˜π‘”))))
df-sbg 12882-g = (𝑔 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜π‘”), 𝑦 ∈ (Baseβ€˜π‘”) ↦ (π‘₯(+gβ€˜π‘”)((invgβ€˜π‘”)β€˜π‘¦))))
cmg 12983class .g
df-mulg 12984.g = (𝑔 ∈ V ↦ (𝑛 ∈ β„€, π‘₯ ∈ (Baseβ€˜π‘”) ↦ if(𝑛 = 0, (0gβ€˜π‘”), ⦋seq1((+gβ€˜π‘”), (β„• Γ— {π‘₯})) / π‘ β¦Œif(0 < 𝑛, (π‘ β€˜π‘›), ((invgβ€˜π‘”)β€˜(π‘ β€˜-𝑛))))))
csubg 13027class SubGrp
cnsg 13028class NrmSGrp
cqg 13029class ~QG
df-subg 13030SubGrp = (𝑀 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ∣ (𝑀 β†Ύs 𝑠) ∈ Grp})
df-nsg 13031NrmSGrp = (𝑀 ∈ Grp ↦ {𝑠 ∈ (SubGrpβ€˜π‘€) ∣ [(Baseβ€˜π‘€) / 𝑏][(+gβ€˜π‘€) / 𝑝]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 ((π‘₯𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝π‘₯) ∈ 𝑠)})
df-eqg 13032 ~QG = (π‘Ÿ ∈ V, 𝑖 ∈ V ↦ {⟨π‘₯, π‘¦βŸ© ∣ ({π‘₯, 𝑦} βŠ† (Baseβ€˜π‘Ÿ) ∧ (((invgβ€˜π‘Ÿ)β€˜π‘₯)(+gβ€˜π‘Ÿ)𝑦) ∈ 𝑖)})
ccmn 13088class CMnd
cabl 13089class Abel
df-cmn 13090CMnd = {𝑔 ∈ Mnd ∣ βˆ€π‘Ž ∈ (Baseβ€˜π‘”)βˆ€π‘ ∈ (Baseβ€˜π‘”)(π‘Ž(+gβ€˜π‘”)𝑏) = (𝑏(+gβ€˜π‘”)π‘Ž)}
df-abl 13091Abel = (Grp ∩ CMnd)
cmgp 13130class mulGrp
df-mgp 13131mulGrp = (𝑀 ∈ V ↦ (𝑀 sSet ⟨(+gβ€˜ndx), (.rβ€˜π‘€)⟩))
cur 13142class 1r
df-ur 131431r = (0g ∘ mulGrp)
csrg 13146class SRing
df-srg 13147SRing = {𝑓 ∈ CMnd ∣ ((mulGrpβ€˜π‘“) ∈ Mnd ∧ [(Baseβ€˜π‘“) / π‘Ÿ][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑][(0gβ€˜π‘“) / 𝑛]βˆ€π‘₯ ∈ π‘Ÿ (βˆ€π‘¦ ∈ π‘Ÿ βˆ€π‘§ ∈ π‘Ÿ ((π‘₯𝑑(𝑦𝑝𝑧)) = ((π‘₯𝑑𝑦)𝑝(π‘₯𝑑𝑧)) ∧ ((π‘₯𝑝𝑦)𝑑𝑧) = ((π‘₯𝑑𝑧)𝑝(𝑦𝑑𝑧))) ∧ ((𝑛𝑑π‘₯) = 𝑛 ∧ (π‘₯𝑑𝑛) = 𝑛)))}
crg 13179class Ring
ccrg 13180class CRing
df-ring 13181Ring = {𝑓 ∈ Grp ∣ ((mulGrpβ€˜π‘“) ∈ Mnd ∧ [(Baseβ€˜π‘“) / π‘Ÿ][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑]βˆ€π‘₯ ∈ π‘Ÿ βˆ€π‘¦ ∈ π‘Ÿ βˆ€π‘§ ∈ π‘Ÿ ((π‘₯𝑑(𝑦𝑝𝑧)) = ((π‘₯𝑑𝑦)𝑝(π‘₯𝑑𝑧)) ∧ ((π‘₯𝑝𝑦)𝑑𝑧) = ((π‘₯𝑑𝑧)𝑝(𝑦𝑑𝑧))))}
df-cring 13182CRing = {𝑓 ∈ Ring ∣ (mulGrpβ€˜π‘“) ∈ CMnd}
coppr 13239class oppr
df-oppr 13240oppr = (𝑓 ∈ V ↦ (𝑓 sSet ⟨(.rβ€˜ndx), tpos (.rβ€˜π‘“)⟩))
cdsr 13255class βˆ₯r
cui 13256class Unit
cir 13257class Irred
df-dvdsr 13258βˆ₯r = (𝑀 ∈ V ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ (Baseβ€˜π‘€) ∧ βˆƒπ‘§ ∈ (Baseβ€˜π‘€)(𝑧(.rβ€˜π‘€)π‘₯) = 𝑦)})
df-unit 13259Unit = (𝑀 ∈ V ↦ (β—‘((βˆ₯rβ€˜π‘€) ∩ (βˆ₯rβ€˜(opprβ€˜π‘€))) β€œ {(1rβ€˜π‘€)}))
df-irred 13260Irred = (𝑀 ∈ V ↦ ⦋((Baseβ€˜π‘€) βˆ– (Unitβ€˜π‘€)) / π‘β¦Œ{𝑧 ∈ 𝑏 ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘€)𝑦) β‰  𝑧})
cinvr 13289class invr
df-invr 13290invr = (π‘Ÿ ∈ V ↦ (invgβ€˜((mulGrpβ€˜π‘Ÿ) β†Ύs (Unitβ€˜π‘Ÿ))))
cdvr 13300class /r
df-dvr 13301/r = (π‘Ÿ ∈ V ↦ (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑦 ∈ (Unitβ€˜π‘Ÿ) ↦ (π‘₯(.rβ€˜π‘Ÿ)((invrβ€˜π‘Ÿ)β€˜π‘¦))))
crh 13319class RingHom
crs 13320class RingIso
df-rnghom 13321 RingHom = (π‘Ÿ ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Baseβ€˜π‘Ÿ) / π‘£β¦Œβ¦‹(Baseβ€˜π‘ ) / π‘€β¦Œ{𝑓 ∈ (𝑀 β†‘π‘š 𝑣) ∣ ((π‘“β€˜(1rβ€˜π‘Ÿ)) = (1rβ€˜π‘ ) ∧ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘¦ ∈ 𝑣 ((π‘“β€˜(π‘₯(+gβ€˜π‘Ÿ)𝑦)) = ((π‘“β€˜π‘₯)(+gβ€˜π‘ )(π‘“β€˜π‘¦)) ∧ (π‘“β€˜(π‘₯(.rβ€˜π‘Ÿ)𝑦)) = ((π‘“β€˜π‘₯)(.rβ€˜π‘ )(π‘“β€˜π‘¦))))})
df-rngiso 13322 RingIso = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (π‘Ÿ RingHom 𝑠) ∣ ◑𝑓 ∈ (𝑠 RingHom π‘Ÿ)})
cnzr 13323class NzRing
df-nzr 13324NzRing = {π‘Ÿ ∈ Ring ∣ (1rβ€˜π‘Ÿ) β‰  (0gβ€˜π‘Ÿ)}
clring 13331class LRing
df-lring 13332LRing = {π‘Ÿ ∈ NzRing ∣ βˆ€π‘₯ ∈ (Baseβ€˜π‘Ÿ)βˆ€π‘¦ ∈ (Baseβ€˜π‘Ÿ)((π‘₯(+gβ€˜π‘Ÿ)𝑦) = (1rβ€˜π‘Ÿ) β†’ (π‘₯ ∈ (Unitβ€˜π‘Ÿ) ∨ 𝑦 ∈ (Unitβ€˜π‘Ÿ)))}
csubrg 13338class SubRing
crgspn 13339class RingSpan
df-subrg 13340SubRing = (𝑀 ∈ Ring ↦ {𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ∣ ((𝑀 β†Ύs 𝑠) ∈ Ring ∧ (1rβ€˜π‘€) ∈ 𝑠)})
df-rgspn 13341RingSpan = (𝑀 ∈ V ↦ (𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ↦ ∩ {𝑑 ∈ (SubRingβ€˜π‘€) ∣ 𝑠 βŠ† 𝑑}))
capr 13370class #r
df-apr 13371#r = (𝑀 ∈ V ↦ {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (Baseβ€˜π‘€) ∧ 𝑦 ∈ (Baseβ€˜π‘€)) ∧ (π‘₯(-gβ€˜π‘€)𝑦) ∈ (Unitβ€˜π‘€))})
clmod 13377class LMod
cscaf 13378class Β·sf
df-lmod 13379LMod = {𝑔 ∈ Grp ∣ [(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / π‘Ž][(Scalarβ€˜π‘”) / 𝑓][( ·𝑠 β€˜π‘”) / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)))}
df-scaf 13380 Β·sf = (𝑔 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘”)), 𝑦 ∈ (Baseβ€˜π‘”) ↦ (π‘₯( ·𝑠 β€˜π‘”)𝑦)))
cpsmet 13442class PsMet
cxmet 13443class ∞Met
cmet 13444class Met
cbl 13445class ball
cfbas 13446class fBas
cfg 13447class filGen
cmopn 13448class MetOpen
cmetu 13449class metUnif
df-psmet 13450PsMet = (π‘₯ ∈ V ↦ {𝑑 ∈ (ℝ* β†‘π‘š (π‘₯ Γ— π‘₯)) ∣ βˆ€π‘¦ ∈ π‘₯ ((𝑦𝑑𝑦) = 0 ∧ βˆ€π‘§ ∈ π‘₯ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))})
df-xmet 13451∞Met = (π‘₯ ∈ V ↦ {𝑑 ∈ (ℝ* β†‘π‘š (π‘₯ Γ— π‘₯)) ∣ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))})
df-met 13452Met = (π‘₯ ∈ V ↦ {𝑑 ∈ (ℝ β†‘π‘š (π‘₯ Γ— π‘₯)) ∣ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) + (𝑀𝑑𝑧)))})
df-bl 13453ball = (𝑑 ∈ V ↦ (π‘₯ ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (π‘₯𝑑𝑦) < 𝑧}))
df-mopn 13454MetOpen = (𝑑 ∈ βˆͺ ran ∞Met ↦ (topGenβ€˜ran (ballβ€˜π‘‘)))
df-fbas 13455fBas = (𝑀 ∈ V ↦ {π‘₯ ∈ 𝒫 𝒫 𝑀 ∣ (π‘₯ β‰  βˆ… ∧ βˆ… βˆ‰ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (π‘₯ ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)})
df-fg 13456filGen = (𝑀 ∈ V, π‘₯ ∈ (fBasβ€˜π‘€) ↦ {𝑦 ∈ 𝒫 𝑀 ∣ (π‘₯ ∩ 𝒫 𝑦) β‰  βˆ…})
df-metu 13457metUnif = (𝑑 ∈ βˆͺ ran PsMet ↦ ((dom dom 𝑑 Γ— dom dom 𝑑)filGenran (π‘Ž ∈ ℝ+ ↦ (◑𝑑 β€œ (0[,)π‘Ž)))))
ccnfld 13458class β„‚fld
df-icnfld 13459β„‚fld = ({⟨(Baseβ€˜ndx), β„‚βŸ©, ⟨(+gβ€˜ndx), + ⟩, ⟨(.rβ€˜ndx), Β· ⟩} βˆͺ {⟨(*π‘Ÿβ€˜ndx), βˆ—βŸ©})
czring 13483class β„€ring
df-zring 13484β„€ring = (β„‚fld β†Ύs β„€)
ctop 13500class Top
df-top 13501Top = {π‘₯ ∣ (βˆ€π‘¦ ∈ 𝒫 π‘₯βˆͺ 𝑦 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (𝑦 ∩ 𝑧) ∈ π‘₯)}
ctopon 13513class TopOn
df-topon 13514TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = βˆͺ 𝑗})
ctps 13533class TopSp
df-topsp 13534TopSp = {𝑓 ∣ (TopOpenβ€˜π‘“) ∈ (TopOnβ€˜(Baseβ€˜π‘“))}
ctb 13545class TopBases
df-bases 13546TopBases = {π‘₯ ∣ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (𝑦 ∩ 𝑧) βŠ† βˆͺ (π‘₯ ∩ 𝒫 (𝑦 ∩ 𝑧))}
ccld 13595class Clsd
cnt 13596class int
ccl 13597class cls
df-cld 13598Clsd = (𝑗 ∈ Top ↦ {π‘₯ ∈ 𝒫 βˆͺ 𝑗 ∣ (βˆͺ 𝑗 βˆ– π‘₯) ∈ 𝑗})
df-ntr 13599int = (𝑗 ∈ Top ↦ (π‘₯ ∈ 𝒫 βˆͺ 𝑗 ↦ βˆͺ (𝑗 ∩ 𝒫 π‘₯)))
df-cls 13600cls = (𝑗 ∈ Top ↦ (π‘₯ ∈ 𝒫 βˆͺ 𝑗 ↦ ∩ {𝑦 ∈ (Clsdβ€˜π‘—) ∣ π‘₯ βŠ† 𝑦}))
cnei 13641class nei
df-nei 13642nei = (𝑗 ∈ Top ↦ (π‘₯ ∈ 𝒫 βˆͺ 𝑗 ↦ {𝑦 ∈ 𝒫 βˆͺ 𝑗 ∣ βˆƒπ‘” ∈ 𝑗 (π‘₯ βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦)}))
ccn 13688class Cn
ccnp 13689class CnP
clm 13690class ⇝𝑑
df-cn 13691 Cn = (𝑗 ∈ Top, π‘˜ ∈ Top ↦ {𝑓 ∈ (βˆͺ π‘˜ β†‘π‘š βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ (◑𝑓 β€œ 𝑦) ∈ 𝑗})
df-cnp 13692 CnP = (𝑗 ∈ Top, π‘˜ ∈ Top ↦ (π‘₯ ∈ βˆͺ 𝑗 ↦ {𝑓 ∈ (βˆͺ π‘˜ β†‘π‘š βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))}))
df-lm 13693⇝𝑑 = (𝑗 ∈ Top ↦ {βŸ¨π‘“, π‘₯⟩ ∣ (𝑓 ∈ (βˆͺ 𝑗 ↑pm β„‚) ∧ π‘₯ ∈ βˆͺ 𝑗 ∧ βˆ€π‘’ ∈ 𝑗 (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘¦ ∈ ran β„€β‰₯(𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’))})
ctx 13755class Γ—t
df-tx 13756 Γ—t = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ (topGenβ€˜ran (π‘₯ ∈ π‘Ÿ, 𝑦 ∈ 𝑠 ↦ (π‘₯ Γ— 𝑦))))
chmeo 13803class Homeo
df-hmeo 13804Homeo = (𝑗 ∈ Top, π‘˜ ∈ Top ↦ {𝑓 ∈ (𝑗 Cn π‘˜) ∣ ◑𝑓 ∈ (π‘˜ Cn 𝑗)})
cxms 13839class ∞MetSp
cms 13840class MetSp
ctms 13841class toMetSp
df-xms 13842∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpenβ€˜π‘“) = (MetOpenβ€˜((distβ€˜π‘“) β†Ύ ((Baseβ€˜π‘“) Γ— (Baseβ€˜π‘“))))}
df-ms 13843MetSp = {𝑓 ∈ ∞MetSp ∣ ((distβ€˜π‘“) β†Ύ ((Baseβ€˜π‘“) Γ— (Baseβ€˜π‘“))) ∈ (Metβ€˜(Baseβ€˜π‘“))}
df-tms 13844toMetSp = (𝑑 ∈ βˆͺ ran ∞Met ↦ ({⟨(Baseβ€˜ndx), dom dom π‘‘βŸ©, ⟨(distβ€˜ndx), π‘‘βŸ©} sSet ⟨(TopSetβ€˜ndx), (MetOpenβ€˜π‘‘)⟩))
ccncf 14060class –cnβ†’
df-cncf 14061–cnβ†’ = (π‘Ž ∈ 𝒫 β„‚, 𝑏 ∈ 𝒫 β„‚ ↦ {𝑓 ∈ (𝑏 β†‘π‘š π‘Ž) ∣ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘’ ∈ ℝ+ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘¦ ∈ π‘Ž ((absβ€˜(π‘₯ βˆ’ 𝑦)) < 𝑑 β†’ (absβ€˜((π‘“β€˜π‘₯) βˆ’ (π‘“β€˜π‘¦))) < 𝑒)})
climc 14126class limβ„‚
cdv 14127class D
df-limced 14128 limβ„‚ = (𝑓 ∈ (β„‚ ↑pm β„‚), π‘₯ ∈ β„‚ ↦ {𝑦 ∈ β„‚ ∣ ((𝑓:dom π‘“βŸΆβ„‚ ∧ dom 𝑓 βŠ† β„‚) ∧ (π‘₯ ∈ β„‚ ∧ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘§ ∈ dom 𝑓((𝑧 # π‘₯ ∧ (absβ€˜(𝑧 βˆ’ π‘₯)) < 𝑑) β†’ (absβ€˜((π‘“β€˜π‘§) βˆ’ 𝑦)) < 𝑒)))})
df-dvap 14129 D = (𝑠 ∈ 𝒫 β„‚, 𝑓 ∈ (β„‚ ↑pm 𝑠) ↦ βˆͺ π‘₯ ∈ ((intβ€˜((MetOpenβ€˜(abs ∘ βˆ’ )) β†Ύt 𝑠))β€˜dom 𝑓)({π‘₯} Γ— ((𝑧 ∈ {𝑀 ∈ dom 𝑓 ∣ 𝑀 # π‘₯} ↦ (((π‘“β€˜π‘§) βˆ’ (π‘“β€˜π‘₯)) / (𝑧 βˆ’ π‘₯))) limβ„‚ π‘₯)))
clog 14280class log
ccxp 14281class ↑𝑐
df-relog 14282log = β—‘(exp β†Ύ ℝ)
df-rpcxp 14283↑𝑐 = (π‘₯ ∈ ℝ+, 𝑦 ∈ β„‚ ↦ (expβ€˜(𝑦 Β· (logβ€˜π‘₯))))
clogb 14364class logb
df-logb 14365 logb = (π‘₯ ∈ (β„‚ βˆ– {0, 1}), 𝑦 ∈ (β„‚ βˆ– {0}) ↦ ((logβ€˜π‘¦) / (logβ€˜π‘₯)))
clgs 14401class /L
df-lgs 14402 /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 14548wff 𝐴 DECIDin 𝐡
df-dcin 14549(𝐴 DECIDin 𝐡 ↔ βˆ€π‘₯ ∈ 𝐡 DECID π‘₯ ∈ 𝐴)
wbd 14567wff BOUNDED πœ‘
ax-bd0 14568(πœ‘ ↔ πœ“)    β‡’   (BOUNDED πœ‘ β†’ BOUNDED πœ“)
ax-bdim 14569BOUNDED πœ‘    &   BOUNDED πœ“    β‡’   BOUNDED (πœ‘ β†’ πœ“)
ax-bdan 14570BOUNDED πœ‘    &   BOUNDED πœ“    β‡’   BOUNDED (πœ‘ ∧ πœ“)
ax-bdor 14571BOUNDED πœ‘    &   BOUNDED πœ“    β‡’   BOUNDED (πœ‘ ∨ πœ“)
ax-bdn 14572BOUNDED πœ‘    β‡’   BOUNDED Β¬ πœ‘
ax-bdal 14573BOUNDED πœ‘    β‡’   BOUNDED βˆ€π‘₯ ∈ 𝑦 πœ‘
ax-bdex 14574BOUNDED πœ‘    β‡’   BOUNDED βˆƒπ‘₯ ∈ 𝑦 πœ‘
ax-bdeq 14575BOUNDED π‘₯ = 𝑦
ax-bdel 14576BOUNDED π‘₯ ∈ 𝑦
ax-bdsb 14577BOUNDED πœ‘    β‡’   BOUNDED [𝑦 / π‘₯]πœ‘
wbdc 14595wff BOUNDED 𝐴
df-bdc 14596(BOUNDED 𝐴 ↔ βˆ€π‘₯BOUNDED π‘₯ ∈ 𝐴)
ax-bdsep 14639BOUNDED πœ‘    β‡’   βˆ€π‘Žβˆƒπ‘βˆ€π‘₯(π‘₯ ∈ 𝑏 ↔ (π‘₯ ∈ π‘Ž ∧ πœ‘))
ax-bj-d0cl 14679BOUNDED πœ‘    β‡’   DECID πœ‘
wind 14681wff Ind 𝐴
df-bj-ind 14682(Ind 𝐴 ↔ (βˆ… ∈ 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 suc π‘₯ ∈ 𝐴))
ax-infvn 14696βˆƒπ‘₯(Ind π‘₯ ∧ βˆ€π‘¦(Ind 𝑦 β†’ π‘₯ βŠ† 𝑦))
ax-bdsetind 14723BOUNDED πœ‘    β‡’   (βˆ€π‘Ž(βˆ€π‘¦ ∈ π‘Ž [𝑦 / π‘Ž]πœ‘ β†’ πœ‘) β†’ βˆ€π‘Žπœ‘)
ax-inf2 14731βˆƒπ‘Žβˆ€π‘₯(π‘₯ ∈ π‘Ž ↔ (π‘₯ = βˆ… ∨ βˆƒπ‘¦ ∈ π‘Ž π‘₯ = suc 𝑦))
ax-strcoll 14737βˆ€π‘Ž(βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦πœ‘ β†’ βˆƒπ‘(βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦ ∈ 𝑏 πœ‘ ∧ βˆ€π‘¦ ∈ 𝑏 βˆƒπ‘₯ ∈ π‘Ž πœ‘))
ax-sscoll 14742βˆ€π‘Žβˆ€π‘βˆƒπ‘βˆ€π‘§(βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦ ∈ 𝑏 πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑐 (βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦ ∈ 𝑑 πœ‘ ∧ βˆ€π‘¦ ∈ 𝑑 βˆƒπ‘₯ ∈ π‘Ž πœ‘))
ax-ddkcomp 14744(((𝐴 βŠ† ℝ ∧ βˆƒπ‘₯ π‘₯ ∈ 𝐴) ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ 𝐴 𝑦 < π‘₯ ∧ βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ < 𝑦 β†’ (βˆƒπ‘§ ∈ 𝐴 π‘₯ < 𝑧 ∨ βˆ€π‘§ ∈ 𝐴 𝑧 < 𝑦))) β†’ βˆƒπ‘₯ ∈ ℝ (βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ π‘₯ ∧ ((𝐡 ∈ 𝑅 ∧ βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ 𝐡) β†’ π‘₯ ≀ 𝐡)))
walsi 14826wff βˆ€!π‘₯(πœ‘ β†’ πœ“)
walsc 14827wff βˆ€!π‘₯ ∈ π΄πœ‘
df-alsi 14828(βˆ€!π‘₯(πœ‘ β†’ πœ“) ↔ (βˆ€π‘₯(πœ‘ β†’ πœ“) ∧ βˆƒπ‘₯πœ‘))
df-alsc 14829(βˆ€!π‘₯ ∈ π΄πœ‘ ↔ (βˆ€π‘₯ ∈ 𝐴 πœ‘ ∧ βˆƒπ‘₯ π‘₯ ∈ 𝐴))
  Copyright terms: Public domain W3C validator