P. 178 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17701-17800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isohom 17701	An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋𝐻𝑌))
Theorem	isoco 17702	The composition of two isomorphisms is an isomorphism. Proposition 3.14(2) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐼𝑍))
Theorem	oppcsect 17703	A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝑇 = (Sect‘𝑂)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑇𝑌)𝐺 ↔ 𝐺(𝑋𝑆𝑌)𝐹))
Theorem	oppcsect2 17704	A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝑇 = (Sect‘𝑂)    ⇒   ⊢ (𝜑 → (𝑋𝑇𝑌) = ◡(𝑋𝑆𝑌))
Theorem	oppcinv 17705	An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Inv‘𝐶)    &   ⊢ 𝐽 = (Inv‘𝑂)    ⇒   ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝑌𝐼𝑋))
Theorem	oppciso 17706	An isomorphism in the opposite category. See also remark 3.9 in [Adamek] p. 28. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝐽 = (Iso‘𝑂)    ⇒   ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝑌𝐼𝑋))
Theorem	sectmon 17707	If 𝐹 is a section of 𝐺, then 𝐹 is a monomorphism. Proposition 7.35 of [Adamek] p. 110. A monomorphism that arises from a section is also known as a split monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌))
Theorem	monsect 17708	If 𝐹 is a monomorphism and 𝐺 is a section of 𝐹, then 𝐺 is an inverse of 𝐹 and they are both isomorphisms. This is also stated as "a monomorphism which is also a split epimorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌))    &   ⊢ (𝜑 → 𝐺(𝑌𝑆𝑋)𝐹)    ⇒   ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺)
Theorem	sectepi 17709	If 𝐹 is a section of 𝐺, then 𝐺 is an epimorphism. Proposition 7.42 of [Adamek] p. 112. An epimorphism that arises from a section is also known as a split epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐸𝑋))
Theorem	episect 17710	If 𝐹 is an epimorphism and 𝐹 is a section of 𝐺, then 𝐺 is an inverse of 𝐹 and they are both isomorphisms. This is also stated as "an epimorphism which is also a split monomorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐸𝑌))    &   ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺)
Theorem	sectid 17711	The identity is a section of itself. (Contributed by AV, 8-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Sect‘𝐶)𝑋)(𝐼‘𝑋))
Theorem	invid 17712	The inverse of the identity is the identity. (Contributed by AV, 8-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Inv‘𝐶)𝑋)(𝐼‘𝑋))
Theorem	idiso 17713	The identity is an isomorphism. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 8-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋(Iso‘𝐶)𝑋))
Theorem	idinv 17714	The inverse of the identity is the identity. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 9-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋(Inv‘𝐶)𝑋)‘(𝐼‘𝑋)) = (𝐼‘𝑋))
Theorem	invisoinvl 17715	The inverse of an isomorphism 𝐹 (which is unique because of invf 17693 and is therefore denoted by ((𝑋𝑁𝑌)‘𝐹), see also remark 3.12 in [Adamek] p. 28) is invers to the isomorphism. (Contributed by AV, 9-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → ((𝑋𝑁𝑌)‘𝐹)(𝑌𝑁𝑋)𝐹)
Theorem	invisoinvr 17716	The inverse of an isomorphism is invers to the isomorphism. (Contributed by AV, 9-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹))
Theorem	invcoisoid 17717	The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 5-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ ⚬ = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)    ⇒   ⊢ (𝜑 → (((𝑋𝑁𝑌)‘𝐹) ⚬ 𝐹) = ( 1 ‘𝑋))
Theorem	isocoinvid 17718	The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 10-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ ⚬ = (⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ⚬ ((𝑋𝑁𝑌)‘𝐹)) = ( 1 ‘𝑌))
Theorem	rcaninv 17719	Right cancellation of an inverse of an isomorphism. (Contributed by AV, 5-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑌(Iso‘𝐶)𝑋))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑍))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑌(Hom ‘𝐶)𝑍))    &   ⊢ 𝑅 = ((𝑌𝑁𝑋)‘𝐹)    &   ⊢ ⚬ = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑍)    ⇒   ⊢ (𝜑 → ((𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅) → 𝐺 = 𝐻))
8.1.5  Isomorphic objects In this subsection, the "is isomorphic to" relation between objects of a category ≃𝑐 is defined (see df-cic 17721). It is shown that this relation is an equivalence relation, see cicer 17731.
Syntax	ccic 17720	Extend class notation to include the category isomorphism relation.
class ≃𝑐
Definition	df-cic 17721	Function returning the set of isomorphic objects for each category 𝑐. Definition 3.15 of [Adamek] p. 29. Analogous to the definition of the group isomorphism relation ≃𝑔, see df-gic 19157. (Contributed by AV, 4-Apr-2020.)
⊢ ≃𝑐 = (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅))
Theorem	cicfval 17722	The set of isomorphic objects of the category 𝑐. (Contributed by AV, 4-Apr-2020.)
⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) = ((Iso‘𝐶) supp ∅))
Theorem	brcic 17723	The relation "is isomorphic to" for categories. (Contributed by AV, 5-Apr-2020.)
⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ (𝑋𝐼𝑌) ≠ ∅))
Theorem	cic 17724*	Objects 𝑋 and 𝑌 in a category are isomorphic provided that there is an isomorphism 𝑓:𝑋⟶𝑌, see definition 3.15 of [Adamek] p. 29. (Contributed by AV, 4-Apr-2020.)
⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓 𝑓 ∈ (𝑋𝐼𝑌)))
Theorem	brcici 17725	Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020.)
⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)
Theorem	cicref 17726	Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (Base‘𝐶)) → 𝑂( ≃𝑐 ‘𝐶)𝑂)
Theorem	ciclcl 17727	Isomorphism implies the left side is an object. (Contributed by AV, 5-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑅 ∈ (Base‘𝐶))
Theorem	cicrcl 17728	Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆 ∈ (Base‘𝐶))
Theorem	cicsym 17729	Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆( ≃𝑐 ‘𝐶)𝑅)
Theorem	cictr 17730	Isomorphism is transitive. (Contributed by AV, 5-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆 ∧ 𝑆( ≃𝑐 ‘𝐶)𝑇) → 𝑅( ≃𝑐 ‘𝐶)𝑇)
Theorem	cicer 17731	Isomorphism is an equivalence relation on objects of a category. Remark 3.16 in [Adamek] p. 29. (Contributed by AV, 5-Apr-2020.)
⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) Er (Base‘𝐶))
8.1.6  Subcategories
Syntax	cssc 17732	Extend class notation to include the subset relation for subcategories.
class ⊆cat
Syntax	cresc 17733	Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms).
class ↾cat
Syntax	csubc 17734	Extend class notation to include the collection of subcategories of a category.
class Subcat
Definition	df-ssc 17735*	Define the subset relation for subcategories. Despite the name, this is not really a "category-aware" definition, which is to say it makes no explicit references to homsets or composition; instead this is a subset-like relation on the functions that are used as subcategory specifications in df-subc 17737, which makes it play an analogous role to the subset relation applied to the subgroups of a group. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ⊆cat = {⟨ℎ, 𝑗⟩ ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))}
Definition	df-resc 17736*	Define the restriction of a category to a given set of arrows. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ↾cat = (𝑐 ∈ V, ℎ ∈ V ↦ ((𝑐 ↾s dom dom ℎ) sSet ⟨(Hom ‘ndx), ℎ⟩))
Definition	df-subc 17737*	(Subcat‘𝐶) is the set of all the subcategory specifications of the category 𝐶. Like df-subg 19020, this is not actually a collection of categories (as in definition 4.1(a) of [Adamek] p. 48), but only sets which when given operations from the base category (using df-resc 17736) form a category. All the objects and all the morphisms of the subcategory belong to the supercategory. The identity of an object, the domain and the codomain of a morphism are the same in the subcategory and the supercategory. The composition of the subcategory is a restriction of the composition of the supercategory. (Contributed by FL, 17-Sep-2009.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ Subcat = (𝑐 ∈ Cat ↦ {ℎ ∣ (ℎ ⊆cat (Homf ‘𝑐) ∧ [dom dom ℎ / 𝑠]∀𝑥 ∈ 𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥) ∧ ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)))})
Theorem	sscrel 17738	The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ Rel ⊆cat
Theorem	brssc 17739*	The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))
Theorem	sscpwex 17740*	An analogue of pwex 5322 for the subcategory subset relation: The collection of subcategory subsets of a given set 𝐽 is a set. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ {ℎ ∣ ℎ ⊆cat 𝐽} ∈ V
Theorem	subcrcl 17741	Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat)
Theorem	sscfn1 17742	The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 ⊆cat 𝐽)    &   ⊢ (𝜑 → 𝑆 = dom dom 𝐻)    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
Theorem	sscfn2 17743	The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 ⊆cat 𝐽)    &   ⊢ (𝜑 → 𝑇 = dom dom 𝐽)    ⇒   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))
Theorem	ssclem 17744	Lemma for ssc1 17746 and similar theorems. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    ⇒   ⊢ (𝜑 → (𝐻 ∈ V ↔ 𝑆 ∈ V))
Theorem	isssc 17745*	Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
Theorem	ssc1 17746	Infer subset relation on objects from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))    &   ⊢ (𝜑 → 𝐻 ⊆cat 𝐽)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝑇)
Theorem	ssc2 17747	Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐻 ⊆cat 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) ⊆ (𝑋𝐽𝑌))
Theorem	sscres 17748	Any function restricted to a square domain is a subcategory subset of the original. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → (𝐻 ↾ (𝑇 × 𝑇)) ⊆cat 𝐻)
Theorem	sscid 17749	The subcategory subset relation is reflexive. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → 𝐻 ⊆cat 𝐻)
Theorem	ssctr 17750	The subcategory subset relation is transitive. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶) → 𝐴 ⊆cat 𝐶)
Theorem	ssceq 17751	The subcategory subset relation is antisymmetric. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴) → 𝐴 = 𝐵)
Theorem	rescval 17752	Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    ⇒   ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → 𝐷 = ((𝐶 ↾s dom dom 𝐻) sSet ⟨(Hom ‘ndx), 𝐻⟩))
Theorem	rescval2 17753	Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    ⇒   ⊢ (𝜑 → 𝐷 = ((𝐶 ↾s 𝑆) sSet ⟨(Hom ‘ndx), 𝐻⟩))
Theorem	rescbas 17754	Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by AV, 18-Oct-2024.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝑆 = (Base‘𝐷))
Theorem	reschom 17755	Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐷))
Theorem	reschomf 17756	Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐻 = (Homf ‘𝐷))
Theorem	rescco 17757	Composition in the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (comp‘𝐷))
Theorem	rescabs 17758	Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 9-Nov-2024.)
⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽))
Theorem	rescabs2 17759	Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐶 ↾s 𝑆) ↾cat 𝐽) = (𝐶 ↾cat 𝐽))
Theorem	issubc 17760*	Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑆 = dom dom 𝐽)    ⇒   ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
Theorem	issubc2 17761*	Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    ⇒   ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
Theorem	0ssc 17762	For any category 𝐶, the empty set is a subcategory subset of 𝐶. (Contributed by AV, 23-Apr-2020.)
⊢ (𝐶 ∈ Cat → ∅ ⊆cat (Homf ‘𝐶))
Theorem	0subcat 17763	For any category 𝐶, the empty set is a (full) subcategory of 𝐶, see example 4.3(1.a) in [Adamek] p. 48. (Contributed by AV, 23-Apr-2020.)
⊢ (𝐶 ∈ Cat → ∅ ∈ (Subcat‘𝐶))
Theorem	catsubcat 17764	For any category 𝐶, 𝐶 itself is a (full) subcategory of 𝐶, see example 4.3(1.b) in [Adamek] p. 48. (Contributed by AV, 23-Apr-2020.)
⊢ (𝐶 ∈ Cat → (Homf ‘𝐶) ∈ (Subcat‘𝐶))
Theorem	subcssc 17765	An element in the set of subcategories is a subset of the category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ 𝐻 = (Homf ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐽 ⊆cat 𝐻)
Theorem	subcfn 17766	An element in the set of subcategories is a binary function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝑆 = dom dom 𝐽)    ⇒   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))
Theorem	subcss1 17767	The objects of a subcategory are a subset of the objects of the original. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
Theorem	subcss2 17768	The morphisms of a subcategory are a subset of the morphisms of the original. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋𝐽𝑌) ⊆ (𝑋𝐻𝑌))
Theorem	subcidcl 17769	The identity of the original category is contained in each subcategory. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐽𝑋))
Theorem	subccocl 17770	A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐽𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐽𝑍))
Theorem	subccatid 17771*	A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑥 ∈ 𝑆 ↦ ( 1 ‘𝑥))))
Theorem	subcid 17772	The identity in a subcategory is the same as the original category. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = ((Id‘𝐷)‘𝑋))
Theorem	subccat 17773	A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    ⇒   ⊢ (𝜑 → 𝐷 ∈ Cat)
Theorem	issubc3 17774*	Alternate definition of a subcategory, as a subset of the category which is itself a category. The assumption that the identity be closed is necessary just as in the case of a monoid, issubm2 18696, for the same reasons, since categories are a generalization of monoids. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    ⇒   ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)))
Theorem	fullsubc 17775	The full subcategory generated by a subset of objects is the category with these objects and the same morphisms as the original. The result is always a subcategory (and it is full, meaning that all morphisms of the original category between objects in the subcategory is also in the subcategory), see definition 4.1(2) of [Adamek] p. 48. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ↾ (𝑆 × 𝑆)) ∈ (Subcat‘𝐶))
Theorem	fullresc 17776	The category formed by structure restriction is the same as the category restriction. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ 𝐷 = (𝐶 ↾s 𝑆)    &   ⊢ 𝐸 = (𝐶 ↾cat (𝐻 ↾ (𝑆 × 𝑆)))    ⇒   ⊢ (𝜑 → ((Homf ‘𝐷) = (Homf ‘𝐸) ∧ (compf‘𝐷) = (compf‘𝐸)))
Theorem	resscat 17777	A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾s 𝑆) ∈ Cat)
Theorem	subsubc 17778	A subcategory of a subcategory is a subcategory. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    ⇒   ⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻)))
8.1.7  Functors
Syntax	cfunc 17779	Extend class notation with the class of all functors.
class Func
Syntax	cidfu 17780	Extend class notation with identity functor.
class idfunc
Syntax	ccofu 17781	Extend class notation with functor composition.
class ∘func
Syntax	cresf 17782	Extend class notation to include restriction of a functor to a subcategory.
class ↾f
Definition	df-func 17783*	Function returning all the functors from a category 𝑡 to a category 𝑢. Definition 3.17 of [Adamek] p. 29, and definition in [Lang] p. 62 ("covariant functor"). Intuitively a functor associates any morphism of 𝑡 to a morphism of 𝑢, any object of 𝑡 to an object of 𝑢, and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of 𝑡 to an object of 𝑢 we write it associates any identity of 𝑡 to an identity of 𝑢 which simplifies the definition. According to remark 3.19 in [Adamek] p. 30, "a functor F : A -> B is technically a family of functions; one from Ob(A) to Ob(B) [here: f, called "the object part" in the following], and for each pair (A,A') of A-objects, one from hom(A,A') to hom(FA, FA') [here: g, called "the morphism part" in the following]". (Contributed by FL, 10-Feb-2008.) (Revised by Mario Carneiro, 2-Jan-2017.)
⊢ Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
Definition	df-idfu 17784*	Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ idfunc = (𝑡 ∈ Cat ↦ ⦋(Base‘𝑡) / 𝑏⦌⟨( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))⟩)
Definition	df-cofu 17785*	Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ ∘func = (𝑔 ∈ V, 𝑓 ∈ V ↦ ⟨((1st ‘𝑔) ∘ (1st ‘𝑓)), (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))⟩)
Definition	df-resf 17786*	Define the restriction of a functor to a subcategory (analogue of df-res 5635). (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ↾f = (𝑓 ∈ V, ℎ ∈ V ↦ ⟨((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))⟩)
Theorem	relfunc 17787	The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ Rel (𝐷 Func 𝐸)
Theorem	funcrcl 17788	Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝐹 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
Theorem	isfunc 17789*	Value of the set of functors between two categories. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ · = (comp‘𝐷)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    ⇒   ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
Theorem	isfuncd 17790*	Deduce that an operation is a functor of categories. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ · = (comp‘𝐷)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧))) → ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))    ⇒   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
Theorem	funcf1 17791	The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
Theorem	funcixp 17792*	The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
Theorem	funcf2 17793	The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	funcfn2 17794	The morphism part of a functor is a function. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵))
Theorem	funcid 17795	A functor maps each identity to the corresponding identity in the target category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝐹‘𝑋)))
Theorem	funcco 17796	A functor maps composition in the source category to composition in the target. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐷)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌⟩ · 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀)))
Theorem	funcsect 17797	The image of a section under a functor is a section. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝑆 = (Sect‘𝐷)    &   ⊢ 𝑇 = (Sect‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀(𝑋𝑆𝑌)𝑁)    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝑇(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁))
Theorem	funcinv 17798	The image of an inverse under a functor is an inverse. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐼 = (Inv‘𝐷)    &   ⊢ 𝐽 = (Inv‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀(𝑋𝐼𝑌)𝑁)    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝐽(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁))
Theorem	funciso 17799	The image of an isomorphism under a functor is an isomorphism. Proposition 3.21 of [Adamek] p. 32. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐼 = (Iso‘𝐷)    &   ⊢ 𝐽 = (Iso‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	funcoppc 17800	A functor on categories yields a functor on the opposite categories (in the same direction), see definition 3.41 of [Adamek] p. 39. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝑂 Func 𝑃)tpos 𝐺)