P. 177 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17601-17700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isacs1i 17601*	A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (ACS‘𝑋))
Theorem	mreacs 17602	Algebraicity is a composable property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))
Theorem	acsfn 17603*	Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋) ∧ (𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇 ⊆ 𝑎 → 𝐾 ∈ 𝑎)} ∈ (ACS‘𝑋))
Theorem	acsfn0 17604*	Algebraicity of a point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ 𝐾 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	acsfn1 17605*	Algebraicity of a one-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	acsfn1c 17606*	Algebraicity of a one-argument closure condition with additional constant. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝐾 ∀𝑐 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝐾 ∀𝑐 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	acsfn2 17607*	Algebraicity of a two-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
PART 8  BASIC CATEGORY THEORY
8.1  Categories
8.1.1  Categories
Syntax	ccat 17608	Extend class notation with the class of categories.
class Cat
Syntax	ccid 17609	Extend class notation with the identity arrow of a category.
class Id
Syntax	chomf 17610	Extend class notation to include functionalized Hom-set extractor.
class Homf
Syntax	ccomf 17611	Extend class notation to include functionalized composition operation.
class compf
Definition	df-cat 17612*	A category is an abstraction of a structure (a group, a topology, an order...) Category theory consists in finding new formulation of the concepts associated with those structures (product, substructure...) using morphisms instead of the belonging relation. That trick has the interesting property that heterogeneous structures like topologies or groups for instance become comparable. Definition in [Lang] p. 53, without the axiom CAT 1, i.e., pairwise disjointness of hom-sets (cat1 18047). See setc2obas 18044 and setc2ohom 18045 for a counterexample. In contrast to definition 3.1 of [Adamek] p. 21, where "A category is a quadruple A = (O, hom, id, o)", a category is defined as an extensible structure consisting of three slots: the objects "O" ((Base‘𝑐)), the morphisms "hom" ((Hom ‘𝑐)) and the composition law "o" ((comp‘𝑐)). The identities "id" are defined by their properties related to morphisms and their composition, see condition 3.1(b) in [Adamek] p. 21 and df-cid 17613. (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)
⊢ Cat = {𝑐 ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))))}
Definition	df-cid 17613*	Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ Id = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))
Definition	df-homf 17614*	Define the functionalized Hom-set operator, which is exactly like Hom but is guaranteed to be a function on the base. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Homf = (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦)))
Definition	df-comf 17615*	Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ compf = (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))))
Theorem	iscat 17616*	The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))))))
Theorem	iscatd 17617*	Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈ (𝑥𝐻𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(⟨𝑥, 𝑥⟩ · 𝑦) 1 ) = 𝑓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    &   ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	catidex 17618*	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋⟩ · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋⟩ · 𝑦)𝑔) = 𝑓))
Theorem	catideu 17619*	Each object in a category has a unique identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋⟩ · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋⟩ · 𝑦)𝑔) = 𝑓))
Theorem	cidfval 17620*	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 1 = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓))))
Theorem	cidval 17621*	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = (℩𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋⟩ · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋⟩ · 𝑦)𝑔) = 𝑓)))
Theorem	cidffn 17622	The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ Id Fn Cat
Theorem	cidfn 17623	The identity arrow operator is a function from objects to arrows. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → 1 Fn 𝐵)
Theorem	catidd 17624*	Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈ (𝑥𝐻𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(⟨𝑥, 𝑥⟩ · 𝑦) 1 ) = 𝑓)    ⇒   ⊢ (𝜑 → (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ 1 ))
Theorem	iscatd2 17625*	Version of iscatd 17617 with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1 ∈ (𝑦𝐻𝑦))    &   ⊢ ((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    &   ⊢ ((𝜑 ∧ 𝜓) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))    ⇒   ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 )))
Theorem	catidcl 17626	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐻𝑋))
Theorem	catlid 17627	Left identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝐹) = 𝐹)
Theorem	catrid 17628	Right identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (𝐹(⟨𝑋, 𝑋⟩ · 𝑌)( 1 ‘𝑋)) = 𝐹)
Theorem	catcocl 17629	Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))
Theorem	catass 17630	Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑊))    ⇒   ⊢ (𝜑 → ((𝐾(⟨𝑌, 𝑍⟩ · 𝑊)𝐺)(⟨𝑋, 𝑌⟩ · 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍⟩ · 𝑊)(𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)))
Theorem	catcone0 17631	Composition of non-empty hom-sets is non-empty. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋𝐻𝑌) ≠ ∅)    &   ⊢ (𝜑 → (𝑌𝐻𝑍) ≠ ∅)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑍) ≠ ∅)
Theorem	0catg 17632	Any structure with an empty set of objects is a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ Cat)
Theorem	0cat 17633	The empty set is a category, the empty category, see example 3.3(4.c) in [Adamek] p. 24. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ ∅ ∈ Cat
Theorem	homffval 17634*	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.)
⊢ 𝐹 = (Homf ‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥𝐻𝑦))
Theorem	fnhomeqhomf 17635	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 17636	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐹 = (Homf ‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑋𝐻𝑌))
Theorem	homffn 17637	The functionalized Hom-set operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐹 = (Homf ‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝐹 Fn (𝐵 × 𝐵)
Theorem	homfeq 17638*	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 17639	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 17640	Deduce equality of base sets from equality of Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    ⇒   ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))
Theorem	homfeqval 17641	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋𝐽𝑌))
Theorem	comfffval 17642*	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 17643*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑂𝑍) = (𝑔 ∈ (𝑌𝐻𝑍), 𝑓 ∈ (𝑋𝐻𝑌) ↦ (𝑔(⟨𝑋, 𝑌⟩ · 𝑍)𝑓)))
Theorem	comfval 17644	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
Theorem	comfffval2 17645*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))
Theorem	comffval2 17646*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑂𝑍) = (𝑔 ∈ (𝑌𝐻𝑍), 𝑓 ∈ (𝑋𝐻𝑌) ↦ (𝑔(⟨𝑋, 𝑌⟩ · 𝑍)𝑓)))
Theorem	comfval2 17647	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
Theorem	comfffn 17648	The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝑂 Fn ((𝐵 × 𝐵) × 𝐵)
Theorem	comffn 17649	The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑂𝑍) Fn ((𝑌𝐻𝑍) × (𝑋𝐻𝑌)))
Theorem	comfeq 17650*	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 17651	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 17652	Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ ∙ 𝑍)𝐹))
Theorem	catpropd 17653	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 17654	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 17655	The opposite category operation.
class oppCat
Definition	df-oppc 17656*	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 17657*	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 17658	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	oppchomfvalOLD 17659	Obsolete proof of oppchomfval 17658 as of 14-Oct-2024. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ tpos 𝐻 = (Hom ‘𝑂)
Theorem	oppchom 17660	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝑋(Hom ‘𝑂)𝑌) = (𝑌𝐻𝑋)
Theorem	oppccofval 17661	Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩(comp‘𝑂)𝑍) = tpos (⟨𝑍, 𝑌⟩ · 𝑋))
Theorem	oppcco 17662	Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩(comp‘𝑂)𝑍)𝐹) = (𝐹(⟨𝑍, 𝑌⟩ · 𝑋)𝐺))
Theorem	oppcbas 17663	Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 18-Oct-2024.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	oppcbasOLD 17664	Obsolete version of oppcbas 17663 as of 18-Oct-2024. Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	oppccatid 17665	Lemma for oppccat 17668. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧ (Id‘𝑂) = (Id‘𝐶)))
Theorem	oppchomf 17666	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    ⇒   ⊢ tpos 𝐻 = (Homf ‘𝑂)
Theorem	oppcid 17667	Identity function of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Id‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = 𝐵)
Theorem	oppccat 17668	An opposite category is a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
Theorem	2oppcbas 17669	The double opposite category has the same objects as the original category. Intended for use with property lemmas such as monpropd 17684. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝐵 = (Base‘(oppCat‘𝑂))
Theorem	2oppchomf 17670	The double opposite category has the same morphisms as the original category. Intended for use with property lemmas such as monpropd 17684. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (Homf ‘𝐶) = (Homf ‘(oppCat‘𝑂))
Theorem	2oppccomf 17671	The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd 17684. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (compf‘𝐶) = (compf‘(oppCat‘𝑂))
Theorem	oppchomfpropd 17672	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 17673	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 17674	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 17675	Extend class notation with the class of all monomorphisms.
class Mono
Syntax	cepi 17676	Extend class notation with the class of all epimorphisms.
class Epi
Definition	df-mon 17677*	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 17678	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 17679*	Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑀 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩ · 𝑦)𝑔))}))
Theorem	ismon 17680*	Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(⟨𝑧, 𝑋⟩ · 𝑌)𝑔)))))
Theorem	ismon2 17681*	Write out the monomorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑧𝐻𝑋)∀ℎ ∈ (𝑧𝐻𝑋)((𝐹(⟨𝑧, 𝑋⟩ · 𝑌)𝑔) = (𝐹(⟨𝑧, 𝑋⟩ · 𝑌)ℎ) → 𝑔 = ℎ))))
Theorem	monhom 17682	A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝑀𝑌) ⊆ (𝑋𝐻𝑌))
Theorem	moni 17683	Property of a monomorphism. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋))    ⇒   ⊢ (𝜑 → ((𝐹(⟨𝑍, 𝑋⟩ · 𝑌)𝐺) = (𝐹(⟨𝑍, 𝑋⟩ · 𝑌)𝐾) ↔ 𝐺 = 𝐾))
Theorem	monpropd 17684	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 17685	A monomorphism in the opposite category is an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝑀 = (Mono‘𝑂)    &   ⊢ 𝐸 = (Epi‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑌𝐸𝑋))
Theorem	oppcepi 17686	An epimorphism in the opposite category is a monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐸 = (Epi‘𝑂)    &   ⊢ 𝑀 = (Mono‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑌𝑀𝑋))
Theorem	isepi 17687*	Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(⟨𝑋, 𝑌⟩ · 𝑧)𝐹)))))
Theorem	isepi2 17688*	Write out the epimorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(⟨𝑋, 𝑌⟩ · 𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩ · 𝑧)𝐹) → 𝑔 = ℎ))))
Theorem	epihom 17689	An epimorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) ⊆ (𝑋𝐻𝑌))
Theorem	epii 17690	Property of an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐸𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → ((𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐾(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ↔ 𝐺 = 𝐾))
8.1.4  Sections, inverses, isomorphisms
Syntax	csect 17691	Extend class notation with the sections of a morphism.
class Sect
Syntax	cinv 17692	Extend class notation with the inverses of a morphism.
class Inv
Syntax	ciso 17693	Extend class notation with the class of all isomorphisms.
class Iso
Definition	df-sect 17694*	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 17695*	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 17696*	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 17697*	Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑆 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩ · 𝑥)𝑓) = ( 1 ‘𝑥))}))
Theorem	sectfval 17698*	Value of the section relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝑆𝑌) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(⟨𝑋, 𝑌⟩ · 𝑋)𝑓) = ( 1 ‘𝑋))})
Theorem	sectss 17699	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 17700	The property "𝐹 is a section of 𝐺". (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑋) ∧ (𝐺(⟨𝑋, 𝑌⟩ · 𝑋)𝐹) = ( 1 ‘𝑋))))