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 952	wff ∀xφ
cv 953	class x
wceq 954	wff A = B
wcel 956	wff A ∈ B
ax-5 958	⊢ (∀x(φ → ψ) → (∀xφ → ∀xψ))
ax-6 959	⊢ (¬ ∀xφ → ∀x ¬ ∀xφ)
ax-7 960	⊢ (∀x∀yφ → ∀y∀xφ)
ax-gen 961	⊢ φ    ⇒   ⊢ ∀xφ
ax-8 962	⊢ (x = y → (x = z → y = z))
ax-9 963	⊢ ¬ ∀x ¬ x = y
ax-10 964	⊢ (∀x x = y → ∀y y = x)
ax-11 965	⊢ (x = y → (∀yφ → ∀x(x = y → φ)))
ax-12 966	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
ax-13 967	⊢ (x = y → (x ∈ z → y ∈ z))
ax-14 968	⊢ (x = y → (z ∈ x → z ∈ y))
ax-17 969	⊢ (φ → ∀xφ)
ax-4 971	⊢ (∀xφ → φ)
ax-5o 973	⊢ (∀x(∀xφ → ψ) → (∀xφ → ∀xψ))
ax-6o 976	⊢ (¬ ∀x ¬ ∀xφ → φ)
wex 978	wff ∃xφ
df-ex 979	⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
ax-9o 1121	⊢ (∀x(x = y → ∀xφ) → φ)
ax-10o 1138	⊢ (∀x x = y → (∀xφ → ∀yφ))
wsbc 1168	wff [A / x]φ
df-sb 1170	⊢ ([y / x]φ ↔ ((x = y → φ) ⋀ ∃x(x = y ⋀ φ)))
ax-16 1208	⊢ (∀x x = y → (φ → ∀xφ))
ax-11o 1216	⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
ax-15 1358	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))
weu 1378	wff ∃!xφ
wmo 1379	wff ∃*xφ
df-eu 1380	⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))
df-mo 1381	⊢ (∃*xφ ↔ (∃xφ → ∃!xφ))
ax-ext 1457	⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y)
cab 1461	class {x∣φ}
df-clab 1462	⊢ (x ∈ {y∣φ} ↔ [x / y]φ)
df-cleq 1467	⊢ (∀x(x ∈ y ↔ x ∈ z) → y = z)    ⇒   ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
df-clel 1470	⊢ (A ∈ B ↔ ∃x(x = A ⋀ x ∈ B))
wne 1582	wff A ≠ B
wnel 1583	wff A ∉ B
df-ne 1584	⊢ (A ≠ B ↔ ¬ A = B)
df-nel 1585	⊢ (A ∉ B ↔ ¬ A ∈ B)
wral 1642	wff ∀x ∈ A φ
wrex 1643	wff ∃x ∈ A φ
wreu 1644	wff ∃!x ∈ A φ
crab 1645	class {x ∈ A∣φ}
df-ral 1646	⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
df-rex 1647	⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ⋀ φ))
df-reu 1648	⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ⋀ φ))
df-rab 1649	⊢ {x ∈ A∣φ} = {x∣(x ∈ A ⋀ φ)}
cvv 1807	class V
df-v 1808	⊢ V = {x∣x = x}
df-sbc 1938	⊢ ([A / x]φ ↔ A ∈ {x∣φ})
csb 1997	class [A / x]B
df-csb 1998	⊢ [A / x]B = {y∣[A / x]y ∈ B}
cdif 2040	class (A ∖ B)
cun 2041	class (A ∪ B)
cin 2042	class (A ∩ B)
wss 2043	wff A ⊆ B
wpss 2044	wff A ⊂ B
df-dif 2045	⊢ (A ∖ B) = {x∣(x ∈ A ⋀ ¬ x ∈ B)}
df-un 2046	⊢ (A ∪ B) = {x∣(x ∈ A ⋁ x ∈ B)}
df-in 2047	⊢ (A ∩ B) = {x∣(x ∈ A ⋀ x ∈ B)}
df-ss 2049	⊢ (A ⊆ B ↔ (A ∩ B) = A)
df-pss 2051	⊢ (A ⊂ B ↔ (A ⊆ B ⋀ A ≠ B))
c0 2276	class ∅
df-nul 2277	⊢ ∅ = (V ∖ V)
cif 2357	class if(φ, A, B)
df-if 2358	⊢ if(φ, A, B) = {x∣((x ∈ A ⋀ φ) ⋁ (x ∈ B ⋀ ¬ φ))}
cpw 2397	class ℘A
df-pw 2398	⊢ ℘A = {x∣x ⊆ A}
csn 2405	class {A}
cpr 2406	class {A, B}
cop 2407	class ⟨A, B⟩
df-sn 2408	⊢ {A} = {x∣x = A}
df-pr 2409	⊢ {A, B} = ({A} ∪ {B})
ctp 2410	class {A, B, C}
df-tp 2411	⊢ {A, B, C} = ({A, B} ∪ {C})
df-op 2412	⊢ ⟨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 2827	class E
cid 2828	class I
df-eprel 2829	⊢ E = {⟨x, y⟩∣x ∈ y}
df-id 2832	⊢ I = {⟨x, y⟩∣x = y}
wpo 2837	wff R Po A
wor 2838	wff R Or A
df-po 2839	⊢ (R Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ⋀ ((xRy ⋀ yRz) → xRz)))
df-so 2849	⊢ (R Or A ↔ (R Po A ⋀ ∀x ∈ A ∀y ∈ A (xRy ⋁ x = y ⋁ yRx)))
ax-un 2865	⊢ ∃y∀z(∃w(z ∈ w ⋀ w ∈ x) → z ∈ y)
wfr 2914	wff R Fr A
wwe 2915	wff R We A
df-fr 2916	⊢ (R Fr A ↔ ∀x((x ⊆ A ⋀ x ≠ ∅) → ∃y ∈ x ∀z ∈ x ¬ zRy))
df-we 2933	⊢ (R We A ↔ (R Fr A ⋀ R Or A))
word 2946	wff Ord A
con0 2947	class On
wlim 2948	wff Lim A
csuc 2949	class suc A
df-ord 2950	⊢ (Ord A ↔ (Tr A ⋀ E We A))
df-on 2951	⊢ On = {x∣Ord x}
df-lim 2952	⊢ (Lim A ↔ (Ord A ⋀ A ≠ ∅ ⋀ A = ∪A))
df-suc 2953	⊢ suc A = (A ∪ {A})
com 3131	class ω
df-om 3132	⊢ ω = {x∣(Ord x ⋀ ∀y(Lim y → x ∈ y))}
cxp 3168	class (A × B)
ccnv 3169	class ◡A
cdm 3170	class dom A
crn 3171	class ran A
cres 3172	class (A ↾ B)
cima 3173	class (A “ B)
ccom 3174	class (A ∘ B)
wrel 3175	wff Rel A
wfun 3176	wff Fun A
wfn 3177	wff A Fn B
wf 3178	wff F:A–→B
wf1 3179	wff F:A–1-1→B
wfo 3180	wff F:A–onto→B
wf1o 3181	wff F:A–1-1-onto→B
cfv 3182	class (F ‘A)
wiso 3183	wff H Isom R, S (A, B)
df-xp 3184	⊢ (A × B) = {⟨x, y⟩∣(x ∈ A ⋀ y ∈ B)}
df-rel 3185	⊢ (Rel A ↔ A ⊆ (V × V))
df-cnv 3186	⊢ ◡A = {⟨x, y⟩∣yAx}
df-co 3187	⊢ (A ∘ B) = {⟨x, y⟩∣∃z(xBz ⋀ zAy)}
df-dm 3188	⊢ dom A = {x∣∃y xAy}
df-rn 3189	⊢ ran A = dom ◡ A
df-res 3190	⊢ (A ↾ B) = (A ∩ (B × V))
df-ima 3191	⊢ (A “ B) = ran ( A ↾ B)
df-fun 3192	⊢ (Fun A ↔ (Rel A ⋀ (A ∘ ◡A) ⊆ I))
df-fn 3193	⊢ (A Fn B ↔ (Fun A ⋀ dom A = B))
df-f 3194	⊢ (F:A–→B ↔ (F Fn A ⋀ ran F ⊆ B))
df-f1 3195	⊢ (F:A–1-1→B ↔ (F:A–→B ⋀ Fun ◡F))
df-fo 3196	⊢ (F:A–onto→B ↔ (F Fn A ⋀ ran F = B))
df-f1o 3197	⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ⋀ F:A–onto→B))
df-fv 3198	⊢ (F ‘A) = ∪{x∣(F “ {A}) = {x}}
df-iso 3199	⊢ (H Isom R, S (A, B) ↔ (H:A–1-1-onto→B ⋀ ∀x ∈ A ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))))
crdg 3932	class rec(A, B)
df-rdg 3933	⊢ 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 3964	class (AFB)
copab2 3965	class {⟨⟨x, y⟩, z⟩∣φ}
df-opr 3966	⊢ (AFB) = (F ‘⟨A, B⟩)
df-oprab 3967	⊢ {⟨⟨x, y⟩, z⟩∣φ} = {w∣∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ⋀ φ)}
cmpt 4073	class (x ∈ A ↦ B)
cmpt2 4074	class (x ∈ A, y ∈ B ↦ C)
df-mpt 4075	⊢ (x ∈ A ↦ B) = {⟨x, y⟩∣(x ∈ A ⋀ y = B)}
df-mpt2 4076	⊢ (x ∈ A, y ∈ B ↦ C) = {⟨⟨x, y⟩, z⟩∣((x ∈ A ⋀ y ∈ B) ⋀ z = C)}
c1st 4077	class 1st
c2nd 4078	class 2nd
df-1st 4079	⊢ 1st = {⟨x, y⟩∣y = ∪dom { x}}
df-2nd 4080	⊢ 2nd = {⟨x, y⟩∣y = ∪ran { x}}
c1o 4128	class 1o
c2o 4129	class 2o
coa 4130	class +o
comu 4131	class ·o
coe 4132	class ↑o
df-1o 4133	⊢ 1o = suc ∅
df-2o 4134	⊢ 2o = suc 1o
df-oadd 4135	⊢ +o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ⋀ y ∈ On) ⋀ z = (rec({⟨w, v⟩∣v = suc w}, x) ‘y))}
df-omul 4136	⊢ ·o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ⋀ y ∈ On) ⋀ z = (rec({⟨w, v⟩∣v = (w +o x)}, ∅) ‘y))}
df-oexp 4137	⊢ ↑o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ⋀ y ∈ On) ⋀ z = if(x = ∅, (1o ∖ y), (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y)))}
wer 4258	wff Er R
cec 4259	class [A]R
cqs 4260	class (A / R)
df-er 4261	⊢ (Er R ↔ (◡R ∪ (R ∘ R)) ⊆ R)
df-ec 4263	⊢ [A]R = (R “ {A})
df-qs 4266	⊢ (A / R) = {y∣∃x ∈ A y = [x]R}
cm 4322	class ↑m
cpm 4323	class ↑pm
df-map 4324	⊢ ↑m = {⟨⟨x, y⟩, z⟩∣z = {f∣f:y–→x}}
df-pm 4325	⊢ ↑pm = {⟨⟨x, y⟩, z⟩∣z = {f∣(Fun f ⋀ f ⊆ (y × x))}}
cixp 4347	class Xx ∈ A B
df-ixp 4348	⊢ Xx ∈ A B = {f∣(f Fn A ⋀ ∀x ∈ A (f ‘x) ∈ B)}
cen 4364	class ≈
cdom 4365	class ≼
csdm 4366	class ≺
df-en 4367	⊢ ≈ = {⟨x, y⟩∣∃f f:x–1-1-onto→y}
df-dom 4368	⊢ ≼ = {⟨x, y⟩∣∃f f:x–1-1→y}
df-sdom 4369	⊢ ≺ = ( ≼ ∖ ≈ )
csup 4564	class sup(A, B, R)
df-sup 4565	⊢ sup(B, A, R) = ∪{x ∈ A∣(∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))}
ax-reg 4584	⊢ (∃y y ∈ x → ∃y(y ∈ x ⋀ ∀z(z ∈ y → ¬ z ∈ x)))
ax-inf 4613	⊢ ∃y(x ∈ y ⋀ ∀z(z ∈ y → ∃w(z ∈ w ⋀ w ∈ y)))
ax-inf2 4616	⊢ ∃x(∃y(y ∈ x ⋀ ∀z ¬ z ∈ y) ⋀ ∀y(y ∈ x → ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y)))))
cr1 4632	class R1
crnk 4633	class rank
df-r1 4634	⊢ R1 = rec({⟨x, y⟩∣y = ℘x}, ∅)
df-rank 4635	⊢ rank = {⟨x, y⟩∣y = ∩{z ∈ On∣x ∈ (R1 ‘suc z)}}
ax-ac 4735	⊢ ∃y∀z∀w((z ∈ w ⋀ w ∈ x) → ∃v∀u(∃t((u ∈ w ⋀ w ∈ t) ⋀ (u ∈ t ⋀ t ∈ y)) ↔ u = v))
ccrd 4804	class card
cale 4805	class ℵ
ccf 4806	class cf
df-card 4807	⊢ card = {⟨x, y⟩∣y = ∩{z ∈ On∣z ≈ x}}
df-aleph 4808	⊢ ℵ = rec({⟨x, y⟩∣y = ∩{z ∈ On∣x ≺ z}}, ω)
df-cf 4809	⊢ cf = {⟨x, y⟩∣(x ∈ On ⋀ y = ∩{z∣∃w(z = (card ‘w) ⋀ (w ⊆ x ⋀ ∀v ∈ x ∃u ∈ w v ⊆ u))})}
ccda 4908	class +c
df-cda 4909	⊢ +c = {⟨⟨x, y⟩, z⟩∣z = ((x × {∅}) ∪ (y × {1o}))}
cnpi 4963	class N
cpli 4964	class +N
cmi 4965	class ·N
clti 4966	class <N
cplpq 4967	class +pQ
cmpq 4968	class ·pQ
ceq 4969	class ~Q
cnq 4970	class Q
c1q 4971	class 1Q
cplq 4972	class +Q
cmq 4973	class ·Q
crq 4974	class *Q
cltq 4975	class <Q
cnp 4976	class P
c1p 4977	class 1P
cpp 4978	class +P
cmp 4979	class ·P
cltp 4980	class <P
cplpr 4981	class +pR
cmpr 4982	class ·pR
cer 4983	class ~R
cnr 4984	class R
c0r 4985	class 0R
c1r 4986	class 1R
cm1r 4987	class -1R
cplr 4988	class +R
cmr 4989	class ·R
cltr 4990	class <R
df-ni 4991	⊢ N = (ω ∖ {∅})
df-pli 4992	⊢ +N = ( +o ↾ (N × N))
df-mi 4993	⊢ ·N = ( ·o ↾ (N × N))
df-lti 4994	⊢ <N = (E ∩ (N × N))
df-plpq 5026	⊢ +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 5027	⊢ ·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 5028	⊢ ~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 5029	⊢ Q = ((N × N) / ~Q )
df-plq 5030	⊢ +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 5031	⊢ ·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 5032	⊢ *Q = {⟨x, y⟩∣(x ∈ Q ⋀ (x ·Q y) = 1Q)}
df-ltq 5033	⊢ <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 5034	⊢ 1Q = [⟨1o, 1o⟩] ~Q
df-np 5077	⊢ P = {x∣((∅ ⊂ x ⋀ x ⊂ Q) ⋀ ∀y ∈ x (∀z(z <Q y → z ∈ x) ⋀ ∃z ∈ x y <Q z))}
df-1p 5078	⊢ 1P = {x∣x <Q 1Q}
df-plp 5079	⊢ +P = {⟨⟨x, y⟩, z⟩∣((x ∈ P ⋀ y ∈ P) ⋀ z = {w∣∃v ∈ x ∃u ∈ y w = (v +Q u)})}
df-mp 5080	⊢ ·P = {⟨⟨x, y⟩, z⟩∣((x ∈ P ⋀ y ∈ P) ⋀ z = {w∣∃v ∈ x ∃u ∈ y w = (v ·Q u)})}
df-ltp 5081	⊢ <P = {⟨x, y⟩∣((x ∈ P ⋀ y ∈ P) ⋀ x ⊂ y)}
df-plpr 5155	⊢ +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 5156	⊢ ·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 5157	⊢ ~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 5158	⊢ R = ((P × P) / ~R )
df-plr 5159	⊢ +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 5160	⊢ ·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 5161	⊢ <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 5162	⊢ 0R = [⟨1P, 1P⟩] ~R
df-1r 5163	⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 5164	⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 5223	class ℂ
cr 5224	class ℝ
cc0 5225	class 0
c1 5226	class 1
ci 5227	class i
caddc 5228	class +
cltrr 5229	class <ℝ
cmul 5230	class ·
df-c 5231	⊢ ℂ = (R × R)
df-0 5232	⊢ 0 = ⟨0R, 0R⟩
df-1 5233	⊢ 1 = ⟨1R, 0R⟩
df-i 5234	⊢ i = ⟨0R, 1R⟩
df-r 5235	⊢ ℝ = (R × {0R})
df-plus 5236	⊢ + = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ⋀ y ∈ ℂ) ⋀ ∃w∃v∃u∃f((x = ⟨w, v⟩ ⋀ y = ⟨u, f⟩) ⋀ z = ⟨(w +R u), (v +R f)⟩))}
df-mul 5237	⊢ · = {⟨⟨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 5238	⊢ <ℝ = {⟨x, y⟩∣((x ∈ ℝ ⋀ y ∈ ℝ) ⋀ ∃z∃w((x = ⟨z, 0R⟩ ⋀ y = ⟨w, 0R⟩) ⋀ z <R w))}
cmin 5283	class −
cneg 5284	class -A
cdiv 5285	class /
cle 5286	class ≤
cn 5287	class ℕ
cn0 5288	class ℕ0
cz 5289	class ℤ
cq 5290	class ℚ
crp 5291	class ℝ+
df-sub 5347	⊢ − = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ⋀ y ∈ ℂ) ⋀ z = ∪{w ∈ ℂ∣(y + w) = x})}
df-neg 5349	⊢ -A = (0 − A)
cpnf 5474	class +∞
cmnf 5475	class -∞
cxr 5476	class ℝ*
clt 5477	class <
df-pnf 5478	⊢ +∞ = ℘∪ℂ
df-mnf 5479	⊢ -∞ = ℘ +∞
df-xr 5480	⊢ ℝ* = (ℝ ∪ { +∞, -∞})
df-ltxr 5481	⊢ < = ((( <ℝ ∩ (ℝ × ℝ)) ∪ {⟨ -∞, +∞⟩}) ∪ ((ℝ × { +∞}) ∪ ({ -∞} × ℝ)))
df-le 5482	⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
df-div 5691	⊢ / = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ⋀ y ∈ (ℂ ∖ {0})) ⋀ z = ∪{w ∈ ℂ∣(y · w) = x})}
df-n 5892	⊢ ℕ = ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)}
c2 5927	class 2
c3 5928	class 3
c4 5929	class 4
c5 5930	class 5
c6 5931	class 6
c7 5932	class 7
c8 5933	class 8
c9 5934	class 9
c10 5935	class 10
df-2 5936	⊢ 2 = (1 + 1)
df-3 5937	⊢ 3 = (2 + 1)
df-4 5938	⊢ 4 = (3 + 1)
df-5 5939	⊢ 5 = (4 + 1)
df-6 5940	⊢ 6 = (5 + 1)
df-7 5941	⊢ 7 = (6 + 1)
df-8 5942	⊢ 8 = (7 + 1)
df-9 5943