P. 55 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5401-5500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	funfvbrb 5401	Two ways to say that A is in the domain of F. (Contributed by Mario Carneiro, 1-May-2014.)
|- (Fun F -> (A e. dom F <-> AF(F` A)))
Theorem	fvimacnvi 5402	A member of a preimage is a function value argument. (Contributed by set.mm contributors, 4-May-2007.)
|- ((Fun F /\ A e. (`'F"B)) -> (F` A) e. B)
Theorem	fvimacnv 5403	The argument of a function value belongs to the preimage of any class containing the function value. (Contributed by Raph Levien, 20-Nov-2006.) He remarks: "This proof is unsatisfying, because it seems to me that funimass2 5170 could probably be strengthened to a biconditional."
|- ((Fun F /\ A e. dom F) -> ((F` A) e. B <-> A e. (`'F"B)))
Theorem	funimass3 5404	A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by Raph Levien, 20-Nov-2006.) He remarks: "Likely this could be proved directly, and fvimacnv 5403 would be the special case of A being a singleton, but it works this way round too."
|- ((Fun F /\ A C_ dom F) -> ((F"A) C_ B <-> A C_ (`'F"B)))
Theorem	funimass5 5405*	A subclass of a preimage in terms of function values. (Contributed by set.mm contributors, 15-May-2007.)
|- ((Fun F /\ A C_ dom F) -> (A C_ (`'F"B) <-> A.x e. A (F` x) e. B))
Theorem	funconstss 5406*	Two ways of specifying that a function is constant on a subdomain. (Contributed by set.mm contributors, 8-Mar-2007.)
|- ((Fun F /\ A C_ dom F) -> (A.x e. A (F` x) = B <-> A C_ (`'F"{B})))
Theorem	elpreima 5407	Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- (F Fn A -> (B e. (`'F"C) <-> (B e. A /\ (F` B) e. C)))
Theorem	unpreima 5408	Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- (Fun F -> (`'F"(A u. B)) = ((`'F"A) u. (`'F"B)))
Theorem	inpreima 5409	Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- (Fun F -> (`'F"(A i^i B)) = ((`'F"A) i^i (`'F"B)))
Theorem	respreima 5410	The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- (Fun F -> (`'(F |` B)"A) = ((`'F"A) i^i B))
Theorem	fimacnv 5411	The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.)
|- (F:A-->B -> (`'F"B) = A)
Theorem	fnopfv 5412	Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by set.mm contributors, 30-Sep-2004.)
|- ((F Fn A /\ B e. A) -> <.B, (F` B)>. e. F)
Theorem	fvelrn 5413	A function's value belongs to its range. (Contributed by set.mm contributors, 14-Oct-1996.)
|- ((Fun F /\ A e. dom F) -> (F` A) e. ran F)
Theorem	fnfvelrn 5414	A function's value belongs to its range. (Contributed by set.mm contributors, 15-Oct-1996.)
|- ((F Fn A /\ B e. A) -> (F` B) e. ran F)
Theorem	ffvelrn 5415	A function's value belongs to its codomain. (Contributed by set.mm contributors, 12-Aug-1999.)
|- ((F:A-->B /\ C e. A) -> (F` C) e. B)
Theorem	ffvelrni 5416	A function's value belongs to its codomain. (Contributed by set.mm contributors, 6-Apr-2005.)
|- F:A-->B   =>   |- (C e. A -> (F` C) e. B)
Theorem	fnasrn 5417*	A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013.)
|- (F Fn A -> F = ran {<.x, y>. | (x e. A /\ y = <.x, (F` x)>.)})
Theorem	f0cli 5418	Unconditional closure of a function when the range includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.)
|- F:A-->B   &   |- (/) e. B   =>   |- (F` C) e. B
Theorem	dff2 5419	Alternate definition of a mapping. (Contributed by set.mm contributors, 14-Nov-2007.)
|- (F:A-->B <-> (F Fn A /\ F C_ (A X. B)))
Theorem	dff3 5420*	Alternate definition of a mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
|- (F:A-->B <-> (F C_ (A X. B) /\ A.x e. A E!y xFy))
Theorem	dff4 5421*	Alternate definition of a mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
|- (F:A-->B <-> (F C_ (A X. B) /\ A.x e. A E!y e. B xFy))
Theorem	dffo3 5422*	An onto mapping expressed in terms of function values. (Contributed by set.mm contributors, 29-Oct-2006.)
|- (F:A-onto->B <-> (F:A-->B /\ A.y e. B E.x e. A y = (F` x)))
Theorem	dffo4 5423*	Alternate definition of an onto mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
|- (F:A-onto->B <-> (F:A-->B /\ A.y e. B E.x e. A xFy))
Theorem	dffo5 5424*	Alternate definition of an onto mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
|- (F:A-onto->B <-> (F:A-->B /\ A.y e. B E.x xFy))
Theorem	foelrn 5425*	Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
|- ((F:A-onto->B /\ C e. B) -> E.x e. A C = (F` x))
Theorem	foco2 5426	If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ((F:B-->C /\ G:A-->B /\ (F o. G):A-onto->C) -> F:B-onto->C)
Theorem	ffnfv 5427*	A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)
|- (F:A-->B <-> (F Fn A /\ A.x e. A (F` x) e. B))
Theorem	ffnfvf 5428	A function maps to a class to which all values belong. This version of ffnfv 5427 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.)
|- F/_xA   &   |- F/_xB   &   |- F/_xF   =>   |- (F:A-->B <-> (F Fn A /\ A.x e. A (F` x) e. B))
Theorem	fnfvrnss 5429*	An upper bound for range determined by function values. (Contributed by set.mm contributors, 8-Oct-2004.)
|- ((F Fn A /\ A.x e. A (F` x) e. B) -> ran F C_ B)
Theorem	fopabfv 5430*	Representation of a mapping in terms of its values. (Contributed by set.mm contributors, 21-Feb-2004.)
|- (F:A-->B <-> (F = {<.x, y>. | (x e. A /\ y = (F` x))} /\ A.x e. A (F` x) e. B))
Theorem	ffvresb 5431*	A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- (Fun F -> ((F |` A):A-->B <-> A.x e. A (x e. dom F /\ (F` x) e. B)))
Theorem	fsn 5432	A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003.)
|- A e. _V   &   |- B e. _V   =>   |- (F:{A}-->{B} <-> F = {<.A, B>.})
Theorem	fsng 5433	A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by set.mm contributors, 26-Oct-2012.)
|- ((A e. C /\ B e. D) -> (F:{A}-->{B} <-> F = {<.A, B>.}))
Theorem	fsn2 5434	A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by set.mm contributors, 19-May-2004.)
|- A e. _V   =>   |- (F:{A}-->B <-> ((F` A) e. B /\ F = {<.A, (F` A)>.}))
Theorem	xpsn 5435	The cross product of two singletons. (Contributed by set.mm contributors, 4-Nov-2006.)
|- A e. _V   &   |- B e. _V   =>   |- ({A} X. {B}) = {<.A, B>.}
Theorem	ressnop0 5436	If A is not in C, then the restriction of a singleton of <.A, B>. to C is null. (Contributed by Scott Fenton, 15-Apr-2011.)
|- (-. A e. C -> ({<.A, B>.} |` C) = (/))
Theorem	fpr 5437	A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (The proof was shortened by Andrew Salmon, 22-Oct-2011.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- D e. _V   =>   |- (A =/= B -> {<.A, C>., <.B, D>.}:{A, B}-->{C, D})
Theorem	fnressn 5438	A function restricted to a singleton. (Contributed by set.mm contributors, 9-Oct-2004.)
|- ((F Fn A /\ B e. A) -> (F |` {B}) = {<.B, (F` B)>.})
Theorem	fressnfv 5439	The value of a function restricted to a singleton. (Contributed by set.mm contributors, 9-Oct-2004.)
|- ((F Fn A /\ B e. A) -> ((F |` {B}):{B}-->C <-> (F` B) e. C))
Theorem	fvconst 5440	The value of a constant function. (Contributed by set.mm contributors, 30-May-1999.)
|- ((F:A-->{B} /\ C e. A) -> (F` C) = B)
Theorem	fopabsn 5441*	The singleton of an ordered pair expressed as an ordered pair class abstraction. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 6-Jun-2006.) (Revised by set.mm contributors, 22-Oct-2011.)
|- A e. _V   &   |- B e. _V   =>   |- {<.A, B>.} = {<.x, y>. | (x e. {A} /\ y = B)}
Theorem	fvi 5442	The value of the identity function. (Contributed by set.mm contributors, 1-May-2004.)
|- (A e. V -> ( _I ` A) = A)
Theorem	fvresi 5443	The value of a restricted identity function. (Contributed by set.mm contributors, 19-May-2004.)
|- (B e. A -> (( _I |` A)` B) = B)
Theorem	fvunsn 5444	Remove an ordered pair not participating in a function value. (Contributed by set.mm contributors, 1-Oct-2013.) (Revised by Mario Carneiro, 28-May-2014.)
|- (B =/= D -> ((A u. {<.B, C>.})` D) = (A` D))
Theorem	fvsn 5445	The value of a singleton of an ordered pair is the second member. (Contributed by set.mm contributors, 12-Aug-1994.)
|- A e. _V   &   |- B e. _V   =>   |- ({<.A, B>.}` A) = B
Theorem	fvsng 5446	The value of a singleton of an ordered pair is the second member. (Contributed by set.mm contributors, 26-Oct-2012.)
|- ((A e. V /\ B e. W) -> ({<.A, B>.}` A) = B)
Theorem	fvsnun1 5447	The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 5448. (Contributed by set.mm contributors, 23-Sep-2007.)
|- A e. _V   &   |- B e. _V   &   |- G = ({<.A, B>.} u. (F |` (C \ {A})))   =>   |- (G` A) = B
Theorem	fvsnun2 5448	The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 5447. (Contributed by set.mm contributors, 23-Sep-2007.)
|- A e. _V   &   |- B e. _V   &   |- G = ({<.A, B>.} u. (F |` (C \ {A})))   =>   |- (D e. (C \ {A}) -> (G` D) = (F` D))
Theorem	fvpr1 5449	The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
|- A e. _V   &   |- C e. _V   =>   |- (A =/= B -> ({<.A, C>., <.B, D>.}` A) = C)
Theorem	fvpr2 5450	The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
|- B e. _V   &   |- D e. _V   =>   |- (A =/= B -> ({<.A, C>., <.B, D>.}` B) = D)
Theorem	fvconst2g 5451	The value of a constant function. (Contributed by set.mm contributors, 20-Aug-2005.)
|- ((B e. D /\ C e. A) -> ((A X. {B})` C) = B)
Theorem	fconst2g 5452	A constant function expressed as a cross product. (Contributed by set.mm contributors, 27-Nov-2007.)
|- (B e. C -> (F:A-->{B} <-> F = (A X. {B})))
Theorem	fvconst2 5453	The value of a constant function. (Contributed by set.mm contributors, 16-Apr-2005.)
|- B e. _V   =>   |- (C e. A -> ((A X. {B})` C) = B)
Theorem	fconst2 5454	A constant function expressed as a cross product. (Contributed by set.mm contributors, 20-Aug-1999.)
|- B e. _V   =>   |- (F:A-->{B} <-> F = (A X. {B}))
Theorem	fconst5 5455	Two ways to express that a function is constant. (Contributed by set.mm contributors, 27-Nov-2007.)
|- ((F Fn A /\ A =/= (/)) -> (F = (A X. {B}) <-> ran F = {B}))
Theorem	fconstfv 5456*	A constant function expressed in terms of its functionality, domain, and value. See also fconst2 5454. (Contributed by NM, 27-Aug-2004.)
|- (F:A-->{B} <-> (F Fn A /\ A.x e. A (F` x) = B))
Theorem	fconst3 5457	Two ways to express a constant function. (Contributed by set.mm contributors, 15-Mar-2007.)
|- (F:A-->{B} <-> (F Fn A /\ A C_ (`'F"{B})))
Theorem	fconst4 5458	Two ways to express a constant function. (Contributed by set.mm contributors, 8-Mar-2007.)
|- (F:A-->{B} <-> (F Fn A /\ (`'F"{B}) = A))
Theorem	funfvima 5459	A function's value in a preimage belongs to the image. (Contributed by set.mm contributors, 23-Sep-2003.)
|- ((Fun F /\ B e. dom F) -> (B e. A -> (F` B) e. (F"A)))
Theorem	funfvima2 5460	A function's value in an included preimage belongs to the image. (Contributed by set.mm contributors, 3-Feb-1997.)
|- ((Fun F /\ A C_ dom F) -> (B e. A -> (F` B) e. (F"A)))
Theorem	funfvima3 5461	A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by set.mm contributors, 23-Mar-2004.)
|- ((Fun F /\ F C_ G) -> (A e. dom F -> (F` A) e. (G"{A})))
Theorem	fvclss 5462*	Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995.)
|- {y | E.x y = (F` x)} C_ (ran F u. {(/)})
Theorem	abrexco 5463*	Composition of two image maps C(y) and B(w). (Contributed by set.mm contributors, 27-May-2013.)
|- B e. _V   &   |- (y = B -> C = D)   =>   |- {x | E.y e. {z | E.w e. A z = B}x = C} = {x | E.w e. A x = D}
Theorem	imaiun 5464*	The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- (A"U_x e. B C) = U_x e. B (A"C)
Theorem	imauni 5465*	The image of a union is the indexed union of the images. Theorem 3K(a) of [Enderton] p. 50. (The proof was shortened by Mario Carneiro, 18-Jun-2014.) (Contributed by set.mm contributors, 9-Aug-2004.) (Revised by set.mm contributors, 18-Jun-2014.)
|- (A"U.B) = U_x e. B (A"x)
Theorem	fniunfv 5466*	The indexed union of a function's values is the union of its range. Compare Definition 5.4 of [Monk1] p. 50. (Contributed by set.mm contributors, 27-Sep-2004.)
|- (F Fn A -> U_x e. A (F` x) = U.ran F)
Theorem	funiunfv 5467*	The indexed union of a function's values is the union of its image under the index class. Note: This theorem depends on the fact that our function value is the empty set outside of its domain. If the antecedent is changed to F Fn A, the theorem can be proved without this dependency. (Contributed by set.mm contributors, 26-Mar-2006.)
|- (Fun F -> U_x e. A (F` x) = U.(F"A))
Theorem	funiunfvf 5468*	The indexed union of a function's values is the union of its image under the index class. This version of funiunfv 5467 uses a bound-variable hypothesis in place of a distinct variable condition. (Contributed by NM, 26-Mar-2006.) (Revised by David Abernethy, 15-Apr-2013.)
|- F/_xF   =>   |- (Fun F -> U_x e. A (F` x) = U.(F"A))
Theorem	eluniima 5469*	Membership in the union of an image of a function. (Contributed by set.mm contributors, 28-Sep-2006.)
|- (Fun F -> (B e. U.(F"A) <-> E.x e. A B e. (F` x)))
Theorem	elunirn 5470*	Membership in the union of the range of a function. (Contributed by set.mm contributors, 24-Sep-2006.)
|- (Fun F -> (A e. U.ran F <-> E.x e. dom F A e. (F` x)))
Theorem	dff13 5471*	A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by set.mm contributors, 29-Oct-1996.)
|- (F:A-1-1->B <-> (F:A-->B /\ A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))
Theorem	dff13f 5472*	A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 31-Jul-2003.)
|- F/_xF   &   |- F/_yF   =>   |- (F:A-1-1->B <-> (F:A-->B /\ A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))
Theorem	f1fveq 5473	Equality of function values for a one-to-one function. (Contributed by set.mm contributors, 11-Feb-1997.)
|- ((F:A-1-1->B /\ (C e. A /\ D e. A)) -> ((F` C) = (F` D) <-> C = D))
Theorem	f1elima 5474	Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ((F:A-1-1->B /\ X e. A /\ Y C_ A) -> ((F` X) e. (F"Y) <-> X e. Y))
Theorem	dff1o6 5475*	A one-to-one onto function in terms of function values. (Contributed by set.mm contributors, 29-Mar-2008.)
|- (F:A-1-1-onto->B <-> (F Fn A /\ ran F = B /\ A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))
Theorem	f1ocnvfv1 5476	The converse value of the value of a one-to-one onto function. (Contributed by set.mm contributors, 20-May-2004.)
|- ((F:A-1-1-onto->B /\ C e. A) -> (`'F` (F` C)) = C)
Theorem	f1ocnvfv2 5477	The value of the converse value of a one-to-one onto function. (Contributed by set.mm contributors, 20-May-2004.)
|- ((F:A-1-1-onto->B /\ C e. B) -> (F` (`'F` C)) = C)
Theorem	f1ocnvfv 5478	Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004.)
|- ((F:A-1-1-onto->B /\ C e. A) -> ((F` C) = D -> (`'F` D) = C))
Theorem	f1ocnvfvb 5479	Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by set.mm contributors, 20-May-2004.) (Revised by set.mm contributors, 9-Aug-2006.)
|- ((F:A-1-1-onto->B /\ C e. A /\ D e. B) -> ((F` C) = D <-> (`'F` D) = C))
Theorem	f1ofveu 5480*	There is one domain element for each value of a one-to-one onto function. (Contributed by set.mm contributors, 26-May-2006.)
|- ((F:A-1-1-onto->B /\ C e. B) -> E!x e. A (F` x) = C)
Theorem	f1ocnvdm 5481	The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by set.mm contributors, 26-May-2006.)
|- ((F:A-1-1-onto->B /\ C e. B) -> (`'F` C) e. A)
Theorem	isoeq1 5482	Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.)
|- (H = G -> (H Isom R, S (A, B) <-> G Isom R, S (A, B)))
Theorem	isoeq2 5483	Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.)
|- (R = T -> (H Isom R, S (A, B) <-> H Isom T, S (A, B)))
Theorem	isoeq3 5484	Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.)
|- (S = T -> (H Isom R, S (A, B) <-> H Isom R, T (A, B)))
Theorem	isoeq4 5485	Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.)
|- (A = C -> (H Isom R, S (A, B) <-> H Isom R, S (C, B)))
Theorem	isoeq5 5486	Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.)
|- (B = C -> (H Isom R, S (A, B) <-> H Isom R, S (A, C)))
Theorem	nfiso 5487	Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- F/_xH   &   |- F/_xR   &   |- F/_xS   &   |- F/_xA   &   |- F/_xB   =>   |- F/x H Isom R, S (A, B)
Theorem	isof1o 5488	An isomorphism is a one-to-one onto function. (Contributed by set.mm contributors, 27-Apr-2004.)
|- (H Isom R, S (A, B) -> H:A-1-1-onto->B)
Theorem	isorel 5489	An isomorphism connects binary relations via its function values. (Contributed by set.mm contributors, 27-Apr-2004.)
|- ((H Isom R, S (A, B) /\ (C e. A /\ D e. A)) -> (CRD <-> (H` C)S(H` D)))
Theorem	isoid 5490	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 27-Apr-2004.)
|- ( _I |` A) Isom R, R (A, A)
Theorem	isocnv 5491	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 27-Apr-2004.)
|- (H Isom R, S (A, B) -> `'H Isom S, R (B, A))
Theorem	isocnv2 5492	Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
|- (H Isom R, S (A, B) <-> H Isom `'R, `'S(A, B))
Theorem	isores2 5493	An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
|- (H Isom R, S (A, B) <-> H Isom R, (S i^i (B X. B))(A, B))
Theorem	isores1 5494	An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
|- (H Isom R, S (A, B) <-> H Isom (R i^i (A X. A)), S(A, B))
Theorem	isotr 5495	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 27-Apr-2004.)
|- ((H Isom R, S (A, B) /\ G Isom S, T (B, C)) -> (G o. H) Isom R, T (A, C))
Theorem	isomin 5496	Isomorphisms preserve minimal elements. Note that (`'R"{D}) is Takeuti and Zaring's idiom for the initial segment {x | xRD}. Proposition 6.31(1) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 19-Apr-2004.)
|- ((H Isom R, S (A, B) /\ (C C_ A /\ D e. A)) -> ((C i^i (`'R"{D})) = (/) <-> ((H"C) i^i (`'S"{(H` D)})) = (/)))
Theorem	isoini 5497	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 20-Apr-2004.)
|- ((H Isom R, S (A, B) /\ D e. A) -> (H"(A i^i (`'R"{D}))) = (B i^i (`'S"{(H` D)})))
Theorem	isoini2 5498	Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
|- C = (A i^i (`'R"{X}))   &   |- D = (B i^i (`'S"{(H` X)}))   =>   |- ((H Isom R, S (A, B) /\ X e. A) -> (H |` C) Isom R, S (C, D))
Theorem	f1oiso 5499*	Any one-to-one onto function determines an isomorphism with an induced relation S. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by set.mm contributors, 30-Apr-2004.)
|- ((H:A-1-1-onto->B /\ S = {<.z, w>. | E.x e. A E.y e. A ((z = (H` x) /\ w = (H` y)) /\ xRy)}) -> H Isom R, S (A, B))
Theorem	f1oiso2 5500*	Any one-to-one onto function determines an isomorphism with an induced relation S. (Contributed by Mario Carneiro, 9-Mar-2013.)
|- S = {<.x, y>. | ((x e. B /\ y e. B) /\ (`'H` x)R(`'H` y))}   =>   |- (H:A-1-1-onto->B -> H Isom R, S (A, B))