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 2737class V
df-v 2739V = {π‘₯ ∣ π‘₯ = π‘₯}
wcdeq 2945wff CondEq(π‘₯ = 𝑦 β†’ πœ‘)
df-cdeq 2946(CondEq(π‘₯ = 𝑦 β†’ πœ‘) ↔ (π‘₯ = 𝑦 β†’ πœ‘))
wsbc 2962wff [𝐴 / π‘₯]πœ‘
df-sbc 2963([𝐴 / π‘₯]πœ‘ ↔ 𝐴 ∈ {π‘₯ ∣ πœ‘})
csb 3057class ⦋𝐴 / π‘₯⦌𝐡
df-csb 3058⦋𝐴 / π‘₯⦌𝐡 = {𝑦 ∣ [𝐴 / π‘₯]𝑦 ∈ 𝐡}
cdif 3126class (𝐴 βˆ– 𝐡)
cun 3127class (𝐴 βˆͺ 𝐡)
cin 3128class (𝐴 ∩ 𝐡)
wss 3129wff 𝐴 βŠ† 𝐡
df-dif 3131(𝐴 βˆ– 𝐡) = {π‘₯ ∣ (π‘₯ ∈ 𝐴 ∧ Β¬ π‘₯ ∈ 𝐡)}
df-un 3133(𝐴 βˆͺ 𝐡) = {π‘₯ ∣ (π‘₯ ∈ 𝐴 ∨ π‘₯ ∈ 𝐡)}
df-in 3135(𝐴 ∩ 𝐡) = {π‘₯ ∣ (π‘₯ ∈ 𝐴 ∧ π‘₯ ∈ 𝐡)}
df-ss 3142(𝐴 βŠ† 𝐡 ↔ (𝐴 ∩ 𝐡) = 𝐴)
c0 3422class βˆ…
df-nul 3423βˆ… = (V βˆ– V)
cif 3534class if(πœ‘, 𝐴, 𝐡)
df-if 3535if(πœ‘, 𝐴, 𝐡) = {π‘₯ ∣ ((π‘₯ ∈ 𝐴 ∧ πœ‘) ∨ (π‘₯ ∈ 𝐡 ∧ Β¬ πœ‘))}
cpw 3575class 𝒫 𝐴
df-pw 3577𝒫 𝐴 = {π‘₯ ∣ π‘₯ βŠ† 𝐴}
csn 3592class {𝐴}
cpr 3593class {𝐴, 𝐡}
ctp 3594class {𝐴, 𝐡, 𝐢}
cop 3595class ⟨𝐴, 𝐡⟩
cotp 3596class ⟨𝐴, 𝐡, 𝐢⟩
df-sn 3598{𝐴} = {π‘₯ ∣ π‘₯ = 𝐴}
df-pr 3599{𝐴, 𝐡} = ({𝐴} βˆͺ {𝐡})
df-tp 3600{𝐴, 𝐡, 𝐢} = ({𝐴, 𝐡} βˆͺ {𝐢})
df-op 3601⟨𝐴, 𝐡⟩ = {π‘₯ ∣ (𝐴 ∈ V ∧ 𝐡 ∈ V ∧ π‘₯ ∈ {{𝐴}, {𝐴, 𝐡}})}
df-ot 3602⟨𝐴, 𝐡, 𝐢⟩ = ⟨⟨𝐴, 𝐡⟩, 𝐢⟩
cuni 3809class βˆͺ 𝐴
df-uni 3810βˆͺ 𝐴 = {π‘₯ ∣ βˆƒπ‘¦(π‘₯ ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)}
cint 3844class ∩ 𝐴
df-int 3845∩ 𝐴 = {π‘₯ ∣ βˆ€π‘¦(𝑦 ∈ 𝐴 β†’ π‘₯ ∈ 𝑦)}
ciun 3886class βˆͺ π‘₯ ∈ 𝐴 𝐡
ciin 3887class ∩ π‘₯ ∈ 𝐴 𝐡
df-iun 3888βˆͺ π‘₯ ∈ 𝐴 𝐡 = {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 ∈ 𝐡}
df-iin 3889∩ π‘₯ ∈ 𝐴 𝐡 = {𝑦 ∣ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ 𝐡}
wdisj 3980wff Disj π‘₯ ∈ 𝐴 𝐡
df-disj 3981(Disj π‘₯ ∈ 𝐴 𝐡 ↔ βˆ€π‘¦βˆƒ*π‘₯ ∈ 𝐴 𝑦 ∈ 𝐡)
wbr 4003wff 𝐴𝑅𝐡
df-br 4004(𝐴𝑅𝐡 ↔ ⟨𝐴, 𝐡⟩ ∈ 𝑅)
copab 4063class {⟨π‘₯, π‘¦βŸ© ∣ πœ‘}
cmpt 4064class (π‘₯ ∈ 𝐴 ↦ 𝐡)
df-opab 4065{⟨π‘₯, π‘¦βŸ© ∣ πœ‘} = {𝑧 ∣ βˆƒπ‘₯βˆƒπ‘¦(𝑧 = ⟨π‘₯, π‘¦βŸ© ∧ πœ‘)}
df-mpt 4066(π‘₯ ∈ 𝐴 ↦ 𝐡) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 = 𝐡)}
wtr 4101wff Tr 𝐴
df-tr 4102(Tr 𝐴 ↔ βˆͺ 𝐴 βŠ† 𝐴)
ax-coll 4118β„²π‘πœ‘    β‡’   (βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦πœ‘ β†’ βˆƒπ‘βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦ ∈ 𝑏 πœ‘)
ax-sep 4121βˆƒπ‘¦βˆ€π‘₯(π‘₯ ∈ 𝑦 ↔ (π‘₯ ∈ 𝑧 ∧ πœ‘))
ax-nul 4129βˆƒπ‘₯βˆ€π‘¦ Β¬ 𝑦 ∈ π‘₯
ax-pow 4174βˆƒπ‘¦βˆ€π‘§(βˆ€π‘€(𝑀 ∈ 𝑧 β†’ 𝑀 ∈ π‘₯) β†’ 𝑧 ∈ 𝑦)
wem 4194wff EXMID
df-exmid 4195(EXMID ↔ βˆ€π‘₯(π‘₯ βŠ† {βˆ…} β†’ DECID βˆ… ∈ π‘₯))
ax-pr 4209βˆƒπ‘§βˆ€π‘€((𝑀 = π‘₯ ∨ 𝑀 = 𝑦) β†’ 𝑀 ∈ 𝑧)
cep 4287class E
cid 4288class I
df-eprel 4289 E = {⟨π‘₯, π‘¦βŸ© ∣ π‘₯ ∈ 𝑦}
df-id 4293 I = {⟨π‘₯, π‘¦βŸ© ∣ π‘₯ = 𝑦}
wpo 4294wff 𝑅 Po 𝐴
wor 4295wff 𝑅 Or 𝐴
df-po 4296(𝑅 Po 𝐴 ↔ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘§ ∈ 𝐴 (Β¬ π‘₯𝑅π‘₯ ∧ ((π‘₯𝑅𝑦 ∧ 𝑦𝑅𝑧) β†’ π‘₯𝑅𝑧)))
df-iso 4297(𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘§ ∈ 𝐴 (π‘₯𝑅𝑦 β†’ (π‘₯𝑅𝑧 ∨ 𝑧𝑅𝑦))))
wfrfor 4327wff FrFor 𝑅𝐴𝑆
wfr 4328wff 𝑅 Fr 𝐴
wse 4329wff 𝑅 Se 𝐴
wwe 4330wff 𝑅 We 𝐴
df-frfor 4331( FrFor 𝑅𝐴𝑆 ↔ (βˆ€π‘₯ ∈ 𝐴 (βˆ€π‘¦ ∈ 𝐴 (𝑦𝑅π‘₯ β†’ 𝑦 ∈ 𝑆) β†’ π‘₯ ∈ 𝑆) β†’ 𝐴 βŠ† 𝑆))
df-frind 4332(𝑅 Fr 𝐴 ↔ βˆ€π‘  FrFor 𝑅𝐴𝑠)
df-se 4333(𝑅 Se 𝐴 ↔ βˆ€π‘₯ ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅π‘₯} ∈ V)
df-wetr 4334(𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘§ ∈ 𝐴 ((π‘₯𝑅𝑦 ∧ 𝑦𝑅𝑧) β†’ π‘₯𝑅𝑧)))
word 4362wff Ord 𝐴
con0 4363class On
wlim 4364wff Lim 𝐴
csuc 4365class suc 𝐴
df-iord 4366(Ord 𝐴 ↔ (Tr 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 Tr π‘₯))
df-on 4368On = {π‘₯ ∣ Ord π‘₯}
df-ilim 4369(Lim 𝐴 ↔ (Ord 𝐴 ∧ βˆ… ∈ 𝐴 ∧ 𝐴 = βˆͺ 𝐴))
df-suc 4371suc 𝐴 = (𝐴 βˆͺ {𝐴})
ax-un 4433βˆƒπ‘¦βˆ€π‘§(βˆƒπ‘€(𝑧 ∈ 𝑀 ∧ 𝑀 ∈ π‘₯) β†’ 𝑧 ∈ 𝑦)
ax-setind 4536(βˆ€π‘Ž(βˆ€π‘¦ ∈ π‘Ž [𝑦 / π‘Ž]πœ‘ β†’ πœ‘) β†’ βˆ€π‘Žπœ‘)
ax-iinf 4587βˆƒπ‘₯(βˆ… ∈ π‘₯ ∧ βˆ€π‘¦(𝑦 ∈ π‘₯ β†’ suc 𝑦 ∈ π‘₯))
com 4589class Ο‰
df-iom 4590Ο‰ = ∩ {π‘₯ ∣ (βˆ… ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ suc 𝑦 ∈ π‘₯)}
cxp 4624class (𝐴 Γ— 𝐡)
ccnv 4625class ◑𝐴
cdm 4626class dom 𝐴
crn 4627class ran 𝐴
cres 4628class (𝐴 β†Ύ 𝐡)
cima 4629class (𝐴 β€œ 𝐡)
ccom 4630class (𝐴 ∘ 𝐡)
wrel 4631wff Rel 𝐴
df-xp 4632(𝐴 Γ— 𝐡) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐡)}
df-rel 4633(Rel 𝐴 ↔ 𝐴 βŠ† (V Γ— V))
df-cnv 4634◑𝐴 = {⟨π‘₯, π‘¦βŸ© ∣ 𝑦𝐴π‘₯}
df-co 4635(𝐴 ∘ 𝐡) = {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘§(π‘₯𝐡𝑧 ∧ 𝑧𝐴𝑦)}
df-dm 4636dom 𝐴 = {π‘₯ ∣ βˆƒπ‘¦ π‘₯𝐴𝑦}
df-rn 4637ran 𝐴 = dom ◑𝐴
df-res 4638(𝐴 β†Ύ 𝐡) = (𝐴 ∩ (𝐡 Γ— V))
df-ima 4639(𝐴 β€œ 𝐡) = ran (𝐴 β†Ύ 𝐡)
cio 5176class (β„©π‘₯πœ‘)
df-iota 5178(β„©π‘₯πœ‘) = βˆͺ {𝑦 ∣ {π‘₯ ∣ πœ‘} = {𝑦}}
wfun 5210wff Fun 𝐴
wfn 5211wff 𝐴 Fn 𝐡
wf 5212wff 𝐹:𝐴⟢𝐡
wf1 5213wff 𝐹:𝐴–1-1→𝐡
wfo 5214wff 𝐹:𝐴–onto→𝐡
wf1o 5215wff 𝐹:𝐴–1-1-onto→𝐡
cfv 5216class (πΉβ€˜π΄)
wiso 5217wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐡)
df-fun 5218(Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◑𝐴) βŠ† I ))
df-fn 5219(𝐴 Fn 𝐡 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐡))
df-f 5220(𝐹:𝐴⟢𝐡 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 βŠ† 𝐡))
df-f1 5221(𝐹:𝐴–1-1→𝐡 ↔ (𝐹:𝐴⟢𝐡 ∧ Fun ◑𝐹))
df-fo 5222(𝐹:𝐴–onto→𝐡 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐡))
df-f1o 5223(𝐹:𝐴–1-1-onto→𝐡 ↔ (𝐹:𝐴–1-1→𝐡 ∧ 𝐹:𝐴–onto→𝐡))
df-fv 5224(πΉβ€˜π΄) = (β„©π‘₯𝐴𝐹π‘₯)
df-isom 5225(𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐡) ↔ (𝐻:𝐴–1-1-onto→𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯𝑅𝑦 ↔ (π»β€˜π‘₯)𝑆(π»β€˜π‘¦))))
crio 5829class (β„©π‘₯ ∈ 𝐴 πœ‘)
df-riota 5830(β„©π‘₯ ∈ 𝐴 πœ‘) = (β„©π‘₯(π‘₯ ∈ 𝐴 ∧ πœ‘))
co 5874class (𝐴𝐹𝐡)
coprab 5875class {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ πœ‘}
cmpo 5876class (π‘₯ ∈ 𝐴, 𝑦 ∈ 𝐡 ↦ 𝐢)
df-ov 5877(𝐴𝐹𝐡) = (πΉβ€˜βŸ¨π΄, 𝐡⟩)
df-oprab 5878{⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ πœ‘} = {𝑀 ∣ βˆƒπ‘₯βˆƒπ‘¦βˆƒπ‘§(𝑀 = ⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∧ πœ‘)}
df-mpo 5879(π‘₯ ∈ 𝐴, 𝑦 ∈ 𝐡 ↦ 𝐢) = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 = 𝐢)}
cof 6080class βˆ˜π‘“ 𝑅
cofr 6081class βˆ˜π‘Ÿ 𝑅
df-of 6082 βˆ˜π‘“ 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (π‘₯ ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((π‘“β€˜π‘₯)𝑅(π‘”β€˜π‘₯))))
df-ofr 6083 βˆ˜π‘Ÿ 𝑅 = {βŸ¨π‘“, π‘”βŸ© ∣ βˆ€π‘₯ ∈ (dom 𝑓 ∩ dom 𝑔)(π‘“β€˜π‘₯)𝑅(π‘”β€˜π‘₯)}
c1st 6138class 1st
c2nd 6139class 2nd
df-1st 61401st = (π‘₯ ∈ V ↦ βˆͺ dom {π‘₯})
df-2nd 61412nd = (π‘₯ ∈ V ↦ βˆͺ ran {π‘₯})
ctpos 6244class tpos 𝐹
df-tpos 6245tpos 𝐹 = (𝐹 ∘ (π‘₯ ∈ (β—‘dom 𝐹 βˆͺ {βˆ…}) ↦ βˆͺ β—‘{π‘₯}))
wsmo 6285wff Smo 𝐴
df-smo 6286(Smo 𝐴 ↔ (𝐴:dom 𝐴⟢On ∧ Ord dom 𝐴 ∧ βˆ€π‘₯ ∈ dom π΄βˆ€π‘¦ ∈ dom 𝐴(π‘₯ ∈ 𝑦 β†’ (π΄β€˜π‘₯) ∈ (π΄β€˜π‘¦))))
crecs 6304class recs(𝐹)
df-recs 6305recs(𝐹) = βˆͺ {𝑓 ∣ βˆƒπ‘₯ ∈ On (𝑓 Fn π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (π‘“β€˜π‘¦) = (πΉβ€˜(𝑓 β†Ύ 𝑦)))}
crdg 6369class rec(𝐹, 𝐼)
df-irdg 6370rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 βˆͺ βˆͺ π‘₯ ∈ dom 𝑔(πΉβ€˜(π‘”β€˜π‘₯)))))
cfrec 6390class frec(𝐹, 𝐼)
df-frec 6391frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {π‘₯ ∣ (βˆƒπ‘š ∈ Ο‰ (dom 𝑔 = suc π‘š ∧ π‘₯ ∈ (πΉβ€˜(π‘”β€˜π‘š))) ∨ (dom 𝑔 = βˆ… ∧ π‘₯ ∈ 𝐼))})) β†Ύ Ο‰)
c1o 6409class 1o
c2o 6410class 2o
c3o 6411class 3o
c4o 6412class 4o
coa 6413class +o
comu 6414class Β·o
coei 6415class ↑o
df-1o 64161o = suc βˆ…
df-2o 64172o = suc 1o
df-3o 64183o = suc 2o
df-4o 64194o = suc 3o
df-oadd 6420 +o = (π‘₯ ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), π‘₯)β€˜π‘¦))
df-omul 6421 Β·o = (π‘₯ ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o π‘₯)), βˆ…)β€˜π‘¦))
df-oexpi 6422 ↑o = (π‘₯ ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 Β·o π‘₯)), 1o)β€˜π‘¦))
wer 6531wff 𝑅 Er 𝐴
cec 6532class [𝐴]𝑅
cqs 6533class (𝐴 / 𝑅)
df-er 6534(𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◑𝑅 βˆͺ (𝑅 ∘ 𝑅)) βŠ† 𝑅))
df-ec 6536[𝐴]𝑅 = (𝑅 β€œ {𝐴})
df-qs 6540(𝐴 / 𝑅) = {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = [π‘₯]𝑅}
cmap 6647class β†‘π‘š
cpm 6648class ↑pm
df-map 6649 β†‘π‘š = (π‘₯ ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:π‘¦βŸΆπ‘₯})
df-pm 6650 ↑pm = (π‘₯ ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 Γ— π‘₯) ∣ Fun 𝑓})
cixp 6697class Xπ‘₯ ∈ 𝐴 𝐡
df-ixp 6698Xπ‘₯ ∈ 𝐴 𝐡 = {𝑓 ∣ (𝑓 Fn {π‘₯ ∣ π‘₯ ∈ 𝐴} ∧ βˆ€π‘₯ ∈ 𝐴 (π‘“β€˜π‘₯) ∈ 𝐡)}
cen 6737class β‰ˆ
cdom 6738class β‰Ό
cfn 6739class Fin
df-en 6740 β‰ˆ = {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ 𝑓:π‘₯–1-1-onto→𝑦}
df-dom 6741 β‰Ό = {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ 𝑓:π‘₯–1-1→𝑦}
df-fin 6742Fin = {π‘₯ ∣ βˆƒπ‘¦ ∈ Ο‰ π‘₯ β‰ˆ 𝑦}
cfi 6966class fi
df-fi 6967fi = (π‘₯ ∈ V ↦ {𝑧 ∣ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑧 = ∩ 𝑦})
csup 6980class sup(𝐴, 𝐡, 𝑅)
cinf 6981class inf(𝐴, 𝐡, 𝑅)
df-sup 6982sup(𝐴, 𝐡, 𝑅) = βˆͺ {π‘₯ ∈ 𝐡 ∣ (βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯𝑅𝑦 ∧ βˆ€π‘¦ ∈ 𝐡 (𝑦𝑅π‘₯ β†’ βˆƒπ‘§ ∈ 𝐴 𝑦𝑅𝑧))}
df-inf 6983inf(𝐴, 𝐡, 𝑅) = sup(𝐴, 𝐡, ◑𝑅)
cdju 7035class (𝐴 βŠ” 𝐡)
df-dju 7036(𝐴 βŠ” 𝐡) = (({βˆ…} Γ— 𝐴) βˆͺ ({1o} Γ— 𝐡))
cinl 7043class inl
cinr 7044class inr
df-inl 7045inl = (π‘₯ ∈ V ↦ βŸ¨βˆ…, π‘₯⟩)
df-inr 7046inr = (π‘₯ ∈ V ↦ ⟨1o, π‘₯⟩)
cdjucase 7081class case(𝑅, 𝑆)
df-case 7082case(𝑅, 𝑆) = ((𝑅 ∘ β—‘inl) βˆͺ (𝑆 ∘ β—‘inr))
cdjud 7100class (𝑅 βŠ”d 𝑆)
df-djud 7101(𝑅 βŠ”d 𝑆) = ((𝑅 ∘ β—‘(inl β†Ύ dom 𝑅)) βˆͺ (𝑆 ∘ β—‘(inr β†Ύ dom 𝑆)))
xnninf 7117class β„•βˆž
df-nninf 7118β„•βˆž = {𝑓 ∈ (2o β†‘π‘š Ο‰) ∣ βˆ€π‘– ∈ Ο‰ (π‘“β€˜suc 𝑖) βŠ† (π‘“β€˜π‘–)}
comni 7131class Omni
df-omni 7132Omni = {𝑦 ∣ βˆ€π‘“(𝑓:π‘¦βŸΆ2o β†’ (βˆƒπ‘₯ ∈ 𝑦 (π‘“β€˜π‘₯) = βˆ… ∨ βˆ€π‘₯ ∈ 𝑦 (π‘“β€˜π‘₯) = 1o))}
cmarkov 7148class Markov
df-markov 7149Markov = {𝑦 ∣ βˆ€π‘“(𝑓:π‘¦βŸΆ2o β†’ (Β¬ βˆ€π‘₯ ∈ 𝑦 (π‘“β€˜π‘₯) = 1o β†’ βˆƒπ‘₯ ∈ 𝑦 (π‘“β€˜π‘₯) = βˆ…))}
cwomni 7160class WOmni
df-womni 7161WOmni = {𝑦 ∣ βˆ€π‘“(𝑓:π‘¦βŸΆ2o β†’ DECID βˆ€π‘₯ ∈ 𝑦 (π‘“β€˜π‘₯) = 1o)}
ccrd 7177class card
df-card 7178card = (π‘₯ ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑦 β‰ˆ π‘₯})
wac 7203wff CHOICE
df-ac 7204(CHOICE ↔ βˆ€π‘₯βˆƒπ‘“(𝑓 βŠ† π‘₯ ∧ 𝑓 Fn dom π‘₯))
wap 7245wff 𝑅 Ap 𝐴
df-pap 7246(𝑅 Ap 𝐴 ↔ ((𝑅 βŠ† (𝐴 Γ— 𝐴) ∧ βˆ€π‘₯ ∈ 𝐴 Β¬ π‘₯𝑅π‘₯) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯𝑅𝑦 β†’ 𝑦𝑅π‘₯) ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘§ ∈ 𝐴 (π‘₯𝑅𝑦 β†’ (π‘₯𝑅𝑧 ∨ 𝑦𝑅𝑧)))))
wtap 7247wff 𝑅 TAp 𝐴
df-tap 7248(𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (Β¬ π‘₯𝑅𝑦 β†’ π‘₯ = 𝑦)))
wacc 7260wff CCHOICE
df-cc 7261(CCHOICE ↔ βˆ€π‘₯(dom π‘₯ β‰ˆ Ο‰ β†’ βˆƒπ‘“(𝑓 βŠ† π‘₯ ∧ 𝑓 Fn dom π‘₯)))
cnpi 7270class N
cpli 7271class +N
cmi 7272class Β·N
clti 7273class <N
cplpq 7274class +pQ
cmpq 7275class Β·pQ
cltpq 7276class <pQ
ceq 7277class ~Q
cnq 7278class Q
c1q 7279class 1Q
cplq 7280class +Q
cmq 7281class Β·Q
crq 7282class *Q
cltq 7283class <Q
ceq0 7284class ~Q0
cnq0 7285class Q0
c0q0 7286class 0Q0
cplq0 7287class +Q0
cmq0 7288class Β·Q0
cnp 7289class P
c1p 7290class 1P
cpp 7291class +P
cmp 7292class Β·P
cltp 7293class <P
cer 7294class ~R
cnr 7295class R
c0r 7296class 0R
c1r 7297class 1R
cm1r 7298class -1R
cplr 7299class +R
cmr 7300class Β·R
cltr 7301class <R
df-ni 7302N = (Ο‰ βˆ– {βˆ…})
df-pli 7303 +N = ( +o β†Ύ (N Γ— N))
df-mi 7304 Β·N = ( Β·o β†Ύ (N Γ— N))
df-lti 7305 <N = ( E ∩ (N Γ— N))
df-plpq 7342 +pQ = (π‘₯ ∈ (N Γ— N), 𝑦 ∈ (N Γ— N) ↦ ⟨(((1st β€˜π‘₯) Β·N (2nd β€˜π‘¦)) +N ((1st β€˜π‘¦) Β·N (2nd β€˜π‘₯))), ((2nd β€˜π‘₯) Β·N (2nd β€˜π‘¦))⟩)
df-mpq 7343 Β·pQ = (π‘₯ ∈ (N Γ— N), 𝑦 ∈ (N Γ— N) ↦ ⟨((1st β€˜π‘₯) Β·N (1st β€˜π‘¦)), ((2nd β€˜π‘₯) Β·N (2nd β€˜π‘¦))⟩)
df-ltpq 7344 <pQ = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (N Γ— N) ∧ 𝑦 ∈ (N Γ— N)) ∧ ((1st β€˜π‘₯) Β·N (2nd β€˜π‘¦)) <N ((1st β€˜π‘¦) Β·N (2nd β€˜π‘₯)))}
df-enq 7345 ~Q = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (N Γ— N) ∧ 𝑦 ∈ (N Γ— N)) ∧ βˆƒπ‘§βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’((π‘₯ = βŸ¨π‘§, π‘€βŸ© ∧ 𝑦 = βŸ¨π‘£, π‘’βŸ©) ∧ (𝑧 Β·N 𝑒) = (𝑀 Β·N 𝑣)))}
df-nqqs 7346Q = ((N Γ— N) / ~Q )
df-plqqs 7347 +Q = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ Q ∧ 𝑦 ∈ Q) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~Q ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~Q ) ∧ 𝑧 = [(βŸ¨π‘€, π‘£βŸ© +pQ βŸ¨π‘’, π‘“βŸ©)] ~Q ))}
df-mqqs 7348 Β·Q = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ Q ∧ 𝑦 ∈ Q) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~Q ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~Q ) ∧ 𝑧 = [(βŸ¨π‘€, π‘£βŸ© Β·pQ βŸ¨π‘’, π‘“βŸ©)] ~Q ))}
df-1nqqs 73491Q = [⟨1o, 1o⟩] ~Q
df-rq 7350*Q = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ Q ∧ 𝑦 ∈ Q ∧ (π‘₯ Β·Q 𝑦) = 1Q)}
df-ltnqqs 7351 <Q = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ Q ∧ 𝑦 ∈ Q) ∧ βˆƒπ‘§βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’((π‘₯ = [βŸ¨π‘§, π‘€βŸ©] ~Q ∧ 𝑦 = [βŸ¨π‘£, π‘’βŸ©] ~Q ) ∧ (𝑧 Β·N 𝑒) <N (𝑀 Β·N 𝑣)))}
df-enq0 7422 ~Q0 = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (Ο‰ Γ— N) ∧ 𝑦 ∈ (Ο‰ Γ— N)) ∧ βˆƒπ‘§βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’((π‘₯ = βŸ¨π‘§, π‘€βŸ© ∧ 𝑦 = βŸ¨π‘£, π‘’βŸ©) ∧ (𝑧 Β·o 𝑒) = (𝑀 Β·o 𝑣)))}
df-nq0 7423Q0 = ((Ο‰ Γ— N) / ~Q0 )
df-0nq0 74240Q0 = [βŸ¨βˆ…, 1o⟩] ~Q0
df-plq0 7425 +Q0 = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~Q0 ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~Q0 ) ∧ 𝑧 = [⟨((𝑀 Β·o 𝑓) +o (𝑣 Β·o 𝑒)), (𝑣 Β·o 𝑓)⟩] ~Q0 ))}
df-mq0 7426 Β·Q0 = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~Q0 ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~Q0 ) ∧ 𝑧 = [⟨(𝑀 Β·o 𝑒), (𝑣 Β·o 𝑓)⟩] ~Q0 ))}
df-inp 7464P = {βŸ¨π‘™, π‘’βŸ© ∣ (((𝑙 βŠ† Q ∧ 𝑒 βŠ† Q) ∧ (βˆƒπ‘ž ∈ Q π‘ž ∈ 𝑙 ∧ βˆƒπ‘Ÿ ∈ Q π‘Ÿ ∈ 𝑒)) ∧ ((βˆ€π‘ž ∈ Q (π‘ž ∈ 𝑙 ↔ βˆƒπ‘Ÿ ∈ Q (π‘ž <Q π‘Ÿ ∧ π‘Ÿ ∈ 𝑙)) ∧ βˆ€π‘Ÿ ∈ Q (π‘Ÿ ∈ 𝑒 ↔ βˆƒπ‘ž ∈ Q (π‘ž <Q π‘Ÿ ∧ π‘ž ∈ 𝑒))) ∧ βˆ€π‘ž ∈ Q Β¬ (π‘ž ∈ 𝑙 ∧ π‘ž ∈ 𝑒) ∧ βˆ€π‘ž ∈ Q βˆ€π‘Ÿ ∈ Q (π‘ž <Q π‘Ÿ β†’ (π‘ž ∈ 𝑙 ∨ π‘Ÿ ∈ 𝑒))))}
df-i1p 74651P = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑒 ∣ 1Q <Q 𝑒}⟩
df-iplp 7466 +P = (π‘₯ ∈ P, 𝑦 ∈ P ↦ ⟨{π‘ž ∈ Q ∣ βˆƒπ‘Ÿ ∈ Q βˆƒπ‘  ∈ Q (π‘Ÿ ∈ (1st β€˜π‘₯) ∧ 𝑠 ∈ (1st β€˜π‘¦) ∧ π‘ž = (π‘Ÿ +Q 𝑠))}, {π‘ž ∈ Q ∣ βˆƒπ‘Ÿ ∈ Q βˆƒπ‘  ∈ Q (π‘Ÿ ∈ (2nd β€˜π‘₯) ∧ 𝑠 ∈ (2nd β€˜π‘¦) ∧ π‘ž = (π‘Ÿ +Q 𝑠))}⟩)
df-imp 7467 Β·P = (π‘₯ ∈ P, 𝑦 ∈ P ↦ ⟨{π‘ž ∈ Q ∣ βˆƒπ‘Ÿ ∈ Q βˆƒπ‘  ∈ Q (π‘Ÿ ∈ (1st β€˜π‘₯) ∧ 𝑠 ∈ (1st β€˜π‘¦) ∧ π‘ž = (π‘Ÿ Β·Q 𝑠))}, {π‘ž ∈ Q ∣ βˆƒπ‘Ÿ ∈ Q βˆƒπ‘  ∈ Q (π‘Ÿ ∈ (2nd β€˜π‘₯) ∧ 𝑠 ∈ (2nd β€˜π‘¦) ∧ π‘ž = (π‘Ÿ Β·Q 𝑠))}⟩)
df-iltp 7468<P = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ P ∧ 𝑦 ∈ P) ∧ βˆƒπ‘ž ∈ Q (π‘ž ∈ (2nd β€˜π‘₯) ∧ π‘ž ∈ (1st β€˜π‘¦)))}
df-enr 7724 ~R = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (P Γ— P) ∧ 𝑦 ∈ (P Γ— P)) ∧ βˆƒπ‘§βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’((π‘₯ = βŸ¨π‘§, π‘€βŸ© ∧ 𝑦 = βŸ¨π‘£, π‘’βŸ©) ∧ (𝑧 +P 𝑒) = (𝑀 +P 𝑣)))}
df-nr 7725R = ((P Γ— P) / ~R )
df-plr 7726 +R = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ R ∧ 𝑦 ∈ R) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~R ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~R ) ∧ 𝑧 = [⟨(𝑀 +P 𝑒), (𝑣 +P 𝑓)⟩] ~R ))}
df-mr 7727 Β·R = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ R ∧ 𝑦 ∈ R) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = [βŸ¨π‘€, π‘£βŸ©] ~R ∧ 𝑦 = [βŸ¨π‘’, π‘“βŸ©] ~R ) ∧ 𝑧 = [⟨((𝑀 Β·P 𝑒) +P (𝑣 Β·P 𝑓)), ((𝑀 Β·P 𝑓) +P (𝑣 Β·P 𝑒))⟩] ~R ))}
df-ltr 7728 <R = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ R ∧ 𝑦 ∈ R) ∧ βˆƒπ‘§βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’((π‘₯ = [βŸ¨π‘§, π‘€βŸ©] ~R ∧ 𝑦 = [βŸ¨π‘£, π‘’βŸ©] ~R ) ∧ (𝑧 +P 𝑒)<P (𝑀 +P 𝑣)))}
df-0r 77290R = [⟨1P, 1P⟩] ~R
df-1r 77301R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 7731-1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 7808class β„‚
cr 7809class ℝ
cc0 7810class 0
c1 7811class 1
ci 7812class i
caddc 7813class +
cltrr 7814class <ℝ
cmul 7815class Β·
df-c 7816β„‚ = (R Γ— R)
df-0 78170 = ⟨0R, 0R⟩
df-1 78181 = ⟨1R, 0R⟩
df-i 7819i = ⟨0R, 1R⟩
df-r 7820ℝ = (R Γ— {0R})
df-add 7821 + = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = βŸ¨π‘€, π‘£βŸ© ∧ 𝑦 = βŸ¨π‘’, π‘“βŸ©) ∧ 𝑧 = ⟨(𝑀 +R 𝑒), (𝑣 +R 𝑓)⟩))}
df-mul 7822 Β· = {⟨⟨π‘₯, π‘¦βŸ©, π‘§βŸ© ∣ ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚) ∧ βˆƒπ‘€βˆƒπ‘£βˆƒπ‘’βˆƒπ‘“((π‘₯ = βŸ¨π‘€, π‘£βŸ© ∧ 𝑦 = βŸ¨π‘’, π‘“βŸ©) ∧ 𝑧 = ⟨((𝑀 Β·R 𝑒) +R (-1R Β·R (𝑣 Β·R 𝑓))), ((𝑣 Β·R 𝑒) +R (𝑀 Β·R 𝑓))⟩))}
df-lt 7823 <ℝ = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ βˆƒπ‘§βˆƒπ‘€((π‘₯ = βŸ¨π‘§, 0R⟩ ∧ 𝑦 = βŸ¨π‘€, 0R⟩) ∧ 𝑧 <R 𝑀))}
ax-cnex 7901β„‚ ∈ V
ax-resscn 7902ℝ βŠ† β„‚
ax-1cn 79031 ∈ β„‚
ax-1re 79041 ∈ ℝ
ax-icn 7905i ∈ β„‚
ax-addcl 7906((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 + 𝐡) ∈ β„‚)
ax-addrcl 7907((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴 + 𝐡) ∈ ℝ)
ax-mulcl 7908((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 Β· 𝐡) ∈ β„‚)
ax-mulrcl 7909((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴 Β· 𝐡) ∈ ℝ)
ax-addcom 7910((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 + 𝐡) = (𝐡 + 𝐴))
ax-mulcom 7911((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 Β· 𝐡) = (𝐡 Β· 𝐴))
ax-addass 7912((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐴 + 𝐡) + 𝐢) = (𝐴 + (𝐡 + 𝐢)))
ax-mulass 7913((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐴 Β· 𝐡) Β· 𝐢) = (𝐴 Β· (𝐡 Β· 𝐢)))
ax-distr 7914((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ (𝐴 Β· (𝐡 + 𝐢)) = ((𝐴 Β· 𝐡) + (𝐴 Β· 𝐢)))
ax-i2m1 7915((i Β· i) + 1) = 0
ax-0lt1 79160 <ℝ 1
ax-1rid 7917(𝐴 ∈ ℝ β†’ (𝐴 Β· 1) = 𝐴)
ax-0id 7918(𝐴 ∈ β„‚ β†’ (𝐴 + 0) = 𝐴)
ax-rnegex 7919(𝐴 ∈ ℝ β†’ βˆƒπ‘₯ ∈ ℝ (𝐴 + π‘₯) = 0)
ax-precex 7920((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) β†’ βˆƒπ‘₯ ∈ ℝ (0 <ℝ π‘₯ ∧ (𝐴 Β· π‘₯) = 1))
ax-cnre 7921(𝐴 ∈ β„‚ β†’ βˆƒπ‘₯ ∈ ℝ βˆƒπ‘¦ ∈ ℝ 𝐴 = (π‘₯ + (i Β· 𝑦)))
ax-pre-ltirr 7922(𝐴 ∈ ℝ β†’ Β¬ 𝐴 <ℝ 𝐴)
ax-pre-ltwlin 7923((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ (𝐴 <ℝ 𝐡 β†’ (𝐴 <ℝ 𝐢 ∨ 𝐢 <ℝ 𝐡)))
ax-pre-lttrn 7924((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ ((𝐴 <ℝ 𝐡 ∧ 𝐡 <ℝ 𝐢) β†’ 𝐴 <ℝ 𝐢))
ax-pre-apti 7925((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ Β¬ (𝐴 <ℝ 𝐡 ∨ 𝐡 <ℝ 𝐴)) β†’ 𝐴 = 𝐡)
ax-pre-ltadd 7926((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ (𝐴 <ℝ 𝐡 β†’ (𝐢 + 𝐴) <ℝ (𝐢 + 𝐡)))
ax-pre-mulgt0 7927((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐡) β†’ 0 <ℝ (𝐴 Β· 𝐡)))
ax-pre-mulext 7928((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ ((𝐴 Β· 𝐢) <ℝ (𝐡 Β· 𝐢) β†’ (𝐴 <ℝ 𝐡 ∨ 𝐡 <ℝ 𝐴)))
ax-arch 7929(𝐴 ∈ ℝ β†’ βˆƒπ‘› ∈ ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}𝐴 <ℝ 𝑛)
ax-caucvg 7930𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    &   (πœ‘ β†’ 𝐹:π‘βŸΆβ„)    &   (πœ‘ β†’ βˆ€π‘› ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑛 <ℝ π‘˜ β†’ ((πΉβ€˜π‘›) <ℝ ((πΉβ€˜π‘˜) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)) ∧ (πΉβ€˜π‘˜) <ℝ ((πΉβ€˜π‘›) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)))))    β‡’   (πœ‘ β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘₯ ∈ ℝ (0 <ℝ π‘₯ β†’ βˆƒπ‘— ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯)))))
ax-pre-suploc 7931(((𝐴 βŠ† ℝ ∧ βˆƒπ‘₯ π‘₯ ∈ 𝐴) ∧ (βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ 𝐴 𝑦 <ℝ π‘₯ ∧ βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ <ℝ 𝑦 β†’ (βˆƒπ‘§ ∈ 𝐴 π‘₯ <ℝ 𝑧 ∨ βˆ€π‘§ ∈ 𝐴 𝑧 <ℝ 𝑦)))) β†’ βˆƒπ‘₯ ∈ ℝ (βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <ℝ 𝑦 ∧ βˆ€π‘¦ ∈ ℝ (𝑦 <ℝ π‘₯ β†’ βˆƒπ‘§ ∈ 𝐴 𝑦 <ℝ 𝑧)))
ax-addf 7932 + :(β„‚ Γ— β„‚)βŸΆβ„‚
ax-mulf 7933 Β· :(β„‚ Γ— β„‚)βŸΆβ„‚
cpnf 7988class +∞
cmnf 7989class -∞
cxr 7990class ℝ*
clt 7991class <
cle 7992class ≀
df-pnf 7993+∞ = 𝒫 βˆͺ β„‚
df-mnf 7994-∞ = 𝒫 +∞
df-xr 7995ℝ* = (ℝ βˆͺ {+∞, -∞})
df-ltxr 7996 < = ({⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ π‘₯ <ℝ 𝑦)} βˆͺ (((ℝ βˆͺ {-∞}) Γ— {+∞}) βˆͺ ({-∞} Γ— ℝ)))
df-le 7997 ≀ = ((ℝ* Γ— ℝ*) βˆ– β—‘ < )
cmin 8127class βˆ’
cneg 8128class -𝐴
df-sub 8129 βˆ’ = (π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (℩𝑧 ∈ β„‚ (𝑦 + 𝑧) = π‘₯))
df-neg 8130-𝐴 = (0 βˆ’ 𝐴)
creap 8530class #ℝ
df-reap 8531 #ℝ = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (π‘₯ < 𝑦 ∨ 𝑦 < π‘₯))}
cap 8537class #
df-ap 8538 # = {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘Ÿ ∈ ℝ βˆƒπ‘  ∈ ℝ βˆƒπ‘‘ ∈ ℝ βˆƒπ‘’ ∈ ℝ ((π‘₯ = (π‘Ÿ + (i Β· 𝑠)) ∧ 𝑦 = (𝑑 + (i Β· 𝑒))) ∧ (π‘Ÿ #ℝ 𝑑 ∨ 𝑠 #ℝ 𝑒))}
cdiv 8628class /
df-div 8629 / = (π‘₯ ∈ β„‚, 𝑦 ∈ (β„‚ βˆ– {0}) ↦ (℩𝑧 ∈ β„‚ (𝑦 Β· 𝑧) = π‘₯))
cn 8918class β„•
df-inn 8919β„• = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}
c2 8969class 2
c3 8970class 3
c4 8971class 4
c5 8972class 5
c6 8973class 6
c7 8974class 7
c8 8975class 8
c9 8976class 9
df-2 89772 = (1 + 1)
df-3 89783 = (2 + 1)
df-4 89794 = (3 + 1)
df-5 89805 = (4 + 1)
df-6 89816 = (5 + 1)
df-7 89827 = (6 + 1)
df-8 89838 = (7 + 1)
df-9 89849 = (8 + 1)
cn0 9175class β„•0
df-n0 9176β„•0 = (β„• βˆͺ {0})
cxnn0 9238class β„•0*
df-xnn0 9239β„•0* = (β„•0 βˆͺ {+∞})
cz 9252class β„€
df-z 9253β„€ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ β„• ∨ -𝑛 ∈ β„•)}
cdc 9383class 𝐴𝐡
df-dec 9384𝐴𝐡 = (((9 + 1) Β· 𝐴) + 𝐡)
cuz 9527class β„€β‰₯
df-uz 9528β„€β‰₯ = (𝑗 ∈ β„€ ↦ {π‘˜ ∈ β„€ ∣ 𝑗 ≀ π‘˜})
cq 9618class β„š
df-q 9619β„š = ( / β€œ (β„€ Γ— β„•))
crp 9652class ℝ+
df-rp 9653ℝ+ = {π‘₯ ∈ ℝ ∣ 0 < π‘₯}
cxne 9768class -𝑒𝐴
cxad 9769class +𝑒
cxmu 9770class Β·e
df-xneg 9771-𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
df-xadd 9772 +𝑒 = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(π‘₯ = +∞, if(𝑦 = -∞, 0, +∞), if(π‘₯ = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (π‘₯ + 𝑦))))))
df-xmul 9773 Β·e = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((π‘₯ = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ π‘₯ = +∞) ∨ (𝑦 < 0 ∧ π‘₯ = -∞)) ∨ ((0 < π‘₯ ∧ 𝑦 = +∞) ∨ (π‘₯ < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ π‘₯ = -∞) ∨ (𝑦 < 0 ∧ π‘₯ = +∞)) ∨ ((0 < π‘₯ ∧ 𝑦 = -∞) ∨ (π‘₯ < 0 ∧ 𝑦 = +∞))), -∞, (π‘₯ Β· 𝑦)))))
cioo 9887class (,)
cioc 9888class (,]
cico 9889class [,)
cicc 9890class [,]
df-ioo 9891(,) = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (π‘₯ < 𝑧 ∧ 𝑧 < 𝑦)})
df-ioc 9892(,] = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (π‘₯ < 𝑧 ∧ 𝑧 ≀ 𝑦)})
df-ico 9893[,) = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (π‘₯ ≀ 𝑧 ∧ 𝑧 < 𝑦)})
df-icc 9894[,] = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (π‘₯ ≀ 𝑧 ∧ 𝑧 ≀ 𝑦)})
cfz 10007class ...
df-fz 10008... = (π‘š ∈ β„€, 𝑛 ∈ β„€ ↦ {π‘˜ ∈ β„€ ∣ (π‘š ≀ π‘˜ ∧ π‘˜ ≀ 𝑛)})
cfzo 10141class ..^
df-fzo 10142..^ = (π‘š ∈ β„€, 𝑛 ∈ β„€ ↦ (π‘š...(𝑛 βˆ’ 1)))
cfl 10267class ⌊
cceil 10268class ⌈
df-fl 10269⌊ = (π‘₯ ∈ ℝ ↦ (℩𝑦 ∈ β„€ (𝑦 ≀ π‘₯ ∧ π‘₯ < (𝑦 + 1))))
df-ceil 10270⌈ = (π‘₯ ∈ ℝ ↦ -(βŒŠβ€˜-π‘₯))
cmo 10321class mod
df-mod 10322 mod = (π‘₯ ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (π‘₯ βˆ’ (𝑦 Β· (βŒŠβ€˜(π‘₯ / 𝑦)))))
cseq 10444class seq𝑀( + , 𝐹)
df-seqfrec 10445seq𝑀( + , 𝐹) = ran frec((π‘₯ ∈ (β„€β‰₯β€˜π‘€), 𝑦 ∈ V ↦ ⟨(π‘₯ + 1), (𝑦 + (πΉβ€˜(π‘₯ + 1)))⟩), βŸ¨π‘€, (πΉβ€˜π‘€)⟩)
cexp 10518class ↑
df-exp 10519↑ = (π‘₯ ∈ β„‚, 𝑦 ∈ β„€ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( Β· , (β„• Γ— {π‘₯}))β€˜π‘¦), (1 / (seq1( Β· , (β„• Γ— {π‘₯}))β€˜-𝑦)))))
cfa 10704class !
df-fac 10705! = ({⟨0, 1⟩} βˆͺ seq1( Β· , I ))
cbc 10726class C
df-bc 10727C = (𝑛 ∈ β„•0, π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ (0...𝑛), ((!β€˜π‘›) / ((!β€˜(𝑛 βˆ’ π‘˜)) Β· (!β€˜π‘˜))), 0))
chash 10754class β™―
df-ihash 10755β™― = ((frec((π‘₯ ∈ β„€ ↦ (π‘₯ + 1)), 0) βˆͺ {βŸ¨Ο‰, +∞⟩}) ∘ (π‘₯ ∈ V ↦ βˆͺ {𝑦 ∈ (Ο‰ βˆͺ {Ο‰}) ∣ 𝑦 β‰Ό π‘₯}))
cshi 10822class shift
df-shft 10823 shift = (𝑓 ∈ V, π‘₯ ∈ β„‚ ↦ {βŸ¨π‘¦, π‘§βŸ© ∣ (𝑦 ∈ β„‚ ∧ (𝑦 βˆ’ π‘₯)𝑓𝑧)})
ccj 10847class βˆ—
cre 10848class β„œ
cim 10849class β„‘
df-cj 10850βˆ— = (π‘₯ ∈ β„‚ ↦ (℩𝑦 ∈ β„‚ ((π‘₯ + 𝑦) ∈ ℝ ∧ (i Β· (π‘₯ βˆ’ 𝑦)) ∈ ℝ)))
df-re 10851β„œ = (π‘₯ ∈ β„‚ ↦ ((π‘₯ + (βˆ—β€˜π‘₯)) / 2))
df-im 10852β„‘ = (π‘₯ ∈ β„‚ ↦ (β„œβ€˜(π‘₯ / i)))
csqrt 11004class √
cabs 11005class abs
df-rsqrt 11006√ = (π‘₯ ∈ ℝ ↦ (℩𝑦 ∈ ℝ ((𝑦↑2) = π‘₯ ∧ 0 ≀ 𝑦)))
df-abs 11007abs = (π‘₯ ∈ β„‚ ↦ (βˆšβ€˜(π‘₯ Β· (βˆ—β€˜π‘₯))))
cli 11285class ⇝
df-clim 11286 ⇝ = {βŸ¨π‘“, π‘¦βŸ© ∣ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((π‘“β€˜π‘˜) ∈ β„‚ ∧ (absβ€˜((π‘“β€˜π‘˜) βˆ’ 𝑦)) < π‘₯))}
csu 11360class Ξ£π‘˜ ∈ 𝐴 𝐡
df-sumdc 11361Ξ£π‘˜ ∈ 𝐴 𝐡 = (β„©π‘₯(βˆƒπ‘š ∈ β„€ (𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴 ∧ seqπ‘š( + , (𝑛 ∈ β„€ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / π‘˜β¦Œπ΅, 0))) ⇝ π‘₯) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( + , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 0)))β€˜π‘š))))
cprod 11557class βˆπ‘˜ ∈ 𝐴 𝐡
df-proddc 11558βˆπ‘˜ ∈ 𝐴 𝐡 = (β„©π‘₯(βˆƒπ‘š ∈ β„€ ((𝐴 βŠ† (β„€β‰₯β€˜π‘š) ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘š)DECID 𝑗 ∈ 𝐴) ∧ (βˆƒπ‘› ∈ (β„€β‰₯β€˜π‘š)βˆƒπ‘¦(𝑦 # 0 ∧ seq𝑛( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ 𝑦) ∧ seqπ‘š( Β· , (π‘˜ ∈ β„€ ↦ if(π‘˜ ∈ 𝐴, 𝐡, 1))) ⇝ π‘₯)) ∨ βˆƒπ‘š ∈ β„• βˆƒπ‘“(𝑓:(1...π‘š)–1-1-onto→𝐴 ∧ π‘₯ = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ≀ π‘š, ⦋(π‘“β€˜π‘›) / π‘˜β¦Œπ΅, 1)))β€˜π‘š))))
ce 11649class exp
ceu 11650class e
csin 11651class sin
ccos 11652class cos
ctan 11653class tan
cpi 11654class Ο€
df-ef 11655exp = (π‘₯ ∈ β„‚ ↦ Ξ£π‘˜ ∈ β„•0 ((π‘₯β†‘π‘˜) / (!β€˜π‘˜)))
df-e 11656e = (expβ€˜1)
df-sin 11657sin = (π‘₯ ∈ β„‚ ↦ (((expβ€˜(i Β· π‘₯)) βˆ’ (expβ€˜(-i Β· π‘₯))) / (2 Β· i)))
df-cos 11658cos = (π‘₯ ∈ β„‚ ↦ (((expβ€˜(i Β· π‘₯)) + (expβ€˜(-i Β· π‘₯))) / 2))
df-tan 11659tan = (π‘₯ ∈ (β—‘cos β€œ (β„‚ βˆ– {0})) ↦ ((sinβ€˜π‘₯) / (cosβ€˜π‘₯)))
df-pi 11660Ο€ = inf((ℝ+ ∩ (β—‘sin β€œ {0})), ℝ, < )
ctau 11781class Ο„
df-tau 11782Ο„ = inf((ℝ+ ∩ (β—‘cos β€œ {1})), ℝ, < )
cdvds 11793class βˆ₯
df-dvds 11794 βˆ₯ = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ β„€ ∧ 𝑦 ∈ β„€) ∧ βˆƒπ‘› ∈ β„€ (𝑛 Β· π‘₯) = 𝑦)}
cgcd 11942class gcd
df-gcd 11943 gcd = (π‘₯ ∈ β„€, 𝑦 ∈ β„€ ↦ if((π‘₯ = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ β„€ ∣ (𝑛 βˆ₯ π‘₯ ∧ 𝑛 βˆ₯ 𝑦)}, ℝ, < )))
clcm 12059class lcm
df-lcm 12060 lcm = (π‘₯ ∈ β„€, 𝑦 ∈ β„€ ↦ if((π‘₯ = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ β„• ∣ (π‘₯ βˆ₯ 𝑛 ∧ 𝑦 βˆ₯ 𝑛)}, ℝ, < )))
cprime 12106class β„™
df-prm 12107β„™ = {𝑝 ∈ β„• ∣ {𝑛 ∈ β„• ∣ 𝑛 βˆ₯ 𝑝} β‰ˆ 2o}
cnumer 12180class numer
cdenom 12181class denom
df-numer 12182numer = (𝑦 ∈ β„š ↦ (1st β€˜(β„©π‘₯ ∈ (β„€ Γ— β„•)(((1st β€˜π‘₯) gcd (2nd β€˜π‘₯)) = 1 ∧ 𝑦 = ((1st β€˜π‘₯) / (2nd β€˜π‘₯))))))
df-denom 12183denom = (𝑦 ∈ β„š ↦ (2nd β€˜(β„©π‘₯ ∈ (β„€ Γ— β„•)(((1st β€˜π‘₯) gcd (2nd β€˜π‘₯)) = 1 ∧ 𝑦 = ((1st β€˜π‘₯) / (2nd β€˜π‘₯))))))
codz 12207class odβ„€
cphi 12208class Ο•
df-odz 12209odβ„€ = (𝑛 ∈ β„• ↦ (π‘₯ ∈ {π‘₯ ∈ β„€ ∣ (π‘₯ gcd 𝑛) = 1} ↦ inf({π‘š ∈ β„• ∣ 𝑛 βˆ₯ ((π‘₯β†‘π‘š) βˆ’ 1)}, ℝ, < )))
df-phi 12210Ο• = (𝑛 ∈ β„• ↦ (β™―β€˜{π‘₯ ∈ (1...𝑛) ∣ (π‘₯ gcd 𝑛) = 1}))
cpc 12283class pCnt
df-pc 12284 pCnt = (𝑝 ∈ β„™, π‘Ÿ ∈ β„š ↦ if(π‘Ÿ = 0, +∞, (β„©π‘§βˆƒπ‘₯ ∈ β„€ βˆƒπ‘¦ ∈ β„• (π‘Ÿ = (π‘₯ / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ β„•0 ∣ (𝑝↑𝑛) βˆ₯ π‘₯}, ℝ, < ) βˆ’ sup({𝑛 ∈ β„•0 ∣ (𝑝↑𝑛) βˆ₯ 𝑦}, ℝ, < ))))))
cgz 12366class β„€[i]
df-gz 12367β„€[i] = {π‘₯ ∈ β„‚ ∣ ((β„œβ€˜π‘₯) ∈ β„€ ∧ (β„‘β€˜π‘₯) ∈ β„€)}
cstr 12457class Struct
cnx 12458class ndx
csts 12459class sSet
cslot 12460class Slot 𝐴
cbs 12461class Base
cress 12462class β†Ύs
df-struct 12463 Struct = {βŸ¨π‘“, π‘₯⟩ ∣ (π‘₯ ∈ ( ≀ ∩ (β„• Γ— β„•)) ∧ Fun (𝑓 βˆ– {βˆ…}) ∧ dom 𝑓 βŠ† (...β€˜π‘₯))}
df-ndx 12464ndx = ( I β†Ύ β„•)
df-slot 12465Slot 𝐴 = (π‘₯ ∈ V ↦ (π‘₯β€˜π΄))
df-base 12467Base = Slot 1
df-sets 12468 sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 β†Ύ (V βˆ– dom {𝑒})) βˆͺ {𝑒}))
df-iress 12469 β†Ύs = (𝑀 ∈ V, π‘₯ ∈ V ↦ (𝑀 sSet ⟨(Baseβ€˜ndx), (π‘₯ ∩ (Baseβ€˜π‘€))⟩))
cplusg 12535class +g
cmulr 12536class .r
cstv 12537class *π‘Ÿ
csca 12538class Scalar
cvsca 12539class ·𝑠
cip 12540class ·𝑖
cts 12541class TopSet
cple 12542class le
coc 12543class oc
cds 12544class dist
cunif 12545class UnifSet
chom 12546class Hom
cco 12547class comp
df-plusg 12548+g = Slot 2
df-mulr 12549.r = Slot 3
df-starv 12550*π‘Ÿ = Slot 4
df-sca 12551Scalar = Slot 5
df-vsca 12552 ·𝑠 = Slot 6
df-ip 12553·𝑖 = Slot 8
df-tset 12554TopSet = Slot 9
df-ple 12555le = Slot 10
df-ocomp 12556oc = Slot 11
df-ds 12557dist = Slot 12
df-unif 12558UnifSet = Slot 13
df-hom 12559Hom = Slot 14
df-cco 12560comp = Slot 15
crest 12687class β†Ύt
ctopn 12688class TopOpen
df-rest 12689 β†Ύt = (𝑗 ∈ V, π‘₯ ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ π‘₯)))
df-topn 12690TopOpen = (𝑀 ∈ V ↦ ((TopSetβ€˜π‘€) β†Ύt (Baseβ€˜π‘€)))
ctg 12702class topGen
cpt 12703class ∏t
c0g 12704class 0g
cgsu 12705class Ξ£g
df-0g 127060g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Baseβ€˜π‘”) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘”)((𝑒(+gβ€˜π‘”)π‘₯) = π‘₯ ∧ (π‘₯(+gβ€˜π‘”)𝑒) = π‘₯))))
df-gsum 12707 Ξ£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 12708topGen = (π‘₯ ∈ V ↦ {𝑦 ∣ 𝑦 βŠ† βˆͺ (π‘₯ ∩ 𝒫 𝑦)})
df-pt 12709∏t = (𝑓 ∈ V ↦ (topGenβ€˜{π‘₯ ∣ βˆƒπ‘”((𝑔 Fn dom 𝑓 ∧ βˆ€π‘¦ ∈ dom 𝑓(π‘”β€˜π‘¦) ∈ (π‘“β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (dom 𝑓 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ (π‘“β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ dom 𝑓(π‘”β€˜π‘¦))}))
cprds 12713class Xs
cpws 12714class ↑s
df-prds 12715Xs = (𝑠 ∈ 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 12718 ↑s = (π‘Ÿ ∈ V, 𝑖 ∈ V ↦ ((Scalarβ€˜π‘Ÿ)Xs(𝑖 Γ— {π‘Ÿ})))
cimas 12719class β€œs
cqus 12720class /s
cxps 12721class Γ—s
df-iimas 12722 β€œs = (𝑓 ∈ V, π‘Ÿ ∈ V ↦ ⦋(Baseβ€˜π‘Ÿ) / π‘£β¦Œ{⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩})
df-qus 12723 /s = (π‘Ÿ ∈ V, 𝑒 ∈ V ↦ ((π‘₯ ∈ (Baseβ€˜π‘Ÿ) ↦ [π‘₯]𝑒) β€œs π‘Ÿ))
df-xps 12724 Γ—s = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ (β—‘(π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑦 ∈ (Baseβ€˜π‘ ) ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) β€œs ((Scalarβ€˜π‘Ÿ)Xs{βŸ¨βˆ…, π‘ŸβŸ©, ⟨1o, π‘ βŸ©})))
cplusf 12771class +𝑓
cmgm 12772class Mgm
df-plusf 12773+𝑓 = (𝑔 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜π‘”), 𝑦 ∈ (Baseβ€˜π‘”) ↦ (π‘₯(+gβ€˜π‘”)𝑦)))
df-mgm 12774Mgm = {𝑔 ∣ [(Baseβ€˜π‘”) / 𝑏][(+gβ€˜π‘”) / π‘œ]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯π‘œπ‘¦) ∈ 𝑏}
csgrp 12806class Smgrp
df-sgrp 12807Smgrp = {𝑔 ∈ Mgm ∣ [(Baseβ€˜π‘”) / 𝑏][(+gβ€˜π‘”) / π‘œ]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 ((π‘₯π‘œπ‘¦)π‘œπ‘§) = (π‘₯π‘œ(π‘¦π‘œπ‘§))}
cmnd 12816class Mnd
df-mnd 12817Mnd = {𝑔 ∈ Smgrp ∣ [(Baseβ€˜π‘”) / 𝑏][(+gβ€˜π‘”) / 𝑝]βˆƒπ‘’ ∈ 𝑏 βˆ€π‘₯ ∈ 𝑏 ((𝑒𝑝π‘₯) = π‘₯ ∧ (π‘₯𝑝𝑒) = π‘₯)}
cmhm 12848class MndHom
csubmnd 12849class SubMnd
df-mhm 12850 MndHom = (𝑠 ∈ Mnd, 𝑑 ∈ Mnd ↦ {𝑓 ∈ ((Baseβ€˜π‘‘) β†‘π‘š (Baseβ€˜π‘ )) ∣ (βˆ€π‘₯ ∈ (Baseβ€˜π‘ )βˆ€π‘¦ ∈ (Baseβ€˜π‘ )(π‘“β€˜(π‘₯(+gβ€˜π‘ )𝑦)) = ((π‘“β€˜π‘₯)(+gβ€˜π‘‘)(π‘“β€˜π‘¦)) ∧ (π‘“β€˜(0gβ€˜π‘ )) = (0gβ€˜π‘‘))})
df-submnd 12851SubMnd = (𝑠 ∈ Mnd ↦ {𝑑 ∈ 𝒫 (Baseβ€˜π‘ ) ∣ ((0gβ€˜π‘ ) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘ )𝑦) ∈ 𝑑)})
cgrp 12876class Grp
cminusg 12877class invg
csg 12878class -g
df-grp 12879Grp = {𝑔 ∈ Mnd ∣ βˆ€π‘Ž ∈ (Baseβ€˜π‘”)βˆƒπ‘š ∈ (Baseβ€˜π‘”)(π‘š(+gβ€˜π‘”)π‘Ž) = (0gβ€˜π‘”)}
df-minusg 12880invg = (𝑔 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜π‘”) ↦ (℩𝑀 ∈ (Baseβ€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯) = (0gβ€˜π‘”))))
df-sbg 12881-g = (𝑔 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜π‘”), 𝑦 ∈ (Baseβ€˜π‘”) ↦ (π‘₯(+gβ€˜π‘”)((invgβ€˜π‘”)β€˜π‘¦))))
cmg 12982class .g
df-mulg 12983.g = (𝑔 ∈ V ↦ (𝑛 ∈ β„€, π‘₯ ∈ (Baseβ€˜π‘”) ↦ if(𝑛 = 0, (0gβ€˜π‘”), ⦋seq1((+gβ€˜π‘”), (β„• Γ— {π‘₯})) / π‘ β¦Œif(0 < 𝑛, (π‘ β€˜π‘›), ((invgβ€˜π‘”)β€˜(π‘ β€˜-𝑛))))))
csubg 13025class SubGrp
cnsg 13026class NrmSGrp
cqg 13027class ~QG
df-subg 13028SubGrp = (𝑀 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ∣ (𝑀 β†Ύs 𝑠) ∈ Grp})
df-nsg 13029NrmSGrp = (𝑀 ∈ Grp ↦ {𝑠 ∈ (SubGrpβ€˜π‘€) ∣ [(Baseβ€˜π‘€) / 𝑏][(+gβ€˜π‘€) / 𝑝]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 ((π‘₯𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝π‘₯) ∈ 𝑠)})
df-eqg 13030 ~QG = (π‘Ÿ ∈ V, 𝑖 ∈ V ↦ {⟨π‘₯, π‘¦βŸ© ∣ ({π‘₯, 𝑦} βŠ† (Baseβ€˜π‘Ÿ) ∧ (((invgβ€˜π‘Ÿ)β€˜π‘₯)(+gβ€˜π‘Ÿ)𝑦) ∈ 𝑖)})
ccmn 13086class CMnd
cabl 13087class Abel
df-cmn 13088CMnd = {𝑔 ∈ Mnd ∣ βˆ€π‘Ž ∈ (Baseβ€˜π‘”)βˆ€π‘ ∈ (Baseβ€˜π‘”)(π‘Ž(+gβ€˜π‘”)𝑏) = (𝑏(+gβ€˜π‘”)π‘Ž)}
df-abl 13089Abel = (Grp ∩ CMnd)
cmgp 13128class mulGrp
df-mgp 13129mulGrp = (𝑀 ∈ V ↦ (𝑀 sSet ⟨(+gβ€˜ndx), (.rβ€˜π‘€)⟩))
cur 13140class 1r
df-ur 131411r = (0g ∘ mulGrp)
csrg 13144class SRing
df-srg 13145SRing = {𝑓 ∈ CMnd ∣ ((mulGrpβ€˜π‘“) ∈ Mnd ∧ [(Baseβ€˜π‘“) / π‘Ÿ][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑][(0gβ€˜π‘“) / 𝑛]βˆ€π‘₯ ∈ π‘Ÿ (βˆ€π‘¦ ∈ π‘Ÿ βˆ€π‘§ ∈ π‘Ÿ ((π‘₯𝑑(𝑦𝑝𝑧)) = ((π‘₯𝑑𝑦)𝑝(π‘₯𝑑𝑧)) ∧ ((π‘₯𝑝𝑦)𝑑𝑧) = ((π‘₯𝑑𝑧)𝑝(𝑦𝑑𝑧))) ∧ ((𝑛𝑑π‘₯) = 𝑛 ∧ (π‘₯𝑑𝑛) = 𝑛)))}
crg 13177class Ring
ccrg 13178class CRing
df-ring 13179Ring = {𝑓 ∈ Grp ∣ ((mulGrpβ€˜π‘“) ∈ Mnd ∧ [(Baseβ€˜π‘“) / π‘Ÿ][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑]βˆ€π‘₯ ∈ π‘Ÿ βˆ€π‘¦ ∈ π‘Ÿ βˆ€π‘§ ∈ π‘Ÿ ((π‘₯𝑑(𝑦𝑝𝑧)) = ((π‘₯𝑑𝑦)𝑝(π‘₯𝑑𝑧)) ∧ ((π‘₯𝑝𝑦)𝑑𝑧) = ((π‘₯𝑑𝑧)𝑝(𝑦𝑑𝑧))))}
df-cring 13180CRing = {𝑓 ∈ Ring ∣ (mulGrpβ€˜π‘“) ∈ CMnd}
coppr 13237class oppr
df-oppr 13238oppr = (𝑓 ∈ V ↦ (𝑓 sSet ⟨(.rβ€˜ndx), tpos (.rβ€˜π‘“)⟩))
cdsr 13253class βˆ₯r
cui 13254class Unit
cir 13255class Irred
df-dvdsr 13256βˆ₯r = (𝑀 ∈ V ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ (Baseβ€˜π‘€) ∧ βˆƒπ‘§ ∈ (Baseβ€˜π‘€)(𝑧(.rβ€˜π‘€)π‘₯) = 𝑦)})
df-unit 13257Unit = (𝑀 ∈ V ↦ (β—‘((βˆ₯rβ€˜π‘€) ∩ (βˆ₯rβ€˜(opprβ€˜π‘€))) β€œ {(1rβ€˜π‘€)}))
df-irred 13258Irred = (𝑀 ∈ V ↦ ⦋((Baseβ€˜π‘€) βˆ– (Unitβ€˜π‘€)) / π‘β¦Œ{𝑧 ∈ 𝑏 ∣ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(.rβ€˜π‘€)𝑦) β‰  𝑧})
cinvr 13287class invr
df-invr 13288invr = (π‘Ÿ ∈ V ↦ (invgβ€˜((mulGrpβ€˜π‘Ÿ) β†Ύs (Unitβ€˜π‘Ÿ))))
cdvr 13298class /r
df-dvr 13299/r = (π‘Ÿ ∈ V ↦ (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑦 ∈ (Unitβ€˜π‘Ÿ) ↦ (π‘₯(.rβ€˜π‘Ÿ)((invrβ€˜π‘Ÿ)β€˜π‘¦))))
crh 13317class RingHom
crs 13318class RingIso
df-rnghom 13319 RingHom = (π‘Ÿ ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Baseβ€˜π‘Ÿ) / π‘£β¦Œβ¦‹(Baseβ€˜π‘ ) / π‘€β¦Œ{𝑓 ∈ (𝑀 β†‘π‘š 𝑣) ∣ ((π‘“β€˜(1rβ€˜π‘Ÿ)) = (1rβ€˜π‘ ) ∧ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘¦ ∈ 𝑣 ((π‘“β€˜(π‘₯(+gβ€˜π‘Ÿ)𝑦)) = ((π‘“β€˜π‘₯)(+gβ€˜π‘ )(π‘“β€˜π‘¦)) ∧ (π‘“β€˜(π‘₯(.rβ€˜π‘Ÿ)𝑦)) = ((π‘“β€˜π‘₯)(.rβ€˜π‘ )(π‘“β€˜π‘¦))))})
df-rngiso 13320 RingIso = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (π‘Ÿ RingHom 𝑠) ∣ ◑𝑓 ∈ (𝑠 RingHom π‘Ÿ)})
cnzr 13321class NzRing
df-nzr 13322NzRing = {π‘Ÿ ∈ Ring ∣ (1rβ€˜π‘Ÿ) β‰  (0gβ€˜π‘Ÿ)}
clring 13329class LRing
df-lring 13330LRing = {π‘Ÿ ∈ NzRing ∣ βˆ€π‘₯ ∈ (Baseβ€˜π‘Ÿ)βˆ€π‘¦ ∈ (Baseβ€˜π‘Ÿ)((π‘₯(+gβ€˜π‘Ÿ)𝑦) = (1rβ€˜π‘Ÿ) β†’ (π‘₯ ∈ (Unitβ€˜π‘Ÿ) ∨ 𝑦 ∈ (Unitβ€˜π‘Ÿ)))}
csubrg 13336class SubRing
crgspn 13337class RingSpan
df-subrg 13338SubRing = (𝑀 ∈ Ring ↦ {𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ∣ ((𝑀 β†Ύs 𝑠) ∈ Ring ∧ (1rβ€˜π‘€) ∈ 𝑠)})
df-rgspn 13339RingSpan = (𝑀 ∈ V ↦ (𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ↦ ∩ {𝑑 ∈ (SubRingβ€˜π‘€) ∣ 𝑠 βŠ† 𝑑}))
capr 13368class #r
df-apr 13369#r = (𝑀 ∈ V ↦ {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (Baseβ€˜π‘€) ∧ 𝑦 ∈ (Baseβ€˜π‘€)) ∧ (π‘₯(-gβ€˜π‘€)𝑦) ∈ (Unitβ€˜π‘€))})
cpsmet 13375class PsMet
cxmet 13376class ∞Met
cmet 13377class Met
cbl 13378class ball
cfbas 13379class fBas
cfg 13380class filGen
cmopn 13381class MetOpen
cmetu 13382class metUnif
df-psmet 13383PsMet = (π‘₯ ∈ V ↦ {𝑑 ∈ (ℝ* β†‘π‘š (π‘₯ Γ— π‘₯)) ∣ βˆ€π‘¦ ∈ π‘₯ ((𝑦𝑑𝑦) = 0 ∧ βˆ€π‘§ ∈ π‘₯ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))})
df-xmet 13384∞Met = (π‘₯ ∈ V ↦ {𝑑 ∈ (ℝ* β†‘π‘š (π‘₯ Γ— π‘₯)) ∣ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))})
df-met 13385Met = (π‘₯ ∈ V ↦ {𝑑 ∈ (ℝ β†‘π‘š (π‘₯ Γ— π‘₯)) ∣ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) + (𝑀𝑑𝑧)))})
df-bl 13386ball = (𝑑 ∈ V ↦ (π‘₯ ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (π‘₯𝑑𝑦) < 𝑧}))
df-mopn 13387MetOpen = (𝑑 ∈ βˆͺ ran ∞Met ↦ (topGenβ€˜ran (ballβ€˜π‘‘)))
df-fbas 13388fBas = (𝑀 ∈ V ↦ {π‘₯ ∈ 𝒫 𝒫 𝑀 ∣ (π‘₯ β‰  βˆ… ∧ βˆ… βˆ‰ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (π‘₯ ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)})
df-fg 13389filGen = (𝑀 ∈ V, π‘₯ ∈ (fBasβ€˜π‘€) ↦ {𝑦 ∈ 𝒫 𝑀 ∣ (π‘₯ ∩ 𝒫 𝑦) β‰  βˆ…})
df-metu 13390metUnif = (𝑑 ∈ βˆͺ ran PsMet ↦ ((dom dom 𝑑 Γ— dom dom 𝑑)filGenran (π‘Ž ∈ ℝ+ ↦ (◑𝑑 β€œ (0[,)π‘Ž)))))
ccnfld 13391class β„‚fld
df-icnfld 13392β„‚fld = ({⟨(Baseβ€˜ndx), β„‚βŸ©, ⟨(+gβ€˜ndx), + ⟩, ⟨(.rβ€˜ndx), Β· ⟩} βˆͺ {⟨(*π‘Ÿβ€˜ndx), βˆ—βŸ©})
czring 13416class β„€ring
df-zring 13417β„€ring = (β„‚fld β†Ύs β„€)
ctop 13433class Top
df-top 13434Top = {π‘₯ ∣ (βˆ€π‘¦ ∈ 𝒫 π‘₯βˆͺ 𝑦 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (𝑦 ∩ 𝑧) ∈ π‘₯)}
ctopon 13446class TopOn
df-topon 13447TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = βˆͺ 𝑗})
ctps 13466class TopSp
df-topsp 13467TopSp = {𝑓 ∣ (TopOpenβ€˜π‘“) ∈ (TopOnβ€˜(Baseβ€˜π‘“))}
ctb 13478class TopBases
df-bases 13479TopBases = {π‘₯ ∣ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (𝑦 ∩ 𝑧) βŠ† βˆͺ (π‘₯ ∩ 𝒫 (𝑦 ∩ 𝑧))}
ccld 13528class Clsd
cnt 13529class int
ccl 13530class cls
df-cld 13531Clsd = (𝑗 ∈ Top ↦ {π‘₯ ∈ 𝒫 βˆͺ 𝑗 ∣ (βˆͺ 𝑗 βˆ– π‘₯) ∈ 𝑗})
df-ntr 13532int = (𝑗 ∈ Top ↦ (π‘₯ ∈ 𝒫 βˆͺ 𝑗 ↦ βˆͺ (𝑗 ∩ 𝒫 π‘₯)))
df-cls 13533cls = (𝑗 ∈ Top ↦ (π‘₯ ∈ 𝒫 βˆͺ 𝑗 ↦ ∩ {𝑦 ∈ (Clsdβ€˜π‘—) ∣ π‘₯ βŠ† 𝑦}))
cnei 13574class nei
df-nei 13575nei = (𝑗 ∈ Top ↦ (π‘₯ ∈ 𝒫 βˆͺ 𝑗 ↦ {𝑦 ∈ 𝒫 βˆͺ 𝑗 ∣ βˆƒπ‘” ∈ 𝑗 (π‘₯ βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦)}))
ccn 13621class Cn
ccnp 13622class CnP
clm 13623class ⇝𝑑
df-cn 13624 Cn = (𝑗 ∈ Top, π‘˜ ∈ Top ↦ {𝑓 ∈ (βˆͺ π‘˜ β†‘π‘š βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ (◑𝑓 β€œ 𝑦) ∈ 𝑗})
df-cnp 13625 CnP = (𝑗 ∈ Top, π‘˜ ∈ Top ↦ (π‘₯ ∈ βˆͺ 𝑗 ↦ {𝑓 ∈ (βˆͺ π‘˜ β†‘π‘š βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))}))
df-lm 13626⇝𝑑 = (𝑗 ∈ Top ↦ {βŸ¨π‘“, π‘₯⟩ ∣ (𝑓 ∈ (βˆͺ 𝑗 ↑pm β„‚) ∧ π‘₯ ∈ βˆͺ 𝑗 ∧ βˆ€π‘’ ∈ 𝑗 (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘¦ ∈ ran β„€β‰₯(𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’))})
ctx 13688class Γ—t
df-tx 13689 Γ—t = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ (topGenβ€˜ran (π‘₯ ∈ π‘Ÿ, 𝑦 ∈ 𝑠 ↦ (π‘₯ Γ— 𝑦))))
chmeo 13736class Homeo
df-hmeo 13737Homeo = (𝑗 ∈ Top, π‘˜ ∈ Top ↦ {𝑓 ∈ (𝑗 Cn π‘˜) ∣ ◑𝑓 ∈ (π‘˜ Cn 𝑗)})
cxms 13772class ∞MetSp
cms 13773class MetSp
ctms 13774class toMetSp
df-xms 13775∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpenβ€˜π‘“) = (MetOpenβ€˜((distβ€˜π‘“) β†Ύ ((Baseβ€˜π‘“) Γ— (Baseβ€˜π‘“))))}
df-ms 13776MetSp = {𝑓 ∈ ∞MetSp ∣ ((distβ€˜π‘“) β†Ύ ((Baseβ€˜π‘“) Γ— (Baseβ€˜π‘“))) ∈ (Metβ€˜(Baseβ€˜π‘“))}
df-tms 13777toMetSp = (𝑑 ∈ βˆͺ ran ∞Met ↦ ({⟨(Baseβ€˜ndx), dom dom π‘‘βŸ©, ⟨(distβ€˜ndx), π‘‘βŸ©} sSet ⟨(TopSetβ€˜ndx), (MetOpenβ€˜π‘‘)⟩))
ccncf 13993class –cnβ†’
df-cncf 13994–cnβ†’ = (π‘Ž ∈ 𝒫 β„‚, 𝑏 ∈ 𝒫 β„‚ ↦ {𝑓 ∈ (𝑏 β†‘π‘š π‘Ž) ∣ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘’ ∈ ℝ+ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘¦ ∈ π‘Ž ((absβ€˜(π‘₯ βˆ’ 𝑦)) < 𝑑 β†’ (absβ€˜((π‘“β€˜π‘₯) βˆ’ (π‘“β€˜π‘¦))) < 𝑒)})
climc 14059class limβ„‚
cdv 14060class D
df-limced 14061 limβ„‚ = (𝑓 ∈ (β„‚ ↑pm β„‚), π‘₯ ∈ β„‚ ↦ {𝑦 ∈ β„‚ ∣ ((𝑓:dom π‘“βŸΆβ„‚ ∧ dom 𝑓 βŠ† β„‚) ∧ (π‘₯ ∈ β„‚ ∧ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘§ ∈ dom 𝑓((𝑧 # π‘₯ ∧ (absβ€˜(𝑧 βˆ’ π‘₯)) < 𝑑) β†’ (absβ€˜((π‘“β€˜π‘§) βˆ’ 𝑦)) < 𝑒)))})
df-dvap 14062 D = (𝑠 ∈ 𝒫 β„‚, 𝑓 ∈ (β„‚ ↑pm 𝑠) ↦ βˆͺ π‘₯ ∈ ((intβ€˜((MetOpenβ€˜(abs ∘ βˆ’ )) β†Ύt 𝑠))β€˜dom 𝑓)({π‘₯} Γ— ((𝑧 ∈ {𝑀 ∈ dom 𝑓 ∣ 𝑀 # π‘₯} ↦ (((π‘“β€˜π‘§) βˆ’ (π‘“β€˜π‘₯)) / (𝑧 βˆ’ π‘₯))) limβ„‚ π‘₯)))
clog 14213class log
ccxp 14214class ↑𝑐
df-relog 14215log = β—‘(exp β†Ύ ℝ)
df-rpcxp 14216↑𝑐 = (π‘₯ ∈ ℝ+, 𝑦 ∈ β„‚ ↦ (expβ€˜(𝑦 Β· (logβ€˜π‘₯))))
clogb 14297class logb
df-logb 14298 logb = (π‘₯ ∈ (β„‚ βˆ– {0, 1}), 𝑦 ∈ (β„‚ βˆ– {0}) ↦ ((logβ€˜π‘¦) / (logβ€˜π‘₯)))
clgs 14334class /L
df-lgs 14335 /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 14481wff 𝐴 DECIDin 𝐡
df-dcin 14482(𝐴 DECIDin 𝐡 ↔ βˆ€π‘₯ ∈ 𝐡 DECID π‘₯ ∈ 𝐴)
wbd 14500wff BOUNDED πœ‘
ax-bd0 14501(πœ‘ ↔ πœ“)    β‡’   (BOUNDED πœ‘ β†’ BOUNDED πœ“)
ax-bdim 14502BOUNDED πœ‘    &   BOUNDED πœ“    β‡’   BOUNDED (πœ‘ β†’ πœ“)
ax-bdan 14503BOUNDED πœ‘    &   BOUNDED πœ“    β‡’   BOUNDED (πœ‘ ∧ πœ“)
ax-bdor 14504BOUNDED πœ‘    &   BOUNDED πœ“    β‡’   BOUNDED (πœ‘ ∨ πœ“)
ax-bdn 14505BOUNDED πœ‘    β‡’   BOUNDED Β¬ πœ‘
ax-bdal 14506BOUNDED πœ‘    β‡’   BOUNDED βˆ€π‘₯ ∈ 𝑦 πœ‘
ax-bdex 14507BOUNDED πœ‘    β‡’   BOUNDED βˆƒπ‘₯ ∈ 𝑦 πœ‘
ax-bdeq 14508BOUNDED π‘₯ = 𝑦
ax-bdel 14509BOUNDED π‘₯ ∈ 𝑦
ax-bdsb 14510BOUNDED πœ‘    β‡’   BOUNDED [𝑦 / π‘₯]πœ‘
wbdc 14528wff BOUNDED 𝐴
df-bdc 14529(BOUNDED 𝐴 ↔ βˆ€π‘₯BOUNDED π‘₯ ∈ 𝐴)
ax-bdsep 14572BOUNDED πœ‘    β‡’   βˆ€π‘Žβˆƒπ‘βˆ€π‘₯(π‘₯ ∈ 𝑏 ↔ (π‘₯ ∈ π‘Ž ∧ πœ‘))
ax-bj-d0cl 14612BOUNDED πœ‘    β‡’   DECID πœ‘
wind 14614wff Ind 𝐴
df-bj-ind 14615(Ind 𝐴 ↔ (βˆ… ∈ 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 suc π‘₯ ∈ 𝐴))
ax-infvn 14629βˆƒπ‘₯(Ind π‘₯ ∧ βˆ€π‘¦(Ind 𝑦 β†’ π‘₯ βŠ† 𝑦))
ax-bdsetind 14656BOUNDED πœ‘    β‡’   (βˆ€π‘Ž(βˆ€π‘¦ ∈ π‘Ž [𝑦 / π‘Ž]πœ‘ β†’ πœ‘) β†’ βˆ€π‘Žπœ‘)
ax-inf2 14664βˆƒπ‘Žβˆ€π‘₯(π‘₯ ∈ π‘Ž ↔ (π‘₯ = βˆ… ∨ βˆƒπ‘¦ ∈ π‘Ž π‘₯ = suc 𝑦))
ax-strcoll 14670βˆ€π‘Ž(βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦πœ‘ β†’ βˆƒπ‘(βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦ ∈ 𝑏 πœ‘ ∧ βˆ€π‘¦ ∈ 𝑏 βˆƒπ‘₯ ∈ π‘Ž πœ‘))
ax-sscoll 14675βˆ€π‘Žβˆ€π‘βˆƒπ‘βˆ€π‘§(βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦ ∈ 𝑏 πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑐 (βˆ€π‘₯ ∈ π‘Ž βˆƒπ‘¦ ∈ 𝑑 πœ‘ ∧ βˆ€π‘¦ ∈ 𝑑 βˆƒπ‘₯ ∈ π‘Ž πœ‘))
ax-ddkcomp 14677(((𝐴 βŠ† ℝ ∧ βˆƒπ‘₯ π‘₯ ∈ 𝐴) ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ 𝐴 𝑦 < π‘₯ ∧ βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ < 𝑦 β†’ (βˆƒπ‘§ ∈ 𝐴 π‘₯ < 𝑧 ∨ βˆ€π‘§ ∈ 𝐴 𝑧 < 𝑦))) β†’ βˆƒπ‘₯ ∈ ℝ (βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ π‘₯ ∧ ((𝐡 ∈ 𝑅 ∧ βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ 𝐡) β†’ π‘₯ ≀ 𝐡)))
walsi 14759wff βˆ€!π‘₯(πœ‘ β†’ πœ“)
walsc 14760wff βˆ€!π‘₯ ∈ π΄πœ‘
df-alsi 14761(βˆ€!π‘₯(πœ‘ β†’ πœ“) ↔ (βˆ€π‘₯(πœ‘ β†’ πœ“) ∧ βˆƒπ‘₯πœ‘))
df-alsc 14762(βˆ€!π‘₯ ∈ π΄πœ‘ ↔ (βˆ€π‘₯ ∈ 𝐴 πœ‘ ∧ βˆƒπ‘₯ π‘₯ ∈ 𝐴))
  Copyright terms: Public domain W3C validator