Metamath Proof Explorer - mmdefinitions

List of Syntax, Axioms (ax-) and Definitions (df-)

Ref	Expression (see link for any distinct variable requirements)
wn 1	wff ¬ φ
wi 2	wff (φ → ψ)
ax-1 3	⊢ (φ → (ψ → φ))
ax-2 4	⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))
ax-3 5	⊢ ((¬ φ → ¬ ψ) → (ψ → φ))
ax-mp 6	⊢ φ    &   ⊢ (φ → ψ)    ⇒   ⊢ ψ
wb 127	wff (φ ↔ ψ)
df-bi 128	⊢ ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))
wo 195	wff (φ ∨ ψ)
wa 196	wff (φ ∧ ψ)
df-or 197	⊢ ((φ ∨ ψ) ↔ (¬ φ → ψ))
df-an 198	⊢ ((φ ∧ ψ) ↔ ¬ (φ → ¬ ψ))
w3o 580	wff (φ ∨ ψ ∨ χ)
w3a 581	wff (φ ∧ ψ ∧ χ)
df-3or 582	⊢ ((φ ∨ ψ ∨ χ) ↔ ((φ ∨ ψ) ∨ χ))
df-3an 583	⊢ ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))
wal 672	wff ∀xφ
ax-4 673	⊢ (∀xφ → φ)
ax-5 674	⊢ (∀x(∀xφ → ψ) → (∀xφ → ∀xψ))
ax-6 675	⊢ (¬ ∀x ¬ ∀xφ → φ)
ax-7 676	⊢ (∀x∀yφ → ∀y∀xφ)
ax-gen 677	⊢ φ    ⇒   ⊢ ∀xφ
wex 678	wff ∃xφ
df-ex 679	⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
weq 797	wff x = y
ax-8 798	⊢ (x = y → (x = z → y = z))
ax-9 799	⊢ ¬ ∀x ¬ x = y
ax-10 800	⊢ (∀x x = y → (∀xφ → ∀yφ))
ax-11 801	⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
ax-12 802	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
wel 803	wff x ∈ y
ax-13 804	⊢ (x = y → (x ∈ z → y ∈ z))
ax-14 805	⊢ (x = y → (z ∈ x → z ∈ y))
ax-15 806	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))
wsb 852	wff [y / x]φ
df-sb 853	⊢ ([y / x]φ ↔ ((x = y → φ) ∧ ∃x(x = y ∧ φ)))
ax-16 922	⊢ (∀x x = y → (φ → ∀xφ))
ax-17 925	⊢ (φ → ∀xφ)
weu 1007	wff ∃!xφ
wmo 1008	wff ∃*xφ
df-eu 1009	⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))
df-mo 1010	⊢ (∃*xφ ↔ (∃xφ → ∃!xφ))
ax-ext 1074	⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y)
ax-rep 1075	⊢ (∀w∃y∀z(∀yφ → z = y) → ∃y∀z(z ∈ y ↔ ∃w(w ∈ x ∧ ∀yφ)))
ax-un 1076	⊢ ∃y∀z(∃w(z ∈ w ∧ w ∈ x) → z ∈ y)
ax-pow 1077	⊢ ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)
ax-reg 1078	⊢ (∃y y ∈ x → ∃y(y ∈ x ∧ ∀z(z ∈ y → ¬ z ∈ x)))
ax-inf 1079	⊢ ∃y(x ∈ y ∧ ∀z(z ∈ y → ∃w(z ∈ w ∧ w ∈ y)))
ax-ac 1080	⊢ ∃y∀z∀w((z ∈ w ∧ w ∈ x) → ∃v∀u(∃t((u ∈ w ∧ w ∈ t) ∧ (u ∈ t ∧ t ∈ y)) ↔ u = v))
cv 1089	class x
cab 1090	class {x∣φ}
wceq 1091	wff A = B
wcel 1092	wff A ∈ B
df-clab 1093	⊢ (x ∈ {y∣φ} ↔ [x / y]φ)
df-cleq 1097	⊢ (∀x(x ∈ y ↔ x ∈ z) → y = z)    ⇒   ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
df-clel 1099	⊢ (A ∈ B ↔ ∃x(x = A ∧ x ∈ B))
wne 1190	wff A ≠ B
wnel 1191	wff A ∉ B
df-ne 1192	⊢ (A ≠ B ↔ ¬ A = B)
df-nel 1193	⊢ (A ∉ B ↔ ¬ A ∈ B)
wral 1201	wff ∀x ∈ A φ
wrex 1202	wff ∃x ∈ A φ
wreu 1203	wff ∃!x ∈ A φ
crab 1204	class {x ∈ A∣φ}
df-ral 1205	⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
df-rex 1206	⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
df-reu 1207	⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ))
df-rab 1208	⊢ {x ∈ A∣φ} = {x∣(x ∈ A ∧ φ)}
cvv 1348	class V
df-v 1349	⊢ V = {x∣x = x}
wsbc 1440	wff [A / x]φ
df-sbc 1441	⊢ ([A / x]φ ↔ A ∈ {x∣φ})
cdif 1484	class (A ∖ B)
cun 1485	class (A ∪ B)
cin 1486	class (A ∩ B)
wss 1487	wff A ⊆ B
wpss 1488	wff A ⊂ B
df-dif 1489	⊢ (A ∖ B) = {x∣(x ∈ A ∧ ¬ x ∈ B)}
df-un 1490	⊢ (A ∪ B) = {x∣(x ∈ A ∨ x ∈ B)}
df-in 1491	⊢ (A ∩ B) = {x∣(x ∈ A ∧ x ∈ B)}
df-ss 1492	⊢ (A ⊆ B ↔ (A ∩ B) = A)
df-pss 1494	⊢ (A ⊂ B ↔ (A ⊆ B ∧ A ≠ B))
c0 1707	class ∅
df-nul 1708	⊢ ∅ = (V ∖ V)
cif 1776	class if(φ, A, B)
df-if 1777	⊢ if(φ, A, B) = {x∣((x ∈ A ∧ φ) ∨ (x ∈ B ∧ ¬ φ))}
cpw 1798	class ℘A
df-pw 1799	⊢ ℘A = {x∣x ⊆ A}
csn 1808	class {A}
cpr 1809	class {A, B}
cop 1810	class ⟨A, B⟩
df-sn 1811	⊢ {A} = {x∣x = A}
df-pr 1812	⊢ {A, B} = ({A} ∪ {B})
ctp 1813	class {A, B, C}
df-tp 1814	⊢ {A, B, C} = ({A, B} ∪ {C})
df-op 1815	⊢ ⟨A, B⟩ = {{A}, {A, B}}
cuni 1919	class ∪A
df-uni 1920	⊢ ∪A = {x∣∃y(x ∈ y ∧ y ∈ A)}
cint 1965	class ∩A
df-int 1966	⊢ ∩A = {x∣∀y(y ∈ A → x ∈ y)}
ciun 1994	class ∪x ∈ A B
ciin 1995	class ∩x ∈ A B
df-iun 1996	⊢ ∪x ∈ A B = {y∣∃x ∈ A y ∈ B}
df-iin 1997	⊢ ∩x ∈ A B = {y∣∀x ∈ A y ∈ B}
wtr 2041	wff Tr A
df-tr 2042	⊢ (Tr A ↔ ∪A ⊆ A)
wbr 2054	wff ARB
copab 2055	class {⟨x, y⟩∣φ}
cep 2056	class E
cid 2057	class I
wpo 2058	wff R Po A
wor 2059	wff R Or A
csup 2060	class sup(A, B, R)
wfr 2061	wff R Fr A
wwe 2062	wff R We A
df-br 2063	⊢ (ARB ↔ ⟨A, B⟩ ∈ R)
df-opab 2098	⊢ {⟨x, y⟩∣φ} = {z∣∃x∃y(z = ⟨x, y⟩ ∧ φ)}
df-eprel 2122	⊢ E = {⟨x, y⟩∣x ∈ y}
df-id 2125	⊢ I = {⟨x, y⟩∣x = y}
df-po 2128	⊢ (R Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))
df-so 2138	⊢ (R Or A ↔ (R Po A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)))
df-sup 2154	⊢ sup(B, A, R) = ∪{x ∈ A∣(∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))}
df-fr 2169	⊢ (R Fr A ↔ ∀x((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x ∀z ∈ x ¬ zRy))
df-we 2186	⊢ (R We A ↔ (R Fr A ∧ R Or A))
word 2198	wff Ord A
con0 2199	class On
wlim 2200	wff Lim A
csuc 2201	class suc A
df-ord 2202	⊢ (Ord A ↔ (Tr A ∧ E We A))
df-on 2203	⊢ On = {x∣Ord x}
df-lim 2204	⊢ (Lim A ↔ (Ord A ∧ ¬ A = ∅ ∧ A = ∪A))
df-suc 2205	⊢ suc A = (A ∪ {A})
com 2372	class ω
df-om 2373	⊢ ω = {x∣(Ord x ∧ ∀y(Lim y → x ∈ y))}
cxp 2408	class (A × B)
ccnv 2409	class ◡A
cdm 2410	class dom A
crn 2411	class ran A
cres 2412	class (A ↾ B)
cima 2413	class (A “ B)
ccom 2414	class (A ∘ B)
wrel 2415	wff Rel A
wfun 2416	wff Fun A
wfn 2417	wff A Fn B
wf 2418	wff F:A–→B
wf1 2419	wff F:A–1-1→B
wfo 2420	wff F:A–onto→B
wf1o 2421	wff F:A–1-1-onto→B
cfv 2422	class (F ‘A)
wiso 2423	wff H Isom R, S (A, B)
df-xp 2424	⊢ (A × B) = {⟨x, y⟩∣(x ∈ A ∧ y ∈ B)}
df-rel 2425	⊢ (Rel A ↔ A ⊆ (V × V))
df-cnv 2426	⊢ ◡A = {⟨x, y⟩∣yAx}
df-co 2427	⊢ (A ∘ B) = {⟨x, y⟩∣∃z(xBz ∧ zAy)}
df-dm 2428	⊢ dom A = {x∣∃y xAy}
df-rn 2429	⊢ ran A = dom ◡A
df-res 2430	⊢ (A ↾ B) = (A ∩ (B × V))
df-ima 2431	⊢ (A “ B) = ran (A ↾ B)
df-fun 2432	⊢ (Fun A ↔ (Rel A ∧ (A ∘ ◡A) ⊆ I))
df-fn 2433	⊢ (A Fn B ↔ (Fun A ∧ dom A = B))
df-f 2434	⊢ (F:A–→B ↔ (F Fn A ∧ ran F ⊆ B))
df-f1 2435	⊢ (F:A–1-1→B ↔ (F:A–→B ∧ Fun ◡F))
df-fo 2436	⊢ (F:A–onto→B ↔ (F Fn A ∧ ran F = B))
df-f1o 2437	⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ F:A–onto→B))
df-fv 2438	⊢ (F ‘A) = ∪{x∣(F “ {A}) = {x}}
df-iso 2439	⊢ (H Isom R, S (A, B) ↔ (H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))))
crdg 2969	class rec(A, B)
df-rdg 2970	⊢ rec(F, A) = ∪{f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = ({⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))} ‘(f ↾ y)))}
df-rdgNEW 2971	⊢ rec(F, A) = ∪{f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = ({⟨g, z⟩∣z = if(g = ∅, A, if(Lim dom g, ∪ran g, (F ‘(g ‘∪dom g))))} ‘(f ↾ y)))}
co 3001	class (AFB)
copab2 3002	class {⟨⟨x, y⟩, z⟩∣φ}
df-opr 3003	⊢ (AFB) = (F ‘⟨A, B⟩)
df-oprab 3004	⊢ {⟨⟨x, y⟩, z⟩∣φ} = {w∣∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)}
c1st 3085	class 1st
c2nd 3086	class 2nd
df-1st 3087	⊢ 1st = {⟨x, y⟩∣y = ∪dom {x}}
df-2nd 3088	⊢ 2nd = {⟨x, y⟩∣y = ∪ran {x}}
c1o 3099	class 1o
c2o 3100	class 2o
coa 3101	class +o
comu 3102	class ·o
coe 3103	class ↑o
df-1o 3104	⊢ 1o = suc ∅
df-2o 3105	⊢ 2o = suc 1o
df-oadd 3106	⊢ +o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ∧ y ∈ On) ∧ z = (rec({⟨w, v⟩∣v = suc w}, x) ‘y))}
df-omul 3107	⊢ ·o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ∧ y ∈ On) ∧ z = (rec({⟨w, v⟩∣v = (w +o x)}, ∅) ‘y))}
df-oexp 3108	⊢ ↑o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ∧ y ∈ On) ∧ z = if(x = ∅, (1o ∖ y), (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y)))}
wer 3197	wff Er R
cec 3198	class [A]R
cqs 3199	class (A / R)
df-er 3200	⊢ (Er R ↔ (◡R ∪ (R ∘ R)) ⊆ R)
df-ec 3202	⊢ [A]R = (R “ {A})
df-qs 3205	⊢ (A / R) = {y∣∃x ∈ A y = [x]R}
cm 3258	class ↑m
df-map 3259	⊢ ↑m = {⟨⟨x, y⟩, z⟩∣z = {f∣f:y–→x}}
cen 3271	class ≈
cdom 3272	class ≼
csdm 3273	class ≺
df-en 3274	⊢ ≈ = {⟨x, y⟩∣∃f f:x–1-1-onto→y}
df-dom 3275	⊢ ≼ = {⟨x, y⟩∣∃f f:x–1-1→y}
df-sdom 3276	⊢ ≺ = ( ≼ ∖ ≈ )
cr1 3485	class R1
crnk 3486	class rank
df-r1 3487	⊢ R1 = rec({⟨x, y⟩∣y = ℘x}, ∅)
df-rank 3488	⊢ rank = {⟨x, y⟩∣y = ∩{z ∈ On∣x ∈ (R1 ‘suc z)}}
ccrd 3620	class card
cale 3621	class ℵ
ccf 3622	class cf
df-card 3623	⊢ card = {⟨x, y⟩∣y = ∩{z ∈ On∣z ≈ x}}
df-aleph 3624	⊢ ℵ = rec({⟨x, y⟩∣y = ∩{z ∈ On∣x ≺ z}}, ω)
df-cf 3625	⊢ cf = {⟨x, y⟩∣(x ∈ On ∧ y = ∩{z∣∃w(z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u))})}
ccdn 3711	class Card
df-cardn 3712	⊢ Card = (ω ∪ ran ℵ)
ccda 3714	class +c
df-cda 3715	⊢ +c = {⟨⟨x, y⟩, z⟩∣z = ((x × {∅}) ∪ (y × {1o}))}
cnpi 3766	class N
cpli 3767	class +N
cmi 3768	class ·N
clti 3769	class <N
cplpq 3770	class +pQ
cmpq 3771	class ·pQ
ceq 3772	class ~Q
cnq 3773	class Q
c1q 3774	class 1Q
cplq 3775	class +Q
cmq 3776	class ·Q
crq 3777	class *Q
cltq 3778	class <Q
cnp 3779	class P
c1p 3780	class 1P
cpp 3781	class +P
cmp 3782	class ·P
cltp 3783	class <P
cplpr 3784	class +pR
cmpr 3785	class ·pR
cer 3786	class ~R
cnr 3787	class R
c0r 3788	class 0R
c1r 3789	class 1R
cm1r 3790	class -1R
cplr 3791	class +R
cmr 3792	class ·R
cltr 3793	class <R
df-ni 3794	⊢ N = (ω ∖ {∅})
df-pli 3795	⊢ +N = ( +o ↾ (N × N))
df-mi 3796	⊢ ·N = ( ·o ↾ (N × N))
df-lti 3797	⊢ <N = (E ∩ (N × N))
df-plpq 3829	⊢ +pQ = {⟨⟨x, y⟩, z⟩∣((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·N f) +N (v ·N u)), (v ·N f)⟩))}
df-mpq 3830	⊢ ·pQ = {⟨⟨x, y⟩, z⟩∣((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w ·N u), (v ·N f)⟩))}
df-enq 3831	⊢ ~Q = {⟨x, y⟩∣((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·N u) = (w ·N v)))}
df-nq 3832	⊢ Q = ((N × N) / ~Q )
df-plq 3833	⊢ +Q = {⟨⟨x, y⟩, z⟩∣((x ∈ Q ∧ y ∈ Q) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ +pQ ⟨u, f⟩)] ~Q ))}
df-mq 3834	⊢ ·Q = {⟨⟨x, y⟩, z⟩∣((x ∈ Q ∧ y ∈ Q) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q ))}
df-rq 3835	⊢ *Q = {⟨x, y⟩∣(x ∈ Q ∧ (x ·Q y) = 1Q)}
df-ltq 3836	⊢ <Q = {⟨x, y⟩∣((x ∈ Q ∧ y ∈ Q) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩] ~Q ∧ y = [⟨v, u⟩] ~Q ) ∧ (z ·N u) <N (w ·N v)))}
df-1q 3837	⊢ 1Q = [⟨1o, 1o⟩] ~Q
df-np 3880	⊢ P = {x∣((∅ ⊂ x ∧ x ⊂ Q) ∧ ∀y ∈ x (∀z(z <Q y → z ∈ x) ∧ ∃z ∈ x y <Q z))}
df-1p 3881	⊢ 1P = {x∣x <Q 1Q}
df-plp 3882	⊢ +P = {⟨⟨x, y⟩, z⟩∣((x ∈ P ∧ y ∈ P) ∧ z = {w∣∃v ∈ x ∃u ∈ y w = (v +Q u)})}
df-mp 3883	⊢ ·P = {⟨⟨x, y⟩, z⟩∣((x ∈ P ∧ y ∈ P) ∧ z = {w∣∃v ∈ x ∃u ∈ y w = (v ·Q u)})}
df-ltp 3884	⊢ <P = {⟨x, y⟩∣((x ∈ P ∧ y ∈ P) ∧ x ⊂ y)}
df-plpr 3958	⊢ +pR = {⟨⟨x, y⟩, z⟩∣((x ∈ (P × P) ∧ y ∈ (P × P)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +P u), (v +P f)⟩))}
df-mpr 3959	⊢ ·pR = {⟨⟨x, y⟩, z⟩∣((x ∈ (P × P) ∧ y ∈ (P × P)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·P u) +P (v ·P f)), ((w ·P f) +P (v ·P u))⟩))}
df-enr 3960	⊢ ~R = {⟨x, y⟩∣((x ∈ (P × P) ∧ y ∈ (P × P)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z +P u) = (w +P v)))}
df-nr 3961	⊢ R = ((P × P) / ~R )
df-plr 3962	⊢ +R = {⟨⟨x, y⟩, z⟩∣((x ∈ R ∧ y ∈ R) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~R ∧ y = [⟨u, f⟩] ~R ) ∧ z = [(⟨w, v⟩ +pR ⟨u, f⟩)] ~R ))}
df-mr 3963	⊢ ·R = {⟨⟨x, y⟩, z⟩∣((x ∈ R ∧ y ∈ R) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~R ∧ y = [⟨u, f⟩] ~R ) ∧ z = [(⟨w, v⟩ ·pR ⟨u, f⟩)] ~R ))}
df-ltr 3964	⊢ <R = {⟨x, y⟩∣((x ∈ R ∧ y ∈ R) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩] ~R ∧ y = [⟨v, u⟩] ~R ) ∧ (z +P u)<P (w +P v)))}
df-0r 3965	⊢ 0R = [⟨1P, 1P⟩] ~R
df-1r 3966	⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 3967	⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 4026	class ℂ
cr 4027	class ℝ
cc0 4028	class 0
c1 4029	class 1
ci 4030	class i
caddc 4031	class +
cmulc 4032	class ·
clt 4033	class <
df-c 4034	⊢ ℂ = (R × R)
df-0 4035	⊢ 0 = ⟨0R, 0R⟩
df-1 4036	⊢ 1 = ⟨1R, 0R⟩
df-i 4037	⊢ i = ⟨0R, 1R⟩
df-r 4038	⊢ ℝ = (R × {0R})
df-plus 4039	⊢ + = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +R u), (v +R f)⟩))}
df-mul 4040	⊢ · = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((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 4041	⊢ < = {⟨x, y⟩∣((x ∈ ℝ ∧ y ∈ ℝ) ∧ ∃z∃w((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) ∧ z <R w))}
cmin 4089	class −
cneg 4090	class -A
cdiv 4091	class /
cle 4092	class ≤
cn 4093	class ℕ
cn0 4094	class ℕ0
cz 4095	class ℤ
cq 4096	class ℚ
df-sub 4133	⊢ − = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℂ) ∧ z = ∪{w ∈ ℂ∣(y + w) = x})}
df-neg 4135	⊢ -A = (0 − A)
df-div 4216	⊢ / = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ (ℂ ∖ {0})) ∧ z = ∪{w ∈ ℂ∣(y · w) = x})}
df-le 4277	⊢ ≤ = ((ℝ × ℝ) ∖ ◡ < )
df-n 4423	⊢ ℕ = ∩{x∣(1 ∈ x ∧ ∀y(y ∈ x → (y + 1) ∈ x))}
c2 4454	class 2
c3 4455	class 3
c4 4456	class 4
c5 4457	class 5
c6 4458	class 6
c7 4459	class 7
c8 4460	class 8
c9 4461	class 9
df-2 4462	⊢ 2 = (1 + 1)
df-3 4463	⊢ 3 = (2 + 1)
df-4 4464	⊢ 4 = (3 + 1)
df-5 4465	⊢ 5 = (4 + 1)
df-6 4466	⊢ 6 = (5 + 1)
df-7 4467	⊢ 7 = (6 + 1)
df-8 4468	⊢ 8 = (7 + 1)
df-9 4469	⊢ 9 = (8 + 1)
df-n0 4535	⊢ ℕ0 = (ℕ ∪ {0})
df-z 4564	⊢ ℤ = {x ∈ ℝ∣(x = 0 ∨ x ∈ ℕ ∨ -x ∈ ℕ)}
cfl 4621	class floor
df-fl 4622	⊢ floor = {⟨x, y⟩∣(x ∈ ℝ ∧ y = ∪{z ∈ ℤ∣(z ≤ x ∧ x < (z + 1))})}
df-q 4628	⊢ ℚ = {x∣∃y ∈ ℤ ∃z ∈ ℕ x = (y / z)}
cseq 4660	class seq
df-seq 4661	⊢ seq = {⟨⟨f, g⟩, h⟩∣h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2nd ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))}}
cexp 4675	class ↑
df-exp 4676	⊢ ↑ = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℕ) ∧ z = (( · seq(ℕ × {x})) ‘y))}
csqr 4727	class √
df-sqr 4728	⊢ √ = {⟨x, y⟩∣((x ∈ ℝ ∧ 0 ≤ x) ∧ y = sup({z ∈ ℝ∣(0 ≤ z ∧ (z · z) ≤ x)}, ℝ, < ))}
cre 4786	class ℜ
cim 4787	class ℑ
ccj 4788	class ∗
cabs 4789	class abs
df-re 4790	⊢ ℜ = {⟨x, y⟩∣(x ∈ ℂ ∧ y = ∪{z ∈ ℝ∣∃w ∈ ℝ x = (z + (w · i))})}
df-im 4791	⊢ ℑ = {⟨x, y⟩∣(x ∈ ℂ ∧ y = ∪{w ∈ ℝ∣∃z ∈ ℝ x = (z + (w · i))})}
df-cj 4792	⊢ ∗ = {⟨x, y⟩∣(x ∈ ℂ ∧ y = ((ℜ ‘x) − ((ℑ ‘x) · i)))}
df-abs 4793	⊢ abs = {⟨x, y⟩∣(x ∈ ℂ ∧ y = (√ ‘(x · (∗ ‘x))))}
cfa 4868	class !
df-fac 4869	⊢ ! = (( · seq(I ↾ ℕ)) ∪ {⟨0, 1⟩})
cli 4875	class ⇝
df-clim 4876	⊢ ⇝ = {⟨f, w⟩∣((f:ℕ–→ℂ ∧ w ∈ ℂ) ∧ ∀x ∈ ℝ (0 <