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	fnhomeqhomf 17701	If the Hom-set operation is a function it is equal to the corresponding functionalized Hom-set operation. (Contributed by AV, 1-Mar-2020.)
⊢ 𝐹 = (Homf ‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐻 Fn (𝐵 × 𝐵) → 𝐹 = 𝐻)
Theorem	homfval 17702	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐹 = (Homf ‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑋𝐻𝑌))
Theorem	homffn 17703	The functionalized Hom-set operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐹 = (Homf ‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝐹 Fn (𝐵 × 𝐵)
Theorem	homfeq 17704*	Condition for two categories with the same base to have the same hom-sets. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → ((Homf ‘𝐶) = (Homf ‘𝐷) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) = (𝑥𝐽𝑦)))
Theorem	homfeqd 17705	If two structures have the same Hom slot, they have the same Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))    &   ⊢ (𝜑 → (Hom ‘𝐶) = (Hom ‘𝐷))    ⇒   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))
Theorem	homfeqbas 17706	Deduce equality of base sets from equality of Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    ⇒   ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))
Theorem	homfeqval 17707	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋𝐽𝑌))
Theorem	comfffval 17708*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))
Theorem	comffval 17709*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑂𝑍) = (𝑔 ∈ (𝑌𝐻𝑍), 𝑓 ∈ (𝑋𝐻𝑌) ↦ (𝑔(⟨𝑋, 𝑌⟩ · 𝑍)𝑓)))
Theorem	comfval 17710	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
Theorem	comfffval2 17711*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))
Theorem	comffval2 17712*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑂𝑍) = (𝑔 ∈ (𝑌𝐻𝑍), 𝑓 ∈ (𝑋𝐻𝑌) ↦ (𝑔(⟨𝑋, 𝑌⟩ · 𝑍)𝑓)))
Theorem	comfval2 17713	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
Theorem	comfffn 17714	The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝑂 Fn ((𝐵 × 𝐵) × 𝐵)
Theorem	comffn 17715	The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑂𝑍) Fn ((𝑌𝐻𝑍) × (𝑋𝐻𝑌)))
Theorem	comfeq 17716*	Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ · = (comp‘𝐶)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    ⇒   ⊢ (𝜑 → ((compf‘𝐶) = (compf‘𝐷) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)))
Theorem	comfeqd 17717	Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → (comp‘𝐶) = (comp‘𝐷))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))
Theorem	comfeqval 17718	Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ ∙ 𝑍)𝐹))
Theorem	catpropd 17719	Two structures with the same base, hom-sets and composition operation are either both categories or neither. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
Theorem	cidpropd 17720	Two structures with the same base, hom-sets and composition operation have the same identity function. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷))
8.1.2  Opposite category
Syntax	coppc 17721	The opposite category operation.
class oppCat
Definition	df-oppc 17722*	Define an opposite category, which is the same as the original category but with the direction of arrows the other way around. Definition 3.5 of [Adamek] p. 25. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ oppCat = (𝑓 ∈ V ↦ ((𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd ‘𝑢)⟩(comp‘𝑓)(1st ‘𝑢)))⟩))
Theorem	oppcval 17723*	Value of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ 𝑉 → 𝑂 = ((𝐶 sSet ⟨(Hom ‘ndx), tpos 𝐻⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (⟨𝑧, (2nd ‘𝑢)⟩ · (1st ‘𝑢)))⟩))
Theorem	oppchomfval 17724	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.)
⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ tpos 𝐻 = (Hom ‘𝑂)
Theorem	oppchom 17725	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝑋(Hom ‘𝑂)𝑌) = (𝑌𝐻𝑋)
Theorem	oppccofval 17726	Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩(comp‘𝑂)𝑍) = tpos (⟨𝑍, 𝑌⟩ · 𝑋))
Theorem	oppcco 17727	Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩(comp‘𝑂)𝑍)𝐹) = (𝐹(⟨𝑍, 𝑌⟩ · 𝑋)𝐺))
Theorem	oppcbas 17728	Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 18-Oct-2024.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	oppccatid 17729	Lemma for oppccat 17732. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧ (Id‘𝑂) = (Id‘𝐶)))
Theorem	oppchomf 17730	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    ⇒   ⊢ tpos 𝐻 = (Homf ‘𝑂)
Theorem	oppcid 17731	Identity function of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Id‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = 𝐵)
Theorem	oppccat 17732	An opposite category is a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
Theorem	2oppcbas 17733	The double opposite category has the same objects as the original category. Intended for use with property lemmas such as monpropd 17748. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝐵 = (Base‘(oppCat‘𝑂))
Theorem	2oppchomf 17734	The double opposite category has the same morphisms as the original category. Intended for use with property lemmas such as monpropd 17748. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (Homf ‘𝐶) = (Homf ‘(oppCat‘𝑂))
Theorem	2oppccomf 17735	The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd 17748. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (compf‘𝐶) = (compf‘(oppCat‘𝑂))
Theorem	oppchomfpropd 17736	If two categories have the same hom-sets, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    ⇒   ⊢ (𝜑 → (Homf ‘(oppCat‘𝐶)) = (Homf ‘(oppCat‘𝐷)))
Theorem	oppccomfpropd 17737	If two categories have the same hom-sets and composition, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    ⇒   ⊢ (𝜑 → (compf‘(oppCat‘𝐶)) = (compf‘(oppCat‘𝐷)))
Theorem	oppccatf 17738	oppCat restricted to Cat is a function from Cat to Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ (oppCat ↾ Cat):Cat⟶Cat
8.1.3  Monomorphisms and epimorphisms
Syntax	cmon 17739	Extend class notation with the class of all monomorphisms.
class Mono
Syntax	cepi 17740	Extend class notation with the class of all epimorphisms.
class Epi
Definition	df-mon 17741*	Function returning the monomorphisms of the category 𝑐. JFM CAT1 def. 10. (Contributed by FL, 5-Dec-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)
⊢ Mono = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}))
Definition	df-epi 17742	Function returning the epimorphisms of the category 𝑐. JFM CAT1 def. 11. (Contributed by FL, 8-Aug-2008.) (Revised by Mario Carneiro, 2-Jan-2017.)
⊢ Epi = (𝑐 ∈ Cat ↦ tpos (Mono‘(oppCat‘𝑐)))
Theorem	monfval 17743*	Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑀 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩ · 𝑦)𝑔))}))
Theorem	ismon 17744*	Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(⟨𝑧, 𝑋⟩ · 𝑌)𝑔)))))
Theorem	ismon2 17745*	Write out the monomorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑧𝐻𝑋)∀ℎ ∈ (𝑧𝐻𝑋)((𝐹(⟨𝑧, 𝑋⟩ · 𝑌)𝑔) = (𝐹(⟨𝑧, 𝑋⟩ · 𝑌)ℎ) → 𝑔 = ℎ))))
Theorem	monhom 17746	A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝑀𝑌) ⊆ (𝑋𝐻𝑌))
Theorem	moni 17747	Property of a monomorphism. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋))    ⇒   ⊢ (𝜑 → ((𝐹(⟨𝑍, 𝑋⟩ · 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋⟩ · 𝑌)𝐾) ↔ 𝐺 = 𝐾))
Theorem	monpropd 17748	If two categories have the same set of objects, morphisms, and compositions, then they have the same monomorphisms. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → (Mono‘𝐶) = (Mono‘𝐷))
Theorem	oppcmon 17749	A monomorphism in the opposite category is an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝑀 = (Mono‘𝑂)    &   ⊢ 𝐸 = (Epi‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑌𝐸𝑋))
Theorem	oppcepi 17750	An epimorphism in the opposite category is a monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐸 = (Epi‘𝑂)    &   ⊢ 𝑀 = (Mono‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑌𝑀𝑋))
Theorem	isepi 17751*	Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(⟨𝑋, 𝑌⟩ · 𝑧)𝐹)))))
Theorem	isepi2 17752*	Write out the epimorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(⟨𝑋, 𝑌⟩ · 𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩ · 𝑧)𝐹) → 𝑔 = ℎ))))
Theorem	epihom 17753	An epimorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) ⊆ (𝑋𝐻𝑌))
Theorem	epii 17754	Property of an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐸𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → ((𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐾(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ↔ 𝐺 = 𝐾))
8.1.4  Sections, inverses, isomorphisms
Syntax	csect 17755	Extend class notation with the sections of a morphism.
class Sect
Syntax	cinv 17756	Extend class notation with the inverses of a morphism.
class Inv
Syntax	ciso 17757	Extend class notation with the class of all isomorphisms.
class Iso
Definition	df-sect 17758*	Function returning the section relation in a category. Given arrows 𝑓:𝑋⟶𝑌 and 𝑔:𝑌⟶𝑋, we say 𝑓Sect𝑔, that is, 𝑓 is a section of 𝑔, if 𝑔 ∘ 𝑓 = 1‘𝑋. If there there is an arrow 𝑔 with 𝑓Sect𝑔, the arrow 𝑓 is called a section, see definition 7.19 of [Adamek] p. 106. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ Sect = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))
Definition	df-inv 17759*	The inverse relation in a category. Given arrows 𝑓:𝑋⟶𝑌 and 𝑔:𝑌⟶𝑋, we say 𝑔Inv𝑓, that is, 𝑔 is an inverse of 𝑓, if 𝑔 is a section of 𝑓 and 𝑓 is a section of 𝑔. Definition 3.8 of [Adamek] p. 28. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 2-Jan-2017.)
⊢ Inv = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ ((𝑥(Sect‘𝑐)𝑦) ∩ ◡(𝑦(Sect‘𝑐)𝑥))))
Definition	df-iso 17760*	Function returning the isomorphisms of the category 𝑐. Definition 3.8 of [Adamek] p. 28, and definition in [Lang] p. 54. (Contributed by FL, 9-Jun-2014.) (Revised by Mario Carneiro, 2-Jan-2017.)
⊢ Iso = (𝑐 ∈ Cat ↦ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐)))
Theorem	sectffval 17761*	Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017.) Removed redundant hypotheses. (Revised by Zhi Wang, 27-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑆 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩ · 𝑥)𝑓) = ( 1 ‘𝑥))}))
Theorem	sectfval 17762*	Value of the section relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝑆𝑌) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(⟨𝑋, 𝑌⟩ · 𝑋)𝑓) = ( 1 ‘𝑋))})
Theorem	sectss 17763	The section relation is a relation between morphisms from 𝑋 to 𝑌 and morphisms from 𝑌 to 𝑋. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝑆𝑌) ⊆ ((𝑋𝐻𝑌) × (𝑌𝐻𝑋)))
Theorem	issect 17764	The property "𝐹 is a section of 𝐺". (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑋) ∧ (𝐺(⟨𝑋, 𝑌⟩ · 𝑋)𝐹) = ( 1 ‘𝑋))))
Theorem	issect2 17765	Property of being a section. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑋))    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐺(⟨𝑋, 𝑌⟩ · 𝑋)𝐹) = ( 1 ‘𝑋)))
Theorem	sectcan 17766	If 𝐺 is a section of 𝐹 and 𝐹 is a section of 𝐻, then 𝐺 = 𝐻. Proposition 3.10 of [Adamek] p. 28. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺(𝑋𝑆𝑌)𝐹)    &   ⊢ (𝜑 → 𝐹(𝑌𝑆𝑋)𝐻)    ⇒   ⊢ (𝜑 → 𝐺 = 𝐻)
Theorem	sectco 17767	Composition of two sections. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺)    &   ⊢ (𝜑 → 𝐻(𝑌𝑆𝑍)𝐾)    ⇒   ⊢ (𝜑 → (𝐻(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)(𝑋𝑆𝑍)(𝐺(⟨𝑍, 𝑌⟩ · 𝑋)𝐾))
Theorem	isofval 17768*	Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017.)
⊢ (𝐶 ∈ Cat → (Iso‘𝐶) = ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶)))
Theorem	invffval 17769*	Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) Removed redundant hypotheses. (Revised by Zhi Wang, 27-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝑆𝑦) ∩ ◡(𝑦𝑆𝑥))))
Theorem	invfval 17770	Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑁𝑌) = ((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋)))
Theorem	isinv 17771	Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹)))
Theorem	invss 17772	The inverse relation is a relation between morphisms 𝐹:𝑋⟶𝑌 and their inverses 𝐺:𝑌⟶𝑋. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑁𝑌) ⊆ ((𝑋𝐻𝑌) × (𝑌𝐻𝑋)))
Theorem	invsym 17773	The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐺(𝑌𝑁𝑋)𝐹))
Theorem	invsym2 17774	The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ◡(𝑋𝑁𝑌) = (𝑌𝑁𝑋))
Theorem	invfun 17775	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 17776	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 17777	If 𝐺 is an inverse to 𝐹, then 𝐹 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))
Theorem	inviso2 17778	If 𝐺 is an inverse to 𝐹, then 𝐺 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑋))
Theorem	invf 17779	The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑁𝑌):(𝑋𝐼𝑌)⟶(𝑌𝐼𝑋))
Theorem	invf1o 17780	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 17781	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 17782	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 17783*	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 17784*	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 17785	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 17786	The function value of the function returning the isomorphisms of a category is a function over the Cartesian square of the base set of the category. (Contributed by AV, 5-Apr-2020.)
⊢ (𝐶 ∈ Cat → (Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)))
Theorem	isohom 17787	An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋𝐻𝑌))
Theorem	isoco 17788	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 17789	A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝑇 = (Sect‘𝑂)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑇𝑌)𝐺 ↔ 𝐺(𝑋𝑆𝑌)𝐹))
Theorem	oppcsect2 17790	A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝑇 = (Sect‘𝑂)    ⇒   ⊢ (𝜑 → (𝑋𝑇𝑌) = ◡(𝑋𝑆𝑌))
Theorem	oppcinv 17791	An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Inv‘𝐶)    &   ⊢ 𝐽 = (Inv‘𝑂)    ⇒   ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝑌𝐼𝑋))
Theorem	oppciso 17792	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 17793	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 17794	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 17795	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 17796	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 17797	The identity is a section of itself. (Contributed by AV, 8-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Sect‘𝐶)𝑋)(𝐼‘𝑋))
Theorem	invid 17798	The inverse of the identity is the identity. (Contributed by AV, 8-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Inv‘𝐶)𝑋)(𝐼‘𝑋))
Theorem	idiso 17799	The identity is an isomorphism. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 8-Apr-2020.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋(Iso‘𝐶)𝑋))
Theorem	idinv 17800	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‘𝐶)𝑋)‘(𝐼‘𝑋)) = (𝐼‘𝑋))