mmdefinitions - Metamath Proof Explorer

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

Ref	Expression (see link for any distinct variable requirements)
wn 2	wff ¬ φ
wi 3	wff (φ → ψ)
ax-1 4	⊢ (φ → (ψ → φ))
ax-2 5	⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))
ax-3 6	⊢ ((¬ φ → ¬ ψ) → (ψ → φ))
ax-mp 7	⊢ φ    &   ⊢ (φ → ψ)    ⇒   ⊢ ψ
wb 146	wff (φ ↔ ψ)
df-bi 147	⊢ ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))
wo 222	wff (φ ⋁ ψ)
wa 223	wff (φ ⋀ ψ)
df-or 224	⊢ ((φ ⋁ ψ) ↔ (¬ φ → ψ))
df-an 225	⊢ ((φ ⋀ ψ) ↔ ¬ (φ → ¬ ψ))
w3o 773	wff (φ ⋁ ψ ⋁ χ)
w3a 774	wff (φ ⋀ ψ ⋀ χ)
df-3or 775	⊢ ((φ ⋁ ψ ⋁ χ) ↔ ((φ ⋁ ψ) ⋁ χ))
df-3an 776	⊢ ((φ ⋀ ψ ⋀ χ) ↔ ((φ ⋀ ψ) ⋀ χ))
wal 953	wff ∀xφ
cv 954	class x
wceq 955	wff A = B
wcel 957	wff A ∈ B
ax-5 959	⊢ (∀x(φ → ψ) → (∀xφ → ∀xψ))
ax-6 960	⊢ (¬ ∀xφ → ∀x ¬ ∀xφ)
ax-7 961	⊢ (∀x∀yφ → ∀y∀xφ)
ax-gen 962	⊢ φ    ⇒   ⊢ ∀xφ
ax-8 963	⊢ (x = y → (x = z → y = z))
ax-9 964	⊢ ¬ ∀x ¬ x = y
ax-10 965	⊢ (∀x x = y → ∀y y = x)
ax-11 966	⊢ (x = y → (∀yφ → ∀x(x = y → φ)))
ax-12 967	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
ax-13 968	⊢ (x = y → (x ∈ z → y ∈ z))
ax-14 969	⊢ (x = y → (z ∈ x → z ∈ y))
ax-17 970	⊢ (φ → ∀xφ)
ax-4 972	⊢ (∀xφ → φ)
ax-5o 974	⊢ (∀x(∀xφ → ψ) → (∀xφ → ∀xψ))
ax-6o 977	⊢ (¬ ∀x ¬ ∀xφ → φ)
wex 979	wff ∃xφ
df-ex 980	⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
ax-9o 1122	⊢ (∀x(x = y → ∀xφ) → φ)
ax-10o 1139	⊢ (∀x x = y → (∀xφ → ∀yφ))
wsbc 1169	wff [A / x]φ
df-sb 1171	⊢ ([y / x]φ ↔ ((x = y → φ) ⋀ ∃x(x = y ⋀ φ)))
ax-16 1209	⊢ (∀x x = y → (φ → ∀xφ))
ax-11o 1217	⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
ax-15 1359	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))
weu 1379	wff ∃!xφ
wmo 1380	wff ∃*xφ
df-eu 1381	⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))
df-mo 1382	⊢ (∃*xφ ↔ (∃xφ → ∃!xφ))
ax-ext 1458	⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y)
cab 1462	class {x∣φ}
df-clab 1463	⊢ (x ∈ {y∣φ} ↔ [x / y]φ)
df-cleq 1468	⊢ (∀x(x ∈ y ↔ x ∈ z) → y = z)    ⇒   ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
df-clel 1471	⊢ (A ∈ B ↔ ∃x(x = A ⋀ x ∈ B))
wne 1583	wff A ≠ B
wnel 1584	wff A ∉ B
df-ne 1585	⊢ (A ≠ B ↔ ¬ A = B)
df-nel 1586	⊢ (A ∉ B ↔ ¬ A ∈ B)
wral 1643	wff ∀x ∈ A φ
wrex 1644	wff ∃x ∈ A φ
wreu 1645	wff ∃!x ∈ A φ
crab 1646	class {x ∈ A∣φ}
df-ral 1647	⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
df-rex 1648	⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ⋀ φ))
df-reu 1649	⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ⋀ φ))
df-rab 1650	⊢ {x ∈ A∣φ} = {x∣(x ∈ A ⋀ φ)}
cvv 1808	class V
df-v 1809	⊢ V = {x∣x = x}
df-sbc 1939	⊢ ([A / x]φ ↔ A ∈ {x∣φ})
csb 1998	class [A / x]B
df-csb 1999	⊢ [A / x]B = {y∣[A / x]y ∈ B}
cdif 2041	class (A ∖ B)
cun 2042	class (A ∪ B)
cin 2043	class (A ∩ B)
wss 2044	wff A ⊆ B
wpss 2045	wff A ⊂ B
df-dif 2046	⊢ (A ∖ B) = {x∣(x ∈ A ⋀ ¬ x ∈ B)}
df-un 2047	⊢ (A ∪ B) = {x∣(x ∈ A ⋁ x ∈ B)}
df-in 2048	⊢ (A ∩ B) = {x∣(x ∈ A ⋀ x ∈ B)}
df-ss 2050	⊢ (A ⊆ B ↔ (A ∩ B) = A)
df-pss 2052	⊢ (A ⊂ B ↔ (A ⊆ B ⋀ A ≠ B))
c0 2277	class ∅
df-nul 2278	⊢ ∅ = (V ∖ V)
cif 2358	class if(φ, A, B)
df-if 2359	⊢ if(φ, A, B) = {x∣((x ∈ A ⋀ φ) ⋁ (x ∈ B ⋀ ¬ φ))}
cpw 2398	class ℘A
df-pw 2399	⊢ ℘A = {x∣x ⊆ A}
csn 2406	class {A}
cpr 2407	class {A, B}
cop 2408	class ⟨A, B⟩
df-sn 2409	⊢ {A} = {x∣x = A}
df-pr 2410	⊢ {A, B} = ({A} ∪ {B})
ctp 2411	class {A, B, C}
df-tp 2412	⊢ {A, B, C} = ({A, B} ∪ {C})
df-op 2413	⊢ ⟨A, B⟩ = {{A}, {A, B}}
cuni 2499	class ∪A
df-uni 2500	⊢ ∪A = {x∣∃y(x ∈ y ⋀ y ∈ A)}
cint 2529	class ∩A
df-int 2530	⊢ ∩A = {x∣∀y(y ∈ A → x ∈ y)}
ciun 2562	class ∪x ∈ A B
ciin 2563	class ∩x ∈ A B
df-iun 2564	⊢ ∪x ∈ A B = {y∣∃x ∈ A y ∈ B}
df-iin 2565	⊢ ∩x ∈ A B = {y∣∀x ∈ A y ∈ B}
wbr 2615	wff ARB
df-br 2616	⊢ (ARB ↔ ⟨A, B⟩ ∈ R)
copab 2662	class {⟨x, y⟩∣φ}
df-opab 2663	⊢ {⟨x, y⟩∣φ} = {z∣∃x∃y(z = ⟨x, y⟩ ⋀ φ)}
wtr 2676	wff Tr A
df-tr 2677	⊢ (Tr A ↔ ∪A ⊆ A)
ax-rep 2689	⊢ (∀w∃y∀z(∀yφ → z = y) → ∃y∀z(z ∈ y ↔ ∃w(w ∈ x ⋀ ∀yφ)))
ax-sep 2699	⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ))
ax-nul 2706	⊢ ∃x∀y ¬ y ∈ x
ax-pow 2738	⊢ ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)
ax-pr 2775	⊢ ∃z∀w((w = x ⋁ w = y) → w ∈ z)
cep 2826	class E
cid 2827	class I
df-eprel 2828	⊢ E = {⟨x, y⟩∣x ∈ y}
df-id 2831	⊢ I = {⟨x, y⟩∣x = y}
wpo 2834	wff R Po A
wor 2835	wff R Or A
df-po 2836	⊢ (R Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ⋀ ((xRy ⋀ yRz) → xRz)))
df-so 2846	⊢ (R Or A ↔ (R Po A ⋀ ∀x ∈ A ∀y ∈ A (xRy ⋁ x = y ⋁ yRx)))
ax-un 2862	⊢ ∃y∀z(∃w(z ∈ w ⋀ w ∈ x) → z ∈ y)
wfr 2911	wff R Fr A
wwe 2912	wff R We A
df-fr 2913	⊢ (R Fr A ↔ ∀x((x ⊆ A ⋀ x ≠ ∅) → ∃y ∈ x ∀z ∈ x ¬ zRy))
df-we 2930	⊢ (R We A ↔ (R Fr A ⋀ R Or A))
word 2943	wff Ord A
con0 2944	class On
wlim 2945	wff Lim A
csuc 2946	class suc A
df-ord 2947	⊢ (Ord A ↔ (Tr A ⋀ E We A))
df-on 2948	⊢ On = {x∣Ord x}
df-lim 2949	⊢ (Lim A ↔ (Ord A ⋀ A ≠ ∅ ⋀ A = ∪A))
df-suc 2950	⊢ suc A = (A ∪ {A})
com 3127	class ω
df-om 3128	⊢ ω = {x∣(Ord x ⋀ ∀y(Lim y → x ∈ y))}
cxp 3164	class (A × B)
ccnv 3165	class ◡A
cdm 3166	class dom A
crn 3167	class ran A
cres 3168	class (A ↾ B)
cima 3169	class (A “ B)
ccom 3170	class (A ∘ B)
wrel 3171	wff Rel A
wfun 3172	wff Fun A
wfn 3173	wff A Fn B
wf 3174	wff F:A–→B
wf1 3175	wff F:A–1-1→B
wfo 3176	wff F:A–onto→B
wf1o 3177	wff F:A–1-1-onto→B
cfv 3178	class (F ‘A)
wiso 3179	wff H Isom R, S (A, B)
df-xp 3180	⊢ (A × B) = {⟨x, y⟩∣(x ∈ A ⋀ y ∈ B)}
df-rel 3181	⊢ (Rel A ↔ A ⊆ (V × V))
df-cnv 3182	⊢ ◡A = {⟨x, y⟩∣yAx}
df-co 3183	⊢ (A ∘ B) = {⟨x, y⟩∣∃z(xBz ⋀ zAy)}
df-dm 3184	⊢ dom A = {x∣∃y xAy}
df-rn 3185	⊢ ran A = dom ◡ A
df-res 3186	⊢ (A ↾ B) = (A ∩ (B × V))
df-ima 3187	⊢ (A “ B) = ran ( A ↾ B)
df-fun 3188	⊢ (Fun A ↔ (Rel A ⋀ (A ∘ ◡A) ⊆ I))
df-fn 3189	⊢ (A Fn B ↔ (Fun A ⋀ dom A = B))
df-f 3190	⊢ (F:A–→B ↔ (F Fn A ⋀ ran F ⊆ B))
df-f1 3191	⊢ (F:A–1-1→B ↔ (F:A–→B ⋀ Fun ◡F))
df-fo 3192	⊢ (F:A–onto→B ↔ (F Fn A ⋀ ran F = B))
df-f1o 3193	⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ⋀ F:A–onto→B))
df-fv 3194	⊢ (F ‘A) = ∪{x∣(F “ {A}) = {x}}
df-iso 3195	⊢ (H Isom R, S (A, B) ↔ (H:A–1-1-onto→B ⋀ ∀x ∈ A ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))))
crdg 3926	class rec(A, B)
df-rdg 3927	⊢ 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 3958	class (AFB)
copab2 3959	class {⟨⟨x, y⟩, z⟩∣φ}
df-opr 3960	⊢ (AFB) = (F ‘⟨A, B⟩)
df-oprab 3961	⊢ {⟨⟨x, y⟩, z⟩∣φ} = {w∣∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ⋀ φ)}
cmpt 4066	class (x ∈ A ↦ B)
cmpt2 4067	class (x ∈ A, y ∈ B ↦ C)
df-mpt 4068	⊢ (x ∈ A ↦ B) = {⟨x, y⟩∣(x ∈ A ⋀ y = B)}
df-mpt2 4069	⊢ (x ∈ A, y ∈ B ↦ C) = {⟨⟨x, y⟩, z⟩∣((x ∈ A ⋀ y ∈ B) ⋀ z = C)}
c1st 4070	class 1st
c2nd 4071	class 2nd
df-1st 4072	⊢ 1st = {⟨x, y⟩∣y = ∪dom { x}}
df-2nd 4073	⊢ 2nd = {⟨x, y⟩∣y = ∪ran { x}}
c1o 4121	class 1o
c2o 4122	class 2o
coa 4123	class +o
comu 4124	class ·o
coe 4125	class ↑o
df-1o 4126	⊢ 1o = suc ∅
df-2o 4127	⊢ 2o = suc 1o
df-oadd 4128	⊢ +o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ⋀ y ∈ On) ⋀ z = (rec({⟨w, v⟩∣v = suc w}, x) ‘y))}
df-omul 4129	⊢ ·o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ⋀ y ∈ On) ⋀ z = (rec({⟨w, v⟩∣v = (w +o x)}, ∅) ‘y))}
df-oexp 4130	⊢ ↑o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ⋀ y ∈ On) ⋀ z = if(x = ∅, (1o ∖ y), (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y)))}
wer 4251	wff Er R
cec 4252	class [A]R
cqs 4253	class (A / R)
df-er 4254	⊢ (Er R ↔ (◡R ∪ (R ∘ R)) ⊆ R)
df-ec 4256	⊢ [A]R = (R “ {A})
df-qs 4259	⊢ (A / R) = {y∣∃x ∈ A y = [x]R}
cm 4315	class ↑m
cpm 4316	class ↑pm
df-map 4317	⊢ ↑m = {⟨⟨x, y⟩, z⟩∣z = {f∣f:y–→x}}
df-pm 4318	⊢ ↑pm = {⟨⟨x, y⟩, z⟩∣z = {f∣(Fun f ⋀ f ⊆ (y × x))}}
cixp 4340	class Xx ∈ A B
df-ixp 4341	⊢ Xx ∈ A B = {f∣(f Fn A ⋀ ∀x ∈ A (f ‘x) ∈ B)}
cen 4357	class ≈
cdom 4358	class ≼
csdm 4359	class ≺
df-en 4360	⊢ ≈ = {⟨x, y⟩∣∃f f:x–1-1-onto→y}
df-dom 4361	⊢ ≼ = {⟨x, y⟩∣∃f f:x–1-1→y}
df-sdom 4362	⊢ ≺ = ( ≼ ∖ ≈ )
csup 4556	class sup(A, B, R)
df-sup 4557	⊢ sup(B, A, R) = ∪{x ∈ A∣(∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))}
ax-reg 4576	⊢ (∃y y ∈ x → ∃y(y ∈ x ⋀ ∀z(z ∈ y → ¬ z ∈ x)))
ax-inf 4605	⊢ ∃y(x ∈ y ⋀ ∀z(z ∈ y → ∃w(z ∈ w ⋀ w ∈ y)))
ax-inf2 4608	⊢ ∃x(∃y(y ∈ x ⋀ ∀z ¬ z ∈ y) ⋀ ∀y(y ∈ x → ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y)))))
cr1 4624	class R1
crnk 4625	class rank
df-r1 4626	⊢ R1 = rec({⟨x, y⟩∣y = ℘x}, ∅)
df-rank 4627	⊢ rank = {⟨x, y⟩∣y = ∩{z ∈ On∣x ∈ (R1 ‘suc z)}}
ax-ac 4727	⊢ ∃y∀z∀w((z ∈ w ⋀ w ∈ x) → ∃v∀u(∃t((u ∈ w ⋀ w ∈ t) ⋀ (u ∈ t ⋀ t ∈ y)) ↔ u = v))
ccrd 4796	class card
cale 4797	class ℵ
ccf 4798	class cf
df-card 4799	⊢ card = {⟨x, y⟩∣y = ∩{z ∈ On∣z ≈ x}}
df-aleph 4800	⊢ ℵ = rec({⟨x, y⟩∣y = ∩{z ∈ On∣x ≺ z}}, ω)
df-cf 4801	⊢ cf = {⟨x, y⟩∣(x ∈ On ⋀ y = ∩{z∣∃w(z = (card ‘w) ⋀ (w ⊆ x ⋀ ∀v ∈ x ∃u ∈ w v ⊆ u))})}
ccda 4900	class +c
df-cda 4901	⊢ +c = {⟨⟨x, y⟩, z⟩∣z = ((x × {∅}) ∪ (y × {1o}))}
cnpi 4955	class N
cpli 4956	class +N
cmi 4957	class ·N
clti 4958	class <N
cplpq 4959	class +pQ
cmpq 4960	class ·pQ
ceq 4961	class ~Q
cnq 4962	class Q
c1q 4963	class 1Q
cplq 4964	class +Q
cmq 4965	class ·Q
crq 4966	class *Q
cltq 4967	class <Q
cnp 4968	class P
c1p 4969	class 1P
cpp 4970	class +P
cmp 4971	class ·P
cltp 4972	class <P
cplpr 4973	class +pR
cmpr 4974	class ·pR
cer 4975	class ~R
cnr 4976	class R
c0r 4977	class 0R
c1r 4978	class 1R
cm1r 4979	class -1R
cplr 4980	class +R
cmr 4981	class ·R
cltr 4982	class <R
df-ni 4983	⊢ N = (ω ∖ {∅})
df-pli 4984	⊢ +N = ( +o ↾ (N × N))
df-mi 4985	⊢ ·N = ( ·o ↾ (N × N))
df-lti 4986	⊢ <N = (E ∩ (N × N))
df-plpq 5018	⊢ +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 5019	⊢ ·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 5020	⊢ ~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 5021	⊢ Q = ((N × N) / ~Q )
df-plq 5022	⊢ +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 5023	⊢ ·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 5024	⊢ *Q = {⟨x, y⟩∣(x ∈ Q ⋀ (x ·Q y) = 1Q)}
df-ltq 5025	⊢ <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 5026	⊢ 1Q = [⟨1o, 1o⟩] ~Q
df-np 5069	⊢ P = {x∣((∅ ⊂ x ⋀ x ⊂ Q) ⋀ ∀y ∈ x (∀z(z <Q y → z ∈ x) ⋀ ∃z ∈ x y <Q z))}
df-1p 5070	⊢ 1P = {x∣x <Q 1Q}
df-plp 5071	⊢ +P = {⟨⟨x, y⟩, z⟩∣((x ∈ P ⋀ y ∈ P) ⋀ z = {w∣∃v ∈ x ∃u ∈ y w = (v +Q u)})}
df-mp 5072	⊢ ·P = {⟨⟨x, y⟩, z⟩∣((x ∈ P ⋀ y ∈ P) ⋀ z = {w∣∃v ∈ x ∃u ∈ y w = (v ·Q u)})}
df-ltp 5073	⊢ <P = {⟨x, y⟩∣((x ∈ P ⋀ y ∈ P) ⋀ x ⊂ y)}
df-plpr 5147	⊢ +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 5148	⊢ ·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 5149	⊢ ~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 5150	⊢ R = ((P × P) / ~R )
df-plr 5151	⊢ +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 5152	⊢ ·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 5153	⊢ <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 5154	⊢ 0R = [⟨1P, 1P⟩] ~R
df-1r 5155	⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 5156	⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 5215	class ℂ
cr 5216	class ℝ
cc0 5217	class 0
c1 5218	class 1
ci 5219	class i
caddc 5220	class +
cltrr 5221	class <ℝ
cmul 5222	class ·
df-c 5223	⊢ ℂ = (R × R)
df-0 5224	⊢ 0 = ⟨0R, 0R⟩
df-1 5225	⊢ 1 = ⟨1R, 0R⟩
df-i 5226	⊢ i = ⟨0R, 1R⟩
df-r 5227	⊢ ℝ = (R × {0R})
df-plus 5228	⊢ + = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ⋀ y ∈ ℂ) ⋀ ∃w∃v∃u∃f((x = ⟨w, v⟩ ⋀ y = ⟨u, f⟩) ⋀ z = ⟨(w +R u), (v +R f)⟩))}
df-mul 5229	⊢ · = {⟨⟨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 5230	⊢ <ℝ = {⟨x, y⟩∣((x ∈ ℝ ⋀ y ∈ ℝ) ⋀ ∃z∃w((x = ⟨z, 0R⟩ ⋀ y = ⟨w, 0R⟩) ⋀ z <R w))}
cmin 5275	class −
cneg 5276	class -A
cdiv 5277	class /
cle 5278	class ≤
cn 5279	class ℕ
cn0 5280	class ℕ0
cz 5281	class ℤ
cq 5282	class ℚ
crp 5283	class ℝ+
df-sub 5339	⊢ − = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ⋀ y ∈ ℂ) ⋀ z = ∪{w ∈ ℂ∣(y + w) = x})}
df-neg 5341	⊢ -A = (0 − A)
cpnf 5466	class +∞
cmnf 5467	class -∞
cxr 5468	class ℝ*
clt 5469	class <
df-pnf 5470	⊢ +∞ = ℘∪ℂ
df-mnf 5471	⊢ -∞ = ℘ +∞
df-xr 5472	⊢ ℝ* = (ℝ ∪ { +∞, -∞})
df-ltxr 5473	⊢ < = ((( <ℝ ∩ (ℝ × ℝ)) ∪ {⟨ -∞, +∞⟩}) ∪ ((ℝ × { +∞}) ∪ ({ -∞} × ℝ)))
df-le 5474	⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
df-div 5682	⊢ / = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ⋀ y ∈ (ℂ ∖ {0})) ⋀ z = ∪{w ∈ ℂ∣(y · w) = x})}
df-n 5883	⊢ ℕ = ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)}
c2 5918	class 2
c3 5919	class 3
c4 5920	class 4
c5 5921	class 5
c6 5922	class 6
c7 5923	class 7
c8 5924	class 8
c9 5925	class 9
c10 5926	class 10
df-2 5927	⊢ 2 = (1 + 1)
df-3 5928	⊢ 3 = (2 + 1)
df-4 5929	⊢ 4 = (3 + 1)
df-5 5930	⊢ 5 = (4 + 1)
df-6 5931	⊢ 6 = (5 + 1)
df-7 5932	⊢ 7 = (6 + 1)
df-8 5933	⊢ 8 = (7 + 1)
df-9 5934