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 ∈ 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 ∈ (◡F “ B)) → (F ‘A) ∈ 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 ∈ dom F) → ((F ‘A) ∈ B ↔ A ∈ (◡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 ⊆ dom F) → ((F “ A) ⊆ B ↔ A ⊆ (◡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 ⊆ dom F) → (A ⊆ (◡F “ B) ↔ ∀x ∈ A (F ‘x) ∈ 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 ⊆ dom F) → (∀x ∈ A (F ‘x) = B ↔ A ⊆ (◡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 ∈ (◡F “ C) ↔ (B ∈ A ∧ (F ‘B) ∈ C)))
Theorem	unpreima 5408	Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun F → (◡F “ (A ∪ B)) = ((◡F “ A) ∪ (◡F “ B)))
Theorem	inpreima 5409	Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun F → (◡F “ (A ∩ B)) = ((◡F “ A) ∩ (◡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) ∩ 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 ∈ A) → ⟨B, (F ‘B)⟩ ∈ F)
Theorem	fvelrn 5413	A function's value belongs to its range. (Contributed by set.mm contributors, 14-Oct-1996.)
⊢ ((Fun F ∧ A ∈ dom F) → (F ‘A) ∈ 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 ∈ A) → (F ‘B) ∈ 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 ∈ A) → (F ‘C) ∈ B)
Theorem	ffvelrni 5416	A function's value belongs to its codomain. (Contributed by set.mm contributors, 6-Apr-2005.)
⊢ F:A–→B    ⇒   ⊢ (C ∈ A → (F ‘C) ∈ 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 ∈ 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    &   ⊢ ∅ ∈ B    ⇒   ⊢ (F ‘C) ∈ B
Theorem	dff2 5419	Alternate definition of a mapping. (Contributed by set.mm contributors, 14-Nov-2007.)
⊢ (F:A–→B ↔ (F Fn A ∧ F ⊆ (A × B)))
Theorem	dff3 5420*	Alternate definition of a mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
⊢ (F:A–→B ↔ (F ⊆ (A × B) ∧ ∀x ∈ A ∃!y xFy))
Theorem	dff4 5421*	Alternate definition of a mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
⊢ (F:A–→B ↔ (F ⊆ (A × B) ∧ ∀x ∈ A ∃!y ∈ 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 ∧ ∀y ∈ B ∃x ∈ 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 ∧ ∀y ∈ B ∃x ∈ 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 ∧ ∀y ∈ B ∃x xFy))
Theorem	foelrn 5425*	Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
⊢ ((F:A–onto→B ∧ C ∈ B) → ∃x ∈ 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 ∘ 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 ∧ ∀x ∈ A (F ‘x) ∈ 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.)
⊢ ℲxA    &   ⊢ ℲxB    &   ⊢ ℲxF    ⇒   ⊢ (F:A–→B ↔ (F Fn A ∧ ∀x ∈ A (F ‘x) ∈ B))
Theorem	fnfvrnss 5429*	An upper bound for range determined by function values. (Contributed by set.mm contributors, 8-Oct-2004.)
⊢ ((F Fn A ∧ ∀x ∈ A (F ‘x) ∈ B) → ran F ⊆ 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 ∈ A ∧ y = (F ‘x))} ∧ ∀x ∈ A (F ‘x) ∈ 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 ↔ ∀x ∈ A (x ∈ dom F ∧ (F ‘x) ∈ 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 ∈ V    &   ⊢ B ∈ 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 ∈ C ∧ B ∈ 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 ∈ V    ⇒   ⊢ (F:{A}–→B ↔ ((F ‘A) ∈ B ∧ F = {⟨A, (F ‘A)⟩}))
Theorem	xpsn 5435	The cross product of two singletons. (Contributed by set.mm contributors, 4-Nov-2006.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ({A} × {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 ∈ 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 ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ D ∈ 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 ∈ 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 ∈ A) → ((F ↾ {B}):{B}–→C ↔ (F ‘B) ∈ C))
Theorem	fvconst 5440	The value of a constant function. (Contributed by set.mm contributors, 30-May-1999.)
⊢ ((F:A–→{B} ∧ C ∈ 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 ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ {⟨A, B⟩} = {⟨x, y⟩ ∣ (x ∈ {A} ∧ y = B)}
Theorem	fvi 5442	The value of the identity function. (Contributed by set.mm contributors, 1-May-2004.)
⊢ (A ∈ V → ( I ‘A) = A)
Theorem	fvresi 5443	The value of a restricted identity function. (Contributed by set.mm contributors, 19-May-2004.)
⊢ (B ∈ 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 ∪ {⟨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 ∈ V    &   ⊢ B ∈ 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 ∈ V ∧ B ∈ 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 ∈ V    &   ⊢ B ∈ V    &   ⊢ G = ({⟨A, B⟩} ∪ (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 ∈ V    &   ⊢ B ∈ V    &   ⊢ G = ({⟨A, B⟩} ∪ (F ↾ (C ∖ {A})))    ⇒   ⊢ (D ∈ (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 ∈ V    &   ⊢ C ∈ 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 ∈ V    &   ⊢ D ∈ 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 ∈ D ∧ C ∈ A) → ((A × {B}) ‘C) = B)
Theorem	fconst2g 5452	A constant function expressed as a cross product. (Contributed by set.mm contributors, 27-Nov-2007.)
⊢ (B ∈ C → (F:A–→{B} ↔ F = (A × {B})))
Theorem	fvconst2 5453	The value of a constant function. (Contributed by set.mm contributors, 16-Apr-2005.)
⊢ B ∈ V    ⇒   ⊢ (C ∈ A → ((A × {B}) ‘C) = B)
Theorem	fconst2 5454	A constant function expressed as a cross product. (Contributed by set.mm contributors, 20-Aug-1999.)
⊢ B ∈ V    ⇒   ⊢ (F:A–→{B} ↔ F = (A × {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 × {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 ∧ ∀x ∈ 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 ⊆ (◡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 ∈ dom F) → (B ∈ A → (F ‘B) ∈ (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 ⊆ dom F) → (B ∈ A → (F ‘B) ∈ (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 ⊆ G) → (A ∈ dom F → (F ‘A) ∈ (G “ {A})))
Theorem	fvclss 5462*	Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995.)
⊢ {y ∣ ∃x y = (F ‘x)} ⊆ (ran F ∪ {∅})
Theorem	abrexco 5463*	Composition of two image maps C(y) and B(w). (Contributed by set.mm contributors, 27-May-2013.)
⊢ B ∈ V    &   ⊢ (y = B → C = D)    ⇒   ⊢ {x ∣ ∃y ∈ {z ∣ ∃w ∈ A z = B}x = C} = {x ∣ ∃w ∈ 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 “ ∪x ∈ B C) = ∪x ∈ 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 “ ∪B) = ∪x ∈ 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 → ∪x ∈ A (F ‘x) = ∪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 → ∪x ∈ A (F ‘x) = ∪(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.)
⊢ ℲxF    ⇒   ⊢ (Fun F → ∪x ∈ A (F ‘x) = ∪(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 ∈ ∪(F “ A) ↔ ∃x ∈ A B ∈ (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 ∈ ∪ran F ↔ ∃x ∈ dom F A ∈ (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 ∧ ∀x ∈ A ∀y ∈ 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.)
⊢ ℲxF    &   ⊢ ℲyF    ⇒   ⊢ (F:A–1-1→B ↔ (F:A–→B ∧ ∀x ∈ A ∀y ∈ 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 ∈ A ∧ D ∈ 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 ∈ A ∧ Y ⊆ A) → ((F ‘X) ∈ (F “ Y) ↔ X ∈ 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 ∧ ∀x ∈ A ∀y ∈ 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 ∈ 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 ∈ 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 ∈ 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 ∈ A ∧ D ∈ 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 ∈ B) → ∃!x ∈ 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 ∈ B) → (◡F ‘C) ∈ 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.)
⊢ ℲxH    &   ⊢ ℲxR    &   ⊢ ℲxS    &   ⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎ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 ∈ A ∧ D ∈ 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 ∩ (B × 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 ∩ (A × 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 ∘ 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 ⊆ A ∧ D ∈ A)) → ((C ∩ (◡R “ {D})) = ∅ ↔ ((H “ C) ∩ (◡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 ∈ A) → (H “ (A ∩ (◡R “ {D}))) = (B ∩ (◡S “ {(H ‘D)})))
Theorem	isoini2 5498	Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
⊢ C = (A ∩ (◡R “ {X}))    &   ⊢ D = (B ∩ (◡S “ {(H ‘X)}))    ⇒   ⊢ ((H Isom R, S (A, B) ∧ X ∈ 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⟩ ∣ ∃x ∈ A ∃y ∈ 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 ∈ B ∧ y ∈ B) ∧ (◡H ‘x)R(◡H ‘y))}    ⇒   ⊢ (H:A–1-1-onto→B → H Isom R, S (A, B))