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-1 5(φ → (ψφ))
ax-2 6((φ → (ψχ)) → ((φψ) → (φχ)))
ax-mp 7φ    &   (φψ)       ψ
wa 97wff (φ ψ)
wb 98wff (φψ)
ax-ia1 99((φ ψ) → φ)
ax-ia2 100((φ ψ) → ψ)
ax-ia3 101(φ → (ψ → (φ ψ)))
df-bi 110(((φψ) → ((φψ) (ψφ))) (((φψ) (ψφ)) → (φψ)))
ax-in1 544((φ → ¬ φ) → ¬ φ)
ax-in2 545φ → (φψ))
wo 628wff (φ ψ)
ax-io 629(((φ χ) → ψ) ↔ ((φψ) (χψ)))
wstab 738wff STAB φ
df-stab 739(STAB φ ↔ (¬ ¬ φφ))
wdc 741wff DECID φ
df-dc 742(DECID φ ↔ (φ ¬ φ))
w3o 883wff (φ ψ χ)
w3a 884wff (φ ψ χ)
df-3or 885((φ ψ χ) ↔ ((φ ψ) χ))
df-3an 886((φ ψ χ) ↔ ((φ ψ) χ))
wal 1240wff xφ
cv 1241class x
wceq 1242wff A = B
wtru 1243wff
df-tru 1245( ⊤ ↔ (x x = xx x = x))
wfal 1247wff
df-fal 1248( ⊥ ↔ ¬ ⊤ )
wxo 1265wff (φψ)
df-xor 1266((φψ) ↔ ((φ ψ) ¬ (φ ψ)))
ax-5 1333(x(φψ) → (xφxψ))
ax-7 1334(xyφyxφ)
ax-gen 1335φ       xφ
wnf 1346wff xφ
df-nf 1347(Ⅎxφx(φxφ))
wex 1378wff xφ
ax-ie1 1379(xφxxφ)
ax-ie2 1380(x(ψxψ) → (x(φψ) ↔ (xφψ)))
wcel 1390wff A B
ax-8 1392(x = y → (x = zy = z))
ax-10 1393(x x = yy y = x)
ax-11 1394(x = y → (yφx(x = yφ)))
ax-i12 1395(z z = x (z z = y z(x = yz x = y)))
ax-bndl 1396(z z = x (z z = y xz(x = yz x = y)))
ax-4 1397(xφφ)
ax-13 1401(x = y → (x zy z))
ax-14 1402(x = y → (z xz y))
ax-17 1416(φxφ)
ax-i9 1420x x = y
ax-ial 1424(xφxxφ)
ax-i5r 1425((xφxψ) → x(xφψ))
ax-10o 1601(x x = y → (xφyφ))
wsb 1642wff [y / x]φ
df-sb 1643([y / x]φ ↔ ((x = yφ) x(x = y φ)))
ax-16 1692(x x = y → (φxφ))
ax-11o 1701x x = y → (x = y → (φx(x = yφ))))
weu 1897wff ∃!xφ
wmo 1898wff ∃*xφ
df-eu 1900(∃!xφyx(φx = y))
df-mo 1901(∃*xφ ↔ (xφ∃!xφ))
ax-ext 2019(z(z xz y) → x = y)
cab 2023class {xφ}
df-clab 2024(x {yφ} ↔ [x / y]φ)
df-cleq 2030(x(x yx z) → y = z)       (A = Bx(x Ax B))
df-clel 2033(A Bx(x = A x B))
wnfc 2162wff xA
df-nfc 2164(xAyx y A)
wne 2201wff AB
wnel 2202wff AB
df-ne 2203(AB ↔ ¬ A = B)
df-nel 2204(AB ↔ ¬ A B)
wral 2300wff x A φ
wrex 2301wff x A φ
wreu 2302wff ∃!x A φ
wrmo 2303wff ∃*x A φ
crab 2304class {x Aφ}
df-ral 2305(x A φx(x Aφ))
df-rex 2306(x A φx(x A φ))
df-reu 2307(∃!x A φ∃!x(x A φ))
df-rmo 2308(∃*x A φ∃*x(x A φ))
df-rab 2309{x Aφ} = {x ∣ (x A φ)}
cvv 2551class V
df-v 2553V = {xx = x}
wcdeq 2741wff CondEq(x = yφ)
df-cdeq 2742(CondEq(x = yφ) ↔ (x = yφ))
wsbc 2758wff [A / x]φ
df-sbc 2759([A / x]φA {xφ})
csb 2846class A / xB
df-csb 2847A / xB = {y[A / x]y B}
cdif 2908class (AB)
cun 2909class (AB)
cin 2910class (AB)
wss 2911wff AB
wpss 2912wff AB
df-dif 2914(AB) = {x ∣ (x A ¬ x B)}
df-un 2916(AB) = {x ∣ (x A x B)}
df-in 2918(AB) = {x ∣ (x A x B)}
df-ss 2925(AB ↔ (AB) = A)
df-pss 2927(AB ↔ (AB AB))
c0 3218class
df-nul 3219∅ = (V ∖ V)
cif 3325class if(φ, A, B)
df-if 3326if(φ, A, B) = {x ∣ ((x A φ) (x B ¬ φ))}
cpw 3351class 𝒫 A
df-pw 3353𝒫 A = {xxA}
csn 3367class {A}
cpr 3368class {A, B}
ctp 3369class {A, B, 𝐶}
cop 3370class A, B
cotp 3371class A, B, 𝐶
df-sn 3373{A} = {xx = A}
df-pr 3374{A, B} = ({A} ∪ {B})
df-tp 3375{A, B, 𝐶} = ({A, B} ∪ {𝐶})
df-op 3376A, B⟩ = {x ∣ (A V B V x {{A}, {A, B}})}
df-ot 3377A, B, 𝐶⟩ = ⟨⟨A, B⟩, 𝐶
cuni 3571class A
df-uni 3572 A = {xy(x y y A)}
cint 3606class A
df-int 3607 A = {xy(y Ax y)}
ciun 3648class x A B
ciin 3649class x A B
df-iun 3650 x A B = {yx A y B}
df-iin 3651 x A B = {yx A y B}
wdisj 3736wff Disj x A B
df-disj 3737(Disj x A By∃*x A y B)
wbr 3755wff A𝑅B
df-br 3756(A𝑅B ↔ ⟨A, B 𝑅)
copab 3808class {⟨x, y⟩ ∣ φ}
cmpt 3809class (x AB)
df-opab 3810{⟨x, y⟩ ∣ φ} = {zxy(z = ⟨x, y φ)}
df-mpt 3811(x AB) = {⟨x, y⟩ ∣ (x A y = B)}
wtr 3845wff Tr A
df-tr 3846(Tr A AA)
ax-coll 3863𝑏φ       (x 𝑎 yφ𝑏x 𝑎 y 𝑏 φ)
ax-sep 3866yx(x y ↔ (x z φ))
ax-nul 3874xy ¬ y x
ax-pow 3918yz(w(w zw x) → z y)
ax-pr 3935zw((w = x w = y) → w z)
cep 4015class E
cid 4016class I
df-eprel 4017 E = {⟨x, y⟩ ∣ x y}
df-id 4021 I = {⟨x, y⟩ ∣ x = y}
wpo 4022wff 𝑅 Po A
wor 4023wff 𝑅 Or A
df-po 4024(𝑅 Po Ax A y A z Ax𝑅x ((x𝑅y y𝑅z) → x𝑅z)))
df-iso 4025(𝑅 Or A ↔ (𝑅 Po A x A y A z A (x𝑅y → (x𝑅z z𝑅y))))
wse 4055wff 𝑅 Se A
df-se 4056(𝑅 Se Ax A {y Ay𝑅x} V)
word 4065wff Ord A
con0 4066class On
wlim 4067wff Lim A
csuc 4068class suc A
df-iord 4069(Ord A ↔ (Tr A x A Tr x))
df-on 4071On = {x ∣ Ord x}
df-ilim 4072(Lim A ↔ (Ord A A A = A))
df-suc 4074suc A = (A ∪ {A})
ax-un 4136yz(w(z w w x) → z y)
ax-setind 4220(𝑎(y 𝑎 [y / 𝑎]φφ) → 𝑎φ)
ax-iinf 4254x(∅ x y(y x → suc y x))
com 4256class 𝜔
df-iom 4257𝜔 = {x ∣ (∅ x y x suc y x)}
cxp 4286class (A × B)
ccnv 4287class A
cdm 4288class dom A
crn 4289class ran A
cres 4290class (AB)
cima 4291class (AB)
ccom 4292class (AB)
wrel 4293wff Rel A
df-xp 4294(A × B) = {⟨x, y⟩ ∣ (x A y B)}
df-rel 4295(Rel AA ⊆ (V × V))
df-cnv 4296A = {⟨x, y⟩ ∣ yAx}
df-co 4297(AB) = {⟨x, y⟩ ∣ z(xBz zAy)}
df-dm 4298dom A = {xy xAy}
df-rn 4299ran A = dom A
df-res 4300(AB) = (A ∩ (B × V))
df-ima 4301(AB) = ran (AB)
cio 4808class (℩xφ)
df-iota 4810(℩xφ) = {y ∣ {xφ} = {y}}
wfun 4839wff Fun A
wfn 4840wff A Fn B
wf 4841wff 𝐹:AB
wf1 4842wff 𝐹:A1-1B
wfo 4843wff 𝐹:AontoB
wf1o 4844wff 𝐹:A1-1-ontoB
cfv 4845class (𝐹A)
wiso 4846wff 𝐻 Isom 𝑅, 𝑆 (A, B)
df-fun 4847(Fun A ↔ (Rel A (AA) ⊆ I ))
df-fn 4848(A Fn B ↔ (Fun A dom A = B))
df-f 4849(𝐹:AB ↔ (𝐹 Fn A ran 𝐹B))
df-f1 4850(𝐹:A1-1B ↔ (𝐹:AB Fun 𝐹))
df-fo 4851(𝐹:AontoB ↔ (𝐹 Fn A ran 𝐹 = B))
df-f1o 4852(𝐹:A1-1-ontoB ↔ (𝐹:A1-1B 𝐹:AontoB))
df-fv 4853(𝐹A) = (℩xA𝐹x)
df-isom 4854(𝐻 Isom 𝑅, 𝑆 (A, B) ↔ (𝐻:A1-1-ontoB x A y A (x𝑅y ↔ (𝐻x)𝑆(𝐻y))))
crio 5410class (x A φ)
df-riota 5411(x A φ) = (℩x(x A φ))
co 5455class (A𝐹B)
coprab 5456class {⟨⟨x, y⟩, z⟩ ∣ φ}
cmpt2 5457class (x A, y B𝐶)
df-ov 5458(A𝐹B) = (𝐹‘⟨A, B⟩)
df-oprab 5459{⟨⟨x, y⟩, z⟩ ∣ φ} = {wxyz(w = ⟨⟨x, y⟩, z φ)}
df-mpt2 5460(x A, y B𝐶) = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) z = 𝐶)}
cof 5652class 𝑓 𝑅
cofr 5653class 𝑟 𝑅
df-of 5654𝑓 𝑅 = (f V, g V ↦ (x (dom f ∩ dom g) ↦ ((fx)𝑅(gx))))
df-ofr 5655𝑟 𝑅 = {⟨f, g⟩ ∣ x (dom f ∩ dom g)(fx)𝑅(gx)}
c1st 5707class 1st
c2nd 5708class 2nd
df-1st 57091st = (x V ↦ dom {x})
df-2nd 57102nd = (x V ↦ ran {x})
ctpos 5800class tpos 𝐹
df-tpos 5801tpos 𝐹 = (𝐹 ∘ (x (dom 𝐹 ∪ {∅}) ↦ {x}))
wsmo 5841wff Smo A
df-smo 5842(Smo A ↔ (A:dom A⟶On Ord dom A x dom Ay dom A(x y → (Ax) (Ay))))
crecs 5860class recs(𝐹)
df-recs 5861recs(𝐹) = {fx On (f Fn x y x (fy) = (𝐹‘(fy)))}
crdg 5896class rec(𝐹, 𝐼)
df-irdg 5897rec(𝐹, 𝐼) = recs((g V ↦ (𝐼 x dom g(𝐹‘(gx)))))
cfrec 5917class frec(𝐹, 𝐼)
df-frec 5918frec(𝐹, 𝐼) = (recs((g V ↦ {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x 𝐼))})) ↾ 𝜔)
c1o 5933class 1𝑜
c2o 5934class 2𝑜
c3o 5935class 3𝑜
c4o 5936class 4𝑜
coa 5937class +𝑜
comu 5938class ·𝑜
coei 5939class 𝑜
df-1o 59401𝑜 = suc ∅
df-2o 59412𝑜 = suc 1𝑜
df-3o 59423𝑜 = suc 2𝑜
df-4o 59434𝑜 = suc 3𝑜
df-oadd 5944 +𝑜 = (x On, y On ↦ (rec((z V ↦ suc z), x)‘y))
df-omul 5945 ·𝑜 = (x On, y On ↦ (rec((z V ↦ (z +𝑜 x)), ∅)‘y))
df-oexpi 5946𝑜 = (x On, y On ↦ (rec((z V ↦ (z ·𝑜 x)), 1𝑜)‘y))
wer 6039wff 𝑅 Er A
cec 6040class [A]𝑅
cqs 6041class (A / 𝑅)
df-er 6042(𝑅 Er A ↔ (Rel 𝑅 dom 𝑅 = A (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
df-ec 6044[A]𝑅 = (𝑅 “ {A})
df-qs 6048(A / 𝑅) = {yx A y = [x]𝑅}
cen 6155class
cdom 6156class
cfn 6157class Fin
df-en 6158 ≈ = {⟨x, y⟩ ∣ f f:x1-1-ontoy}
df-dom 6159 ≼ = {⟨x, y⟩ ∣ f f:x1-1y}
df-fin 6160Fin = {xy 𝜔 xy}
cnpi 6256class N
cpli 6257class +N
cmi 6258class ·N
clti 6259class <N
cplpq 6260class +pQ
cmpq 6261class ·pQ
cltpq 6262class <pQ
ceq 6263class ~Q
cnq 6264class Q
c1q 6265class 1Q
cplq 6266class +Q
cmq 6267class ·Q
crq 6268class *Q
cltq 6269class <Q
ceq0 6270class ~Q0
cnq0 6271class Q0
c0q0 6272class 0Q0
cplq0 6273class +Q0
cmq0 6274class ·Q0
cnp 6275class P
c1p 6276class 1P
cpp 6277class +P
cmp 6278class ·P
cltp 6279class <P
cer 6280class ~R
cnr 6281class R
c0r 6282class 0R
c1r 6283class 1R
cm1r 6284class -1R
cplr 6285class +R
cmr 6286class ·R
cltr 6287class <R
df-ni 6288N = (𝜔 ∖ {∅})
df-pli 6289 +N = ( +𝑜 ↾ (N × N))
df-mi 6290 ·N = ( ·𝑜 ↾ (N × N))
df-lti 6291 <N = ( E ∩ (N × N))
df-plpq 6328 +pQ = (x (N × N), y (N × N) ↦ ⟨(((1stx) ·N (2ndy)) +N ((1sty) ·N (2ndx))), ((2ndx) ·N (2ndy))⟩)
df-mpq 6329 ·pQ = (x (N × N), y (N × N) ↦ ⟨((1stx) ·N (1sty)), ((2ndx) ·N (2ndy))⟩)
df-ltpq 6330 <pQ = {⟨x, y⟩ ∣ ((x (N × N) y (N × N)) ((1stx) ·N (2ndy)) <N ((1sty) ·N (2ndx)))}
df-enq 6331 ~Q = {⟨x, y⟩ ∣ ((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v)))}
df-nqqs 6332Q = ((N × N) / ~Q )
df-plqqs 6333 +Q = {⟨⟨x, y⟩, z⟩ ∣ ((x Q y Q) wvuf((x = [⟨w, v⟩] ~Q y = [⟨u, f⟩] ~Q ) z = [(⟨w, v⟩ +pQu, f⟩)] ~Q ))}
df-mqqs 6334 ·Q = {⟨⟨x, y⟩, z⟩ ∣ ((x Q y Q) wvuf((x = [⟨w, v⟩] ~Q y = [⟨u, f⟩] ~Q ) z = [(⟨w, v⟩ ·pQu, f⟩)] ~Q ))}
df-1nqqs 63351Q = [⟨1𝑜, 1𝑜⟩] ~Q
df-rq 6336*Q = {⟨x, y⟩ ∣ (x Q y Q (x ·Q y) = 1Q)}
df-ltnqqs 6337 <Q = {⟨x, y⟩ ∣ ((x Q y Q) zwvu((x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q ) (z ·N u) <N (w ·N v)))}
df-enq0 6407 ~Q0 = {⟨x, y⟩ ∣ ((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))}
df-nq0 6408Q0 = ((𝜔 × N) / ~Q0 )
df-0nq0 64090Q0 = [⟨∅, 1𝑜⟩] ~Q0
df-plq0 6410 +Q0 = {⟨⟨x, y⟩, z⟩ ∣ ((x Q0 y Q0) wvuf((x = [⟨w, v⟩] ~Q0 y = [⟨u, f⟩] ~Q0 ) z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 ))}
df-mq0 6411 ·Q0 = {⟨⟨x, y⟩, z⟩ ∣ ((x Q0 y Q0) wvuf((x = [⟨w, v⟩] ~Q0 y = [⟨u, f⟩] ~Q0 ) z = [⟨(w ·𝑜 u), (v ·𝑜 f)⟩] ~Q0 ))}
df-inp 6449P = {⟨𝑙, u⟩ ∣ (((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)) ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))))}
df-i1p 64501P = ⟨{𝑙𝑙 <Q 1Q}, {u ∣ 1Q <Q u}⟩
df-iplp 6451 +P = (x P, y P ↦ ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))}⟩)
df-imp 6452 ·P = (x P, y P ↦ ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 ·Q 𝑠))}⟩)
df-iltp 6453<P = {⟨x, y⟩ ∣ ((x P y P) 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)))}
df-enr 6654 ~R = {⟨x, y⟩ ∣ ((x (P × P) y (P × P)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z +P u) = (w +P v)))}
df-nr 6655R = ((P × P) / ~R )
df-plr 6656 +R = {⟨⟨x, y⟩, z⟩ ∣ ((x R y R) wvuf((x = [⟨w, v⟩] ~R y = [⟨u, f⟩] ~R ) z = [⟨(w +P u), (v +P f)⟩] ~R ))}
df-mr 6657 ·R = {⟨⟨x, y⟩, z⟩ ∣ ((x R y R) wvuf((x = [⟨w, v⟩] ~R y = [⟨u, f⟩] ~R ) z = [⟨((w ·P u) +P (v ·P f)), ((w ·P f) +P (v ·P u))⟩] ~R ))}
df-ltr 6658 <R = {⟨x, y⟩ ∣ ((x R y R) zwvu((x = [⟨z, w⟩] ~R y = [⟨v, u⟩] ~R ) (z +P u)<P (w +P v)))}
df-0r 66590R = [⟨1P, 1P⟩] ~R
df-1r 66601R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 6661-1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 6709class
cr 6710class
cc0 6711class 0
c1 6712class 1
ci 6713class i
caddc 6714class +
cltrr 6715class <
cmul 6716class ·
df-c 6717ℂ = (R × R)
df-0 67180 = ⟨0R, 0R
df-1 67191 = ⟨1R, 0R
df-i 6720i = ⟨0R, 1R
df-r 6721ℝ = (R × {0R})
df-add 6722 + = {⟨⟨x, y⟩, z⟩ ∣ ((x y ℂ) wvuf((x = ⟨w, v y = ⟨u, f⟩) z = ⟨(w +R u), (v +R f)⟩))}
df-mul 6723 · = {⟨⟨x, y⟩, z⟩ ∣ ((x y ℂ) wvuf((x = ⟨w, v y = ⟨u, f⟩) z = ⟨((w ·R u) +R (-1R ·R (v ·R f))), ((v ·R u) +R (w ·R f))⟩))}
df-lt 6724 < = {⟨x, y⟩ ∣ ((x y ℝ) zw((x = ⟨z, 0R y = ⟨w, 0R⟩) z <R w))}
ax-cnex 6774 V
ax-resscn 6775ℝ ⊆ ℂ
ax-1cn 67761
ax-1re 67771
ax-icn 6778i
ax-addcl 6779((A B ℂ) → (A + B) ℂ)
ax-addrcl 6780((A B ℝ) → (A + B) ℝ)
ax-mulcl 6781((A B ℂ) → (A · B) ℂ)
ax-mulrcl 6782((A B ℝ) → (A · B) ℝ)
ax-addcom 6783((A B ℂ) → (A + B) = (B + A))
ax-mulcom 6784((A B ℂ) → (A · B) = (B · A))
ax-addass 6785((A B 𝐶 ℂ) → ((A + B) + 𝐶) = (A + (B + 𝐶)))
ax-mulass 6786((A B 𝐶 ℂ) → ((A · B) · 𝐶) = (A · (B · 𝐶)))
ax-distr 6787((A B 𝐶 ℂ) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))
ax-i2m1 6788((i · i) + 1) = 0
ax-1rid 6790(A ℝ → (A · 1) = A)
ax-0id 6791(A ℂ → (A + 0) = A)
ax-rnegex 6792(A ℝ → x ℝ (A + x) = 0)
ax-precex 6793((A 0 < A) → x ℝ (0 < x (A · x) = 1))
ax-cnre 6794(A ℂ → x y A = (x + (i · y)))
ax-pre-ltirr 6795(A ℝ → ¬ A < A)
ax-pre-ltwlin 6796((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))
ax-pre-lttrn 6797((A B 𝐶 ℝ) → ((A < B B < 𝐶) → A < 𝐶))
ax-pre-apti 6798((A B ¬ (A < B B < A)) → A = B)
ax-pre-ltadd 6799((A B 𝐶 ℝ) → (A < B → (𝐶 + A) < (𝐶 + B)))
ax-pre-mulgt0 6800((A B ℝ) → ((0 < A 0 < B) → 0 < (A · B)))
ax-pre-mulext 6801((A B 𝐶 ℝ) → ((A · 𝐶) < (B · 𝐶) → (A < B B < A)))
ax-arch 6802(A ℝ → 𝑛 {x ∣ (1 x y x (y + 1) x)}A < 𝑛)
cpnf 6854class +∞
cmnf 6855class -∞
cxr 6856class *
clt 6857class <
cle 6858class
df-pnf 6859+∞ = 𝒫
df-mnf 6860-∞ = 𝒫 +∞
df-xr 6861* = (ℝ ∪ {+∞, -∞})
df-ltxr 6862 < = ({⟨x, y⟩ ∣ (x y x < y)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
df-le 6863 ≤ = ((ℝ* × ℝ*) ∖ < )
cmin 6979class
cneg 6980class -A
df-sub 6981 − = (x ℂ, y ℂ ↦ (z ℂ (y + z) = x))
df-neg 6982-A = (0 − A)
creap 7358class #
df-reap 7359 # = {⟨x, y⟩ ∣ ((x y ℝ) (x < y y < x))}
cap 7365class #
df-ap 7366 # = {⟨x, y⟩ ∣ 𝑟 𝑠 𝑡 u ℝ ((x = (𝑟 + (i · 𝑠)) y = (𝑡 + (i · u))) (𝑟 # 𝑡 𝑠 # u))}
cdiv 7433class /
df-div 7434 / = (x ℂ, y (ℂ ∖ {0}) ↦ (z ℂ (y · z) = x))
cn 7695class
df-inn 7696ℕ = {x ∣ (1 x y x (y + 1) x)}
c2 7744class 2
c3 7745class 3
c4 7746class 4
c5 7747class 5
c6 7748class 6
c7 7749class 7
c8 7750class 8
c9 7751class 9
c10 7752class 10
df-2 77532 = (1 + 1)
df-3 77543 = (2 + 1)
df-4 77554 = (3 + 1)
df-5 77565 = (4 + 1)
df-6 77576 = (5 + 1)
df-7 77587 = (6 + 1)
df-8 77598 = (7 + 1)
df-9 77609 = (8 + 1)
df-10 776110 = (9 + 1)
cn0 7957class 0
df-n0 79580 = (ℕ ∪ {0})
cz 8021class
df-z 8022ℤ = {𝑛 ℝ ∣ (𝑛 = 0 𝑛 -𝑛 ℕ)}
cdc 8144class AB
df-dec 8145AB = ((10 · A) + B)
cuz 8249class
df-uz 8250 = (𝑗 ℤ ↦ {𝑘 ℤ ∣ 𝑗𝑘})
cq 8330class
df-q 8331ℚ = ( / “ (ℤ × ℕ))
crp 8358class +
df-rp 8359+ = {x ℝ ∣ 0 < x}
cxne 8456class -𝑒A
cxad 8457class +𝑒
cxmu 8458class ·e
df-xneg 8459-𝑒A = if(A = +∞, -∞, if(A = -∞, +∞, -A))
df-xadd 8460 +𝑒 = (x *, y * ↦ if(x = +∞, if(y = -∞, 0, +∞), if(x = -∞, if(y = +∞, 0, -∞), if(y = +∞, +∞, if(y = -∞, -∞, (x + y))))))
df-xmul 8461 ·e = (x *, y * ↦ if((x = 0 y = 0), 0, if((((0 < y x = +∞) (y < 0 x = -∞)) ((0 < x y = +∞) (x < 0 y = -∞))), +∞, if((((0 < y x = -∞) (y < 0 x = +∞)) ((0 < x y = -∞) (x < 0 y = +∞))), -∞, (x · y)))))
cioo 8527class (,)
cioc 8528class (,]
cico 8529class [,)
cicc 8530class [,]
df-ioo 8531(,) = (x *, y * ↦ {z * ∣ (x < z z < y)})
df-ioc 8532(,] = (x *, y * ↦ {z * ∣ (x < z zy)})
df-ico 8533[,) = (x *, y * ↦ {z * ∣ (xz z < y)})
df-icc 8534[,] = (x *, y * ↦ {z * ∣ (xz zy)})
cfz 8644class ...
df-fz 8645... = (𝑚 ℤ, 𝑛 ℤ ↦ {𝑘 ℤ ∣ (𝑚𝑘 𝑘𝑛)})
cfzo 8769class ..^
df-fzo 8770..^ = (𝑚 ℤ, 𝑛 ℤ ↦ (𝑚...(𝑛 − 1)))
cseq 8892class seq𝑀( + , 𝐹, 𝑆)
df-iseq 8893seq𝑀( + , 𝐹, 𝑆) = ran frec((x (ℤ𝑀), y 𝑆 ↦ ⟨(x + 1), (y + (𝐹‘(x + 1)))⟩), ⟨𝑀, (𝐹𝑀)⟩)
cexp 8908class
df-iexp 8909↑ = (x ℂ, y ℤ ↦ if(y = 0, 1, if(0 < y, (seq1( · , (ℕ × {x}), ℂ)‘y), (1 / (seq1( · , (ℕ × {x}), ℂ)‘-y)))))
ccj 9067class
cre 9068class
cim 9069class
df-cj 9070∗ = (x ℂ ↦ (y ℂ ((x + y) (i · (xy)) ℝ)))
df-re 9071ℜ = (x ℂ ↦ ((x + (∗‘x)) / 2))
df-im 9072ℑ = (x ℂ ↦ (ℜ‘(x / i)))
csqrt 9205class
cabs 9206class abs
df-rsqrt 9207√ = (x ℝ ↦ (y ℝ ((y↑2) = x 0 ≤ y)))
df-abs 9208abs = (x ℂ ↦ (√‘(x · (∗‘x))))
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wbd 9267wff BOUNDED φ
ax-bd0 9268(φψ)       (BOUNDED φBOUNDED ψ)
ax-bdim 9269BOUNDED φ    &   BOUNDED ψ       BOUNDED (φψ)
ax-bdan 9270BOUNDED φ    &   BOUNDED ψ       BOUNDED (φ ψ)
ax-bdor 9271BOUNDED φ    &   BOUNDED ψ       BOUNDED (φ ψ)
ax-bdn 9272BOUNDED φ       BOUNDED ¬ φ
ax-bdal 9273BOUNDED φ       BOUNDED x y φ
ax-bdex 9274BOUNDED φ       BOUNDED x y φ
ax-bdeq 9275BOUNDED x = y
ax-bdel 9276BOUNDED x y
ax-bdsb 9277BOUNDED φ       BOUNDED [y / x]φ
wbdc 9295wff BOUNDED A
df-bdc 9296(BOUNDED AxBOUNDED x A)
ax-bdsep 9339BOUNDED φ       𝑎𝑏x(x 𝑏 ↔ (x 𝑎 φ))
ax-bj-d0cl 9379BOUNDED φ       DECID φ
wind 9385wff Ind A
df-bj-ind 9386(Ind A ↔ (∅ A x A suc x A))
ax-infvn 9401x(Ind x y(Ind yxy))
ax-bdsetind 9428BOUNDED φ       (𝑎(y 𝑎 [y / 𝑎]φφ) → 𝑎φ)
ax-inf2 9436𝑎x(x 𝑎 ↔ (x = ∅ y 𝑎 x = suc y))
ax-strcoll 9442𝑎(x 𝑎 yφ𝑏y(y 𝑏x 𝑎 φ))
ax-sscoll 9447𝑎𝑏𝑐z(x 𝑎 y 𝑏 φ𝑑 𝑐 y(y 𝑑x 𝑎 φ))
walsi 9449wff ∀!x(φψ)
walsc 9450wff ∀!x Aφ
df-alsi 9451(∀!x(φψ) ↔ (x(φψ) xφ))
df-alsc 9452(∀!x Aφ ↔ (x A φ x x A))
  Copyright terms: Public domain W3C validator