P. 491 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49001-49100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fuco2eld3 49001	Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ Rel 𝑆    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → ((1st ‘(1st ‘𝑈))𝑆(2nd ‘(1st ‘𝑈)) ∧ (1st ‘(2nd ‘𝑈))𝑅(2nd ‘(2nd ‘𝑈))))
Syntax	cfuco 49002	Extend class notation with functor composition bifunctors.
class ∘F
Definition	df-fuco 49003*	Definition of functor composition bifunctors. Given three categories 𝐶, 𝐷, and 𝐸, (⟨𝐶, 𝐷⟩ ∘F 𝐸) is a functor from the product category of two categories of functors to a category of functors (fucofunc 49045). The object part maps two functors to their composition (fuco11 49012 and fuco11b 49023). The morphism part defines the "composition" of two natural transformations (fuco22 49025) into another natural transformation (fuco22nat 49032) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 49038). Note that such "composition" is different from fucco 18006 because they "compose" along different "axes". (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ ∘F = (𝑝 ∈ V, 𝑒 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌⦋((𝑑 Func 𝑒) × (𝑐 Func 𝑑)) / 𝑤⦌⟨( ∘func ↾ 𝑤), (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝑑 Nat 𝑒)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝑐 Nat 𝑑)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)
Theorem	fucofvalg 49004*	Value of the function giving the functor composition bifunctor. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → 𝑃 ∈ 𝑈)    &   ⊢ (𝜑 → (1st ‘𝑃) = 𝐶)    &   ⊢ (𝜑 → (2nd ‘𝑃) = 𝐷)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑃 ∘F 𝐸) = ⚬ )    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → ⚬ = ⟨( ∘func ↾ 𝑊), (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)
Theorem	fucofval 49005*	Value of the function giving the functor composition bifunctor. Hypotheses fucofval.c and fucofval.d are not redundant (fucofvalne 49011). (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ )    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → ⚬ = ⟨( ∘func ↾ 𝑊), (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)
Theorem	fucoelvv 49006	A functor composition bifunctor is an ordered pair. Enables 1st2ndb 8050. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ )    ⇒   ⊢ (𝜑 → ⚬ ∈ (V × V))
Theorem	fuco1 49007	The object part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑂 = ( ∘func ↾ 𝑊))
Theorem	fucof1 49008	The object part of the functor composition bifunctor maps ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) into (𝐶 Func 𝐸). (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑂:𝑊⟶(𝐶 Func 𝐸))
Theorem	fuco2 49009*	The morphism part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑃 = (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))))
Theorem	fucofn2 49010	The morphism part of the functor composition bifunctor is a function on the Cartesian square of the base set. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → 𝑃 Fn (𝑊 × 𝑊))
Theorem	fucofvalne 49011*	Value of the function giving the functor composition bifunctor, if 𝐶 or 𝐷 are not sets. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ (𝜑 → ¬ (𝐶 ∈ V ∧ 𝐷 ∈ V))    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⚬ )    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    ⇒   ⊢ (𝜑 → ⚬ ≠ ⟨( ∘func ↾ 𝑊), (𝑢 ∈ 𝑊, 𝑣 ∈ 𝑊 ↦ ⦋(1st ‘(2nd ‘𝑢)) / 𝑓⦌⦋(1st ‘(1st ‘𝑢)) / 𝑘⦌⦋(2nd ‘(1st ‘𝑢)) / 𝑙⦌⦋(1st ‘(2nd ‘𝑣)) / 𝑚⦌⦋(1st ‘(1st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1st ‘𝑢)(𝐷 Nat 𝐸)(1st ‘𝑣)), 𝑎 ∈ ((2nd ‘𝑢)(𝐶 Nat 𝐷)(2nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝐸)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)
Theorem	fuco11 49012	The object part of the functor composition bifunctor maps two functors to their composition. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → (𝑂‘𝑈) = (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩))
Theorem	fuco11cl 49013	The object part of the functor composition bifunctor maps into (𝐶 Func 𝐸). (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → (𝑂‘𝑈) ∈ (𝐶 Func 𝐸))
Theorem	fuco11a 49014*	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → (𝑂‘𝑈) = ⟨(𝐾 ∘ 𝐹), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐿(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))⟩)
Theorem	fuco112 49015*	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → (2nd ‘(𝑂‘𝑈)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐿(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦))))
Theorem	fuco111 49016	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the object part of the composed functor. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → (1st ‘(𝑂‘𝑈)) = (𝐾 ∘ 𝐹))
Theorem	fuco111x 49017	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the object part of the composed functor. An object is mapped by two functors in succession. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → ((1st ‘(𝑂‘𝑈))‘𝑋) = (𝐾‘(𝐹‘𝑋)))
Theorem	fuco112x 49018	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘(𝑂‘𝑈))𝑌) = (((𝐹‘𝑋)𝐿(𝐹‘𝑌)) ∘ (𝑋𝐺𝑌)))
Theorem	fuco112xa 49019	The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. A morphism is mapped by two functors in succession. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋(Hom ‘𝐶)𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘(𝑂‘𝑈))𝑌)‘𝐴) = (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐴)))
Theorem	fuco11id 49020	The identity morphism of the mapped object. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 1 = (Id‘𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑂‘𝑈)) = ( 1 ∘ (𝐾 ∘ 𝐹)))
Theorem	fuco11idx 49021	The identity morphism of the mapped object. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 1 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → ((𝐼‘(𝑂‘𝑈))‘𝑋) = ( 1 ‘(𝐾‘(𝐹‘𝑋))))
Theorem	fuco21 49022*	The morphism part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑀(𝐶 Func 𝐷)𝑁)    &   ⊢ (𝜑 → 𝑅(𝐷 Func 𝐸)𝑆)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    ⇒   ⊢ (𝜑 → (𝑈𝑃𝑉) = (𝑏 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩), 𝑎 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑀‘𝑥))(⟨(𝐾‘(𝐹‘𝑥)), (𝐾‘(𝑀‘𝑥))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑥)))(((𝐹‘𝑥)𝐿(𝑀‘𝑥))‘(𝑎‘𝑥))))))
Theorem	fuco11b 49023	The object part of the functor composition bifunctor maps two functors to their composition. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑂)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝐺𝑂𝐹) = (𝐺 ∘func 𝐹))
Theorem	fuco11bALT 49024	Alternate proof of fuco11b 49023. (Contributed by Zhi Wang, 11-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑂)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝐺𝑂𝐹) = (𝐺 ∘func 𝐹))
Theorem	fuco22 49025*	The morphism part of the functor composition bifunctor. See also fuco22a 49036. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝐵‘(𝑀‘𝑥))(⟨(𝐾‘(𝐹‘𝑥)), (𝐾‘(𝑀‘𝑥))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑥)))(((𝐹‘𝑥)𝐿(𝑀‘𝑥))‘(𝐴‘𝑥)))))
Theorem	fucofn22 49026	The morphism part of the functor composition bifunctor maps two natural transformations to a function on a base set. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) Fn (Base‘𝐶))
Theorem	fuco23 49027	The morphism part of the functor composition bifunctor. See also fuco23a 49038. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → ∗ = (⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋))))    ⇒   ⊢ (𝜑 → ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) = ((𝐵‘(𝑀‘𝑋)) ∗ (((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))))
Theorem	fuco22natlem1 49028	Lemma for fuco22nat 49032. The commutative square of natural transformation 𝐴 in category 𝐷, mapped to category 𝐸 by the morphism part 𝐿 of the functor. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌))    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    ⇒   ⊢ (𝜑 → ((((𝐹‘𝑌)𝐿(𝑀‘𝑌))‘(𝐴‘𝑌))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝐹‘𝑌))⟩(comp‘𝐸)(𝐾‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐻))) = ((((𝑀‘𝑋)𝐿(𝑀‘𝑌))‘((𝑋𝑁𝑌)‘𝐻))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝐾‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))))
Theorem	fuco22natlem2 49029	Lemma for fuco22nat 49032. The commutative square of natural transformation 𝐵 in category 𝐸, combined with the commutative square of fuco22natlem1 49028. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (((𝐵‘(𝑀‘𝑌))(⟨(𝐾‘(𝐹‘𝑌)), (𝐾‘(𝑀‘𝑌))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))(((𝐹‘𝑌)𝐿(𝑀‘𝑌))‘(𝐴‘𝑌)))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝐹‘𝑌))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐻))) = ((((𝑀‘𝑋)𝑆(𝑀‘𝑌))‘((𝑋𝑁𝑌)‘𝐻))(⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑌)))((𝐵‘(𝑀‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋)))))
Theorem	fuco22natlem3 49030	Combine fuco22natlem2 49029 with fuco23 49027. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑋(Hom ‘𝐶)𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    ⇒   ⊢ (𝜑 → (((𝐵(𝑈𝑃𝑉)𝐴)‘𝑌)(⟨((𝐾 ∘ 𝐹)‘𝑋), ((𝐾 ∘ 𝐹)‘𝑌)⟩(comp‘𝐸)((𝑅 ∘ 𝑀)‘𝑌))((((𝐹‘𝑋)𝐿(𝐹‘𝑌)) ∘ (𝑋𝐺𝑌))‘𝐻)) = (((((𝑀‘𝑋)𝑆(𝑀‘𝑌)) ∘ (𝑋𝑁𝑌))‘𝐻)(⟨((𝐾 ∘ 𝐹)‘𝑋), ((𝑅 ∘ 𝑀)‘𝑋)⟩(comp‘𝐸)((𝑅 ∘ 𝑀)‘𝑌))((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋)))
Theorem	fuco22natlem 49031	The composed natural transformation is a natural transformation. Use fuco22nat 49032 instead. (New usage is discouraged.) (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) ∈ ((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉)))
Theorem	fuco22nat 49032	The composed natural transformation is a natural transformation. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝐶 Nat 𝐷)𝑀))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐾(𝐷 Nat 𝐸)𝑅))    &   ⊢ (𝜑 → 𝑈 = ⟨𝐾, 𝐹⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨𝑅, 𝑀⟩)    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) ∈ ((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉)))
Theorem	fucof21 49033	The morphism part of the functor composition bifunctor maps a hom-set of the product category into a set of natural transformations. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝐽 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑈𝑃𝑉):(𝑈𝐽𝑉)⟶((𝑂‘𝑈)(𝐶 Nat 𝐸)(𝑂‘𝑉)))
Theorem	fucoid 49034	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid2 49035. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 1 = (Id‘𝑇)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑈𝑃𝑈)‘( 1 ‘𝑈)) = (𝐼‘(𝑂‘𝑈)))
Theorem	fucoid2 49035	Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid 49034. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 1 = (Id‘𝑇)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝑈𝑃𝑈)‘( 1 ‘𝑈)) = (𝐼‘(𝑂‘𝑈)))
Theorem	fuco22a 49036*	The morphism part of the functor composition bifunctor. See also fuco22 49025. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨𝐾, 𝐹⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨𝑅, 𝑀⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝐶 Nat 𝐷)𝑀))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐾(𝐷 Nat 𝐸)𝑅))    ⇒   ⊢ (𝜑 → (𝐵(𝑈𝑃𝑉)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝐵‘((1st ‘𝑀)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑀)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑅)‘((1st ‘𝑀)‘𝑥)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐾)((1st ‘𝑀)‘𝑥))‘(𝐴‘𝑥)))))
Theorem	fuco23alem 49037	The naturality property (nati 17999) in category 𝐸. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ · = (comp‘𝐸)    ⇒   ⊢ (𝜑 → ((𝐵‘(𝑀‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩ · (𝑅‘(𝑀‘𝑋)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))) = ((((𝐹‘𝑋)𝑆(𝑀‘𝑋))‘(𝐴‘𝑋))(⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝐹‘𝑋))⟩ · (𝑅‘(𝑀‘𝑋)))(𝐵‘(𝐹‘𝑋))))
Theorem	fuco23a 49038	The morphism part of the functor composition bifunctor. An alternate definition of ∘F. See also fuco23 49027. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩))    &   ⊢ (𝜑 → 𝐵 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)    &   ⊢ (𝜑 → ∗ = (⟨(𝐾‘(𝐹‘𝑋)), (𝑅‘(𝐹‘𝑋))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑋))))    ⇒   ⊢ (𝜑 → ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) = ((((𝐹‘𝑋)𝑆(𝑀‘𝑋))‘(𝐴‘𝑋)) ∗ (𝐵‘(𝐹‘𝑋))))
Theorem	fucocolem1 49039	Lemma for fucoco 49043. Associativity for morphisms in category 𝐸. To simply put, ((𝑎 · 𝑏) · (𝑐 · 𝑑)) = (𝑎 · ((𝑏 · 𝑐) · 𝑑)) for morphism compositions. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ (((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))(Hom ‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋))))    &   ⊢ (𝜑 → 𝐵 ∈ (((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋))(Hom ‘𝐸)((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))))    ⇒   ⊢ (𝜑 → (((𝑈‘((1st ‘𝑁)‘𝑋))(⟨((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑋)))𝐴)(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑋)))(𝐵(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋)))((((1st ‘𝐺)‘𝑋)(2nd ‘𝐹)((1st ‘𝐿)‘𝑋))‘(𝑆‘𝑋)))) = ((𝑈‘((1st ‘𝑁)‘𝑋))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑋)))((𝐴(⟨((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋)), ((1st ‘𝑃)‘((1st ‘𝑄)‘𝑋))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋)))𝐵)(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑋)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑋))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑋)))((((1st ‘𝐺)‘𝑋)(2nd ‘𝐹)((1st ‘𝐿)‘𝑋))‘(𝑆‘𝑋)))))
Theorem	fucocolem2 49040*	Lemma for fucoco 49043. The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)    &   ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ · = (comp‘𝑇)    &   ⊢ ∗ = (comp‘𝐷)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ (((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝑁)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))(𝑅‘((1st ‘𝑁)‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝑁)‘𝑥))‘((𝑉‘𝑥)(⟨((1st ‘𝐺)‘𝑥), ((1st ‘𝐿)‘𝑥)⟩ ∗ ((1st ‘𝑁)‘𝑥))(𝑆‘𝑥))))))
Theorem	fucocolem3 49041*	Lemma for fucoco 49043. The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)    &   ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ · = (comp‘𝑇)    &   ⊢ ∗ = (comp‘𝐷)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))(((𝑅‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐹)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥))))))
Theorem	fucocolem4 49042*	Lemma for fucoco 49043. The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 2-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)    &   ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ ∙ = (comp‘𝑄)    ⇒   ⊢ (𝜑 → (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ (((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥))))))
Theorem	fucoco 49043	Composition in the source category is mapped to composition in the target. See also fucoco2 49044. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)    &   ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)    &   ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)    &   ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ · = (comp‘𝑇)    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)))
Theorem	fucoco2 49044	Composition in the source category is mapped to composition in the target. See also fucoco 49043. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ · = (comp‘𝑇)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ 𝐽 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐽𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑌𝐽𝑍))    ⇒   ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)))
Theorem	fucofunc 49045	The functor composition bifunctor is a functor. See also fucofunca 49046. However, it is unlikely the unique functor compatible with the functor composition. As a counterexample, let 𝐶 and 𝐷 be terminal categories (categories of one object and one morphism, df-termc 49111), for example, (SetCat‘1o) (the trivial category, setc1oterm 49125), and 𝐸 be a category with two objects equipped with only two non-identity morphisms 𝑓 and 𝑔, pointing in the same direction. It is possible to map the ordered pair of natural transformations ⟨𝑎, 𝑖⟩, where 𝑎 sends to 𝑓 and 𝑖 is the identity natural transformation, to the other natural transformation 𝑏 sending to 𝑔, i.e., define the morphism part 𝑃 such that (𝑎(𝑈𝑃𝑉)𝑖) = 𝑏 such that (𝑏‘𝑋) = 𝑔 given hypotheses of fuco23 49027. Such construction should be provable as a functor. Given any 𝑃, it is a morphism part of a functor compatible with the object part, i.e., the functor composition, i.e., the restriction of ∘func, iff both of the following hold. 1. It has the same form as df-fuco 49003 up to fuco23 49027, but ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) might be mapped to a different morphism in category 𝐸. See fucofulem2 48997 for some insights. 2. fuco22nat 49032, fucoid 49034, and fucoco 49043 are satisfied. (Contributed by Zhi Wang, 3-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑂(𝑇 Func 𝑄)𝑃)
Theorem	fucofunca 49046	The functor composition bifunctor is a functor. See also fucofunc 49045. (Contributed by Zhi Wang, 10-Oct-2025.)
⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) ∈ (𝑇 Func 𝑄))
Theorem	fucolid 49047*	Post-compose a natural transformation with an identity natural transformation. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑃)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐺(𝐶 Nat 𝐷)𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → ((𝐼‘𝐹)(⟨𝐹, 𝐺⟩𝑃⟨𝐹, 𝐻⟩)𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐻)‘𝑥))‘(𝐴‘𝑥))))
Theorem	fucorid 49048*	Pre-composing a natural transformation with the identity natural transformation of a functor is pre-composing it with the object part of the functor, in maps-to notation. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑃)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐺(𝐷 Nat 𝐸)𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐴(⟨𝐺, 𝐹⟩𝑃⟨𝐻, 𝐹⟩)(𝐼‘𝐹)) = (𝑥 ∈ (Base‘𝐶) ↦ (𝐴‘((1st ‘𝐹)‘𝑥))))
Theorem	fucorid2 49049	Pre-composing a natural transformation with the identity natural transformation of a functor is pre-composing it with the object part of the functor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ ∘F 𝐸)) = 𝑃)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐺(𝐷 Nat 𝐸)𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐴(⟨𝐺, 𝐹⟩𝑃⟨𝐻, 𝐹⟩)(𝐼‘𝐹)) = (𝐴 ∘ (1st ‘𝐹)))
21.49.14.13  Post-composition functors
Theorem	postcofval 49050*	Value of the post-composition functor as a curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ ⚬ = (⟨𝑅, 𝑄⟩ curryF (⟨𝐶, 𝐷⟩ ∘F 𝐸))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐾 = ((1st ‘ ⚬ )‘𝐹)    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐶 Func 𝐷) ↦ (𝐹 ∘func 𝑔)), (𝑔 ∈ (𝐶 Func 𝐷), ℎ ∈ (𝐶 Func 𝐷) ↦ (𝑎 ∈ (𝑔(𝐶 Nat 𝐷)ℎ) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((((1st ‘𝑔)‘𝑥)(2nd ‘𝐹)((1st ‘ℎ)‘𝑥))‘(𝑎‘𝑥)))))⟩)
Theorem	postcofcl 49051	The post-composition functor as a curry of the functor composition bifunctor is a functor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ ⚬ = (⟨𝑅, 𝑄⟩ curryF (⟨𝐶, 𝐷⟩ ∘F 𝐸))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐾 = ((1st ‘ ⚬ )‘𝐹)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝑄 Func 𝑆))
21.49.14.14  Pre-composition functors
Theorem	precofvallem 49052	Lemma for precofval 49053 to enable catlid 17722 or catrid 17723. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((((𝐹‘𝑋)𝐿(𝐹‘𝑋))‘(( 1 ∘ 𝐹)‘𝑋)) = (𝐼‘(𝐾‘(𝐹‘𝑋))) ∧ (𝐾‘(𝐹‘𝑋)) ∈ 𝐵))
Theorem	precofval 49053*	Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄swapF𝑅))))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹))    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐷 Func 𝐸) ↦ (𝑔 ∘func 𝐹)), (𝑔 ∈ (𝐷 Func 𝐸), ℎ ∈ (𝐷 Func 𝐸) ↦ (𝑎 ∈ (𝑔(𝐷 Nat 𝐸)ℎ) ↦ (𝑥 ∈ (Base‘𝐶) ↦ (𝑎‘((1st ‘𝐹)‘𝑥)))))⟩)
Theorem	precofvalALT 49054*	Alternate proof of precofval 49053. (Contributed by Zhi Wang, 11-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄swapF𝑅))))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹))    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐷 Func 𝐸) ↦ (𝑔 ∘func 𝐹)), (𝑔 ∈ (𝐷 Func 𝐸), ℎ ∈ (𝐷 Func 𝐸) ↦ (𝑎 ∈ (𝑔(𝐷 Nat 𝐸)ℎ) ↦ (𝑥 ∈ (Base‘𝐶) ↦ (𝑎‘((1st ‘𝐹)‘𝑥)))))⟩)
Theorem	precofval2 49055*	Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄swapF𝑅))))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹))    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑔 ∈ (𝐷 Func 𝐸) ↦ (𝑔 ∘func 𝐹)), (𝑔 ∈ (𝐷 Func 𝐸), ℎ ∈ (𝐷 Func 𝐸) ↦ (𝑎 ∈ (𝑔(𝐷 Nat 𝐸)ℎ) ↦ (𝑎 ∘ (1st ‘𝐹))))⟩)
Theorem	precofcl 49056	The pre-composition functor as a transposed curry of the functor composition bifunctor is a functor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → ⚬ = (⟨𝑄, 𝑅⟩ curryF ((⟨𝐶, 𝐷⟩ ∘F 𝐸) ∘func (𝑄swapF𝑅))))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = ((1st ‘ ⚬ )‘𝐹))    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝑅 Func 𝑆))
Theorem	precoffunc 49057*	The pre-composition functor, expressed explicitly, is a functor. (Contributed by Zhi Wang, 11-Oct-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐵 = (𝐷 Func 𝐸)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐾 = (𝑔 ∈ 𝐵 ↦ (𝑔 ∘func ⟨𝐹, 𝐺⟩)))    &   ⊢ (𝜑 → 𝐿 = (𝑔 ∈ 𝐵, ℎ ∈ 𝐵 ↦ (𝑎 ∈ (𝑔𝑁ℎ) ↦ (𝑎 ∘ 𝐹))))    ⇒   ⊢ (𝜑 → 𝐾(𝑅 Func 𝑆)𝐿)
21.49.15  Examples of categories
21.49.15.1  Thin categories
Syntax	cthinc 49058	Extend class notation with the class of thin categories.
class ThinCat
Definition	df-thinc 49059*	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 49060*	The predicate "is a thin category". (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)))
Theorem	isthinc2 49061*	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 49062*	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 49063	A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝐶 ∈ ThinCat → 𝐶 ∈ Cat)
Theorem	thinccd 49064	A thin category is a category (deduction form). (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	thincssc 49065	A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ThinCat ⊆ Cat
Theorem	isthincd2lem1 49066*	Lemma for isthincd2 49077 and thincmo2 49067. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	thincmo2 49067	Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	thincmo 49068*	There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincmoALT 49069*	Alternate proof of thincmo 49068. (Contributed by Zhi Wang, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincmod 49070*	At most one morphism in each hom-set (deduction form). (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincn0eu 49071*	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 49072	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 49073	In a thin category, all morphisms are monomorphisms. The converse does not hold. See grptcmon 49181. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑀 = (Mono‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑋𝐻𝑌))
Theorem	thincepi 49074	In a thin category, all morphisms are epimorphisms. The converse does not hold. See grptcepi 49182. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐸 = (Epi‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑋𝐻𝑌))
Theorem	isthincd2lem2 49075*	Lemma for isthincd2 49077. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))
Theorem	isthincd 49076*	The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ThinCat)
Theorem	isthincd2 49077*	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 49078	The opposite category of a thin category is thin. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat)
Theorem	oppcthinco 49079	If the opposite category of a thin category has the same base and hom-sets as the original category, then it has the same composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂))    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	oppcthinendc 49080*	The opposite category of a thin category whose morphisms are all endomorphisms has the same base, hom-sets (oppcendc 48897) and composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	oppcthinendcALT 49081*	Alternate proof of oppcthinendc 49080. (Contributed by Zhi Wang, 16-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝑂))
Theorem	thincpropd 49082	Two structures with the same base, hom-sets and composition operation are either both thin categories or neither. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ThinCat ↔ 𝐷 ∈ ThinCat))
Theorem	subthinc 49083	A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ThinCat)
Theorem	functhinclem1 49084*	Lemma for functhinc 49088. 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 49085*	Lemma for functhinc 49088. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅ → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))
Theorem	functhinclem3 49086*	Lemma for functhinc 49088. The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))))    &   ⊢ (𝜑 → (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = ∅ → (𝑋𝐻𝑌) = ∅))    &   ⊢ (𝜑 → ∃*𝑛 𝑛 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑀) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	functhinclem4 49087*	Lemma for functhinc 49088. 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 49088*	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 48892), and can be obtained from funcf2 17909, f002 48754, and ralrimivva 3201. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝐻𝑦) × ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝐹‘𝑧)𝐽(𝐹‘𝑤)) = ∅ → (𝑧𝐻𝑤) = ∅))    ⇒   ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐺 = 𝐾))
Theorem	functhincfun 49089	A functor to a thin category is determined entirely by the object part. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ ThinCat)    ⇒   ⊢ (𝜑 → Fun (𝐶 Func 𝐷))
Theorem	fullthinc 49090*	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 49091	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 49092	A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)
Theorem	thincciso 49093*	Two thin categories are isomorphic iff the induced preorders are order-isomorphic. Example 3.26(2) of [Adamek] p. 33. Note that "thincciso.u" is redundant thanks to elbasfv 17249. (Contributed by Zhi Wang, 16-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ 𝐻 = (Hom ‘𝑋)    &   ⊢ 𝐽 = (Hom ‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓(∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 ((𝑥𝐻𝑦) = ∅ ↔ ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) = ∅) ∧ 𝑓:𝑅–1-1-onto→𝑆)))
Theorem	thinccisod 49094*	Two thin categories are isomorphic if the induced preorders are order-isomorphic (deduction form). Example 3.26(2) of [Adamek] p. 33. (Contributed by Zhi Wang, 22-Sep-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ 𝐻 = (Hom ‘𝑋)    &   ⊢ 𝐽 = (Hom ‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    &   ⊢ (𝜑 → 𝐹:𝑅–1-1-onto→𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝑥𝐻𝑦) = ∅ ↔ ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ∅))    ⇒   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)
Theorem	thincciso2 49095	Categories isomorphic to a thin category are thin. Example 3.26(2) of [Adamek] p. 33. Note that "thincciso2.u" is redundant thanks to elbasfv 17249. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑌 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑋 ∈ ThinCat)
Theorem	thincciso3 49096	Categories isomorphic to a thin category are thin. Example 3.26(2) of [Adamek] p. 33. Note that "thincciso2.u" is redundant thanks to elbasfv 17249. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑋 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝑌 ∈ ThinCat)
Theorem	thincciso4 49097	Two isomorphic categories are either both thin or neither. Note that "thincciso2.u" is redundant thanks to elbasfv 17249. (Contributed by Zhi Wang, 18-Oct-2025.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌)    ⇒   ⊢ (𝜑 → (𝑋 ∈ ThinCat ↔ 𝑌 ∈ ThinCat))
Theorem	0thincg 49098	Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ ThinCat)
Theorem	0thinc 49099	The empty category (see 0cat 17728) is thin. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ∅ ∈ ThinCat
Theorem	indthinc 49100*	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 49102, 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‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅)))