mmtheorems46 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 4501-4600 - Page 46 of 175

Type	Label	Description
Statement
Theorem	cofunexg 4501	Existence of a composition when the first member is a function.
|- ((Fun A /\ B e. C) -> (A o. B) e. _V)
Theorem	cofunex2g 4502	Existence of a composition when the second member is one-to-one.
|- ((A e. C /\ Fun `'B) -> (A o. B) e. _V)
Theorem	fneq1 4503	Equality theorem for function predicate with domain.
|- (F = G -> (F Fn A <-> G Fn A))
Theorem	fneq2 4504	Equality theorem for function predicate with domain.
|- (A = B -> (F Fn A <-> F Fn B))
Theorem	fneq1d 4505	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
|- (ph -> F = G)   =>   |- (ph -> (F Fn A <-> G Fn A))
Theorem	fneq2d 4506	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
|- (ph -> A = B)   =>   |- (ph -> (F Fn A <-> F Fn B))
Theorem	fneq1i 4507	Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
|- F = G   =>   |- (F Fn A <-> G Fn A)
Theorem	fneq2i 4508	Equality inference for function predicate with domain.
|- A = B   =>   |- (F Fn A <-> F Fn B)
Theorem	hbfn 4509	Bound-variable hypothesis builder for a function with domain.
|- (y e. F -> A.x y e. F)   &   |- (y e. A -> A.x y e. A)   =>   |- (F Fn A -> A.x F Fn A)
Theorem	fnfun 4510	A function with domain is a function.
|- (F Fn A -> Fun F)
Theorem	fnrel 4511	A function with domain is a relation.
|- (F Fn A -> Rel F)
Theorem	fndm 4512	The domain of a function.
|- (F Fn A -> dom F = A)
Theorem	funfni 4513	Inference to convert a function and domain antecedent.
|- ((Fun F /\ B e. dom F) -> ph)   =>   |- ((F Fn A /\ B e. A) -> ph)
Theorem	fndmu 4514	A function has a unique domain.
|- ((F Fn A /\ F Fn B) -> A = B)
Theorem	fnbr 4515	The first argument of binary relation on a function belongs to the function's domain.
|- ((F Fn A /\ BFC) -> B e. A)
Theorem	fnop 4516	The first argument of an ordered pair in a function belongs to the function's domain.
|- ((F Fn A /\ <.B, C>. e. F) -> B e. A)
Theorem	fneu 4517	There is exactly one value of a function. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- ((F Fn A /\ B e. A) -> E!y BFy)
Theorem	fneuOLD 4518	There is exactly one value of a function.
|- ((F Fn A /\ B e. A) -> E!y BFy)
Theorem	fneu2 4519	There is exactly one value of a function.
|- ((F Fn A /\ B e. A) -> E!y<.B, y>. e. F)
Theorem	fnun 4520	The union of two functions with disjoint domains.
|- (((F Fn A /\ G Fn B) /\ (A i^i B) = (/)) -> (F u. G) Fn (A u. B))
Theorem	fnco 4521	Composition of two functions.
|- ((F Fn A /\ G Fn B /\ ran G C_ A) -> (F o. G) Fn B)
Theorem	fnresdm 4522	A function does not change when restricted to its domain.
|- (F Fn A -> (F |` A) = F)
Theorem	fnresdisj 4523	A function restricted to a class disjoint with its domain is empty.
|- (F Fn A -> ((A i^i B) = (/) <-> (F |` B) = (/)))
Theorem	2elresin 4524	Membership in two functions restricted by each other's domain.
|- ((F Fn A /\ G Fn B) -> ((<.x, y>. e. F /\ <.x, z>. e. G) <-> (<.x, y>. e. (F |` (A i^i B)) /\ <.x, z>. e. (G |` (A i^i B)))))
Theorem	fnssresb 4525	Restriction of a function with a subclass of its domain.
|- (F Fn A -> ((F |` B) Fn B <-> B C_ A))
Theorem	fnssres 4526	Restriction of a function with a subclass of its domain.
|- ((F Fn A /\ B C_ A) -> (F |` B) Fn B)
Theorem	fnresin1 4527	Restriction of a function's domain with an intersection.
|- (F Fn A -> (F |` (A i^i B)) Fn (A i^i B))
Theorem	fnresin2 4528	Restriction of a function's domain with an intersection.
|- (F Fn A -> (F |` (B i^i A)) Fn (B i^i A))
Theorem	fnresi 4529	Functionality and domain of restricted identity.
|- ( _I |` A) Fn A
Theorem	fnima 4530	The image of a function's domain is its range. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- (F Fn A -> (F"A) = ran F)
Theorem	fnimaOLD 4531	The image of a function's domain is its range.
|- (F Fn A -> (F"A) = ran F)
Theorem	fn0 4532	A function with empty domain is empty. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- (F Fn (/) <-> F = (/))
Theorem	fn0OLD 4533	A function with empty domain is empty.
|- (F Fn (/) <-> F = (/))
Theorem	funimadisj 4534	A class that is disjoint with the domain of a function has an empty image under the function. (Contributed by FL, 24-Jan-2007.)
|- ((F Fn A /\ (A i^i C) = (/)) -> (F"C) = (/))
Theorem	fnex 4535	If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg 4500. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- ((F Fn A /\ A e. B) -> F e. _V)
Theorem	fnexALT 4536	If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of funimaexg 4495.
|- ((F Fn A /\ A e. B) -> F e. _V)
Theorem	funex 4537	If the domain of a function exists, so the function. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of fnex 4535. (Note: Any resemblance between F.U.N.E.X. and "Have You Any Eggs" is purely a coincidence originated by Swedish chefs.)
|- ((Fun F /\ dom F e. B) -> F e. _V)
Theorem	opabex 4538	Existence of a function expressed as class of ordered pairs.
|- A e. _V   &   |- (x e. A -> E*yph)   =>   |- {<.x, y>. | (x e. A /\ ph)} e. _V
Theorem	opabex2 4539	Existence of a function expressed as class of ordered pairs.
|- A e. _V   =>   |- {<.x, y>. | (x e. A /\ y = B)} e. _V
Theorem	opabex2g 4540	Existence of a function expressed as class of ordered pairs.
|- (A e. C -> {<.x, y>. | (x e. A /\ y = B)} e. _V)
Theorem	fopabex2 4541	Existence of a function expressed as class of ordered pairs.
|- A e. _V   &   |- F = {<.x, y>. | (x e. A /\ y = B)}   =>   |- F e. _V
Theorem	iunfopab 4542	Two ways to express a function as a class of ordered pairs. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Sep-2011.)
|- B e. _V   =>   |- U_x e. A {<.x, B>.} = {<.x, y>. | (x e. A /\ y = B)}
Theorem	iunfopabOLD 4543	Two ways to express a function as a class of ordered pairs.
|- B e. _V   =>   |- U_x e. A {<.x, B>.} = {<.x, y>. | (x e. A /\ y = B)}
Theorem	funrnex 4544	If the domain of a function exists, so does its range. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of funex 4537.
|- (dom F e. B -> (Fun F -> ran F e. _V))
Theorem	zfrep6 4545	A version of the Axiom of Replacement. Normally ph would have free variables x and y. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 3438 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep 3428.
|- (A.x e. z E!yph -> E.wA.x e. z E.y e. w ph)
Theorem	fnopabg 4546	Functionality and domain of an ordered-pair class abstraction.
|- F = {<.x, y>. | (x e. A /\ ph)}   =>   |- (A.x e. A E!yph <-> F Fn A)
Theorem	fnopab2g 4547	Functionality and domain of an ordered-pair class abstraction.
|- F = {<.x, y>. | (x e. A /\ y = B)}   =>   |- (A.x e. A B e. _V <-> F Fn A)
Theorem	fnopab 4548	Functionality and domain of an ordered-pair class abstraction.
|- (x e. A -> E!yph)   &   |- F = {<.x, y>. | (x e. A /\ ph)}   =>   |- F Fn A
Theorem	fnopab2 4549	Functionality and domain of an ordered-pair class abstraction.
|- B e. _V   &   |- F = {<.x, y>. | (x e. A /\ y = B)}   =>   |- F Fn A
Theorem	dmopab2 4550	Domain of an ordered-pair class abstraction that specifies a function.
|- B e. _V   &   |- F = {<.x, y>. | (x e. A /\ y = B)}   =>   |- dom F = A
Theorem	feq1 4551	Equality theorem for functions.
|- (F = G -> (F:A-->B <-> G:A-->B))
Theorem	feq2 4552	Equality theorem for functions.
|- (A = B -> (F:A-->C <-> F:B-->C))
Theorem	feq3 4553	Equality theorem for functions.
|- (A = B -> (F:C-->A <-> F:C-->B))
Theorem	feq23 4554	Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- ((A = C /\ B = D) -> (F:A-->B <-> F:C-->D))
Theorem	feq23OLD 4555	Equality theorem for functions. (Contributed by FL, 14-Jul-2007.)
|- ((A = C /\ B = D) -> (F:A-->B <-> F:C-->D))
Theorem	feq1d 4556	Equality deduction for functions.
|- (ph -> F = G)   =>   |- (ph -> (F:A-->B <-> G:A-->B))
Theorem	feq2d 4557	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- (ph -> A = B)   =>   |- (ph -> (F:A-->C <-> F:B-->C))
Theorem	feq1i 4558	Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- F = G   =>   |- (F:A-->B <-> G:A-->B)
Theorem	feq2i 4559	Equality inference for functions.
|- A = B   =>   |- (F:A-->C <-> F:B-->C)
Theorem	hbf 4560	Bound-variable hypothesis builder for a mapping.
|- (y e. F -> A.x y e. F)   &   |- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (F:A-->B -> A.x F:A-->B)
Theorem	elimf 4561	Eliminate a mapping hypothesis for the weak deduction theorem dedth 3011, when a special case G:A-->B is provable, in order to convert F:A-->B from a hypothesis to an antecedent.
|- G:A-->B   =>   |- if(F:A-->B, F, G):A-->B
Theorem	ffn 4562	A mapping is a function.
|- (F:A-->B -> F Fn A)
Theorem	dffn2 4563	Any function is a mapping into _V. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- (F Fn A <-> F:A-->_V)
Theorem	dffn2OLD 4564	Any function is a mapping into _V.
|- (F Fn A <-> F:A-->_V)
Theorem	ffun 4565	A mapping is a function.
|- (F:A-->B -> Fun F)
Theorem	frel 4566	A mapping is a relation.
|- (F:A-->B -> Rel F)
Theorem	fdm 4567	The domain of a mapping.
|- (F:A-->B -> dom F = A)
Theorem	fdmi 4568	The domain of a mapping.
|- F:A-->B   =>   |- dom F = A
Theorem	frn 4569	The range of a mapping.
|- (F:A-->B -> ran F C_ B)
Theorem	dffn3 4570	A function maps to its range.
|- (F Fn A <-> F:A-->ran F)
Theorem	fss 4571	Expanding the codomain of a mapping. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- ((F:A-->B /\ B C_ C) -> F:A-->C)
Theorem	fssOLD 4572	Expanding the codomain of a mapping.
|- ((F:A-->B /\ B C_ C) -> F:A-->C)
Theorem	fco 4573	Composition of two mappings. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- ((F:B-->C /\ G:A-->B) -> (F o. G):A-->C)
Theorem	fcoOLD 4574	Composition of two mappings.
|- ((F:B-->C /\ G:A-->B) -> (F o. G):A-->C)
Theorem	fssxp 4575	A mapping is a class of ordered pairs. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- (F:A-->B -> F C_ (A X. B))
Theorem	fssxpOLD 4576	A mapping is a class of ordered pairs.
|- (F:A-->B -> F C_ (A X. B))
Theorem	funssxp 4577	Two ways of specifying a partial function from A to B.
|- ((Fun F /\ F C_ (A X. B)) <-> (F:dom F-->B /\ dom F C_ A))
Theorem	ffdm 4578	A mapping is a partial function.
|- (F:A-->B -> (F:dom F-->B /\ dom F C_ A))
Theorem	opelf 4579	The members of an ordered pair element of a mapping belong to the mapping's domain and codomain.
|- D e. _V   =>   |- ((F:A-->B /\ <.C, D>. e. F) -> (C e. A /\ D e. B))
Theorem	fun 4580	The union of two functions with disjoint domains.
|- (((F:A-->C /\ G:B-->D) /\ (A i^i B) = (/)) -> (F u. G):(A u. B)-->(C u. D))
Theorem	fnfco 4581	Composition of two functions.
|- ((F Fn A /\ G:B-->A) -> (F o. G) Fn B)
Theorem	fssres 4582	Restriction of a function with a subclass of its domain.
|- ((F:A-->B /\ C C_ A) -> (F |` C):C-->B)
Theorem	fssres2 4583	Restriction of a restricted function with a subclass of its domain.
|- (((F |` A):A-->B /\ C C_ A) -> (F |` C):C-->B)
Theorem	fcoi1 4584	Composition of a mapping and restricted identity. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- (F:A-->B -> (F o. ( _I |` A)) = F)
Theorem	fcoi1OLD 4585	Composition of a mapping and restricted identity.
|- (F:A-->B -> (F o. ( _I |` A)) = F)
Theorem	fcoi2 4586	Composition of restricted identity and a mapping. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- (F:A-->B -> (( _I |` B) o. F) = F)
Theorem	fcoi2OLD 4587	Composition of restricted identity and a mapping.
|- (F:A-->B -> (( _I |` B) o. F) = F)
Theorem	feu 4588	There is exactly one value of a function in its codomain.
|- ((F:A-->B /\ C e. A) -> E!y e. B <.C, y>. e. F)
Theorem	fcnvres 4589	The converse of a restriction of a function.
|- (F:A-->B -> `'(F |` A) = (`'F |` B))
Theorem	fimacnvdisj 4590	The pre-image of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007.)
|- ((F:A-->B /\ (B i^i C) = (/)) -> (`'F"C) = (/))
Theorem	fint 4591	Function into an intersection. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- B =/= (/)   =>   |- (F:A-->|^|B <-> A.x e. B F:A-->x)
Theorem	fintOLD 4592	Function into an intersection.
|- B =/= (/)   =>   |- (F:A-->|^|B <-> A.x e. B F:A-->x)
Theorem	fin 4593	Mapping into an intersection. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- (F:A-->(B i^i C) <-> (F:A-->B /\ F:A-->C))
Theorem	finOLD 4594	Mapping into an intersection.
|- (F:A-->(B i^i C) <-> (F:A-->B /\ F:A-->C))
Theorem	fex 4595	If the domain of a mapping is a set, the function is a set.
|- ((F:A-->B /\ A e. C) -> F e. _V)
Theorem	fabexg 4596	Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.)
|- F = {x | (x:A-->B /\ ph)}   =>   |- ((A e. C /\ B e. D) -> F e. _V)
Theorem	fabex 4597	Existence of a set of functions.
|- A e. _V   &   |- B e. _V   &   |- F = {x | (x:A-->B /\ ph)}   =>   |- F e. _V
Theorem	dmfex 4598	If a mapping is a set, its domain is a set. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- ((F e. C /\ F:A-->B) -> A e. _V)
Theorem	dmfexOLD 4599	If a mapping is a set, its domain is a set.
|- ((F e. C /\ F:A-->B) -> A e. _V)
Theorem	f0 4600	The empty function.
|- (/):(/)-->A