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-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

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

Type	Label	Description
Statement
Theorem	isoeq1 4001	Equality theorem for isomorphisms.
|- (H = G -> (H Isom R, S (A, B) <-> G Isom R, S (A, B)))
Theorem	isoeq2 4002	Equality theorem for isomorphisms.
|- (R = T -> (H Isom R, S (A, B) <-> H Isom T, S (A, B)))
Theorem	isoeq3 4003	Equality theorem for isomorphisms.
|- (S = T -> (H Isom R, S (A, B) <-> H Isom R, T (A, B)))
Theorem	isoeq4 4004	Equality theorem for isomorphisms.
|- (A = C -> (H Isom R, S (A, B) <-> H Isom R, S (C, B)))
Theorem	isoeq5 4005	Equality theorem for isomorphisms.
|- (B = C -> (H Isom R, S (A, B) <-> H Isom R, S (A, C)))
Theorem	hbiso 4006	Bound-variable hypothesis builder for an isomorphism.
|- (y e. H -> A.x y e. H)   &   |- (y e. R -> A.x y e. R)   &   |- (y e. S -> A.x y e. S)   &   |- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (H Isom R, S (A, B) -> A.x H Isom R, S (A, B))
Theorem	isof1o 4007	An isomorphism is a one-to-one onto function.
|- (H Isom R, S (A, B) -> H:A-1-1-onto->B)
Theorem	isorel 4008	An isomorphism connects binary relations via its function values.
|- ((H Isom R, S (A, B) /\ (C e. A /\ D e. A)) -> (CRD <-> (H` C)S(H` D)))
Theorem	isoid 4009	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33.
|- (I |` A) Isom R, R (A, A)
Theorem	isocnv 4010	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33.
|- (H Isom R, S (A, B) -> `'H Isom S, R (B, A))
Theorem	isotr 4011	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33.
|- ((H Isom R, S (A, B) /\ G Isom S, T (B, C)) -> (G o. H) Isom R, T (A, C))
Theorem	isotrALT 4012	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. This proof is shorter than isotr 4011 in set.mm and uses fewer dummy variables, but it takes 240K vs. 207K for the web page.
|- ((H Isom R, S (A, B) /\ G Isom S, T (B, C)) -> (G o. H) Isom R, T (A, C))
Theorem	isomin 4013	Isomorphisms preserve minimal elements. Note that (`'R"{D}) is Takeuti and Zaring's idiom for the initial segment {x | xRD}. Proposition 6.31(1) of [TakeutiZaring] p. 33.
|- ((H Isom R, S (A, B) /\ (C (_ A /\ D e. A)) -> ((C i^i (`'R"{D})) = (/) <-> ((H"C) i^i (`'S"{(H` D)})) = (/)))
Theorem	isoini 4014	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33.
|- ((H Isom R, S (A, B) /\ D e. A) -> (H"(A i^i (`'R"{D}))) = (B i^i (`'S"{(H` D)})))
Theorem	isofrlem 4015	Lemma for isofr 4016.
Theorem	isofr 4016	An isomorphism preserves foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33.
|- (H Isom R, S (A, B) -> (R Fr A <-> S Fr B))
Theorem	isowe 4017	An isomorphism preserves well ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33.
|- (H Isom R, S (A, B) -> (R We A <-> S We B))
Theorem	f1oiso 4018	Any one-to-one onto function determines an isomorphism with an induced relation S. Proposition 6.33 of [TakeutiZaring] p. 34.
|- ((H:A-1-1-onto->B /\ S = {<.z, w>. | E.x e. A E.y e. A ((z = (H` x) /\ w = (H` y)) /\ xRy)}) -> H Isom R, S (A, B))
Theorem	f1owe 4019	Well-ordering of isomorphic relations.
|- R = {<.x, y>. | (F` x)S(F` y)}   =>   |- (F:A-1-1-onto->B -> (S We B -> R We A))
Theorem	f1oweALT 4020	Well-ordering of isomorphic relations. (This version is proved directly instead of wit the isomorphism predicate.)
|- R = {<.x, y>. | (F` x)S(F` y)}   =>   |- (F:A-1-1-onto->B -> (S We B -> R We A))
Operations
Syntax	co 4021	Extend class notation to include the value of an operation F (such as +) for two arguments A and B. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 5447.)
class (AFB)
Syntax	copab2 4022	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {<.<.x, y>., z>. | ph}
Definition	df-opr 4023	Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation F and its arguments A and B - will be useful for proving meaningful theorems. For example, if class F is the operation + and arguments A and B are 3 and 2, the expression (3 + 2) can be proved to equal 5 (see 3p2e5 6153). This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets); see oprprc1 4042 and oprprc2 4043. On the other hand, we often find uses for this definition when F is a proper class, such as +o in oav 4286. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 4024.
|- (AFB) = (F` <.A, B>.)
Definition	df-oprab 4024	Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is 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. See df-opr 4023 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by oprabval2 4088.
|- {<.<.x, y>., z>. | ph} = {w | E.xE.yE.z(w = <.<.x, y>., z>. /\ ph)}
Theorem	opreq 4025	Equality theorem for operation value.
|- (F = G -> (AFB) = (AGB))
Theorem	opreq1 4026	Equality theorem for operation value.
|- (A = B -> (AFC) = (BFC))
Theorem	opreq2 4027	Equality theorem for operation value.
|- (A = B -> (CFA) = (CFB))
Theorem	opreq12 4028	Equality theorem for operation value.
|- ((A = B /\ C = D) -> (AFC) = (BFD))
Theorem	opreq1i 4029	Equality inference for operation value.
|- A = B   =>   |- (AFC) = (BFC)
Theorem	opreq2i 4030	Equality inference for operation value.
|- A = B   =>   |- (CFA) = (CFB)
Theorem	opreq12i 4031	Equality inference for operation value.
|- A = B   &   |- C = D   =>   |- (AFC) = (BFD)
Theorem	opreqi 4032	Equality inference for operation value.
|- A = B   =>   |- (CAD) = (CBD)
Theorem	opreq1d 4033	Equality deduction for operation value.
|- (ph -> A = B)   =>   |- (ph -> (AFC) = (BFC))
Theorem	opreq2d 4034	Equality deduction for operation value.
|- (ph -> A = B)   =>   |- (ph -> (CFA) = (CFB))
Theorem	opreqd 4035	Equality deduction for operation value.
|- (ph -> A = B)   =>   |- (ph -> (CAD) = (CBD))
Theorem	opreq12d 4036	Equality deduction for operation value.
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (AFC) = (BFD))
Theorem	opreqan12d 4037	Equality deduction for operation value.
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ph /\ ps) -> (AFC) = (BFD))
Theorem	opreqan12rd 4038	Equality deduction for operation value.
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ps /\ ph) -> (AFC) = (BFD))
Theorem	hbopr 4039	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	hboprd 4040	Deduction version of bound-variable hypothesis builder hbopr 4039.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   &   |- (ph -> (y e. F -> A.x y e. F))   &   |- (ph -> (y e. B -> A.x y e. B))   =>   |- (ph -> (y e. (AFB) -> A.x y e. (AFB)))
Theorem	oprex 4041	The result of an operation is a set.
|- (AFB) e. V
Theorem	oprprc1 4042	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 4043	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	csboprg 4044	Move class substitution in and out of an operation.
|- (A e. D -> [_A / x]_(BFC) = ([_A / x]_B[_A / x]_F[_A / x]_C))
Theorem	csbopr12g 4045	Move class substitution in and out of an operation.
|- (A e. D -> [_A / x]_(BFC) = ([_A / x]_BF[_A / x]_C))
Theorem	csbopr1g 4046	Move class substitution in and out of an operation.
|- (A e. D -> [_A / x]_(BFC) = ([_A / x]_BFC))
Theorem	csbopr2g 4047	Move class substitution in and out of an operation.
|- (A e. D -> [_A / x]_(BFC) = (BF[_A / x]_C))
Theorem	rcla4eopr 4048	A frequently used special case of rcla42ev 1927 for operation values.
|- ((C e. A /\ D e. B /\ S = (CFD)) -> E.x e. A E.y e. B S = (xFy))
Theorem	fnotoprb 4049	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 3865.
|- R e. V   =>   |- ((F Fn (A X. B) /\ C e. A /\ D e. B) -> ((CFD) = R <-> <.<.C, D>., R>. e. F))
Theorem	dfoprab2 4050	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 4051	An operation class abstraction is a relation.
|- Rel {<.<.x, y>., z>. | ph}
Theorem	hboprab1 4052	The abstraction variables in an operation class abstraction are not free.
|- (w e. {<.<.x, y>., z>. | ph} -> A.x w e. {<.<.x, y>., z>. | ph})
Theorem	hboprab2 4053	The abstraction variables in an operation class abstraction are not free.
|- (w e. {<.<.x, y>., z>. | ph} -> A.y w e. {<.<.x, y>., z>. | ph})
Theorem	oprabbid 4054	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	oprabbidv 4055	Equivalent wff's yield equal operation class abstractions (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> {<.<.x, y>., z>. | ps} = {<.<.x, y>., z>. | ch})
Theorem	oprabbii 4056	Equivalent wff's yield equal operation class abstractions.
|- (ph <-> ps)   =>   |- {<.<.x, y>., z>. | ph} = {<.<.x, y>., z>. | ps}
Theorem	cbvoprab1 4057	Rule used to change first bound variable in an operation abstraction, using implicit substitution.
|- (ph -> A.wph)   &   |- (ps -> A.xps)   &   |- (x = w -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.w, y>., z>. | ps}
Theorem	cbvoprab12 4058	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 4059	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 4060	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	elimdeloprv 4061	Eliminate a hypothesis which is a predicate expressing membership in the result of an operator (deduction version). See ghomgrplem 10674 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 4062	The domain of an operation class abstraction.
|- dom {<.<.x, y>., z>. | ph} = {<.x, y>. | E.zph}
Theorem	dmoprabss 4063	The domain of an operation class abstraction.
|- dom {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} (_ (A X. B)
Theorem	rnoprab 4064	The range of an operation class abstraction.
|- ran {<.<.x, y>., z>. | ph} = {z | E.xE.yph}
Theorem	reldmoprab 4065	The domain of an operation class abstraction is a relation.
|- Rel dom {<.<.x, y>., z>. | ph}
Theorem	oprabss 4066	Structure of an operation class abstraction.
|- {<.<.x, y>., z>. | ph} (_ ((V X. V) X. V)
Theorem	eloprabg 4067	The law of concretion for operation class abstraction. Compare elopab 2888.
|- (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 4068	Inference of operation class abstraction subclass from implication.
|- (ph -> ps)   =>   |- {<.<.x, y>., z>. | ph} (_ {<.<.x, y>., z>. | ps}
Theorem	resoprab 4069	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 4070	"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 4071	"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 4072	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 4073	Functionality and domain of an operation class abstraction.
|- (ph -> E!zps)   =>   |- {<.<.x, y>., z>. | (ph /\ ps)} Fn {<.x, y>. | ph}
Theorem	ffnoprv 4074	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 4075	Closure law for an operation.
|- F:(R X. S)-->C   =>   |- ((A e. R /\ B e. S) -> (AFB) e. C)
Theorem	eqfnoprv 4076	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	fnoprv 4077	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	foprv 4078	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 4079	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 4080	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 4081	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 4082	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 4083	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 4084	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 4085	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 4086	The value of an operation class abstraction. A version of oprabval2g 4087 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 4087	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 4088	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 4089	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 4090	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, B>.F<.C, D>.) = S)
Theorem	oprabval4g 4091	Value of an operation given by an ordered-pair class abstraction. (This is the operation analog of fvopab2 3902.)
|- F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}   =>   |- ((x e. A /\ y e. B /\ C e. D) -> (xFy) = C)
Theorem	oprabval4gALT 4092	Value of an operation given by an ordered-pair class abstraction. (This is the operation analog of fvopab2 3902.)
|- F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}   =>   |- ((x e. A /\ y e. B /\ C e. D) -> (xFy) = C)
Theorem	oprabval6g 4093	The value of an operation class abstraction. Special case.
|- (<.x, y>. = <.A, B>. -> R = S)   &   |- F = {<.<.x, y>., z>. | (<.x, y>. e. C /\ z = R)}   =>   |- (((A e. G /\ B e. H /\ <.A, B>. e. C) /\ S e. J) -> (AFB) = S)
Theorem	oprvres 4094	The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|- ((A e. C /\ B e. D) -> (A(F |` (C X. D))B) = (AFB))
Theorem	oprssoprv 4095	The value of a member of the domain of a subclass of an operation.
|- (((Fun F /\ G Fn (C X. D) /\ G (_ F) /\ (A e. C /\ B e. D)) -> (AFB) = (AGB))
Theorem	foprrn 4096	A operations's value belongs to its codomain.
|- ((F:(R X. S)-->C /\ A e. R /\ B e. S) -> (AFB) e. C)
Theorem	fnrnoprv 4097	The range of an operation expressed as a collection of the operation's values.
|- (F Fn (A X. B) -> ran F = {z | E.x e. A E.y e. B z = (xFy)})
Theorem	fooprv 4098	An onto mapping of an operation expressed in terms of operation values.
|- (F:(A X. B)-onto->C <-> (F:(A X. B)-->C /\ A.z e. C E.x e. A E.y e. B z = (xFy)))
Theorem	fnoprvrn 4099	An operation's value belongs to its range.
|- ((F Fn (A X. B) /\ C e. A /\ D e. B) -> (CFD) e. ran F)
Theorem	oprvelrn 4100	A member of an operation's range is a value of the operation.
|- (F Fn (A X. B) -> (C e. ran F <-> E.x e. A E.y e. B (xFy) = C))