P. 180 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17901-18000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	termoval 17901*	The value of the terminal object function, i.e. the set of all terminal objects of a category. (Contributed by AV, 3-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (TermO‘𝐶) = {𝑎 ∈ 𝐵 ∣ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑎)})
Theorem	zerooval 17902	The value of the zero object function, i.e. the set of all zero objects of a category. (Contributed by AV, 3-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (ZeroO‘𝐶) = ((InitO‘𝐶) ∩ (TermO‘𝐶)))
Theorem	isinito 17903*	The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝐼𝐻𝑏)))
Theorem	istermo 17904*	The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (TermO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝐼)))
Theorem	iszeroo 17905	The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ∈ (ZeroO‘𝐶) ↔ (𝐼 ∈ (InitO‘𝐶) ∧ 𝐼 ∈ (TermO‘𝐶))))
Theorem	isinitoi 17906*	Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑏)))
Theorem	istermoi 17907*	Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑂)))
Theorem	initoid 17908	For an initial object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 6-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})
Theorem	termoid 17909	For a terminal object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 18-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})
Theorem	dfinito2 17910	An initial object is a terminal object in the opposite category. An alternate definition of df-inito 17891 depending on df-termo 17892. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO = (𝑐 ∈ Cat ↦ (TermO‘(oppCat‘𝑐)))
Theorem	dftermo2 17911	A terminal object is an initial object in the opposite category. An alternate definition of df-termo 17892 depending on df-inito 17891. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO = (𝑐 ∈ Cat ↦ (InitO‘(oppCat‘𝑐)))
Theorem	dfinito3 17912	An alternate definition of df-inito 17891 depending on df-termo 17892, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ InitO = (TermO ∘ (oppCat ↾ Cat))
Theorem	dftermo3 17913	An alternate definition of df-termo 17892 depending on df-inito 17891, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ TermO = (InitO ∘ (oppCat ↾ Cat))
Theorem	initoo 17914	An initial object is an object. (Contributed by AV, 14-Apr-2020.)
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ (Base‘𝐶)))
Theorem	termoo 17915	A terminal object is an object. (Contributed by AV, 18-Apr-2020.)
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ (Base‘𝐶)))
Theorem	iszeroi 17916	Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (ZeroO‘𝐶)) → (𝑂 ∈ (Base‘𝐶) ∧ (𝑂 ∈ (InitO‘𝐶) ∧ 𝑂 ∈ (TermO‘𝐶))))
Theorem	2initoinv 17917	Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))    ⇒   ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺)
Theorem	initoeu1 17918*	Initial objects are essentially unique (strong form), i.e. there is a unique isomorphism between two initial objects, see statement in [Lang] p. 58 ("... if P, P' are two universal objects [...] then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 14-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))
Theorem	initoeu1w 17919	Initial objects are essentially unique (weak form), i.e. if A and B are initial objects, then A and B are isomorphic. Proposition 7.3 (1) of [Adamek] p. 102. (Contributed by AV, 6-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))    ⇒   ⊢ (𝜑 → 𝐴( ≃𝑐 ‘𝐶)𝐵)
Theorem	initoeu2lem0 17920	Lemma 0 for initoeu2 17923. (Contributed by AV, 9-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ (((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) ∧ ((𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾)(⟨𝐴, 𝐵⟩ ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵⟩ ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) → 𝐺 = (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾))
Theorem	initoeu2lem1 17921*	Lemma 1 for initoeu2 17923. (Contributed by AV, 9-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾)))
Theorem	initoeu2lem2 17922*	Lemma 2 for initoeu2 17923. (Contributed by AV, 10-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ ⚬ = (comp‘𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ (𝐹(⟨𝐵, 𝐴⟩ ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) → ∃!𝑔 𝑔 ∈ (𝐵𝐻𝐷)))
Theorem	initoeu2 17923	Initial objects are essentially unique, if A is an initial object, then so is every object that is isomorphic to A. Proposition 7.3 (2) in [Adamek] p. 102. (Contributed by AV, 10-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶))    &   ⊢ (𝜑 → 𝐴( ≃𝑐 ‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶))
Theorem	2termoinv 17924	Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶))    ⇒   ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺)
Theorem	termoeu1 17925*	Terminal objects are essentially unique (strong form), i.e. there is a unique isomorphism between two terminal objects, see statement in [Lang] p. 58 ("... if P, P' are two universal objects [...] then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶))    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓 ∈ (𝐴(Iso‘𝐶)𝐵))
Theorem	termoeu1w 17926	Terminal objects are essentially unique (weak form), i.e. if A and B are terminal objects, then A and B are isomorphic. Proposition 7.6 of [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶))    ⇒   ⊢ (𝜑 → 𝐴( ≃𝑐 ‘𝐶)𝐵)
8.2  Arrows (disjointified hom-sets)
Syntax	cdoma 17927	Extend class notation to include the domain extractor for an arrow.
class doma
Syntax	ccoda 17928	Extend class notation to include the codomain extractor for an arrow.
class coda
Syntax	carw 17929	Extend class notation to include the collection of all arrows of a category.
class Arrow
Syntax	choma 17930	Extend class notation to include the set of all arrows with a specific domain and codomain.
class Homa
Definition	df-doma 17931	Definition of the domain extractor for an arrow. (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ doma = (1st ∘ 1st )
Definition	df-coda 17932	Definition of the codomain extractor for an arrow. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ coda = (2nd ∘ 1st )
Definition	df-homa 17933*	Definition of the hom-set extractor for arrows, which tags the morphisms of the underlying hom-set with domain and codomain, which can then be extracted using df-doma 17931 and df-coda 17932. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))
Definition	df-arw 17934	Definition of the set of arrows of a category. We will use the term "arrow" to denote a morphism tagged with its domain and codomain, as opposed to Hom, which allows hom-sets for distinct objects to overlap. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ Arrow = (𝑐 ∈ Cat ↦ ∪ ran (Homa‘𝑐))
Theorem	homarcl 17935	Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐶 ∈ Cat)
Theorem	homafval 17936*	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ (𝐵 × 𝐵) ↦ ({𝑥} × (𝐽‘𝑥))))
Theorem	homaf 17937	Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐻:(𝐵 × 𝐵)⟶𝒫 ((𝐵 × 𝐵) × V))
Theorem	homaval 17938	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = ({⟨𝑋, 𝑌⟩} × (𝑋𝐽𝑌)))
Theorem	elhoma 17939	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍(𝑋𝐻𝑌)𝐹 ↔ (𝑍 = ⟨𝑋, 𝑌⟩ ∧ 𝐹 ∈ (𝑋𝐽𝑌))))
Theorem	elhomai 17940	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    ⇒   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩(𝑋𝐻𝑌)𝐹)
Theorem	elhomai2 17941	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐽 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    ⇒   ⊢ (𝜑 → ⟨𝑋, 𝑌, 𝐹⟩ ∈ (𝑋𝐻𝑌))
Theorem	homarcl2 17942	Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
Theorem	homarel 17943	An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ Rel (𝑋𝐻𝑌)
Theorem	homa1 17944	The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝑍(𝑋𝐻𝑌)𝐹 → 𝑍 = ⟨𝑋, 𝑌⟩)
Theorem	homahom2 17945	The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝑍(𝑋𝐻𝑌)𝐹 → 𝐹 ∈ (𝑋𝐽𝑌))
Theorem	homahom 17946	The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (2nd ‘𝐹) ∈ (𝑋𝐽𝑌))
Theorem	homadm 17947	The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (doma‘𝐹) = 𝑋)
Theorem	homacd 17948	The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌)
Theorem	homadmcd 17949	Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹 = ⟨𝑋, 𝑌, (2nd ‘𝐹)⟩)
Theorem	arwval 17950	The set of arrows is the union of all the disjointified hom-sets. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ 𝐴 = ∪ ran 𝐻
Theorem	arwrcl 17951	The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐶 ∈ Cat)
Theorem	arwhoma 17952	An arrow is contained in the hom-set corresponding to its domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹 ∈ ((doma‘𝐹)𝐻(coda‘𝐹)))
Theorem	homarw 17953	A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝑋𝐻𝑌) ⊆ 𝐴
Theorem	arwdm 17954	The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (doma‘𝐹) ∈ 𝐵)
Theorem	arwcd 17955	The codomain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (coda‘𝐹) ∈ 𝐵)
Theorem	dmaf 17956	The domain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (doma ↾ 𝐴):𝐴⟶𝐵
Theorem	cdaf 17957	The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (coda ↾ 𝐴):𝐴⟶𝐵
Theorem	arwhom 17958	The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (2nd ‘𝐹) ∈ ((doma‘𝐹)𝐽(coda‘𝐹)))
Theorem	arwdmcd 17959	Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹 = ⟨(doma‘𝐹), (coda‘𝐹), (2nd ‘𝐹)⟩)
8.2.1  Identity and composition for arrows
Syntax	cida 17960	Extend class notation to include identity for arrows.
class Ida
Syntax	ccoa 17961	Extend class notation to include composition for arrows.
class compa
Definition	df-ida 17962*	Definition of the identity arrow, which is just the identity morphism tagged with its domain and codomain. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
⊢ Ida = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))
Definition	df-coa 17963*	Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a quinary operation like the regular composition in a category comp. Instead, it is a partial binary operation on arrows, which is defined when the domain of the first arrow matches the codomain of the second. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ compa = (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ ⟨(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(⟨(doma‘𝑓), (doma‘𝑔)⟩(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))⟩))
Theorem	idafval 17964*	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵 ↦ ⟨𝑥, 𝑥, ( 1 ‘𝑥)⟩))
Theorem	idaval 17965	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) = ⟨𝑋, 𝑋, ( 1 ‘𝑋)⟩)
Theorem	ida2 17966	Morphism part of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐼‘𝑋)) = ( 1 ‘𝑋))
Theorem	idahom 17967	Domain and codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐻 = (Homa‘𝐶)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐻𝑋))
Theorem	idadm 17968	Domain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (doma‘(𝐼‘𝑋)) = 𝑋)
Theorem	idacd 17969	Codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (coda‘(𝐼‘𝑋)) = 𝑋)
Theorem	idaf 17970	The identity arrow function is a function from objects to arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐼 = (Ida‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝜑 → 𝐼:𝐵⟶𝐴)
Theorem	coafval 17971*	The value of the composition of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    &   ⊢ ∙ = (comp‘𝐶)    ⇒   ⊢ · = (𝑔 ∈ 𝐴, 𝑓 ∈ {ℎ ∈ 𝐴 ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ ⟨(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(⟨(doma‘𝑓), (doma‘𝑔)⟩ ∙ (coda‘𝑔))(2nd ‘𝑓))⟩)
Theorem	eldmcoa 17972	A pair ⟨𝐺, 𝐹⟩ is in the domain of the arrow composition, if the domain of 𝐺 equals the codomain of 𝐹. (In this case we say 𝐺 and 𝐹 are composable.) (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ (𝐺dom · 𝐹 ↔ (𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ (coda‘𝐹) = (doma‘𝐺)))
Theorem	dmcoass 17973	The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ dom · ⊆ (𝐴 × 𝐴)
Theorem	homdmcoa 17974	If 𝐹:𝑋⟶𝑌 and 𝐺:𝑌⟶𝑍, then 𝐺 and 𝐹 are composable. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → 𝐺dom · 𝐹)
Theorem	coaval 17975	Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ ∙ = (comp‘𝐶)    ⇒   ⊢ (𝜑 → (𝐺 · 𝐹) = ⟨𝑋, 𝑍, ((2nd ‘𝐺)(⟨𝑋, 𝑌⟩ ∙ 𝑍)(2nd ‘𝐹))⟩)
Theorem	coa2 17976	The morphism part of arrow composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ ∙ = (comp‘𝐶)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐺 · 𝐹)) = ((2nd ‘𝐺)(⟨𝑋, 𝑌⟩ ∙ 𝑍)(2nd ‘𝐹)))
Theorem	coahom 17977	The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺 · 𝐹) ∈ (𝑋𝐻𝑍))
Theorem	coapm 17978	Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ · = (compa‘𝐶)    &   ⊢ 𝐴 = (Arrow‘𝐶)    ⇒   ⊢ · ∈ (𝐴 ↑pm (𝐴 × 𝐴))
Theorem	arwlid 17979	Left identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ · = (compa‘𝐶)    &   ⊢ 1 = (Ida‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (( 1 ‘𝑌) · 𝐹) = 𝐹)
Theorem	arwrid 17980	Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ · = (compa‘𝐶)    &   ⊢ 1 = (Ida‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (𝐹 · ( 1 ‘𝑋)) = 𝐹)
Theorem	arwass 17981	Associativity of composition in a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝐻 = (Homa‘𝐶)    &   ⊢ · = (compa‘𝐶)    &   ⊢ 1 = (Ida‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑊))    ⇒   ⊢ (𝜑 → ((𝐾 · 𝐺) · 𝐹) = (𝐾 · (𝐺 · 𝐹)))
8.3  Examples of categories
8.3.1  The category of sets
Syntax	csetc 17982	Extend class notation to include the category Set.
class SetCat
Definition	df-setc 17983*	Definition of the category Set, relativized to a subset 𝑢. Example 3.3(1) of [Adamek] p. 22. This is the category of all sets in 𝑢 and functions between these sets. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by FL, 8-Nov-2013.) (Revised by Mario Carneiro, 3-Jan-2017.)
⊢ SetCat = (𝑢 ∈ V ↦ {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ (𝑦 ↑m 𝑥))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩})
Theorem	setcval 17984*	Value of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ (𝑦 ↑m 𝑥)))    &   ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓))))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝑈⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	setcbas 17985	Set of objects of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
Theorem	setchomfval 17986*	Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ (𝑦 ↑m 𝑥)))
Theorem	setchom 17987	Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑌 ↑m 𝑋))
Theorem	elsetchom 17988	A morphism of sets is a function. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ↔ 𝐹:𝑋⟶𝑌))
Theorem	setccofval 17989*	Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓))))
Theorem	setcco 17990	Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐺:𝑌⟶𝑍)    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘ 𝐹))
Theorem	setccatid 17991*	Lemma for setccat 17992. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝑈 ↦ ( I ↾ 𝑥))))
Theorem	setccat 17992	The category of sets is a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	setcid 17993	The identity arrow in the category of sets is the identity function. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑋))
Theorem	setcmon 17994	A monomorphism of sets is an injection. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝑀 = (Mono‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ 𝐹:𝑋–1-1→𝑌))
Theorem	setcepi 17995	An epimorphism of sets is a surjection. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ (𝜑 → 2o ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ 𝐹:𝑋–onto→𝑌))
Theorem	setcsect 17996	A section in the category of sets, written out. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹:𝑋⟶𝑌 ∧ 𝐺:𝑌⟶𝑋 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝑋))))
Theorem	setcinv 17997	An inverse in the category of sets is the converse operation. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹:𝑋–1-1-onto→𝑌 ∧ 𝐺 = ◡𝐹)))
Theorem	setciso 17998	An isomorphism in the category of sets is a bijection. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹:𝑋–1-1-onto→𝑌))
Theorem	resssetc 17999	The restriction of the category of sets to a subset is the category of sets in the subset. Thus, the SetCat‘𝑈 categories for different 𝑈 are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ 𝐷 = (SetCat‘𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ((Homf ‘(𝐶 ↾s 𝑉)) = (Homf ‘𝐷) ∧ (compf‘(𝐶 ↾s 𝑉)) = (compf‘𝐷)))
Theorem	funcsetcres2 18000	A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝐶 = (SetCat‘𝑈)    &   ⊢ 𝐷 = (SetCat‘𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → (𝐸 Func 𝐷) ⊆ (𝐸 Func 𝐶))