P. 72 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7101-7200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imauni 7101*	The image of a union is the indexed union of the images. Theorem 3K(a) of [Enderton] p. 50. (Contributed by NM, 9-Aug-2004.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐴 “ ∪ 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝑥)
Theorem	fniunfv 7102*	The indexed union of a function's values is the union of its range. Compare Definition 5.4 of [Monk1] p. 50. (Contributed by NM, 27-Sep-2004.)
⊢ (𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ ran 𝐹)
Theorem	funiunfv 7103*	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 𝐹 Fn 𝐴, the theorem can be proved without this dependency. (Contributed by NM, 26-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ (Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴))
Theorem	funiunfvf 7104*	The indexed union of a function's values is the union of its image under the index class. This version of funiunfv 7103 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.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ (Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴))
Theorem	eluniima 7105*	Membership in the union of an image of a function. (Contributed by NM, 28-Sep-2006.)
⊢ (Fun 𝐹 → (𝐵 ∈ ∪ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ (𝐹‘𝑥)))
Theorem	elunirn 7106*	Membership in the union of the range of a function. See elunirnALT 7107 for a shorter proof which uses ax-pow 5283. (Contributed by NM, 24-Sep-2006.)
⊢ (Fun 𝐹 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥)))
Theorem	elunirnALT 7107*	Alternate proof of elunirn 7106. It is shorter but requires ax-pow 5283 (through eluniima 7105, funiunfv 7103, ndmfv 6786). (Contributed by NM, 24-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fun 𝐹 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥)))
Theorem	fnunirn 7108*	Membership in a union of some function-defined family of sets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐹 Fn 𝐼 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝐼 𝐴 ∈ (𝐹‘𝑥)))
Theorem	dff13 7109*	A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 29-Oct-1996.)
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
Theorem	dff13f 7110*	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.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑦𝐹    ⇒   ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
Theorem	f1veqaeq 7111	If the values of a one-to-one function for two arguments are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷))
Theorem	f1cofveqaeq 7112	If the values of a composition of one-to-one functions for two arguments are equal, the arguments themselves must be equal. (Contributed by AV, 3-Feb-2021.)
⊢ (((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → ((𝐹‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑌)) → 𝑋 = 𝑌))
Theorem	f1cofveqaeqALT 7113	Alternate proof of f1cofveqaeq 7112, 1 essential step shorter, but having more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → ((𝐹‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑌)) → 𝑋 = 𝑌))
Theorem	2f1fvneq 7114	If two one-to-one functions are applied on different arguments, also the values are different. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ 𝐴 ≠ 𝐵) → (((𝐸‘(𝐹‘𝐴)) = 𝑋 ∧ (𝐸‘(𝐹‘𝐵)) = 𝑌) → 𝑋 ≠ 𝑌))
Theorem	f1mpt 7115*	Express injection for a mapping operation. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))
Theorem	f1fveq 7116	Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) ↔ 𝐶 = 𝐷))
Theorem	f1elima 7117	Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ 𝑋 ∈ 𝑌))
Theorem	f1imass 7118	Taking images under a one-to-one function preserves subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) ⊆ (𝐹 “ 𝐷) ↔ 𝐶 ⊆ 𝐷))
Theorem	f1imaeq 7119	Taking images under a one-to-one function preserves equality. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) = (𝐹 “ 𝐷) ↔ 𝐶 = 𝐷))
Theorem	f1imapss 7120	Taking images under a one-to-one function preserves proper subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) ⊊ (𝐹 “ 𝐷) ↔ 𝐶 ⊊ 𝐷))
Theorem	fpropnf1 7121	A function, given by an unordered pair of ordered pairs, which is not injective/one-to-one. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.)
⊢ 𝐹 = {⟨𝑋, 𝑍⟩, ⟨𝑌, 𝑍⟩}    ⇒   ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑋 ≠ 𝑌) → (Fun 𝐹 ∧ ¬ Fun ◡𝐹))
Theorem	f1dom3fv3dif 7122	The function values for a 1-1 function from a set with three different elements are different. (Contributed by AV, 20-Mar-2019.)
⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))    &   ⊢ (𝜑 → 𝐹:{𝐴, 𝐵, 𝐶}–1-1→𝑅)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) ≠ (𝐹‘𝐵) ∧ (𝐹‘𝐴) ≠ (𝐹‘𝐶) ∧ (𝐹‘𝐵) ≠ (𝐹‘𝐶)))
Theorem	f1dom3el3dif 7123*	The range of a 1-1 function from a set with three different elements has (at least) three different elements. (Contributed by AV, 20-Mar-2019.)
⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))    &   ⊢ (𝜑 → 𝐹:{𝐴, 𝐵, 𝐶}–1-1→𝑅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 ∃𝑧 ∈ 𝑅 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧))
Theorem	dff14a 7124*	A one-to-one function in terms of different function values for different arguments. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐹‘𝑥) ≠ (𝐹‘𝑦))))
Theorem	dff14b 7125*	A one-to-one function in terms of different function values for different arguments. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)))
Theorem	f12dfv 7126	A one-to-one function with a domain with at least two different elements in terms of function values. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
⊢ 𝐴 = {𝑋, 𝑌}    ⇒   ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌))))
Theorem	f13dfv 7127	A one-to-one function with a domain with at least three different elements in terms of function values. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
⊢ 𝐴 = {𝑋, 𝑌, 𝑍}    ⇒   ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))))
Theorem	dff1o6 7128*	A one-to-one onto function in terms of function values. (Contributed by NM, 29-Mar-2008.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
Theorem	f1ocnvfv1 7129	The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶)
Theorem	f1ocnvfv2 7130	The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)
Theorem	f1ocnvfv 7131	Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) = 𝐷 → (◡𝐹‘𝐷) = 𝐶))
Theorem	f1ocnvfvb 7132	Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by NM, 20-May-2004.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐹‘𝐶) = 𝐷 ↔ (◡𝐹‘𝐷) = 𝐶))
Theorem	nvof1o 7133	An involution is a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴–1-1-onto→𝐴)
Theorem	nvocnv 7134*	The converse of an involution is the function itself. (Contributed by Thierry Arnoux, 7-May-2019.)
⊢ ((𝐹:𝐴⟶𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝐹‘𝑥)) = 𝑥) → ◡𝐹 = 𝐹)
Theorem	fsnex 7135*	Relate a function with a singleton as domain and one variable. (Contributed by Thierry Arnoux, 12-Jul-2020.)
⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜑))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 𝜓))
Theorem	f1prex 7136*	Relate a one-to-one function with a pair as domain and two different variables. (Contributed by Thierry Arnoux, 12-Jul-2020.)
⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = (𝑓‘𝐵) → (𝜒 ↔ 𝜑))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
Theorem	f1ocnvdm 7137	The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴)
Theorem	f1ocnvfvrneq 7138	If the values of a one-to-one function for two arguments from the range of the function are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹)) → ((◡𝐹‘𝐶) = (◡𝐹‘𝐷) → 𝐶 = 𝐷))
Theorem	fcof1 7139	An application is injective if a retraction exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 11-Nov-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑅 ∘ 𝐹) = ( I ↾ 𝐴)) → 𝐹:𝐴–1-1→𝐵)
Theorem	fcofo 7140	An application is surjective if a section exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 17-Nov-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑆:𝐵⟶𝐴 ∧ (𝐹 ∘ 𝑆) = ( I ↾ 𝐵)) → 𝐹:𝐴–onto→𝐵)
Theorem	cbvfo 7141*	Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐹:𝐴–onto→𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓))
Theorem	cbvexfo 7142*	Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.)
⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐹:𝐴–onto→𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓))
Theorem	cocan1 7143	An injection is left-cancelable. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐻:𝐴⟶𝐵 ∧ 𝐾:𝐴⟶𝐵) → ((𝐹 ∘ 𝐻) = (𝐹 ∘ 𝐾) ↔ 𝐻 = 𝐾))
Theorem	cocan2 7144	A surjection is right-cancelable. (Contributed by FL, 21-Nov-2011.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐻 Fn 𝐵 ∧ 𝐾 Fn 𝐵) → ((𝐻 ∘ 𝐹) = (𝐾 ∘ 𝐹) ↔ 𝐻 = 𝐾))
Theorem	fcof1oinvd 7145	Show that a function is the inverse of a bijective function if their composition is the identity function. Formerly part of proof of fcof1o 7148. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵))    ⇒   ⊢ (𝜑 → ◡𝐹 = 𝐺)
Theorem	fcof1od 7146	A function is bijective if a "retraction" and a "section" exist, see comments for fcof1 7139 and fcofo 7140. Formerly part of proof of fcof1o 7148. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))    &   ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵))    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	2fcoidinvd 7147	Show that a function is the inverse of a function if their compositions are the identity functions. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))    &   ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵))    ⇒   ⊢ (𝜑 → ◡𝐹 = 𝐺)
Theorem	fcof1o 7148	Show that two functions are inverse to each other by computing their compositions. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by AV, 15-Dec-2019.)
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((𝐹 ∘ 𝐺) = ( I ↾ 𝐵) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))) → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = 𝐺))
Theorem	2fvcoidd 7149*	Show that the composition of two functions is the identity function by applying both functions to each value of the domain of the first function. (Contributed by AV, 15-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))
Theorem	2fvidf1od 7150*	A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎)    &   ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	2fvidinvd 7151*	Show that two functions are inverse to each other by applying them twice to each value of their domains. (Contributed by AV, 13-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎)    &   ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏)    ⇒   ⊢ (𝜑 → ◡𝐹 = 𝐺)
Theorem	foeqcnvco 7152	Condition for function equality in terms of vanishing of the composition with the converse. EDITORIAL: Is there a relation-algebraic proof of this? (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 = 𝐺 ↔ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)))
Theorem	f1eqcocnv 7153	Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Proof shortened by Wolf Lammen, 29-May-2024.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
Theorem	f1eqcocnvOLD 7154	Obsolete version of f1eqcocnv 7153 as of 29-May-2024. (Contributed by Stefan O'Rear, 12-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
Theorem	fveqf1o 7155	Given a bijection 𝐹, produce another bijection 𝐺 which additionally maps two specified points. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝐺 = (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝐶, (◡𝐹‘𝐷)})) ∪ {⟨𝐶, (◡𝐹‘𝐷)⟩, ⟨(◡𝐹‘𝐷), 𝐶⟩}))    ⇒   ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐺:𝐴–1-1-onto→𝐵 ∧ (𝐺‘𝐶) = 𝐷))
Theorem	nf1const 7156	A constant function from at least two elements is not one-to-one. (Contributed by AV, 30-Mar-2024.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1→𝐶)
Theorem	nf1oconst 7157	A constant function from at least two elements is not bijective. (Contributed by AV, 30-Mar-2024.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1-onto→𝐶)
Theorem	f1ofvswap 7158	Swapping two values in a bijection between two classes yields another bijection between those classes. (Contributed by BTernaryTau, 31-Aug-2024.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {⟨𝑋, (𝐹‘𝑌)⟩, ⟨𝑌, (𝐹‘𝑋)⟩}):𝐴–1-1-onto→𝐵)
Theorem	fliftrel 7159*	𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐹 ⊆ (𝑅 × 𝑆))
Theorem	fliftel 7160*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐶𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶 = 𝐴 ∧ 𝐷 = 𝐵)))
Theorem	fliftel1 7161*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴𝐹𝐵)
Theorem	fliftcnv 7162*	Converse of the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ◡𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐵, 𝐴⟩))
Theorem	fliftfun 7163*	The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷)))
Theorem	fliftfund 7164*	The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 = 𝐶)) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	fliftfuns 7165*	The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵)))
Theorem	fliftf 7166*	The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:ran (𝑥 ∈ 𝑋 ↦ 𝐴)⟶𝑆))
Theorem	fliftval 7167*	The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ ((𝜑 ∧ 𝑌 ∈ 𝑋) → (𝐹‘𝐶) = 𝐷)
Theorem	isoeq1 7168	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵)))
Theorem	isoeq2 7169	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝑅 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑇, 𝑆 (𝐴, 𝐵)))
Theorem	isoeq3 7170	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝑆 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑇 (𝐴, 𝐵)))
Theorem	isoeq4 7171	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵)))
Theorem	isoeq5 7172	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))
Theorem	nfiso 7173	Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ Ⅎ𝑥𝐻    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
Theorem	isof1o 7174	An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)
Theorem	isof1oidb 7175	A function is a bijection iff it is an isomorphism regarding the identity relation. (Contributed by AV, 9-May-2021.)
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻 Isom I , I (𝐴, 𝐵))
Theorem	isof1oopb 7176	A function is a bijection iff it is an isomorphism regarding the universal class of ordered pairs as relations. (Contributed by AV, 9-May-2021.)
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻 Isom (V × V), (V × V)(𝐴, 𝐵))
Theorem	isorel 7177	An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))
Theorem	soisores 7178*	Express the condition of isomorphism on two strict orders for a function's restriction. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (((𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶) ∧ (𝐹:𝐵⟶𝐶 ∧ 𝐴 ⊆ 𝐵)) → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, (𝐹 “ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦))))
Theorem	soisoi 7179*	Infer isomorphism from one direction of an order proof for isomorphisms between strict orders. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))
Theorem	isoid 7180	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
⊢ ( I ↾ 𝐴) Isom 𝑅, 𝑅 (𝐴, 𝐴)
Theorem	isocnv 7181	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))
Theorem	isocnv2 7182	Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom ◡𝑅, ◡𝑆(𝐴, 𝐵))
Theorem	isocnv3 7183	Complementation law for isomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐶 = ((𝐴 × 𝐴) ∖ 𝑅)    &   ⊢ 𝐷 = ((𝐵 × 𝐵) ∖ 𝑆)    ⇒   ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝐶, 𝐷 (𝐴, 𝐵))
Theorem	isores2 7184	An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, (𝑆 ∩ (𝐵 × 𝐵))(𝐴, 𝐵))
Theorem	isores1 7185	An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom (𝑅 ∩ (𝐴 × 𝐴)), 𝑆(𝐴, 𝐵))
Theorem	isores3 7186	Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐾 ⊆ 𝐴 ∧ 𝑋 = (𝐻 “ 𝐾)) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋))
Theorem	isotr 7187	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑆, 𝑇 (𝐵, 𝐶)) → (𝐺 ∘ 𝐻) Isom 𝑅, 𝑇 (𝐴, 𝐶))
Theorem	isomin 7188	Isomorphisms preserve minimal elements. Note that (◡𝑅 “ {𝐷}) is Takeuti and Zaring's idiom for the initial segment {𝑥 ∣ 𝑥𝑅𝐷}. Proposition 6.31(1) of [TakeutiZaring] p. 33. (Contributed by NM, 19-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐶 ∩ (◡𝑅 “ {𝐷})) = ∅ ↔ ((𝐻 “ 𝐶) ∩ (◡𝑆 “ {(𝐻‘𝐷)})) = ∅))
Theorem	isoini 7189	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐷 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝐷}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝐷)})))
Theorem	isoini2 7190	Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋}))    &   ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)}))    ⇒   ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))
Theorem	isofrlem 7191*	Lemma for isofr 7193. (Contributed by NM, 29-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
Theorem	isoselem 7192*	Lemma for isose 7194. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵))
Theorem	isofr 7193	An isomorphism preserves well-foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐵))
Theorem	isose 7194	An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐵))
Theorem	isofr2 7195	A weak form of isofr 7193 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐵 ∈ 𝑉) → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
Theorem	isopolem 7196	Lemma for isopo 7197. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Po 𝐵 → 𝑅 Po 𝐴))
Theorem	isopo 7197	An isomorphism preserves the property of being a partial order. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐵))
Theorem	isosolem 7198	Lemma for isoso 7199. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Or 𝐵 → 𝑅 Or 𝐴))
Theorem	isoso 7199	An isomorphism preserves the property of being a strict total order. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵))
Theorem	isowe 7200	An isomorphism preserves the property of being a well-ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵))