Metamath Proof Explorer - mmtheorems28

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 - 2701-2800 - Page 28 of 58

Type	Label	Description
Statement
Theorem	funcnvcnv 2701	The double converse of a function is a function.
|- (Fun A -> Fun `'`'A)
Theorem	funcnv2 2702	A simpler equivalence for single-rooted (see funcnv 2703).
|- (Fun `'A <-> A.yE*x xAy)
Theorem	funcnv 2703	The converse of a class is a function iff the class is single-rooted, which means that for any y in the range of A there is at most one x such that xAy. Definition of single-rooted in [Enderton] p. 43. See funcnv2 2702 for a simpler version.
|- (Fun `'A <-> A.y e. ran AE*x xAy)
Theorem	fun2cnv 2704	The double converse of a class is a function iff the class is single-valued. Each side is equivalent to Definition 6.4(2) of [TakeutiZaring] p. 23, who use the notation "Un(A)" for single-valued. Note that A is not necessarily a function.
|- (Fun `'`'A <-> A.xE*y xAy)
Theorem	fununi 2705	The union of a chain (with respect to inclusion) of functions is a function.
|- (A.f e. A (Fun f /\ A.g e. A (f (_ g \/ g (_ f)) -> Fun U.A)
Theorem	funcnvuni 2706	The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 2703 for "single-rooted" definition.)
|- (A.f e. A (Fun `'f /\ A.g e. A (f (_ g \/ g (_ f)) -> Fun `'U.A)
Theorem	fun11uni 2707	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function.
|- (A.f e. A ((Fun f /\ Fun `'f) /\ A.g e. A (f (_ g \/ g (_ f)) -> (Fun U.A /\ Fun `'U.A))
Theorem	funin 2708	The intersection with a function is a function. Exercise 14(a) of [Enderton] p. 53.
|- (Fun F -> Fun (F i^i G))
Theorem	funres11 2709	The restriction of a one-to-one function is one-to-one.
|- (Fun `'F -> Fun `'(F |` A))
Theorem	funcnvres 2710	The converse of a restricted function.
|- (Fun `'F -> `'(F |` A) = (`'F |` (F"A)))
Theorem	funimacnv 2711	The image of the converse image of a function.
|- (Fun F -> (F"(`'F"A)) = (A i^i ran F))
Theorem	funimass1 2712	A kind of contraposition law that infers a subclass of an image from a converse image subclass.
|- ((Fun F /\ A (_ ran F) -> ((`'F"A) (_ B -> A (_ (F"B)))
Theorem	funimass2 2713	A kind of contraposition law that infers an image subclass from a subclass of a converse image.
|- (Fun F -> (A (_ (`'F"B) -> (F"A) (_ B))
Theorem	imadif 2714	The image of a difference is the difference of images.
|- (Fun `'F -> (F"(A \ B)) = ((F"A) \ (F"B)))
Theorem	funimaexg 2715	Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29.
|- (B e. C -> (Fun A -> (A"B) e. V))
Theorem	funimaex 2716	The image of a set under any function is also a set. Equivalent of Axiom of Replacement ax-rep 1075. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29.
|- B e. V   =>   |- (Fun A -> (A"B) e. V)
Theorem	resfunexg 2717	The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28.
|- (B e. C -> (Fun A -> (A |` B) e. V))
Theorem	fneq1 2718	Equality theorem for function predicate with domain.
|- (F = G -> (F Fn A <-> G Fn A))
Theorem	fneq2 2719	Equality theorem for function predicate with domain.
|- (A = B -> (F Fn A <-> F Fn B))
Theorem	hbfn 2720	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 2721	A function with domain is a function.
|- (F Fn A -> Fun F)
Theorem	fnrel 2722	A function with domain is a relation.
|- (F Fn A -> Rel F)
Theorem	fndm 2723	The domain of a function.
|- (F Fn A -> dom F = A)
Theorem	funfni 2724	Inference to convert a function and domain antecedent.
|- ((Fun F /\ B e. dom F) -> ph)   =>   |- ((F Fn A /\ B e. A) -> ph)
Theorem	fndmu 2725	A function has a unique domain.
|- ((F Fn A /\ F Fn B) -> A = B)
Theorem	fnbr 2726	The first argument of binary relation on a function belongs to the function's domain.
|- B e. V   &   |- C e. V   =>   |- ((F Fn A /\ BFC) -> B e. A)
Theorem	fnop 2727	The first argument of an ordered pair in a function belongs to the function's domain.
|- B e. V   &   |- C e. V   =>   |- ((F Fn A /\ <.B, C>. e. F) -> B e. A)
Theorem	fneu 2728	There is exactly one value of a function.
|- ((F Fn A /\ B e. A) -> E!y BFy)
Theorem	fneu2 2729	There is exactly one value of a function.
|- ((F Fn A /\ B e. A) -> E!y<.B, y>. e. F)
Theorem	fnun 2730	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	fnresdm 2731	A function does not change when restricted to its domain.
|- (F Fn A -> (F |` A) = F)
Theorem	fnresdisj 2732	A function restricted to a class disjoint with its domain is empty.
|- (F Fn A -> ((A i^i B) = (/) <-> (F |` B) = (/)))
Theorem	2elresin 2733	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	fnssres 2734	Restriction of a function with a subclass of its domain.
|- ((F Fn A /\ B (_ A) -> (F |` B) Fn B)
Theorem	fnresin1 2735	Restriction of a function's domain with an intersection.
|- (F Fn A -> (F |` (A i^i B)) Fn (A i^i B))
Theorem	fnresin2 2736	Restriction of a function's domain with an intersection.
|- (F Fn A -> (F |` (B i^i A)) Fn (B i^i A))
Theorem	fnresi 2737	Functionality and domain of restricted identity.
|- (I |` A) Fn A
Theorem	fnima 2738	The image of a function's domain is its range.
|- (F Fn A -> (F"A) = ran F)
Theorem	fn0 2739	A function with empty domain is empty.
|- (F Fn (/) <-> F = (/))
Theorem	fnex 2740	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 2715.
|- (A e. B -> (F Fn A -> F e. V))
Theorem	funex 2741	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 2740. (Note: Any resemblance between F.U.N.E.X. and "Have You Any Eggs" is purely a coincidence originated by Swedish chefs.)
|- (dom F e. B -> (Fun F -> F e. V))
Theorem	funopabex 2742	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	funrnex 2743	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 2741.
|- (dom F e. B -> (Fun F -> ran F e. V))
Theorem	zfrep6 2744	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 zfaus 1480 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 1075.
|- (A.x e. z E!yph -> E.wA.x e. z E.y e. w ph)
Theorem	fnopabg 2745	Functionality and domain of an ordered pair abstraction.
|- F = {<.x, y>. | (x e. A /\ ph)}   =>   |- (A.x e. A E!yph <-> F Fn A)
Theorem	fnopab 2746	Functionality and domain of an ordered pair abstraction.
|- (x e. A -> E!yph)   &   |- F = {<.x, y>. | (x e. A /\ ph)}   =>   |- F Fn A
Theorem	fnopab2 2747	Functionality and domain of an ordered pair abstraction.
|- B e. V   &   |- F = {<.x, y>. | (x e. A /\ y = B)}   =>   |- F Fn A
Theorem	feq1 2748	Equality theorem for functions.
|- (F = G -> (F:A-->B <-> G:A-->B))
Theorem	feq2 2749	Equality theorem for functions.
|- (A = B -> (F:A-->C <-> F:B-->C))
Theorem	feq3 2750	Equality theorem for functions.
|- (A = B -> (F:C-->A <-> F:C-->B))
Theorem	hbf 2751	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	ffn 2752	A mapping is a function.
|- (F:A-->B -> F Fn A)
Theorem	fnf 2753	Any function is a mapping into V.
|- (F Fn A <-> F:A-->V)
Theorem	ffun 2754	A mapping is a function.
|- (F:A-->B -> Fun F)
Theorem	frel 2755	A mapping is a relation.
|- (F:A-->B -> Rel F)
Theorem	fdm 2756	The domain of a mapping.
|- (F:A-->B -> dom F = A)
Theorem	frn 2757	The range of a mapping.
|- (F:A-->B -> ran F (_ B)
Theorem	fnfrn 2758	A function maps to its range.
|- (F Fn A <-> F:A-->ran F)
Theorem	fss 2759	Expanding the co-domain of a mapping.
|- ((F:A-->B /\ B (_ C) -> F:A-->C)
Theorem	fco 2760	Composition of two mappings.
|- ((F:B-->C /\ G:A-->B) -> (F o. G):A-->C)
Theorem	fssxp 2761	A mapping is a class of ordered pairs.
|- (F:A-->B -> F (_ (A X. B))
Theorem	opelf 2762	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 2763	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	fssres 2764	Restriction of a function with a subclass of its domain.
|- ((F:A-->B /\ C (_ A) -> (F |` C):C-->B)
Theorem	fcoi1 2765	Composition of a mapping and restricted identity.
|- (F:A-->B -> (F o. (I |` A)) = F)
Theorem	fcoi2 2766	Composition of restricted identity and a mapping.
|- (F:A-->B -> ((I |` B) o. F) = F)
Theorem	feu 2767	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 2768	The converse of a restriction of a function.
|- (F:A-->B -> `'(F |` A) = (`'F |` B))
Theorem	fint 2769	Function into an intersection.
|- -. B = (/)   =>   |- (F:A-->|^|B <-> A.x e. B F:A-->x)
Theorem	fin 2770	Function into an intersection.
|- (F:A-->(B i^i C) <-> (F:A-->B /\ F:A-->C))
Theorem	fex 2771	If the domain of a function is a set, the function is a set.
|- (A e. C -> (F:A-->B -> F e. V))
Theorem	f0