P. 179 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17801-17900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isofval 17801*	Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017.)
⊢ (𝐶 ∈ Cat → (Iso‘𝐶) = ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶)))
Theorem	invffval 17802*	Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝑆𝑦) ∩ ◡(𝑦𝑆𝑥))))
Theorem	invfval 17803	Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑁𝑌) = ((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋)))
Theorem	isinv 17804	Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹)))
Theorem	invss 17805	The inverse relation is a relation between morphisms 𝐹:𝑋⟶𝑌 and their inverses 𝐺:𝑌⟶𝑋. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑁𝑌) ⊆ ((𝑋𝐻𝑌) × (𝑌𝐻𝑋)))
Theorem	invsym 17806	The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐺(𝑌𝑁𝑋)𝐹))
Theorem	invsym2 17807	The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ◡(𝑋𝑁𝑌) = (𝑌𝑁𝑋))
Theorem	invfun 17808	The inverse relation is a function, which is to say that every morphism has at most one inverse. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → Fun (𝑋𝑁𝑌))
Theorem	isoval 17809	The isomorphisms are the domain of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 21-May-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌))
Theorem	inviso1 17810	If 𝐺 is an inverse to 𝐹, then 𝐹 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))
Theorem	inviso2 17811	If 𝐺 is an inverse to 𝐹, then 𝐺 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑋))
Theorem	invf 17812	The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑁𝑌):(𝑋𝐼𝑌)⟶(𝑌𝐼𝑋))
Theorem	invf1o 17813	The inverse relation is a bijection from isomorphisms to isomorphisms. This means that every isomorphism 𝐹 ∈ (𝑋𝐼𝑌) has a unique inverse, denoted by ((Inv‘𝐶)‘𝐹). Remark 3.12 of [Adamek] p. 28. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑁𝑌):(𝑋𝐼𝑌)–1-1-onto→(𝑌𝐼𝑋))
Theorem	invinv 17814	The inverse of the inverse of an isomorphism is itself. Proposition 3.14(1) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → ((𝑌𝑁𝑋)‘((𝑋𝑁𝑌)‘𝐹)) = 𝐹)
Theorem	invco 17815	The composition of two isomorphisms is an isomorphism, and the inverse is the composition of the individual inverses. Proposition 3.14(2) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)(𝑋𝑁𝑍)(((𝑋𝑁𝑌)‘𝐹)(⟨𝑍, 𝑌⟩ · 𝑋)((𝑌𝑁𝑍)‘𝐺)))
Theorem	dfiso2 17816*	Alternate definition of an isomorphism of a category, according to definition 3.8 in [Adamek] p. 28. (Contributed by AV, 10-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ ⚬ = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)    &   ⊢ ∗ = (⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌))))
Theorem	dfiso3 17817*	Alternate definition of an isomorphism of a category as a section in both directions. (Contributed by AV, 11-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)(𝑔(𝑌𝑆𝑋)𝐹 ∧ 𝐹(𝑋𝑆𝑌)𝑔)))
Theorem	inveq 17818	If there are two inverses of a morphism, these inverses are equal. Corollary 3.11 of [Adamek] p. 28. (Contributed by AV, 10-Apr-2020.) (Revised by AV, 3-Jul-2022.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹(𝑋𝑁𝑌)𝐺 ∧ 𝐹(𝑋𝑁𝑌)𝐾) → 𝐺 = 𝐾))
Theorem	isofn 17819	The function value of the function returning the isomorphisms of a category is a function over the square product of the base set of the category. (Contributed by AV, 5-Apr-2020.)
⊢ (𝐶 ∈ Cat → (Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)))
Theorem	isohom 17820	An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋𝐻𝑌))
Theorem	isoco 17821	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 17822	A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝑇 = (Sect‘𝑂)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑇𝑌)𝐺 ↔ 𝐺(𝑋𝑆𝑌)𝐹))
Theorem	oppcsect2 17823	A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝑇 = (Sect‘𝑂)    ⇒   ⊢ (𝜑 → (𝑋𝑇𝑌) = ◡(𝑋𝑆𝑌))
Theorem	oppcinv 17824	An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Inv‘𝐶)    &   ⊢ 𝐽 = (Inv‘𝑂)    ⇒   ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝑌𝐼𝑋))
Theorem	oppciso 17825	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 17826	If 𝐹 is a section of 𝐺, then 𝐹 is a monomorphism. 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 17827	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 17828	If 𝐹 is a section of 𝐺, then 𝐺 is an epimorphism. 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 17829	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 17830	The identity is a section of itself. (Contributed by AV, 8-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Sect‘𝐶)𝑋)(𝐼‘𝑋))
Theorem	invid 17831	The inverse of the identity is the identity. (Contributed by AV, 8-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Inv‘𝐶)𝑋)(𝐼‘𝑋))
Theorem	idiso 17832	The identity is an isomorphism. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 8-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋(Iso‘𝐶)𝑋))
Theorem	idinv 17833	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 17834	The inverse of an isomorphism 𝐹 (which is unique because of invf 17812 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 17835	The inverse of an isomorphism is invers to the isomorphism. (Contributed by AV, 9-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹))
Theorem	invcoisoid 17836	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 17837	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 17838	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 17840). It is shown that this relation is an equivalence relation, see cicer 17850.
Syntax	ccic 17839	Extend class notation to include the category isomorphism relation.
class ≃𝑐
Definition	df-cic 17840	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 19278. (Contributed by AV, 4-Apr-2020.)
⊢ ≃𝑐 = (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅))
Theorem	cicfval 17841	The set of isomorphic objects of the category 𝑐. (Contributed by AV, 4-Apr-2020.)
⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) = ((Iso‘𝐶) supp ∅))
Theorem	brcic 17842	The relation "is isomorphic to" for categories. (Contributed by AV, 5-Apr-2020.)
⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ (𝑋𝐼𝑌) ≠ ∅))
Theorem	cic 17843*	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 17844	Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020.)
⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)
Theorem	cicref 17845	Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (Base‘𝐶)) → 𝑂( ≃𝑐 ‘𝐶)𝑂)
Theorem	ciclcl 17846	Isomorphism implies the left side is an object. (Contributed by AV, 5-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑅 ∈ (Base‘𝐶))
Theorem	cicrcl 17847	Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆 ∈ (Base‘𝐶))
Theorem	cicsym 17848	Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆( ≃𝑐 ‘𝐶)𝑅)
Theorem	cictr 17849	Isomorphism is transitive. (Contributed by AV, 5-Apr-2020.)
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆 ∧ 𝑆( ≃𝑐 ‘𝐶)𝑇) → 𝑅( ≃𝑐 ‘𝐶)𝑇)
Theorem	cicer 17850	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 17851	Extend class notation to include the subset relation for subcategories.
class ⊆cat
Syntax	cresc 17852	Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms).
class ↾cat
Syntax	csubc 17853	Extend class notation to include the collection of subcategories of a category.
class Subcat
Definition	df-ssc 17854*	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 17856, 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 17855*	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 17856*	(Subcat‘𝐶) is the set of all the subcategory specifications of the category 𝐶. Like df-subg 19141, 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 17855) 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 17857	The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ Rel ⊆cat
Theorem	brssc 17858*	The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))
Theorem	sscpwex 17859*	An analogue of pwex 5380 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 17860	Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat)
Theorem	sscfn1 17861	The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 ⊆cat 𝐽)    &   ⊢ (𝜑 → 𝑆 = dom dom 𝐻)    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
Theorem	sscfn2 17862	The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 ⊆cat 𝐽)    &   ⊢ (𝜑 → 𝑇 = dom dom 𝐽)    ⇒   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))
Theorem	ssclem 17863	Lemma for ssc1 17865 and similar theorems. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    ⇒   ⊢ (𝜑 → (𝐻 ∈ V ↔ 𝑆 ∈ V))
Theorem	isssc 17864*	Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
Theorem	ssc1 17865	Infer subset relation on objects from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))    &   ⊢ (𝜑 → 𝐻 ⊆cat 𝐽)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝑇)
Theorem	ssc2 17866	Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐻 ⊆cat 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) ⊆ (𝑋𝐽𝑌))
Theorem	sscres 17867	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 17868	The subcategory subset relation is reflexive. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → 𝐻 ⊆cat 𝐻)
Theorem	ssctr 17869	The subcategory subset relation is transitive. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶) → 𝐴 ⊆cat 𝐶)
Theorem	ssceq 17870	The subcategory subset relation is antisymmetric. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴) → 𝐴 = 𝐵)
Theorem	rescval 17871	Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    ⇒   ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → 𝐷 = ((𝐶 ↾s dom dom 𝐻) sSet ⟨(Hom ‘ndx), 𝐻⟩))
Theorem	rescval2 17872	Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    ⇒   ⊢ (𝜑 → 𝐷 = ((𝐶 ↾s 𝑆) sSet ⟨(Hom ‘ndx), 𝐻⟩))
Theorem	rescbas 17873	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 17874	Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐷))
Theorem	reschomf 17875	Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐻)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐻 = (Homf ‘𝐷))
Theorem	rescco 17876	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 17877	Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 9-Nov-2024.)
⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽))
Theorem	rescabsOLD 17878	Obsolete version of seqp1d 14059 as of 10-Nov-2024. Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽))
Theorem	rescabs2 17879	Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐶 ↾s 𝑆) ↾cat 𝐽) = (𝐶 ↾cat 𝐽))
Theorem	issubc 17880*	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 17881*	Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    ⇒   ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
Theorem	0ssc 17882	For any category 𝐶, the empty set is a subcategory subset of 𝐶. (Contributed by AV, 23-Apr-2020.)
⊢ (𝐶 ∈ Cat → ∅ ⊆cat (Homf ‘𝐶))
Theorem	0subcat 17883	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 17884	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 17885	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 17886	An element in the set of subcategories is a binary function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝑆 = dom dom 𝐽)    ⇒   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))
Theorem	subcss1 17887	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 17888	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 17889	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 17890	A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐽𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐽𝑍))
Theorem	subccatid 17891*	A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆))    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑥 ∈ 𝑆 ↦ ( 1 ‘𝑥))))
Theorem	subcid 17892	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 17893	A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    ⇒   ⊢ (𝜑 → 𝐷 ∈ Cat)
Theorem	issubc3 17894*	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 18817, 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 17895	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 17896	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 17897	A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾s 𝑆) ∈ Cat)
Theorem	subsubc 17898	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 17899	Extend class notation with the class of all functors.
class Func
Syntax	cidfu 17900	Extend class notation with identity functor.
class idfunc