P. 477 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47601-47700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ipolublem 47601*	Lemma for ipolubdm 47602 and ipolub 47603. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((∪ 𝑆 ⊆ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∪ 𝑆 ⊆ 𝑧 → 𝑋 ⊆ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑋 ≤ 𝑧))))
Theorem	ipolubdm 47602*	The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥})    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ 𝑇 ∈ 𝐹))
Theorem	ipolub 47603*	The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18366 is in quantified form. mrelatlub 18514 could potentially be shortened using this. See mrelatlubALT 47610. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥})    &   ⊢ (𝜑 → 𝑇 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇)
Theorem	ipoglblem 47604*	Lemma for ipoglbdm 47605 and ipoglb 47606. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋))))
Theorem	ipoglbdm 47605*	The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆})    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹))
Theorem	ipoglb 47606*	The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18367 is in quantified form. mrelatglb 18512 could potentially be shortened using this. See mrelatglbALT 47611. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆})    &   ⊢ (𝜑 → 𝑇 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇)
Theorem	ipolub0 47607	The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹)
Theorem	ipolub00 47608	The LUB of the empty set is the empty set if it is contained. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → ∅ ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑈‘∅) = ∅)
Theorem	ipoglb0 47609	The GLB of the empty set is the union of the base. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → ∪ 𝐹 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐹)
Theorem	mrelatlubALT 47610	Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Zhi Wang, 29-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐹 = (mrCls‘𝐶)    &   ⊢ 𝐿 = (lub‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶) → (𝐿‘𝑈) = (𝐹‘∪ 𝑈))
Theorem	mrelatglbALT 47611	Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Zhi Wang, 29-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅) → (𝐺‘𝑈) = ∩ 𝑈)
Theorem	mreclat 47612	A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat)
Theorem	topclat 47613	A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat)
Theorem	toplatglb0 47614	The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽)
Theorem	toplatlub 47615	Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐽)    &   ⊢ 𝑈 = (lub‘𝐼)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆)
Theorem	toplatglb 47616	Greatest lower bounds in a topology are realized by the interior of the intersection. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐽)    &   ⊢ 𝐺 = (glb‘𝐼)    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = ((int‘𝐽)‘∩ 𝑆))
Theorem	toplatjoin 47617	Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ ∨ = (join‘𝐼)    ⇒   ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵))
Theorem	toplatmeet 47618	Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ ∧ = (meet‘𝐼)    ⇒   ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵))
Theorem	topdlat 47619	A topology is a distributive lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat)
21.46.12  Categories
21.46.12.1  Categories
Theorem	catprslem 47620*	Lemma for catprs 47621. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅))
Theorem	catprs 47621*	A preorder can be extracted from a category. See catprs2 47622 for more details. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	catprs2 47622*	A category equipped with the induced preorder, where an object 𝑥 is defined to be "less than or equal to" 𝑦 iff there is a morphism from 𝑥 to 𝑦, is a preordered set, or a proset. The category might not be thin. See catprsc 47623 and catprsc2 47624 for constructions satisfying the hypothesis "catprs.1". See catprs 47621 for a more primitive version. See prsthinc 47664 for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Proset )
Theorem	catprsc 47623*	A construction of the preorder induced by a category. See catprs2 47622 for details. See also catprsc2 47624 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ (𝑥𝐻𝑦) ≠ ∅)})    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅))
Theorem	catprsc2 47624*	An alternate construction of the preorder induced by a category. See catprs2 47622 for details. See also catprsc 47623 for a different construction. The two constructions are different because df-cat 17611 does not require the domain of 𝐻 to be 𝐵 × 𝐵. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐻𝑦) ≠ ∅})    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅))
Theorem	endmndlem 47625	A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc 47694 for converting a monoid to a category. Lemma for bj-endmnd 36194. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋𝐻𝑋) = (Base‘𝑀))    &   ⊢ (𝜑 → (⟨𝑋, 𝑋⟩ · 𝑋) = (+g‘𝑀))    ⇒   ⊢ (𝜑 → 𝑀 ∈ Mnd)
21.46.12.2  Monomorphisms and epimorphisms
Theorem	idmon 47626	An identity arrow, or an identity morphism, is a monomorphism. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑀 = (Mono‘𝐶)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝑀𝑋))
Theorem	idepi 47627	An identity arrow, or an identity morphism, is an epimorphism. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐸 = (Epi‘𝐶)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐸𝑋))
21.46.12.3  Functors
Theorem	funcf2lem 47628*	A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
21.46.13  Examples of categories
21.46.13.1  Thin categories
Syntax	cthinc 47629	Extend class notation with the class of thin categories.
class ThinCat
Definition	df-thinc 47630*	Definition of the class of thin categories, or posetal categories, whose hom-sets each contain at most one morphism. Example 3.26(2) of [Adamek] p. 33. "ThinCat" was taken instead of "PosCat" because the latter might mean the category of posets. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ThinCat = {𝑐 ∈ Cat ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)}
Theorem	isthinc 47631*	The predicate "is a thin category". (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)))
Theorem	isthinc2 47632*	A thin category is a category in which all hom-sets have cardinality less than or equal to the cardinality of 1o. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ≼ 1o))
Theorem	isthinc3 47633*	A thin category is a category in which, given a pair of objects 𝑥 and 𝑦 and any two morphisms 𝑓, 𝑔 from 𝑥 to 𝑦, the morphisms are equal. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑥𝐻𝑦)𝑓 = 𝑔))
Theorem	thincc 47634	A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝐶 ∈ ThinCat → 𝐶 ∈ Cat)
Theorem	thinccd 47635	A thin category is a category (deduction form). (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	thincssc 47636	A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ThinCat ⊆ Cat
Theorem	isthincd2lem1 47637*	Lemma for isthincd2 47648 and thincmo2 47638. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	thincmo2 47638	Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	thincmo 47639*	There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincmoALT 47640*	Alternate proof for thincmo 47639. (Contributed by Zhi Wang, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincmod 47641*	At most one morphism in each hom-set (deduction form). (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincn0eu 47642*	In a thin category, a hom-set being non-empty is equivalent to having a unique element. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → ((𝑋𝐻𝑌) ≠ ∅ ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌)))
Theorem	thincid 47643	In a thin category, a morphism from an object to itself is an identity morphism. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑋))    ⇒   ⊢ (𝜑 → 𝐹 = ( 1 ‘𝑋))
Theorem	thincmon 47644	In a thin category, all morphisms are monomorphisms. The converse does not hold. See grptcmon 47706. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑀 = (Mono‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋𝐻𝑌))
Theorem	thincepi 47645	In a thin category, all morphisms are epimorphisms. The converse does not hold. See grptcepi 47707. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐸 = (Epi‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌))
Theorem	isthincd2lem2 47646*	Lemma for isthincd2 47648. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))
Theorem	isthincd 47647*	The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	isthincd2 47648*	The predicate "𝐶 is a thin category" without knowing 𝐶 is a category (deduction form). The identity arrow operator is also provided as a byproduct. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))))    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1 ∈ (𝑦𝐻𝑦))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 )))
Theorem	oppcthin 47649	The opposite category of a thin category is thin. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat)
Theorem	subthinc 47650	A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ThinCat)
Theorem	functhinclem1 47651*	Lemma for functhinc 47655. Given the object part, there is only one possible morphism part such that the mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    &   ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))    ⇒   ⊢ (𝜑 → ((𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝐺𝑤):(𝑧𝐻𝑤)⟶((𝐹‘𝑧)𝐽(𝐹‘𝑤))) ↔ 𝐺 = 𝐾))
Theorem	functhinclem2 47652*	Lemma for functhinc 47655. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅ → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))
Theorem	functhinclem3 47653*	Lemma for functhinc 47655. The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))))    &   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))    &   ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	functhinclem4 47654*	Lemma for functhinc 47655. Other requirements on the morphism part are automatically satisfied. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ · = (comp‘𝐷)    &   ⊢ 𝑂 = (comp‘𝐸)    ⇒   ⊢ ((𝜑 ∧ 𝐺 = 𝐾) → ∀𝑎 ∈ 𝐵 (((𝑎𝐺𝑎)‘( 1 ‘𝑎)) = (𝐼‘(𝐹‘𝑎)) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑚 ∈ (𝑎𝐻𝑏)∀𝑛 ∈ (𝑏𝐻𝑐)((𝑎𝐺𝑐)‘(𝑛(⟨𝑎, 𝑏⟩ · 𝑐)𝑚)) = (((𝑏𝐺𝑐)‘𝑛)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩𝑂(𝐹‘𝑐))((𝑎𝐺𝑏)‘𝑚))))
Theorem	functhinc 47655*	A functor to a thin category is determined entirely by the object part. The hypothesis "functhinc.1" is related to a monotone function if preorders induced by the categories are considered (catprs2 47622). (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))    ⇒   ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐺 = 𝐾))
Theorem	fullthinc 47656*	A functor to a thin category is full iff empty hom-sets are mapped to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥𝐻𝑦) = ∅ → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅)))
Theorem	fullthinc2 47657	A full functor to a thin category maps empty hom-sets to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋𝐻𝑌) = ∅ ↔ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅))
Theorem	thincfth 47658	A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)
Theorem	thincciso 47659*	Two thin categories are isomorphic iff the induced preorders are order-isomorphic. Example 3.26(2) of [Adamek] p. 33. (Contributed by Zhi Wang, 16-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ 𝐻 = (Hom ‘𝑋)    &   ⊢ 𝐽 = (Hom ‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓(∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 ((𝑥𝐻𝑦) = ∅ ↔ ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) = ∅) ∧ 𝑓:𝑅–1-1-onto→𝑆)))
Theorem	0thincg 47660	Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ ThinCat)
Theorem	0thinc 47661	The empty category (see 0cat 17632) is thin. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ∅ ∈ ThinCat
Theorem	indthinc 47662*	An indiscrete category in which all hom-sets have exactly one morphism is a thin category. Constructed here is an indiscrete category where all morphisms are ∅. This is a special case of prsthinc 47664, where ≤ = (𝐵 × 𝐵). This theorem also implies a functor from the category of sets to the category of small categories. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof shortened by Zhi Wang, 19-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶))    &   ⊢ (𝜑 → ∅ = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))
Theorem	indthincALT 47663*	An alternate proof for indthinc 47662 assuming more axioms including ax-pow 5363 and ax-un 7724. (Contributed by Zhi Wang, 17-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → ((𝐵 × 𝐵) × {1o}) = (Hom ‘𝐶))    &   ⊢ (𝜑 → ∅ = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))
Theorem	prsthinc 47664*	Preordered sets as categories. Similar to example 3.3(4.d) of [Adamek] p. 24, but the hom-sets are not pairwise disjoint. One can define a functor from the category of prosets to the category of small thin categories. See catprs 47621 and catprs2 47622 for inducing a preorder from a category. Example 3.26(2) of [Adamek] p. 33 indicates that it induces a bijection from the equivalence class of isomorphic small thin categories to the equivalence class of order-isomorphic preordered sets. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → ( ≤ × {1o}) = (Hom ‘𝐶))    &   ⊢ (𝜑 → ∅ = (comp‘𝐶))    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))
Theorem	setcthin 47665*	A category of sets all of whose objects contain at most one element is thin. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (SetCat‘𝑈))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 ∃*𝑝 𝑝 ∈ 𝑥)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	setc2othin 47666	The category (SetCat‘2o) is thin. A special case of setcthin 47665. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (SetCat‘2o) ∈ ThinCat
Theorem	thincsect 47667	In a thin category, one morphism is a section of another iff they are pointing towards each other. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑋))))
Theorem	thincsect2 47668	In a thin category, 𝐹 is a section of 𝐺 iff 𝐺 is a section of 𝐹. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ 𝐺(𝑌𝑆𝑋)𝐹))
Theorem	thincinv 47669	In a thin category, 𝐹 is an inverse of 𝐺 iff 𝐹 is a section of 𝐺 (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐹(𝑋𝑆𝑌)𝐺))
Theorem	thinciso 47670	In a thin category, 𝐹:𝑋⟶𝑌 is an isomorphism iff there is a morphism from 𝑌 to 𝑋. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ (𝑌𝐻𝑋) ≠ ∅))
Theorem	thinccic 47671	In a thin category, two objects are isomorphic iff there are morphisms between them in both directions. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ((𝑋𝐻𝑌) ≠ ∅ ∧ (𝑌𝐻𝑋) ≠ ∅)))
21.46.13.2  Preordered sets as thin categories
Syntax	cprstc 47672	Class function defining preordered sets as categories.
class ProsetToCat
Definition	df-prstc 47673	Definition of the function converting a preordered set to a category. Justified by prsthinc 47664. This definition is somewhat arbitrary. Example 3.3(4.d) of [Adamek] p. 24 demonstrates an alternate definition with pairwise disjoint hom-sets. The behavior of the function is defined entirely, up to isomorphism, by prstcnid 47676, prstchom 47687, and prstcthin 47686. Other important properties include prstcbas 47677, prstcleval 47678, prstcle 47680, prstcocval 47681, prstcoc 47683, prstchom2 47688, and prstcprs 47685. Use those instead. Note that the defining property prstchom 47687 is equivalent to prstchom2 47688 given prstcthin 47686. See thincn0eu 47642 for justification. "ProsetToCat" was taken instead of "ProsetCat" because the latter might mean the category of preordered sets (classes). However, "ProsetToCat" seems too long. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Theorem	prstcval 47674	Lemma for prstcnidlem 47675 and prstcthin 47686. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 = ((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Theorem	prstcnidlem 47675	Lemma for prstcnid 47676 and prstchomval 47684. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (comp‘ndx)    ⇒   ⊢ (𝜑 → (𝐸‘𝐶) = (𝐸‘(𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩)))
Theorem	prstcnid 47676	Components other than Hom and comp are unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (comp‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (Hom ‘ndx)    ⇒   ⊢ (𝜑 → (𝐸‘𝐾) = (𝐸‘𝐶))
Theorem	prstcbas 47677	The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	prstcleval 47678	Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    ⇒   ⊢ (𝜑 → ≤ = (le‘𝐶))
Theorem	prstclevalOLD 47679	Obsolete proof of prstcleval 47678 as of 12-Nov-2024. Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    ⇒   ⊢ (𝜑 → ≤ = (le‘𝐶))
Theorem	prstcle 47680	Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ 𝑋(le‘𝐶)𝑌))
Theorem	prstcocval 47681	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ⊥ = (oc‘𝐶))
Theorem	prstcocvalOLD 47682	Obsolete proof of prstcocval 47681 as of 12-Nov-2024. Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ⊥ = (oc‘𝐶))
Theorem	prstcoc 47683	Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ⊥ = (oc‘𝐾))    ⇒   ⊢ (𝜑 → ( ⊥ ‘𝑋) = ((oc‘𝐶)‘𝑋))
Theorem	prstchomval 47684	Hom-sets of the constructed category which depend on an arbitrary definition. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    ⇒   ⊢ (𝜑 → ( ≤ × {1o}) = (Hom ‘𝐶))
Theorem	prstcprs 47685	The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ Proset )
Theorem	prstcthin 47686	The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	prstchom 47687	Hom-sets of the constructed category are dependent on the preorder. Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat. However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅))
Theorem	prstchom2 47688*	Hom-sets of the constructed category are dependent on the preorder. Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat ( see prstchom2ALT 47689). However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌)))
Theorem	prstchom2ALT 47689*	Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc 47673. See prstchom2 47688 for a version that does not depend on the definition. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌)))
Theorem	postcpos 47690	The converted category is a poset iff the original proset is a poset. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset))
Theorem	postcposALT 47691	Alternate proof for postcpos 47690. (Contributed by Zhi Wang, 25-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐶 ∈ Poset))
Theorem	postc 47692*	The converted category is a poset iff no distinct objects are isomorphic. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Proset )    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → (𝐶 ∈ Poset ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥( ≃𝑐 ‘𝐶)𝑦 → 𝑥 = 𝑦)))
21.46.13.3  Monoids as categories
Syntax	cmndtc 47693	Class function defining monoids as categories.
class MndToCat
Definition	df-mndtc 47694	Definition of the function converting a monoid to a category. Example 3.3(4.e) of [Adamek] p. 24. The definition of the base set is arbitrary. The whole extensible structure becomes the object here (see mndtcbasval 47696), instead of just the base set, as is the case in Example 3.3(4.e) of [Adamek] p. 24. The resulting category is defined entirely, up to isomorphism, by mndtcbas 47697, mndtchom 47700, mndtcco 47701. Use those instead. See example 3.26(3) of [Adamek] p. 33 for more on isomorphism. "MndToCat" was taken instead of "MndCat" because the latter might mean the category of monoids. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})
Theorem	mndtcval 47695	Value of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), {𝑀}⟩, ⟨(Hom ‘ndx), {⟨𝑀, 𝑀, (Base‘𝑀)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑀, 𝑀, 𝑀⟩, (+g‘𝑀)⟩}⟩})
Theorem	mndtcbasval 47696	The base set of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    ⇒   ⊢ (𝜑 → 𝐵 = {𝑀})
Theorem	mndtcbas 47697*	The category built from a monoid contains precisely one object. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    ⇒   ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ 𝐵)
Theorem	mndtcob 47698	Lemma for mndtchom 47700 and mndtcco 47701. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑀)
Theorem	mndtcbas2 47699	Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	mndtchom 47700	The only hom-set of the category built from a monoid is the base set of the monoid. (Contributed by Zhi Wang, 22-Sep-2024.)
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (Base‘𝑀))