Metamath Proof Explorer - mmtheorems31

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 3001-3100 - Page 31 of 58

Type	Label	Description
Statement
Syntax	co 3001	Extend class notation to include operations. Note that the syntax is simply three class symbols in a row surrounded by parentheses.
class (AFB)
Syntax	copab2 3002	Extend class notation to include class abstractions of nested ordered pairs.
class {<.<.x, y>., z>. | ph}
Definition	df-opr 3003	Define the result of an operation. Note that the syntax is simply three class symbols in a row bracketed by parentheses. Definition of [Enderton] p. 79. Class F normally denotes an operation such as + that operates on two classes A and B, which might be numbers such as 1 and 2. This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets). On the other hand we often find uses for this definition when F is a proper class.
|- (AFB) = (F` <.A, B>.)
Definition	df-oprab 3004	Define class abstraction of nested ordered pairs (for use in defining operations). A special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally x, y, and z are distinct, although the definition doesn't strictly require it.
|- {<.<.x, y>., z>. | ph} = {w | E.xE.yE.z(w = <.<.x, y>., z>. /\ ph)}
Theorem	opreq 3005	Equality theorem for operations.
|- (F = G -> (AFB) = (AGB))
Theorem	opreq1 3006	Equality theorem for operations.
|- (A = B -> (AFC) = (BFC))
Theorem	opreq2 3007	Equality theorem for operations.
|- (A = B -> (CFA) = (CFB))
Theorem	opreq12 3008	Equality theorem for operations.
|- ((A = B /\ C = D) -> (AFC) = (BFD))
Theorem	opreq1i 3009	Equality inference for operations.
|- A = B   =>   |- (AFC) = (BFC)
Theorem	opreq2i 3010	Equality inference for operations.
|- A = B   =>   |- (CFA) = (CFB)
Theorem	opreq12i 3011	Equality inference for operations.
|- A = B   &   |- C = D   =>   |- (AFC) = (BFD)
Theorem	opreq1d 3012	Equality deduction for operations.
|- (ph -> A = B)   =>   |- (ph -> (AFC) = (BFC))
Theorem	opreq2d 3013	Equality deduction for operations.
|- (ph -> A = B)   =>   |- (ph -> (CFA) = (CFB))
Theorem	opreq12d 3014	Equality deduction for operations.
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (AFC) = (BFD))
Theorem	opreqan12d 3015	Equality deduction for operations.
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ph /\ ps) -> (AFC) = (BFD))
Theorem	opreqan12rd 3016	Equality deduction for operations.
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ps /\ ph) -> (AFC) = (BFD))
Theorem	hbopr 3017	Bound-variable hypothesis builder for operation value.
|- (y e. A -> A.x y e. A)   &   |- (y e. F -> A.x y e. F)   &   |- (y e. B -> A.x y e. B)   =>   |- (y e. (AFB) -> A.x y e. (AFB))
Theorem	oprex 3018	The result of an operation is a set.
|- (AFB) e. V
Theorem	oprprc1 3019	The value of an operation when the first argument is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair.
|- Rel dom F   =>   |- (-. A e. V -> (AFB) = (/))
Theorem	oprprc2 3020	The value of an operation when the second argument is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair.
|- (-. B e. V -> (AFB) = (AFA))
Theorem	dfoprab2 3021	Class abstraction for operations in terms of class abstraction of ordered pairs.
|- {<.<.x, y>., z>. | ph} = {<.w, z>. | E.xE.y(w = <.x, y>. /\ ph)}
Theorem	reloprab 3022	The operation class abstraction is a relation.
|- Rel {<.<.x, y>., z>. | ph}
Theorem	hboprab1 3023	The abstraction variables in an operation abstraction are not free.
|- (w e. {<.<.x, y>., z>. | ph} -> A.x w e. {<.<.x, y>., z>. | ph})
Theorem	hboprab2 3024	The abstraction variables in an operation abstraction are not free.
|- (w e. {<.<.x, y>., z>. | ph} -> A.y w e. {<.<.x, y>., z>. | ph})
Theorem	bioprabd 3025	Equivalent wff's yield equal operation class abstractions (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- (ph -> A.zph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> {<.<.x, y>., z>. | ps} = {<.<.x, y>., z>. | ch})
Theorem	bioprabdv 3026	Equivalent wff's yield equal operation class abstractions (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> {<.<.x, y>., z>. | ps} = {<.<.x, y>., z>. | ch})
Theorem	bioprabi 3027	Equivalent wff's yield equal operation class abstractions.
|- (ph <-> ps)   =>   |- {<.<.x, y>., z>. | ph} = {<.<.x, y>., z>. | ps}
Theorem	cbvoprab12 3028	Rule used to change first two bound variables in an operation abstraction, using implicit substitution.
|- (ph -> A.wph)   &   |- (ph -> A.vph)   &   |- (ps -> A.xps)   &   |- (ps -> A.yps)   &   |- ((x = w /\ y = v) -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.w, v>., z>. | ps}
Theorem	cbvoprab12v 3029	Rule used to change first two bound variables in an operation abstraction, using implicit substitution.
|- ((x = w /\ y = v) -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.w, v>., z>. | ps}
Theorem	cbvoprab3v 3030	Rule used to change the third bound variable in an operation abstraction, using implicit substitution.
|- (z = w -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.x, y>., w>. | ps}
Theorem	dmoprab 3031	The domain of an operation abstraction.
|- dom {<.<.x, y>., z>. | ph} = {<.x, y>. | E.zph}
Theorem	dmoprabss 3032	The domain of an operation abstraction.
|- dom {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} (_ (A X. B)
Theorem	rnoprab 3033	The range of an operation class abstraction.
|- ran {<.<.x, y>., z>. | ph} = {z | E.xE.yph}
Theorem	reldmoprab 3034	The domain of an operation class abstraction is a relation.
|- Rel dom {<.<.x, y>., z>. | ph}
Theorem	eloprabg 3035	The law of concretion for operation class abstraction. Compare elopab 2110.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   =>   |- ((A e. D /\ B e. R /\ C e. S) -> (<.<.A, B>., C>. e. {<.<.x, y>., z>. | ph} <-> th))
Theorem	ssoprab2i 3036	Inference of operation abstraction subclass from implication.
|- (ph -> ps)   =>   |- {<.<.x, y>., z>. | ph} (_ {<.<.x, y>., z>. | ps}
Theorem	funoprab 3037	"At most one" is sufficient condition for an operation abstraction to be a function.
|- E*zph   =>   |- Fun {<.<.x, y>., z>. | ph}
Theorem	fnoprab 3038	Functionality and domain of an operation abstraction.
|- (ph -> E!zps)   =>   |- {<.<.x, y>., z>. | (ph /\ ps)} Fn {<.x, y>. | ph}
Theorem	fnoprab2 3039	Functionality and domain of an operation abstraction.
|- C e. V   &   |- F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}   =>   |- F Fn (A X. B)
Theorem	dmoprab2 3040	Domain of an operation abstraction.
|- C e. V   &   |- F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}   =>   |- dom F = (A X. B)
Theorem	ffnoprval 3041	An operation maps to a class to which all values belong.
|- (F:(A X. B)-->C <-> (F Fn (A X. B) /\ A.x e. A A.y e. B (xFy) e. C))
Theorem	fnoprval 3042	Representation of an operation abstraction in terms of its values.
|- (F Fn (A X. B) <-> F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = (xFy))})
Theorem	foprval 3043	Representation of an operation abstraction in terms of its values.
|- (F:(A X. B)-->C <-> (F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = (xFy))} /\ A.x e. A A.y e. B (xFy) e. C))
Theorem	oprabex 3044	Existence of an operation abstraction.
|- A e. V   &   |- B e. V   &   |- ((x e. A /\ y e. B) -> E*zph)   &   |- F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)}   =>   |- F e. V
Theorem	oprabex2 3045	Existence of an operation abstraction (special case).
|- A e. V   &   |- B e. V   &   |- F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}   =>   |- F e. V
Theorem	oprabex3 3046	Existence of an operation abstraction (special case).
|- H e. V   &   |- F = {<.<.x, y>., z>. | ((x e. (H X. H) /\ y e. (H X. H)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = R))}   =>   |- F e. V
Theorem	oprabval 3047	The value of an operation abstraction.
|- C e. V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- ((x e. R /\ y e. S) -> E!zph)   &   |- F = {<.<.x, y>., z>. | ((x e. R /\ y e. S) /\ ph)}   =>   |- ((A e.