Metamath Proof Explorer - mmtheorems29

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 - 2801-2900 - Page 29 of 58

Type	Label	Description
Statement
Theorem	f1ofn 2801	A one-to-one onto mapping is function on its domain.
⊢ (F:A–1-1-onto→B → F Fn A)
Theorem	f1ofun 2802	A one-to-one onto mapping is a function.
⊢ (F:A–1-1-onto→B → Fun F)
Theorem	f1orel 2803	A one-to-one onto mapping is a relation.
⊢ (F:A–1-1-onto→B → Rel F)
Theorem	f1o2 2804	Alternate definition of one-to-one onto function.
⊢ (F:A–1-1-onto→B ↔ (F Fn A ∧ Fun ◡F ∧ ran F = B))
Theorem	f1o3 2805	Alternate definition of one-to-one onto function.
⊢ (F:A–1-1-onto→B ↔ (F:A–onto→B ∧ Fun ◡F))
Theorem	f1ofo 2806	A one-to-one onto function is an onto function.
⊢ (F:A–1-1-onto→B → F:A–onto→B)
Theorem	f1o4 2807	Alternate definition of one-to-one onto function.
⊢ (F:A–1-1-onto→B ↔ (F Fn A ∧ ◡F Fn B))
Theorem	f1o5 2808	Alternate definition of one-to-one onto function.
⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ ran F = B))
Theorem	f1orn 2809	A one-to-one function maps onto its range.
⊢ (F:A–1-1-onto→ran F ↔ (F Fn A ∧ Fun ◡F))
Theorem	f1f1orn 2810	A one-to-one function maps one-to-one onto its range.
⊢ (F:A–1-1→B → F:A–1-1-onto→ran F)
Theorem	f1ocnv 2811	The converse of a one-to-one onto function is also one-to-one onto.
⊢ (F:A–1-1-onto→B → ◡F:B–1-1-onto→A)
Theorem	f1ocnvb 2812	A relation is a one-to-one onto function iff its converse is a one-to-one onto function with domain and range interchanged.
⊢ (Rel F → (F:A–1-1-onto→B ↔ ◡F:B–1-1-onto→A))
Theorem	f1ores 2813	The restriction of a one-to-one function maps one-to-one onto the image.
⊢ ((F:A–1-1→B ∧ C ⊆ A) → (F ↾ C):C–1-1-onto→(F “ C))
Theorem	f1imacnv 2814	Converse image of an image.
⊢ ((F:A–1-1→B ∧ C ⊆ A) → (◡F “ (F “ C)) = C)
Theorem	f1oun 2815	The union of two one-to-one onto functions with disjoint domains and ranges.
⊢ (((F:A–1-1-onto→B ∧ G:C–1-1-onto→D) ∧ ((A ∩ C) = ∅ ∧ (B ∩ D) = ∅)) → (F ∪ G):(A ∪ C)–1-1-onto→(B ∪ D))
Theorem	f1oco 2816	Composition of one-to-one onto functions.
⊢ ((F:B–1-1-onto→C ∧ G:A–1-1-onto→B) → (F ∘ G):A–1-1-onto→C)
Theorem	f1ococnv2 2817	The composition of a one-to-one onto function and its converse equals the identity relation restricted to the function's range.
⊢ (F:A–1-1-onto→B → (F ∘ ◡F) = (I ↾ B))
Theorem	f1ococnv1 2818	The composition of a one-to-one onto function's converse and itself equals the identity relation restricted to the function's domain.
⊢ (F:A–1-1-onto→B → (◡F ∘ F) = (I ↾ A))
Theorem	f1dmex 2819	If the codomain of a one-to-one function exists, so does its domain. This theorem is equivalent to the Axiom of Replacement ax-rep 1075.
⊢ (B ∈ C → (F:A–1-1→B → A ∈ V))
Theorem	ffoss 2820	Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145.
⊢ F ∈ V    ⇒   ⊢ (F:A–→B ↔ ∃x(F:A–onto→x ∧ x ⊆ B))
Theorem	f11o 2821	Relationship between one-to-one and one-to-one onto function.
⊢ F ∈ V    ⇒   ⊢ (F:A–1-1→B ↔ ∃x(F:A–1-1-onto→x ∧ x ⊆ B))
Theorem	f10 2822	The empty set maps one-to-one into any class.
⊢ ∅:∅–1-1→A
Theorem	f1o00 2823	One-to-one onto mapping of the empty set.
⊢ (F:∅–1-1-onto→A ↔ (F = ∅ ∧ A = ∅))
Theorem	f1o0 2824	One-to-one onto mapping of the empty set.
⊢ ∅:∅–1-1-onto→∅
Theorem	f1oi 2825	A restriction of the identity relation is a one-to-one onto function.
⊢ (I ↾ A):A–1-1-onto→A
Theorem	f1ovi 2826	The identity relation is a one-to-one onto function on the universe.
⊢ I:V–1-1-onto→V
Theorem	f1osn 2827	A singleton of an ordered pair is one-to-one onto function.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ {⟨A, B⟩}:{A}–1-1-onto→{B}
Theorem	fv2 2828	Alternate definition of function value. Definition 10.11 of [Quine] p. 68.
⊢ A ∈ V    ⇒   ⊢ (F ‘A) = ∪{x∣∀y(AFy ↔ y = x)}
Theorem	fvprc 2829	A function's value at a proper class is the empty set.
⊢ (¬ A ∈ V → (F ‘A) = ∅)
Theorem	elfv 2830	Membership in a function value.
⊢ B ∈ V    ⇒   ⊢ (A ∈ (F ‘B) ↔ ∃x(A ∈ x ∧ ∀y(BFy ↔ y = x)))
Theorem	fveq1 2831	Equality theorem for function value.
⊢ (F = G → (F ‘A) = (G ‘A))
Theorem	fveq2 2832	Equality theorem for function value.
⊢ (A = B → (F ‘A) = (F ‘B))
Theorem	fveq1i 2833	Equality inference for function value.
⊢ F = G    ⇒   ⊢ (F ‘A) = (G ‘A)
Theorem	fveq1d 2834	Equality deduction for function value.
⊢ (φ → F = G)    ⇒   ⊢ (φ → (F ‘A) = (G ‘A))
Theorem	fveq2i 2835	Equality inference for function value.
⊢ A = B    ⇒   ⊢ (F ‘A) = (F ‘B)
Theorem	fveq2d 2836	Equality deduction for function value.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (F ‘A) = (F ‘B))
Theorem	hbfv 2837	Bound-variable hypothesis builder for function value.
⊢ (y ∈ F → ∀x y ∈ F)    &   ⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ (y ∈ (F ‘A) → ∀x y ∈ (F ‘A))
Theorem	fvex 2838	The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27.
⊢ (F ‘A) ∈ V
Theorem	fv3 2839	Alternate definition of the value of a function. Definition 6.11 of [TakeutiZaring] p. 26.
⊢ A ∈ V    ⇒   ⊢ (F ‘A) = {x∣(∃y(x ∈ y ∧ AFy) ∧ ∃!y AFy)}
Theorem	fvres 2840	The value of a restricted function.
⊢ (A ∈ B → ((F ↾ B) ‘A) = (F ‘A))
Theorem	funssfv 2841	The value of a member of the domain of a subclass of a function.
⊢ (((Fun F ∧ G ⊆ F) ∧ A ∈ dom G) → (F ‘A) = (G ‘A))
Theorem	tz6.12-1 2842	Theorem 6.12(1) of [TakeutiZaring] p. 27.
⊢ A ∈ V    ⇒   ⊢ ((AFy ∧ ∃!y AFy) → (F ‘A) = y)
Theorem	tz6.12 2843	Theorem 6.12(1) of [TakeutiZaring] p. 27.
⊢ A ∈ V    ⇒   ⊢ ((⟨A, y⟩ ∈ F ∧ ∃!y⟨A, y⟩ ∈ F) → (F ‘A) = y)
Theorem	tz6.12f 2844	Function value requiring only that y not be 'free' in F (but not necessarily absent from it).
⊢ (w ∈ F → ∀y w ∈ F)    ⇒   ⊢ ((⟨x, y⟩ ∈ F ∧ ∃!y⟨x, y⟩ ∈ F) → (F ‘x) = y)
Theorem	tz6.12-2 2845	Theorem 6.12(2) of [TakeutiZaring] p. 27.
⊢ (¬ ∃!y AFy → (F ‘A) = ∅)
Theorem	tz6.12c 2846	Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27.
⊢ A ∈ V    ⇒   ⊢ (∃!y AFy → ((F ‘A) = y ↔ AFy))
Theorem	tz6.12i 2847	Corollary of Theorem 6.12(2) of [TakeutiZaring] p. 27.
⊢ A ∈ V    ⇒   ⊢ (¬ B = ∅ → ((F ‘A) = B → AFB))
Theorem	ndmfv 2848	The value of a class outside its domain is the empty set.
⊢ (¬ A ∈ dom F → (F ‘A) = ∅)
Theorem	ndmfvrcl 2849	Reverse closure law for function with the empty set not in its domain.
⊢ dom F = S    &   ⊢ ¬ ∅ ∈ S    ⇒   ⊢ ((F ‘A) ∈ S → A ∈ S)
Theorem	nfvres 2850	A non-element of a restriction has empty value.
⊢ (¬ A ∈ B → ((F ↾ B) ‘A) = ∅)
Theorem	fveqres 2851	Equal values imply equal values in a restriction.
⊢ ((F ‘A) = (G ‘A) → ((F ↾ B) ‘A) = ((G ↾ B) ‘A))
Theorem	funbrfv 2852	The second argument of a binary relation on a function is the function's value.
⊢ B ∈ V    ⇒   ⊢ (Fun F → (AFB → (F ‘A) = B))
Theorem	funfvopi 2853	The second element in an ordered pair member of a function is the function's value.
⊢ B ∈ V    ⇒   ⊢ (Fun F → (⟨A, B⟩ ∈ F → (F ‘A) = B))
Theorem	funopfvg 2854	The second element in an ordered pair member of a function is the function's value.
⊢ ((B ∈ C ∧ Fun F) → (⟨A, B⟩ ∈ F → (F ‘A) = B))
Theorem	fnfvbr 2855	Equivalence of function value and binary relation.
⊢ C ∈ V    ⇒   ⊢ ((F Fn A ∧ B ∈ A) → ((F ‘B) = C ↔ BFC))
Theorem	fnfvop 2856	Equivalence of function value and ordered pair membership.
⊢ C ∈ V    ⇒   ⊢ ((F Fn A ∧ B ∈ A) → ((F ‘B) = C ↔ ⟨B, C⟩ ∈ F))
Theorem	funfvop 2857	Equivalence of function value and ordered pair membership. Theorem 4.3(ii) of [Monk1] p. 42.
⊢ B ∈ V    ⇒   ⊢ ((Fun F ∧ A ∈ dom F) → ((F ‘A) = B ↔ ⟨A, B⟩ ∈ F))
Theorem	fnopabfv 2858	Representation of a function in terms of its values.
⊢ (F Fn A ↔ F = {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))})
Theorem	fvelima 2859	Function value in an image. Part of Theorem 4.4(iii) of [Monk1] p. 42.
⊢ ((Fun F ∧ A ∈ (F “ B)) → ∃x ∈ B (F ‘x) = A)
Theorem	fniunfv 2860	The indexed union of a function's values is the union of its range.
⊢ (F Fn A → ∪x ∈ A (F ‘x) = ∪ran F)
Theorem	fnsnfv 2861	Singleton of function value.
⊢ ((F Fn A ∧ B ∈ A) → {(F ‘B)} = (F “ {B}))
Theorem	funfv 2862	A simplified expression for the value of a function when we know it's a function.
⊢ (Fun F → (F ‘A) = ∪(F “ {A}))
Theorem	funfv2 2863	The value of a function. Definition of function value in [Enderton] p. 43.
⊢ (Fun F → (F ‘A) = ∪{y∣⟨A, y⟩ ∈ F})
Theorem	dmfco 2864	Domains of a function composition.
⊢ ((Fun G ∧ A ∈ dom G) → (A ∈ dom (F ∘ G) ↔ (G ‘A) ∈ dom F))
Theorem	fvco 2865	Value of a function composition. Similar to Exercise 5 of [TakeutiZaring] p. 28.
⊢ (((Fun F ∧ Fun G) ∧ A ∈ dom G) → ((F ∘ G) ‘A) = (F ‘(G ‘A)))
Theorem	fvco2 2866	Value of a function composition. Similar to second part of Theorem 3H of [Enderton] p. 47.
⊢ (((Fun F ∧ G Fn A) ∧ C ∈ A) → ((F ∘ G) ‘C) = (F ‘(G ‘C)))
Theorem	fvco3 2867	Value of a function composition.
⊢ (((Fun F ∧ G:A–→B) ∧ C ∈ A) → ((F ∘ G) ‘C) = (F ‘(G ‘C)))
Theorem	fvopab3 2868	Value of a function given by ordered pair abstraction.
⊢ B ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (x ∈ C → ∃!yφ)    &   ⊢ F = {⟨x, y⟩∣(x ∈ C ∧ φ)}    ⇒   ⊢ (A ∈ C → ((F ‘A) = B ↔ χ))
Theorem	fvopab3ig 2869	Value of a function given by ordered pair abstraction.
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (x ∈ C → ∃*yφ)    &   ⊢ F = {⟨x, y⟩∣(x ∈ C ∧ φ)}    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → (χ → (F ‘A) = B))
Theorem	fvopab4g 2870	Value of a function given by ordered pair abstraction.
⊢ (x = A → B = C)    &   ⊢ F = {⟨x, y⟩∣(x ∈ D ∧ y = B)}    ⇒   ⊢ ((A ∈ D ∧ C ∈ R) → (F ‘A) = C)
Theorem	fvopab4 2871	Value of a function given by ordered pair abstraction.
⊢ (x = A → B = C)    &   ⊢ F = {⟨x, y⟩∣(x ∈ D ∧ y = B)}    &   ⊢ C ∈ V    ⇒   ⊢ (A ∈ D → (F ‘A) = C)
Theorem	fvopabg 2872	The value of a function given by ordered pair abstraction.
⊢ (x = A → B = C)    ⇒   ⊢ ((A ∈ D ∧ C ∈ R) → ({⟨x, y⟩∣y = B} ‘A) = C)
Theorem	fvopabn 2873	This somewhat non-intuitive theorem tells us the value of its function is the empty set when the class C it would otherwise map to is a proper class. This is a technical lemma that can help eliminate redundant sethood antecedents otherwise required by fvopabg 2872.
⊢ (x = A → B = C)    ⇒   ⊢ (¬ C ∈ V → ({⟨x, y⟩∣y = B} ‘A) = ∅)
Theorem	fvopabgf 2874	The value of a function given by ordered pair abstraction.
⊢ (z ∈ A → ∀x z ∈ A)    &   ⊢ (z ∈ C → ∀x z ∈ C)    &   ⊢ (x = A → B = C)    ⇒   ⊢ ((A ∈ D ∧ C ∈ R) → ({⟨x, y⟩∣y = B} ‘A) = C)
Theorem	fvopabnf 2875	The value of a function given by an ordered pair abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvopabn 2873 uses bound variable hypotheses instead of distinct variable conditions.
⊢ (z ∈ A → ∀x z ∈ A)    &   ⊢ (z ∈ C → ∀x z ∈ C)    &   ⊢ (x = A → B = C)    ⇒   ⊢ (¬ C ∈ V → ({⟨x, y⟩∣y = B} ‘A) = ∅)
Theorem	fvopabf 2876	The value of a function given by ordered pair abstraction.
⊢ (z ∈ A → ∀x z ∈ A)    &   ⊢ (z ∈ C → ∀x z ∈ C)    &   ⊢ A ∈ V    &   ⊢ C ∈ V    &   ⊢ (x = A → B = C)    ⇒   ⊢ ({⟨x, y⟩∣y = B} ‘A) = C
Theorem	fvopab 2877	The value of a function given by ordered pair abstraction.
⊢ A ∈ V    &   ⊢ C ∈ V    &   ⊢ (x = A → B = C)    ⇒   ⊢ ({⟨x, y⟩∣y = B} ‘A) = C
Theorem	fvopab2 2878	Value of a function given by an ordered pair abstraction.
⊢ ((x ∈ A ∧ B ∈ C) → ({⟨x, y⟩∣(x ∈ A ∧ y = B)} ‘x) = B)
Theorem	fvsn 2879	The value of a singleton of an ordered pair is the second member.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ({⟨A, B⟩} ‘A) = B
Theorem	cleqfv 2880	Equality of functions is determined by their values. Exercise 4 of [TakeutiZaring] p. 28.
⊢ ((F Fn A ∧ G Fn B) → (F = G ↔ (A = B ∧ ∀x ∈ A (F ‘x) = (G ‘x))))
Theorem	cleqfvf 2881	Equality of functions is determined by their values. Exercise 4 of [TakeutiZaring] p. 28. This version of cleqfv 2880 uses bound variable hypotheses instead of distinct variable conditions.
⊢ (y ∈ F → ∀x y ∈ F)    &   ⊢ (y ∈ G → ∀x y ∈ G)    ⇒   ⊢ ((F Fn A ∧ G Fn B) → (F = G ↔ (A = B ∧ ∀x ∈ A (F ‘x) = (G ‘x))))
Theorem	fvreseq 2882	Equality of restricted functions is determined by their values.
⊢ (((F Fn A ∧ G Fn A) ∧ B ⊆ A) → ((F ↾ B) = (G ↾ B) ↔ ∀x ∈ B (F ‘x) = (G ‘x)))
Theorem	fvelrn 2883	A member of a function's range is a value of the function.
⊢ (F Fn A → (B ∈ ran F ↔ ∃x ∈ A (F ‘x) = B))
Theorem	elrnopab 2884	Membership in the range of an operation abstraction.
⊢ B ∈ V    &   ⊢ F = {⟨x, y⟩∣(x ∈ A ∧ y = B)}    ⇒   ⊢ (C ∈ ran F ↔ ∃x ∈ A C = B)
Theorem	chfnrn 2885	The range of a choice function (a function that chooses an element from each member of its domain) is included in the union of its domain.
⊢ ((F Fn A ∧ ∀x ∈ A (F ‘x) ∈ x) → ran F ⊆ ∪A)
Theorem	funopfv 2886	Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41.
⊢ ((Fun F ∧ A ∈ dom F) → ⟨A, (F ‘A)⟩ ∈ F)
Theorem	fnopfv 2887	Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41.
⊢ ((F Fn A ∧ B ∈ A) → ⟨B, (F ‘B)⟩ ∈ F)
Theorem	fvrn 2888	A function's value belongs to its range.
⊢ ((Fun F ∧ A ∈ dom F) → (F ‘A) ∈ ran F)
Theorem	fnfvrn 2889	A function's value belongs to its range.
⊢ ((F Fn A ∧ B ∈ A) → (F ‘B) ∈ ran F)
Theorem	ffvrn 2890	A function's value belongs to its codomain.
⊢ ((F:A–→B ∧ C ∈ A) → (F ‘C) ∈ B)
Theorem	fopab2 2891	Functionality of an ordered pair abstraction.
⊢ F = {⟨x, y⟩∣(x ∈ A ∧ y = C)}    ⇒   ⊢ (∀x ∈ A C ∈ B ↔ F:A–→B)
Theorem	ffnfv 2892	A function maps to a class to which all values belong.
⊢ (F:A–→B ↔ (F Fn A ∧ ∀x ∈ A (F ‘x) ∈ B))
Theorem	fnfvrnss 2893	An upper bound for range determined by function values.
⊢ ((F Fn A ∧ ∀x ∈ A (F ‘x) ∈ B) → ran F ⊆ B)
Theorem	fopabfv 2894	Representation of a mapping in terms of its values.
⊢ (F:A–→B ↔ (F = {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))} ∧ ∀x ∈ A (F ‘x) ∈ B))
Theorem	fsn 2895	A function maps a singleton to a singleton iff it is the singleton of a ordered pair.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (F:{A}–→{B} ↔ F = {⟨A, B⟩})
Theorem	fsn2 2896	A function that maps a singleton to a class is the singleton of an ordered pair.
⊢ A ∈ V    ⇒   ⊢ (F:{A}–→B ↔ ((F ‘A) ∈ B ∧ F = {⟨A, (F ‘A)⟩}))
Theorem	fnressn 2897	A function restricted to a singleton.
⊢ ((F Fn A ∧ B ∈ A) → (F ↾ {B}) = {⟨B, (F ‘B)⟩})
Theorem	fressnfv 2898	The value of a function restricted to a singleton.
⊢ ((F Fn A ∧ B ∈ A) → ((F ↾ {B}):{B}–→C ↔ (F ‘B) ∈ C))
Theorem	fvconst 2899	The value of a constant function.
⊢ ((F:A–→{B} ∧ C ∈ A) → (F ‘C) = B)
Theorem	fvi 2900	The value of the identity function.
⊢ (A ∈ B → (I ‘A) = A)