mmtheorems41 - Metamath Proof Explorer

Jump to page: Contents + 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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10682

Statement List for Metamath Proof Explorer - 4001-4100 - Page 41 of 107

Type	Label	Description
Statement
Theorem	elimdeloprv 4001	Eliminate a hypothesis which is a predicate expressing membership in the result of an operator (deduction version). See ghomgrplem 10350 for an example of its use. (Contributed by Paul Chapman, 25-Mar-2008.)
|- (ph -> C e. (AFB))   &   |- Z e. (XFY)   =>   |- if(ph, C, Z) e. (if(ph, A, X)Fif(ph, B, Y))
Theorem	dmoprab 4002	The domain of an operation class abstraction.
|- dom {<.<.x, y>., z>. | ph} = {<.x, y>. | E.zph}
Theorem	dmoprabss 4003	The domain of an operation class abstraction.
|- dom {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} (_ (A X. B)
Theorem	rnoprab 4004	The range of an operation class abstraction.
|- ran {<.<.x, y>., z>. | ph} = {z | E.xE.yph}
Theorem	reldmoprab 4005	The domain of an operation class abstraction is a relation.
|- Rel dom {<.<.x, y>., z>. | ph}
Theorem	oprabss 4006	Structure of an operation class abstraction.
|- {<.<.x, y>., z>. | ph} (_ ((V X. V) X. V)
Theorem	eloprabg 4007	The law of concretion for operation class abstraction. Compare elopab 2808.
|- (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 4008	Inference of operation class abstraction subclass from implication.
|- (ph -> ps)   =>   |- {<.<.x, y>., z>. | ph} (_ {<.<.x, y>., z>. | ps}
Theorem	resoprab 4009	Restriction of an operation class abstraction.
|- ({<.<.x, y>., z>. | ph} |` (A X. B)) = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)}
Theorem	funoprabg 4010	"At most one" is a sufficient condition for an operation class abstraction to be a function.
|- (A.xA.yE*zph -> Fun {<.<.x, y>., z>. | ph})
Theorem	funoprab 4011	"At most one" is a sufficient condition for an operation class abstraction to be a function.
|- E*zph   =>   |- Fun {<.<.x, y>., z>. | ph}
Theorem	fnoprabg 4012	Functionality and domain of an operation class abstraction.
|- (A.xA.y(ph -> E!zps) -> {<.<.x, y>., z>. | (ph /\ ps)} Fn {<.x, y>. | ph})
Theorem	fnoprab 4013	Functionality and domain of an operation class abstraction.
|- (ph -> E!zps)   =>   |- {<.<.x, y>., z>. | (ph /\ ps)} Fn {<.x, y>. | ph}
Theorem	ffnoprval 4014	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	foprcl 4015	Closure law for an operation.
|- F:(R X. S)-->C   =>   |- ((A e. R /\ B e. S) -> (AFB) e. C)
Theorem	eqfnoprval 4016	Equality of two operations is determined by their values.
|- ((F Fn (A X. B) /\ G Fn (C X. D)) -> (F = G <-> ((A X. B) = (C X. D) /\ A.x e. A A.y e. B (xFy) = (xGy))))
Theorem	fnoprval 4017	Representation of an operation class 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 4018	Representation of an operation class 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 4019	Existence of an operation class 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	oprabex2g 4020	Existence of an operation class abstraction (special case).
|- F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}   =>   |- ((A e. R /\ B e. S) -> F e. V)
Theorem	oprabex2 4021	Existence of an operation class 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 4022	Existence of an operation class 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 4023	The value of an operation class 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. R /\ B e. S) -> ((AFB) = C <-> th))
Theorem	oprabvalig 4024	The value of an operation class abstraction (weak version).
|- (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. R /\ B e. S /\ C e. D) -> (th -> (AFB) = C))
Theorem	oprabvali 4025	The value of an operation class abstraction (weak version).
|- 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. R /\ B e. S) -> (th -> (AFB) = C))
Theorem	oprabval2gf 4026	The value of an operation class abstraction. A version of oprabval2g 4027 using bound-variable hypotheses.
|- (w e. G -> A.x w e. G)   &   |- (w e. S -> A.y w e. S)   &   |- (x = A -> R = G)   &   |- (y = B -> G = S)   &   |- F = {<.<.x, y>., z>. | ((x e. C /\ y e. D) /\ z = R)}   =>   |- ((A e. C /\ B e. D /\ S e. H) -> (AFB) = S)
Theorem	oprabval2g 4027	The value of an operation class abstraction. Special case.
|- (x = A -> R = G)   &   |- (y = B -> G = S)   &   |- F = {<.<.x, y>., z>. | ((x e. C /\ y e. D) /\ z = R)}   =>   |- ((A e. C /\ B e. D /\ S e. H) -> (AFB) = S)
Theorem	oprabval2 4028	The value of an operation class abstraction. Special case.
|- S e. V   &   |- (x = A -> R = G)   &   |- (y = B -> G = S)   &   |- F = {<.<.x, y>., z>. | ((x e. C /\ y e. D) /\ z = R)}   =>   |- ((A e. C /\ B e. D) -> (AFB) = S)
Theorem	oprabval5 4029	The value of an operation class abstraction. Special case.
|- S e. V   &   |- (x = A -> R = G)   &   |- (y = B -> G = S)   &   |- F = {<.<.x, y>., z>. | z = R}   =>   |- ((A e. C /\ B e. D) -> (AFB) = S)
Theorem	oprabval3 4030	The value of an operation class abstraction. Special case.
|- S e. V   &   |- (((w = A /\ v = B) /\ (u = C /\ f = D)) -> R = S)   &   |- 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))}   =>   |- (((A e. H /\ B e. H) /\ (C e. H /\ D e. H)) -> (<.A