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 ↔ ∀y∃*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 ↔ ∀y ∈ ran A∃*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 ↔ ∀x∃*y xAy)
Theorem	fununi 2705	The union of a chain (with respect to inclusion) of functions is a function.
⊢ (∀f ∈ A (Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → Fun ∪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.)
⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → Fun ◡∪A)
Theorem	fun11uni 2707	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function.
⊢ (∀f ∈ A ((Fun f ∧ Fun ◡f) ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → (Fun ∪A ∧ Fun ◡∪A))
Theorem	funin 2708	The intersection with a function is a function. Exercise 14(a) of [Enderton] p. 53.
⊢ (Fun F → Fun (F ∩ 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 ∩ 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 ∈ C → (Fun A → (A “ B) ∈ 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 ∈ V    ⇒   ⊢ (Fun A → (A “ B) ∈ V)
Theorem	resfunexg 2717	The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28.
⊢ (B ∈ C → (Fun A → (A ↾ B) ∈ 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 ∈ F → ∀x y ∈ F)    &   ⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ (F Fn 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 ∈ dom F) → φ)    ⇒   ⊢ ((F Fn A ∧ B ∈ A) → φ)
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 ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ ((F Fn A ∧ BFC) → B ∈ A)
Theorem	fnop 2727	The first argument of an ordered pair in a function belongs to the function's domain.
⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ ((F Fn A ∧ ⟨B, C⟩ ∈ F) → B ∈ A)
Theorem	fneu 2728	There is exactly one value of a function.
⊢ ((F Fn A ∧ B ∈ A) → ∃!y BFy)
Theorem	fneu2 2729	There is exactly one value of a function.
⊢ ((F Fn A ∧ B ∈ A) → ∃!y⟨B, y⟩ ∈ F)
Theorem	fnun 2730	The union of two functions with disjoint domains.
⊢ (((F Fn A ∧ G Fn B) ∧ (A ∩ B) = ∅) → (F ∪ G) Fn (A ∪ 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 ∩ B) = ∅ ↔ (F ↾ B) = ∅))
Theorem	2elresin 2733	Membership in two functions restricted by each other's domain.
⊢ ((F Fn A ∧ G Fn B) → ((⟨x, y⟩ ∈ F ∧ ⟨x, z⟩ ∈ G) ↔ (⟨x, y⟩ ∈ (F ↾ (A ∩ B)) ∧ ⟨x, z⟩ ∈ (G ↾ (A ∩ 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 ∩ B)) Fn (A ∩ B))
Theorem	fnresin2 2736	Restriction of a function's domain with an intersection.
⊢ (F Fn A → (F ↾ (B ∩ A)) Fn (B ∩ 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 ∈ B → (F Fn A → F ∈ 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 ∈ B → (Fun F → F ∈ V))
Theorem	funopabex 2742	Existence of a function expressed as class of ordered pairs.
⊢ A ∈ V    &   ⊢ (x ∈ A → ∃*yφ)    ⇒   ⊢ {⟨x, y⟩∣(x ∈ A ∧ φ)} ∈ 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 ∈ B → (Fun F → ran F ∈ V))
Theorem	zfrep6 2744	A version of the Axiom of Replacement. Normally φ 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.
⊢ (∀x ∈ z ∃!yφ → ∃w∀x ∈ z ∃y ∈ w φ)
Theorem	fnopabg 2745	Functionality and domain of an ordered pair abstraction.
⊢ F = {⟨x, y⟩∣(x ∈ A ∧ φ)}    ⇒   ⊢ (∀x ∈ A ∃!yφ ↔ F Fn A)
Theorem	fnopab 2746	Functionality and domain of an ordered pair abstraction.
⊢ (x ∈ A → ∃!yφ)    &   ⊢ F = {⟨x, y⟩∣(x ∈ A ∧ φ)}    ⇒   ⊢ F Fn A
Theorem	fnopab2 2747	Functionality and domain of an ordered pair abstraction.
⊢ B ∈ V    &   ⊢ F = {⟨x, y⟩∣(x ∈ 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 ∈ F → ∀x y ∈ F)    &   ⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (F:A–→B → ∀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 ∘ G):A–→C)
Theorem	fssxp 2761	A mapping is a class of ordered pairs.
⊢ (F:A–→B → F ⊆ (A × B))
Theorem	opelf 2762	The members of an ordered pair element of a mapping belong to the mapping's domain and codomain.
⊢ D ∈ V    ⇒   ⊢ ((F:A–→B ∧ ⟨C, D⟩ ∈ F) → (C ∈ A ∧ D ∈ B))
Theorem	fun 2763	The union of two functions with disjoint domains.
⊢ (((F:A–→C ∧ G:B–→D) ∧ (A ∩ B) = ∅) → (F ∪ G):(A ∪ B)–→(C ∪ 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 ∘ (I ↾ A)) = F)
Theorem	fcoi2 2766	Composition of restricted identity and a mapping.
⊢ (F:A–→B → ((I ↾ B) ∘ F) = F)
Theorem	feu 2767	There is exactly one value of a function in its codomain.
⊢ ((F:A–→B ∧ C ∈ A) → ∃!y ∈ B ⟨C, y⟩ ∈ 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 ↔ ∀x ∈ B F:A–→x)
Theorem	fin 2770	Function into an intersection.
⊢ (F:A–→(B ∩ 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 ∈ C → (F:A–→B → F ∈ V))
Theorem	f0 2772	The empty function.
⊢ ∅:∅–→A
Theorem	f00 2773	A class is a function with empty codomain iff it and its domain are empty.
⊢ (F:A–→∅ ↔ (F = ∅ ∧ A = ∅))
Theorem	fconst 2774	A cross product with a singleton is a constant function.
⊢ B ∈ V    ⇒   ⊢ (A × {B}):A–→{B}
Theorem	fconstg 2775	A cross product with a singleton is a constant function.
⊢ (B ∈ C → (A × {B}):A–→{B})
Theorem	f1eq1 2776	Equality theorem for one-to-one functions.
⊢ (F = G → (F:A–1-1→B ↔ G:A–1-1→B))
Theorem	f1eq2 2777	Equality theorem for one-to-one functions.
⊢ (A = B → (F:A–1-1→C ↔ F:B–1-1→C))
Theorem	f1eq3 2778	Equality theorem for one-to-one functions.
⊢ (A = B → (F:C–1-1→A ↔ F:C–1-1→B))
Theorem	hbf1 2779	Bound-variable hypothesis builder for a one-to-one function.
⊢ (y ∈ F → ∀x y ∈ F)    &   ⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (F:A–1-1→B → ∀x F:A–1-1→B)
Theorem	f11 2780	Alternate definition of a one-to-one function.
⊢ (F:A–1-1→B ↔ (F:A–→B ∧ ∀y∃*x xFy))
Theorem	f1f 2781	A one-to-one mapping is a mapping.
⊢ (F:A–1-1→B → F:A–→B)
Theorem	f1cnv 2782	Two ways of expressing that a set A (not necessarily a function) is one-to-one. Each side is equivalent to Definition 6.4(3) of [TakeutiZaring] p. 24, who use the notation "Un2 (A)" for one-to-one. We do not introduce a separate notation since we do not use it very often.
⊢ (◡◡A:dom A–1-1→V ↔ (Fun ◡A ∧ Fun ◡◡A))
Theorem	f1co 2783	Composition of one-to-one functions. Exercise 30 of [TakeutiZaring] p. 25.
⊢ ((F:B–1-1→C ∧ G:A–1-1→B) → (F ∘ G):A–1-1→C)
Theorem	foeq1 2784	Equality theorem for onto functions.
⊢ (F = G → (F:A–onto→B ↔ G:A–onto→B))
Theorem	foeq2 2785	Equality theorem for onto functions.
⊢ (A = B → (F:A–onto→C ↔ F:B–onto→C))
Theorem	foeq3 2786	Equality theorem for onto functions.
⊢ (A = B → (F:C–onto→A ↔ F:C–onto→B))
Theorem	hbfo 2787	Bound-variable hypothesis builder for an onto function.
⊢ (y ∈ F → ∀x y ∈ F)    &   ⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (F:A–onto→B → ∀x F:A–onto→B)
Theorem	fof 2788	An onto mapping is a mapping.
⊢ (F:A–onto→B → F:A–→B)
Theorem	forn 2789	The codomain of an onto function is its range.
⊢ (F:A–onto→B → ran F = B)
Theorem	foima 2790	The image of the domain of an onto function.
⊢ (F:A–onto→B → (F “ A) = B)
Theorem	fnforn 2791	A function maps onto its range.
⊢ (F Fn A ↔ F:A–onto→ran F)
Theorem	funforn 2792	A function maps its domain onto its range.
⊢ (Fun A ↔ A:dom A–onto→ran A)
Theorem	fornex 2793	If the domain of an onto function exists, so does its codomain.
⊢ (A ∈ C → (F:A–onto→B → B ∈ V))
Theorem	fores 2794	Restriction of a function.
⊢ ((Fun F ∧ A ⊆ dom F) → (F ↾ A):A–onto→(F “ A))
Theorem	f1oeq1 2795	Equality theorem for one-to-one onto functions.
⊢ (F = G → (F:A–1-1-onto→B ↔ G:A–1-1-onto→B))
Theorem	f1oeq2 2796	Equality theorem for one-to-one onto functions.
⊢ (A = B → (F:A–1-1-onto→C ↔ F:B–1-1-onto→C))
Theorem	f1oeq3 2797	Equality theorem for one-to-one onto functions.
⊢ (A = B → (F:C–1-1-onto→A ↔ F:C–1-1-onto→B))
Theorem	hbf1o 2798	Bound-variable hypothesis builder for a one-to-one onto function.
⊢ (y ∈ F → ∀x y ∈ F)    &   ⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (F:A–1-1-onto→B → ∀x F:A–1-1-onto→B)
Theorem	f1of1 2799	A one-to-one onto mapping is a one-to-one mapping.
⊢ (F:A–1-1-onto→B → F:A–1-1→B)
Theorem	f1of 2800	A one-to-one onto mapping is a mapping.
⊢ (F:A–1-1-onto→B → F:A–→B)