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	0funcALT 49001	Alternate proof of 0func 49000. (Contributed by Zhi Wang, 7-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → (∅ Func 𝐶) = {⟨∅, ∅⟩})
Theorem	func0g 49002	The source cateogry of a functor to the empty category must be empty as well. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐵 = ∅)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐴 = ∅)
Theorem	func0g2 49003	The source cateogry of a functor to the empty category must be empty as well. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐵 = ∅)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → 𝐴 = ∅)
Theorem	rescofuf 49004	The restriction of functor composition is a function from product functor space to functor space. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ ( ∘func ↾ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))):((𝐷 Func 𝐸) × (𝐶 Func 𝐷))⟶(𝐶 Func 𝐸)
Theorem	funchomf 49005	Source categories of a functor have the same set of objects and morphisms. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ (𝜑 → 𝐹(𝐴 Func 𝐶)𝐺)    &   ⊢ (𝜑 → 𝐹(𝐵 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))
Theorem	idfurcl 49006	Reverse closure for an identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ ((idfunc‘𝐶) ∈ (𝐷 Func 𝐸) → 𝐶 ∈ Cat)
Theorem	idfu1stalem 49007	Lemma for idfu1sta 49008. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	idfu1sta 49008	Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → (1st ‘𝐼) = ( I ↾ 𝐵))
Theorem	idfu1a 49009	Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝐼)‘𝑋) = 𝑋)
Theorem	idfu2nda 49010	Value of the morphism part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (𝑋(Hom ‘𝐷)𝑌))    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝐼)𝑌) = ( I ↾ 𝐻))
Theorem	imasubclem1 49011*	Lemma for imasubc 49039. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷) ∈ V)
Theorem	imasubclem2 49012*	Lemma for imasubc 49039. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ 𝐾 = (𝑦 ∈ 𝑋, 𝑧 ∈ 𝑌 ↦ ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷))    ⇒   ⊢ (𝜑 → 𝐾 Fn (𝑋 × 𝑌))
Theorem	imasubclem3 49013*	Lemma for imasubc 49039. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ∪ 𝑧 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐺 “ {𝑦}))((𝐻‘𝐶) “ 𝐷))    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = ∪ 𝑧 ∈ ((◡𝐹 “ {𝑋}) × (◡𝐺 “ {𝑌}))((𝐻‘𝐶) “ 𝐷))
Theorem	imaf1homlem 49014	Lemma for imaf1hom 49015 and other theorems. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ({(◡𝐹‘𝑋)} = (◡𝐹 “ {𝑋}) ∧ (𝐹‘(◡𝐹‘𝑋)) = 𝑋 ∧ (◡𝐹‘𝑋) ∈ 𝐵))
Theorem	imaf1hom 49015*	The hom-set of an image of a functor injective on objects. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = (((◡𝐹‘𝑋)𝐺(◡𝐹‘𝑌)) “ ((◡𝐹‘𝑋)𝐻(◡𝐹‘𝑌))))
Theorem	imaidfu2lem 49016	Lemma for imaidfu2 49018. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → ((1st ‘𝐼) “ (Base‘𝐷)) = (Base‘𝐷))
Theorem	imaidfu 49017*	The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ 𝑆 = ((1st ‘𝐼) “ 𝐴)    ⇒   ⊢ (𝜑 → (𝐽 ↾ (𝑆 × 𝑆)) = 𝐾)
Theorem	imaidfu2 49018*	The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝑆 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → 𝐽 = 𝐾)
21.49.15.8  Opposite functors
Syntax	coppf 49019	Extend class notation with the operation generating opposite functors.
class oppFunc
Definition	df-oppf 49020*	Definition of the operation generating opposite functors. Definition 3.41 of [Adamek] p. 39. The object part of the functor is unchanged while the morphism part is transposed due to reversed direction of arrows in the opposite category. The opposite functor is a functor on opposite categories (oppfoppc 49032). (Contributed by Zhi Wang, 4-Nov-2025.) Better reverse closure. (Revised by Zhi Wang, 13-Nov-2025.)
⊢ oppFunc = (𝑓 ∈ V, 𝑔 ∈ V ↦ if((Rel 𝑔 ∧ Rel dom 𝑔), ⟨𝑓, tpos 𝑔⟩, ∅))
Theorem	reldmoppf 49021	The domain of oppFunc is a relation. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ Rel dom oppFunc
Theorem	oppfvalg 49022	Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹oppFunc𝐺) = if((Rel 𝐺 ∧ Rel dom 𝐺), ⟨𝐹, tpos 𝐺⟩, ∅))
Theorem	oppfrcllem 49023	Lemma for oppfrcl 49024. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → 𝐺 ≠ ∅)
Theorem	oppfrcl 49024	If an opposite functor of a class is a functor, then the original class must be an ordered pair. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    &   ⊢ 𝐺 = (oppFunc‘𝐹)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (V × V))
Theorem	oppfrcl2 49025	If an opposite functor of a class is a functor, then the two components of the original class must be sets. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    &   ⊢ 𝐺 = (oppFunc‘𝐹)    &   ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	oppfrcl3 49026	If an opposite functor of a class is a functor, then the second component of the original class must be a relation whose domain is a relation as well. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    &   ⊢ 𝐺 = (oppFunc‘𝐹)    &   ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → (Rel 𝐵 ∧ Rel dom 𝐵))
Theorem	oppf1st2nd 49027	Rewrite the opposite functor into its components (eqopi 8022). (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    &   ⊢ 𝐺 = (oppFunc‘𝐹)    &   ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → (𝐺 ∈ (V × V) ∧ ((1st ‘𝐺) = 𝐴 ∧ (2nd ‘𝐺) = tpos 𝐵)))
Theorem	2oppf 49028	The double opposite functor is the original functor. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    &   ⊢ 𝐺 = (oppFunc‘𝐹)    ⇒   ⊢ (𝜑 → (oppFunc‘𝐺) = 𝐹)
Theorem	oppfvallem 49029	Lemma for oppfval 49030. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (Rel 𝐺 ∧ Rel dom 𝐺))
Theorem	oppfval 49030	Value of the opposite functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹oppFunc𝐺) = ⟨𝐹, tpos 𝐺⟩)
Theorem	oppfval2 49031	Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (oppFunc‘𝐹) = ⟨(1st ‘𝐹), tpos (2nd ‘𝐹)⟩)
Theorem	oppfoppc 49032	The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (𝐹oppFunc𝐺) ∈ (𝑂 Func 𝑃))
Theorem	oppfoppc2 49033	The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (oppFunc‘𝐹) ∈ (𝑂 Func 𝑃))
Theorem	funcoppc2 49034	A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹(𝑂 Func 𝑃)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)tpos 𝐺)
Theorem	funcoppc4 49035	A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐹oppFunc𝐺) ∈ (𝑂 Func 𝑃))    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)
Theorem	funcoppc5 49036	A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (oppFunc‘𝐹) ∈ (𝑂 Func 𝑃))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
Theorem	2oppffunc 49037	The opposite functor of an opposite functor is a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ 𝐺 = (oppFunc‘𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑃))    ⇒   ⊢ (𝜑 → (oppFunc‘𝐺) ∈ (𝐶 Func 𝐷))
Theorem	funcoppc3 49038	A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹(𝑂 Func 𝑃)tpos 𝐺)    &   ⊢ (𝜑 → 𝐺 Fn (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)
21.49.15.9  Full & faithful functors
Theorem	imasubc 49039*	An image of a full functor is a full subcategory. Remark 4.2(3) of [Adamek] p. 48. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Full 𝐸)𝐺)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐽 = (Homf ‘𝐸)    ⇒   ⊢ (𝜑 → (𝐾 Fn (𝑆 × 𝑆) ∧ 𝑆 ⊆ 𝐶 ∧ (𝐽 ↾ (𝑆 × 𝑆)) = 𝐾))
Theorem	imasubc2 49040*	An image of a full functor is a (full) subcategory. Remark 4.2(3) of [Adamek] p. 48. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Full 𝐸)𝐺)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐸))
Theorem	imassc 49041*	An image of a functor satisfies the subcategory subset relation. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐽 = (Homf ‘𝐸)    ⇒   ⊢ (𝜑 → 𝐾 ⊆cat 𝐽)
Theorem	imaid 49042*	An image of a functor preserves the identity morphism. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐾𝑋))
Theorem	imaf1co 49043*	An image of a functor whose object part is injective preserves the composition. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ ∙ = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐾𝑌))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐾𝑍))    ⇒   ⊢ (𝜑 → (𝑁(⟨𝑋, 𝑌⟩ ∙ 𝑍)𝑀) ∈ (𝑋𝐾𝑍))
Theorem	imasubc3 49044*	An image of a functor injective on objects is a subcategory. Remark 4.2(3) of [Adamek] p. 48. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → Fun ◡𝐹)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐸))
Theorem	fthcomf 49045*	Source categories of a faithful functor have the same base, hom-sets and composition operation if the composition is compatible in images of the functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ (𝜑 → 𝐹(𝐴 Faith 𝐶)𝐺)    &   ⊢ (𝜑 → 𝐹(𝐵 Func 𝐷)𝐺)    &   ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴) ∧ 𝑧 ∈ (Base‘𝐴))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐴)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐴)𝑧))) → (((𝑦𝐺𝑧)‘𝑔)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐶)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))    ⇒   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))
Theorem	idfth 49046	The inclusion functor is a faithful functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    ⇒   ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 ∈ (𝐷 Faith 𝐸))
Theorem	idsubc 49047	The source category of an inclusion functor is a subcategory of the target category. See also Remark 4.4 in [Adamek] p. 49. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐷)    ⇒   ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐻 ∈ (Subcat‘𝐸))
Theorem	idfullsubc 49048	The source category of an inclusion functor is a full subcategory of the target category if the inclusion functor is full. Remark 4.4(2) in [Adamek] p. 49. See also ressffth 17951. (Contributed by Zhi Wang, 11-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐸)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝐼 ∈ (𝐷 Full 𝐸) → (𝐵 ⊆ 𝐶 ∧ (𝐽 ↾ (𝐵 × 𝐵)) = 𝐻))
21.49.15.10  Universal property
Theorem	upciclem1 49049*	Lemma for upcic 49053, upeu 49054, and upeu2 49055. (Contributed by Zhi Wang, 16-Sep-2025.) (Proof shortened by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ (𝑍𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑛 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ∃!𝑙 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑙)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))
Theorem	upciclem2 49050	Lemma for upciclem3 49051 and upeu2 49055. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (((𝑋𝐺𝑍)‘(𝐿(⟨𝑋, 𝑌⟩ · 𝑍)𝐾))(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑍))𝑀) = (((𝑌𝐺𝑍)‘𝐿)(⟨𝑊, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑍))𝑁))
Theorem	upciclem3 49051*	Lemma for upciclem4 49052. (Contributed by Zhi Wang, 17-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑋))    &   ⊢ (𝜑 → 𝑀 = (((𝑌𝐺𝑋)‘𝐿)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑋))𝑁))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (𝐿(⟨𝑋, 𝑌⟩ · 𝑋)𝐾) = ((Id‘𝐷)‘𝑋))
Theorem	upciclem4 49052*	Lemma for upcic 49053 and upeu 49054. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    &   ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐷)𝑌 ∧ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)))
Theorem	upcic 49053*	A universal property defines an object up to isomorphism given its existence. (Contributed by Zhi Wang, 17-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    &   ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))    ⇒   ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐷)𝑌)
Theorem	upeu 49054*	A universal property defines an essentially unique (strong form) pair of object 𝑋 and morphism 𝑀 if it exists. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    &   ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))    ⇒   ⊢ (𝜑 → ∃!𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))
Theorem	upeu2 49055*	Generate new universal morphism through isomorphism from existing universal object. (Contributed by Zhi Wang, 20-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ 𝐼 = (Iso‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)) ∧ ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)))
Syntax	cup 49056	Extend class notation with the class of universal properties.
class UP
Definition	df-up 49057*	Definition of the class of universal properties. Given categories 𝐷 and 𝐸, if 𝐹:𝐷⟶𝐸 is a functor and 𝑊 an object of 𝐸, a universal pair from 𝑊 to 𝐹 is a pair ⟨𝑋, 𝑀⟩ consisting of an object 𝑋 of 𝐷 and a morphism 𝑀:𝑊⟶𝐹𝑋 of 𝐸, such that to every pair ⟨𝑦, 𝑔⟩ with 𝑦 an object of 𝐷 and 𝑔:𝑊⟶𝐹𝑦 a morphism of 𝐸, there is a unique morphism 𝑘:𝑋⟶𝑦 of 𝐷 with 𝐹𝑘 ⚬ 𝑀 = 𝑔. Such property is commonly referred to as a universal property. In our definition, it is denoted as 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀. Note that the universal pair is termed differently as "universal arrow" in p. 55 of Mac Lane, Saunders, Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf (retrieved 6 Oct 2025). Interestingly, the "universal arrow" is referring to the morphism 𝑀 instead of the pair near the end of the same piece of the text, causing name collision. The name "universal arrow" is also adopted in papers such as https://arxiv.org/pdf/2212.08981. Alternatively, the universal pair is called the "universal morphism" in Wikipedia (https://en.wikipedia.org/wiki/Universal_property) as well as published works, e.g., https://arxiv.org/pdf/2412.12179. But the pair ⟨𝑋, 𝑀⟩ should be named differently as the morphism 𝑀, and thus we call 𝑋 the universal object, 𝑀 the universal morphism, and ⟨𝑋, 𝑀⟩ the universal pair. Given its existence, such universal pair is essentially unique (upeu3 49076), and can be generated from an existing universal pair by isomorphisms (upeu4 49077). See also oppcup 49088 for the dual concept. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ UP = (𝑑 ∈ V, 𝑒 ∈ V ↦ ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}))
Theorem	reldmup 49058	The domain of UP is a relation. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ Rel dom UP
Theorem	upfval 49059*	Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.) (Proof shortened by Zhi Wang, 12-Nov-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    ⇒   ⊢ (𝐷 UP 𝐸) = (𝑓 ∈ (𝐷 Func 𝐸), 𝑤 ∈ 𝐶 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑤𝐽((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑤𝐽((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑂((1st ‘𝑓)‘𝑦))𝑚))})
Theorem	upfval2 49060*	Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝐹(𝐷 UP 𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽((1st ‘𝐹)‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽((1st ‘𝐹)‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥(2nd ‘𝐹)𝑦)‘𝑘)(⟨𝑊, ((1st ‘𝐹)‘𝑥)⟩𝑂((1st ‘𝐹)‘𝑦))𝑚))})
Theorem	upfval3 49061*	Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽(𝐹‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑥)⟩𝑂(𝐹‘𝑦))𝑚))})
Theorem	isuplem 49062*	Lemma for isup 49063 and other theorems. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))))
Theorem	isup 49063*	The predicate "is a universal pair". (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)))
Theorem	reldmup2 49064	The domain of (𝐷 UP 𝐸) is a relation. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ Rel dom (𝐷 UP 𝐸)
Theorem	relup 49065	The set of universal pairs is a relation. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ Rel (𝐹(𝐷 UP 𝐸)𝑊)
Theorem	uprcl 49066	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊) → (𝐹 ∈ (𝐷 Func 𝐸) ∧ 𝑊 ∈ 𝐶))
Theorem	up1st2nd 49067	Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)
Theorem	up1st2ndr 49068	Combine separated parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀)
Theorem	up1st2ndb 49069	Combine/separate parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀 ↔ 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀))
Theorem	up1st2nd2 49070	Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊))    ⇒   ⊢ (𝜑 → (1st ‘𝑋)(𝐹(𝐷 UP 𝐸)𝑊)(2nd ‘𝑋))
Theorem	uprcl2 49071	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
Theorem	uprcl3 49072	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝑊 ∈ 𝐶)
Theorem	uprcl4 49073	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    &   ⊢ 𝐵 = (Base‘𝐷)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	uprcl5 49074	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    &   ⊢ 𝐽 = (Hom ‘𝐸)    ⇒   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))
Theorem	isup2 49075*	The universal property of a universal pair. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))
Theorem	upeu3 49076*	The universal pair ⟨𝑋, 𝑀⟩ from object 𝑊 to functor ⟨𝐹, 𝐺⟩ is essentially unique (strong form) if it exists. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ (𝜑 → 𝐼 = (Iso‘𝐷))    &   ⊢ (𝜑 → ⚬ = (⟨𝑊, (𝐹‘𝑋)⟩(comp‘𝐸)(𝐹‘𝑌)))    &   ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    &   ⊢ (𝜑 → 𝑌(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑁)    ⇒   ⊢ (𝜑 → ∃!𝑟 ∈ (𝑋𝐼𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟) ⚬ 𝑀))
Theorem	upeu4 49077	Generate a new universal morphism through an isomorphism from an existing universal object, and pair with the codomain of the isomorphism to form a universal pair. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝐼 = (Iso‘𝐷))    &   ⊢ (𝜑 → ⚬ = (⟨𝑊, (𝐹‘𝑋)⟩(comp‘𝐸)(𝐹‘𝑌)))    &   ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾) ⚬ 𝑀))    ⇒   ⊢ (𝜑 → 𝑌(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑁)
Theorem	uptposlem 49078	Lemma for uptpos 49079. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀)    &   ⊢ (𝜑 → tpos 𝐺 = 𝐻)    ⇒   ⊢ (𝜑 → tpos 𝐻 = 𝐺)
Theorem	uptpos 49079	Rewrite the predicate of universal property in the form of opposite functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀)    &   ⊢ (𝜑 → tpos 𝐺 = 𝐻)    ⇒   ⊢ (𝜑 → 𝑋(⟨𝐹, tpos 𝐻⟩(𝑂 UP 𝑃)𝑊)𝑀)
Theorem	oppcuprcl4 49080	Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀)    &   ⊢ 𝑂 = (oppCat‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	oppcuprcl3 49081	Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀)    &   ⊢ 𝑃 = (oppCat‘𝐸)    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝑊 ∈ 𝐶)
Theorem	oppcuprcl5 49082	Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀)    &   ⊢ 𝑃 = (oppCat‘𝐸)    &   ⊢ 𝐽 = (Hom ‘𝐸)    ⇒   ⊢ (𝜑 → 𝑀 ∈ ((𝐹‘𝑋)𝐽𝑊))
Theorem	oppcuprcl2 49083	Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀)    &   ⊢ 𝑃 = (oppCat‘𝐸)    &   ⊢ 𝑂 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → tpos 𝐺 = 𝐻)    ⇒   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐻)
Theorem	uprcl2a 49084	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝑋(𝐺(𝑂 UP 𝑃)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑃))
Theorem	oppfuprcl 49085	Reverse closure for the class of universal property for opposite functors. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝑋(𝐺(𝑂 UP 𝑃)𝑊)𝑀)    &   ⊢ 𝐺 = (oppFunc‘𝐹)    &   ⊢ 𝑂 = (oppCat‘𝐷)    &   ⊢ 𝑃 = (oppCat‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))
Theorem	oppfuprcl2 49086	Reverse closure for the class of universal property for opposite functors. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝑋(𝐺(𝑂 UP 𝑃)𝑊)𝑀)    &   ⊢ 𝐺 = (oppFunc‘𝐹)    &   ⊢ 𝑂 = (oppCat‘𝐷)    &   ⊢ 𝑃 = (oppCat‘𝐸)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → 𝐴(𝐷 Func 𝐸)𝐵)
Theorem	oppcup3lem 49087*	Lemma for oppcup3 49090. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ ((𝐹‘𝑦)𝐽𝑍)∃!𝑘 ∈ (𝑦𝐻𝑋)𝑛 = (𝑀(⟨(𝐹‘𝑦), (𝐹‘𝑋)⟩𝑂𝑍)((𝑦𝐺𝑋)‘𝑘)))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ((𝐹‘𝑌)𝐽𝑍))    ⇒   ⊢ (𝜑 → ∃!𝑙 ∈ (𝑌𝐻𝑋)𝑁 = (𝑀(⟨(𝐹‘𝑌), (𝐹‘𝑋)⟩𝑂𝑍)((𝑌𝐺𝑋)‘𝑙)))
Theorem	oppcup 49088*	The universal pair ⟨𝑋, 𝑀⟩ from a functor to an object is universal from an object to a functor in the opposite category. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ ∙ = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ((𝐹‘𝑋)𝐽𝑊))    &   ⊢ 𝑂 = (oppCat‘𝐷)    &   ⊢ 𝑃 = (oppCat‘𝐸)    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, tpos 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ ((𝐹‘𝑦)𝐽𝑊)∃!𝑘 ∈ (𝑦𝐻𝑋)𝑔 = (𝑀(⟨(𝐹‘𝑦), (𝐹‘𝑋)⟩ ∙ 𝑊)((𝑦𝐺𝑋)‘𝑘))))
Theorem	oppcup2 49089*	The universal property for the universal pair ⟨𝑋, 𝑀⟩ from a functor to an object, expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ ∙ = (comp‘𝐸)    &   ⊢ 𝑂 = (oppCat‘𝐷)    &   ⊢ 𝑃 = (oppCat‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋(⟨𝐹, tpos 𝐺⟩(𝑂 UP 𝑃)𝑊)𝑀)    ⇒   ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ ((𝐹‘𝑦)𝐽𝑊)∃!𝑘 ∈ (𝑦𝐻𝑋)𝑔 = (𝑀(⟨(𝐹‘𝑦), (𝐹‘𝑋)⟩ ∙ 𝑊)((𝑦𝐺𝑋)‘𝑘)))
Theorem	oppcup3 49090*	The universal property for the universal pair ⟨𝑋, 𝑀⟩ from a functor to an object, expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ ∙ = (comp‘𝐸)    &   ⊢ 𝑂 = (oppCat‘𝐷)    &   ⊢ 𝑃 = (oppCat‘𝐸)    &   ⊢ (𝜑 → 𝑋(⟨𝐹, 𝑇⟩(𝑂 UP 𝑃)𝑊)𝑀)    &   ⊢ (𝜑 → tpos 𝑇 = 𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ((𝐹‘𝑌)𝐽𝑊))    ⇒   ⊢ (𝜑 → ∃!𝑘 ∈ (𝑌𝐻𝑋)𝑁 = (𝑀(⟨(𝐹‘𝑌), (𝐹‘𝑋)⟩ ∙ 𝑊)((𝑌𝐺𝑋)‘𝑘)))
21.49.15.11  Natural transformations and the functor category
Theorem	isnatd 49091*	Property of being a natural transformation; deduction form. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿)    &   ⊢ (𝜑 → 𝐴 Fn 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐴‘𝑥) ∈ ((𝐹‘𝑥)𝐽(𝐾‘𝑥)))    &   ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ℎ ∈ (𝑥𝐻𝑦)) → ((𝐴‘𝑦)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(⟨(𝐹‘𝑥), (𝐾‘𝑥)⟩ · (𝐾‘𝑦))(𝐴‘𝑥)))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))
Theorem	natrcl2 49092	Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    ⇒   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)
Theorem	natrcl3 49093	Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    ⇒   ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿)
Theorem	catbas 49094	The base of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩}    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ 𝐵 = (Base‘𝐶)
Theorem	cathomfval 49095	The hom-sets of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩}    &   ⊢ 𝐻 ∈ V    ⇒   ⊢ 𝐻 = (Hom ‘𝐶)
Theorem	catcofval 49096	Composition of the category structure. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩}    &   ⊢ · ∈ V    ⇒   ⊢ · = (comp‘𝐶)
21.49.15.12  Initial, terminal and zero objects of a category
Theorem	initoo2 49097	An initial object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ 𝐵)
Theorem	termoo2 49098	A terminal object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ 𝐵)
Theorem	zeroo2 49099	A zero object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝑂 ∈ (ZeroO‘𝐶) → 𝑂 ∈ 𝐵)
Theorem	oppcinito 49100	Initial objects are terminal in the opposite category. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝐼 ∈ (InitO‘𝐶) ↔ 𝐼 ∈ (TermO‘(oppCat‘𝐶)))