P. 59 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5801-5900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	unisuc 5801	A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.)
|- A e. _V   =>    |- ( Tr A <-> U. suc A = A )
Theorem	sssucid 5802	A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.)
|- A C_ suc A
Theorem	sucidg 5803	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
|- ( A e. V -> A e. suc A )
Theorem	sucid 5804	A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
|- A e. _V   =>    |- A e. suc A
Theorem	nsuceq0 5805	No successor is empty. (Contributed by NM, 3-Apr-1995.)
|- suc A =/= (/)
Theorem	eqelsuc 5806	A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.)
|- A e. _V   =>    |- ( A = B -> A e. suc B )
Theorem	iunsuc 5807*	Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- A e. _V   &    |- ( x = A -> B = C )   =>    |- U_ x e. suc A B = ( U_ x e. A B u. C )
Theorem	suctr 5808	The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.) (Proof shortened by JJ, 24-Sep-2021.)
|- ( Tr A -> Tr suc A )
Theorem	suctrOLD 5809	Obsolete proof of suctr 5808 as of 24-Sep-2021. (Contributed by Alan Sare, 11-Apr-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( Tr A -> Tr suc A )
Theorem	trsuc 5810	A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- ( ( Tr A /\ suc B e. A ) -> B e. A )
Theorem	trsucss 5811	A member of the successor of a transitive class is a subclass of it. (Contributed by NM, 4-Oct-2003.)
|- ( Tr A -> ( B e. suc A -> B C_ A ) )
Theorem	ordsssuc 5812	A subset of an ordinal belongs to its successor. (Contributed by NM, 28-Nov-2003.)
|- ( ( A e. On /\ Ord B ) -> ( A C_ B <-> A e. suc B ) )
Theorem	onsssuc 5813	A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995.)
|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> A e. suc B ) )
Theorem	ordsssuc2 5814	An ordinal subset of an ordinal number belongs to its successor. (Contributed by NM, 1-Feb-2005.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- ( ( Ord A /\ B e. On ) -> ( A C_ B <-> A e. suc B ) )
Theorem	onmindif 5815	When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass. (Contributed by NM, 1-Dec-2003.)
|- ( ( A C_ On /\ B e. On ) -> B e. |^| ( A \ suc B ) )
Theorem	ordnbtwn 5816	There is no set between an ordinal class and its successor. Generalized Proposition 7.25 of [TakeutiZaring] p. 41. (Contributed by NM, 21-Jun-1998.) (Proof shortened by JJ, 24-Sep-2021.)
|- ( Ord A -> -. ( A e. B /\ B e. suc A ) )
Theorem	ordnbtwnOLD 5817	Obsolete proof of ordnbtwn 5816 as of 24-Sep-2021. (Contributed by NM, 21-Jun-1998.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( Ord A -> -. ( A e. B /\ B e. suc A ) )
Theorem	onnbtwn 5818	There is no set between an ordinal number and its successor. Proposition 7.25 of [TakeutiZaring] p. 41. (Contributed by NM, 9-Jun-1994.)
|- ( A e. On -> -. ( A e. B /\ B e. suc A ) )
Theorem	sucssel 5819	A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995.)
|- ( A e. V -> ( suc A C_ B -> A e. B ) )
Theorem	orddif 5820	Ordinal derived from its successor. (Contributed by NM, 20-May-1998.)
|- ( Ord A -> A = ( suc A \ { A } ) )
Theorem	orduniss 5821	An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.)
|- ( Ord A -> U. A C_ A )
Theorem	ordtri2or 5822	A trichotomy law for ordinal classes. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- ( ( Ord A /\ Ord B ) -> ( A e. B \/ B C_ A ) )
Theorem	ordtri2or2 5823	A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003.)
|- ( ( Ord A /\ Ord B ) -> ( A C_ B \/ B C_ A ) )
Theorem	ordtri2or3 5824	A consequence of total ordering for ordinal classes. Similar to ordtri2or2 5823. (Contributed by David Moews, 1-May-2017.)
|- ( ( Ord A /\ Ord B ) -> ( A = ( A i^i B ) \/ B = ( A i^i B ) ) )
Theorem	ordelinel 5825	The intersection of two ordinal classes is an element of a third if and only if either one of them is. (Contributed by David Moews, 1-May-2017.) (Proof shortened by JJ, 24-Sep-2021.)
|- ( ( Ord A /\ Ord B /\ Ord C ) -> ( ( A i^i B ) e. C <-> ( A e. C \/ B e. C ) ) )
Theorem	ordelinelOLD 5826	Obsolete proof of ordelinel 5825 as of 24-Sep-2021. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( Ord A /\ Ord B /\ Ord C ) -> ( ( A i^i B ) e. C <-> ( A e. C \/ B e. C ) ) )
Theorem	ordssun 5827	Property of a subclass of the maximum (i.e. union) of two ordinals. (Contributed by NM, 28-Nov-2003.)
|- ( ( Ord B /\ Ord C ) -> ( A C_ ( B u. C ) <-> ( A C_ B \/ A C_ C ) ) )
Theorem	ordequn 5828	The maximum (i.e. union) of two ordinals is either one or the other. Similar to Exercise 14 of [TakeutiZaring] p. 40. (Contributed by NM, 28-Nov-2003.)
|- ( ( Ord B /\ Ord C ) -> ( A = ( B u. C ) -> ( A = B \/ A = C ) ) )
Theorem	ordun 5829	The maximum (i.e. union) of two ordinals is ordinal. Exercise 12 of [TakeutiZaring] p. 40. (Contributed by NM, 28-Nov-2003.)
|- ( ( Ord A /\ Ord B ) -> Ord ( A u. B ) )
Theorem	ordunisssuc 5830	A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003.)
|- ( ( A C_ On /\ Ord B ) -> ( U. A C_ B <-> A C_ suc B ) )
Theorem	suc11 5831	The successor operation behaves like a one-to-one function. Compare Exercise 16 of [Enderton] p. 194. (Contributed by NM, 3-Sep-2003.)
|- ( ( A e. On /\ B e. On ) -> ( suc A = suc B <-> A = B ) )
Theorem	onordi 5832	An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- Ord A
Theorem	ontrci 5833	An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- Tr A
Theorem	onirri 5834	An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- -. A e. A
Theorem	oneli 5835	A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- ( B e. A -> B e. On )
Theorem	onelssi 5836	A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.)
|- A e. On   =>    |- ( B e. A -> B C_ A )
Theorem	onssneli 5837	An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.)
|- A e. On   =>    |- ( A C_ B -> -. B e. A )
Theorem	onssnel2i 5838	An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.)
|- A e. On   =>    |- ( B C_ A -> -. A e. B )
Theorem	onelini 5839	An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- ( B e. A -> B = ( B i^i A ) )
Theorem	oneluni 5840	An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.)
|- A e. On   =>    |- ( B e. A -> ( A u. B ) = A )
Theorem	onunisuci 5841	An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.)
|- A e. On   =>    |- U. suc A = A
Theorem	onsseli 5842	Subset is equivalent to membership or equality for ordinal numbers. (Contributed by NM, 15-Sep-1995.)
|- A e. On   &    |- B e. On   =>    |- ( A C_ B <-> ( A e. B \/ A = B ) )
Theorem	onun2i 5843	The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.)
|- A e. On   &    |- B e. On   =>    |- ( A u. B ) e. On
Theorem	unizlim 5844	An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003.)
|- ( Ord A -> ( A = U. A <-> ( A = (/) \/ Lim A ) ) )
Theorem	on0eqel 5845	An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004.)
|- ( A e. On -> ( A = (/) \/ (/) e. A ) )
Theorem	snsn0non 5846	The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 7069). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 5847. (Contributed by NM, 21-May-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- -. { { (/) } } e. On
Theorem	onxpdisj 5847	Ordinal numbers and ordered pairs are disjoint collections. This theorem can be used if we want to extend a set of ordinal numbers or ordered pairs with disjoint elements. See also snsn0non 5846. (Contributed by NM, 1-Jun-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( On i^i ( _V X. _V ) ) = (/)
Theorem	onnev 5848	The class of ordinal numbers is not equal to the universe. (Contributed by NM, 16-Jun-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2013.)
|- On =/= _V
2.3.14  Definite description binder (inverted iota)
Syntax	cio 5849	Extend class notation with Russell's definition description binder (inverted iota).
class ( iota x ph )
Theorem	iotajust 5850*	Soundness justification theorem for df-iota 5851. (Contributed by Andrew Salmon, 29-Jun-2011.)
|- U. { y | { x | ph } = { y } } = U. { z | { x | ph } = { z } }
Definition	df-iota 5851*	Define Russell's definition description binder, which can be read as "the unique x such that ph," where ph ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that ph is true (see iotaval 5862); otherwise, it evaluates to the empty set (see iotanul 5866). Russell used the inverted iota symbol iota to represent the binder. Sometimes proofs need to expand an iota-based definition. That is, given "X = the x for which ... x ... x ..." holds, the proof needs to get to "... X ... X ...". A general strategy to do this is to use riotacl2 6624 (or iotacl 5874 for unbounded iota), as demonstrated in the proof of supub 8365. This can be easier than applying riotasbc 6626 or a version that applies an explicit substitution, because substituting an iota into its own property always has a bound variable clash which must be first renamed or else guarded with NF. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- ( iota x ph ) = U. { y | { x | ph } = { y } }
Theorem	dfiota2 5852*	Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- ( iota x ph ) = U. { y | A. x ( ph <-> x = y ) }
Theorem	nfiota1 5853	Bound-variable hypothesis builder for the iota class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x ( iota x ph )
Theorem	nfiotad 5854	Deduction version of nfiota 5855. (Contributed by NM, 18-Feb-2013.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/_ x ( iota y ps ) )
Theorem	nfiota 5855	Bound-variable hypothesis builder for the iota class. (Contributed by NM, 23-Aug-2011.)
|- F/ x ph   =>    |- F/_ x ( iota y ph )
Theorem	cbviota 5856	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- ( x = y -> ( ph <-> ps ) )   &    |- F/ y ph   &    |- F/ x ps   =>    |- ( iota x ph ) = ( iota y ps )
Theorem	cbviotav 5857*	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( iota x ph ) = ( iota y ps )
Theorem	sb8iota 5858	Variable substitution in description binder. Compare sb8eu 2503. (Contributed by NM, 18-Mar-2013.)
|- F/ y ph   =>    |- ( iota x ph ) = ( iota y [ y / x ] ph )
Theorem	iotaeq 5859	Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- ( A. x x = y -> ( iota x ph ) = ( iota y ph ) )
Theorem	iotabi 5860	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- ( A. x ( ph <-> ps ) -> ( iota x ph ) = ( iota x ps ) )
Theorem	uniabio 5861*	Part of Theorem 8.17 in [Quine] p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( A. x ( ph <-> x = y ) -> U. { x | ph } = y )
Theorem	iotaval 5862*	Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )
Theorem	iotauni 5863	Equivalence between two different forms of iota. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- ( E! x ph -> ( iota x ph ) = U. { x | ph } )
Theorem	iotaint 5864	Equivalence between two different forms of iota. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( E! x ph -> ( iota x ph ) = |^| { x | ph } )
Theorem	iota1 5865	Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- ( E! x ph -> ( ph <-> ( iota x ph ) = x ) )
Theorem	iotanul 5866	Theorem 8.22 in [Quine] p. 57. This theorem is the result if there isn't exactly one x that satisfies ph. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( -. E! x ph -> ( iota x ph ) = (/) )
Theorem	iotassuni 5867	The iota class is a subset of the union of all elements satisfying ph. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( iota x ph ) C_ U. { x | ph }
Theorem	iotaex 5868	Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the iota class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( iota x ph ) e. _V
Theorem	iota4 5869	Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- ( E! x ph -> [. ( iota x ph ) / x ]. ph )
Theorem	iota4an 5870	Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- ( E! x ( ph /\ ps ) -> [. ( iota x ( ph /\ ps ) ) / x ]. ph )
Theorem	iota5 5871*	A method for computing iota. (Contributed by NM, 17-Sep-2013.)
|- ( ( ph /\ A e. V ) -> ( ps <-> x = A ) )   =>    |- ( ( ph /\ A e. V ) -> ( iota x ps ) = A )
Theorem	iotabidv 5872*	Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( iota x ps ) = ( iota x ch ) )
Theorem	iotabii 5873	Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( ph <-> ps )   =>    |- ( iota x ph ) = ( iota x ps )
Theorem	iotacl 5874	Membership law for descriptions. This can be useful for expanding an unbounded iota-based definition (see df-iota 5851). If you have a bounded iota-based definition, riotacl2 6624 may be useful. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- ( E! x ph -> ( iota x ph ) e. { x | ph } )
Theorem	iota2df 5875	A condition that allows us to represent "the unique element such that ph " with a class expression A. (Contributed by NM, 30-Dec-2014.)
|- ( ph -> B e. V )   &    |- ( ph -> E! x ps )   &    |- ( ( ph /\ x = B ) -> ( ps <-> ch ) )   &    |- F/ x ph   &    |- ( ph -> F/ x ch )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> ( ch <-> ( iota x ps ) = B ) )
Theorem	iota2d 5876*	A condition that allows us to represent "the unique element such that ph " with a class expression A. (Contributed by NM, 30-Dec-2014.)
|- ( ph -> B e. V )   &    |- ( ph -> E! x ps )   &    |- ( ( ph /\ x = B ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( ch <-> ( iota x ps ) = B ) )
Theorem	iota2 5877*	The unique element such that ph. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( ( A e. B /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) )
Theorem	sniota 5878	A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- ( E! x ph -> { x | ph } = { ( iota x ph ) } )
Theorem	dfiota4 5879	The iota operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.) (Proof shortened by JJ, 28-Oct-2021.)
|- ( iota x ph ) = if ( E! x ph , U. { x | ph } , (/) )
Theorem	dfiota4OLD 5880	Obsolete proof of dfiota4 5879 as of 28-Oct-2021. (Contributed by Scott Fenton, 6-Oct-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( iota x ph ) = if ( E! x ph , U. { x | ph } , (/) )
Theorem	csbiota 5881*	Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.) (Revised by NM, 23-Aug-2018.)
|- [_ A / x ]_ ( iota y ph ) = ( iota y [. A / x ]. ph )
2.3.15  Functions
Syntax	wfun 5882	Extend the definition of a wff to include the function predicate. (Read: A is a function.)
wff Fun A
Syntax	wfn 5883	Extend the definition of a wff to include the function predicate with a domain. (Read: A is a function on B.)
wff A Fn B
Syntax	wf 5884	Extend the definition of a wff to include the function predicate with domain and codomain. (Read: F maps A into B.)
wff F : A --> B
Syntax	wf1 5885	Extend the definition of a wff to include one-to-one functions. (Read: F maps A one-to-one into B.) The notation ("1-1" above the arrow) is from Definition 6.15(5) of [TakeutiZaring] p. 27.
wff F : A -1-1-> B
Syntax	wfo 5886	Extend the definition of a wff to include onto functions. (Read: F maps A onto B.) The notation ("onto" below the arrow) is from Definition 6.15(4) of [TakeutiZaring] p. 27.
wff F : A -onto-> B
Syntax	wf1o 5887	Extend the definition of a wff to include one-to-one onto functions. (Read: F maps A one-to-one onto B.) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27.
wff F : A -1-1-onto-> B
Syntax	cfv 5888	Extend the definition of a class to include the value of a function. (Read: The value of F at A, or " F of A.")
class ( F ` A )
Syntax	wiso 5889	Extend the definition of a wff to include the isomorphism property. (Read: H is an R, S isomorphism of A onto B.)
wff H Isom R , S ( A , B )
Definition	df-fun 5890	Define predicate that determines if some class A is a function. Definition 10.1 of [Quine] p. 65. For example, the expression Fun cos is true once we define cosine (df-cos 14801). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt 4729 with the maps-to notation (see df-mpt 4730 and df-mpt2 6655). Contrast this predicate with the predicates to determine if some class is a function with a given domain (df-fn 5891), a function with a given domain and codomain (df-f 5892), a one-to-one function (df-f1 5893), an onto function (df-fo 5894), or a one-to-one onto function (df-f1o 5895). For alternate definitions, see dffun2 5898, dffun3 5899, dffun4 5900, dffun5 5901, dffun6 5903, dffun7 5915, dffun8 5916, and dffun9 5917. (Contributed by NM, 1-Aug-1994.)
|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
Definition	df-fn 5891	Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6047, dffn3 6054, dffn4 6121, and dffn5 6241. (Contributed by NM, 1-Aug-1994.)
|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
Definition	df-f 5892	Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. F : A --> B can be read as " F is a function from A to B". For alternate definitions, see dff2 6371, dff3 6372, and dff4 6373. (Contributed by NM, 1-Aug-1994.)
|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
Definition	df-f1 5893	Define a one-to-one function. For equivalent definitions see dff12 6100 and dff13 6512. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). A one-to-one function is also called an "injection" or an "injective function", F : A -1-1-> B can be read as " F is an injection from A into B". Injections are precisely the monomorphisms in the category SetCat of sets and set functions, see setcmon 16737. (Contributed by NM, 1-Aug-1994.)
|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
Definition	df-fo 5894	Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 6119, dffo3 6374, dffo4 6375, and dffo5 6376. An onto function is also called a "surjection" or a "surjective function", F : A -onto-> B can be read as " F is a surjection from A onto B". Surjections are precisely the epimorphisms in the category SetCat of sets and set functions, see setcepi 16738. (Contributed by NM, 1-Aug-1994.)
|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
Definition	df-f1o 5895	Define a one-to-one onto function. For equivalent definitions see dff1o2 6142, dff1o3 6143, dff1o4 6145, and dff1o5 6146. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). A one-to-one onto function is also called a "bijection" or a "bijective function", F : A -1-1-onto-> B can be read as " F is a bijection between A and B". Bijections are precisely the isomorphisms in the category SetCat of sets and set functions, see setciso 16741. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6574, two sets are isomorphic iff there is an isomorphism Isom regarding the identity relation. In this case, the two sets are also "equinumerous", see bren 7964. (Contributed by NM, 1-Aug-1994.)
|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
Definition	df-fv 5896*	Define the value of a function, ( F ` A ), also known as function application. For example, ( cos ` 0 ) = 1 (we prove this in cos0 14880 after we define cosine in df-cos 14801). Typically, function F is defined using maps-to notation (see df-mpt 4730 and df-mpt2 6655), but this is not required. For example, F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ( F ` 3 ) = 9 (ex-fv 27300). Note that df-ov 6653 will define two-argument functions using ordered pairs as ( A F B ) = ( F ` <. A , B >. ). This particular definition is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful (as shown by ndmfv 6218 and fvprc 6185). The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. It means the same thing as the more familiar F ( A ) notation for a function's value at A, i.e. " F of A," but without context-dependent notational ambiguity. Alternate definitions are dffv2 6271, dffv3 6187, fv2 6186, and fv3 6206 (the latter two previously required A to be a set.) Restricted equivalents that require F to be a function are shown in funfv 6265 and funfv2 6266. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 6239. (Contributed by NM, 1-Aug-1994.) Revised to use iota. Original version is now theorem dffv4 6188. (Revised by Scott Fenton, 6-Oct-2017.)
|- ( F ` A ) = ( iota x A F x )
Definition	df-isom 5897*	Define the isomorphism predicate. We read this as " H is an R, S isomorphism of A onto B." Normally, R and S are ordering relations on A and B respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that R and S are subscripts. (Contributed by NM, 4-Mar-1997.)
|- ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
Theorem	dffun2 5898*	Alternate definition of a function. (Contributed by NM, 29-Dec-1996.)
|- ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) )
Theorem	dffun3 5899*	Alternate definition of function. (Contributed by NM, 29-Dec-1996.)
|- ( Fun A <-> ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) )
Theorem	dffun4 5900*	Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 29-Dec-1996.)
|- ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( <. x , y >. e. A /\ <. x , z >. e. A ) -> y = z ) ) )