P. 497 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49601-49700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	funchomf 49601	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 49602	Reverse closure for an identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ ((idfunc‘𝐶) ∈ (𝐷 Func 𝐸) → 𝐶 ∈ Cat)
Theorem	idfu1stf1o 49603	The identity functor/inclusion functor is bijective on objects. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → (1st ‘𝐼):𝐵–1-1-onto→𝐵)
Theorem	idfu1stalem 49604	Lemma for idfu1sta 49605. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	idfu1sta 49605	Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → (1st ‘𝐼) = ( I ↾ 𝐵))
Theorem	idfu1a 49606	Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝐼)‘𝑋) = 𝑋)
Theorem	idfu2nda 49607	Value of the morphism part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (𝑋(Hom ‘𝐷)𝑌))    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝐼)𝑌) = ( I ↾ 𝐻))
Theorem	imasubclem1 49608*	Lemma for imasubc 49655. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷) ∈ V)
Theorem	imasubclem2 49609*	Lemma for imasubc 49655. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ 𝐾 = (𝑦 ∈ 𝑋, 𝑧 ∈ 𝑌 ↦ ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷))    ⇒   ⊢ (𝜑 → 𝐾 Fn (𝑋 × 𝑌))
Theorem	imasubclem3 49610*	Lemma for imasubc 49655. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ∪ 𝑧 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐺 “ {𝑦}))((𝐻‘𝐶) “ 𝐷))    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = ∪ 𝑧 ∈ ((◡𝐹 “ {𝑋}) × (◡𝐺 “ {𝑌}))((𝐻‘𝐶) “ 𝐷))
Theorem	imaf1homlem 49611	Lemma for imaf1hom 49612 and other theorems. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ({(◡𝐹‘𝑋)} = (◡𝐹 “ {𝑋}) ∧ (𝐹‘(◡𝐹‘𝑋)) = 𝑋 ∧ (◡𝐹‘𝑋) ∈ 𝐵))
Theorem	imaf1hom 49612*	The hom-set of an image of a functor injective on objects. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = (((◡𝐹‘𝑋)𝐺(◡𝐹‘𝑌)) “ ((◡𝐹‘𝑋)𝐻(◡𝐹‘𝑌))))
Theorem	imaidfu2lem 49613	Lemma for imaidfu2 49615. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → ((1st ‘𝐼) “ (Base‘𝐷)) = (Base‘𝐷))
Theorem	imaidfu 49614*	The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ 𝑆 = ((1st ‘𝐼) “ 𝐴)    ⇒   ⊢ (𝜑 → (𝐽 ↾ (𝑆 × 𝑆)) = 𝐾)
Theorem	imaidfu2 49615*	The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝑆 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → 𝐽 = 𝐾)
Theorem	cofid1a 49616	Express the object part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷))    &   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼)    ⇒   ⊢ (𝜑 → ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑋)) = 𝑋)
Theorem	cofid2a 49617	Express the morphism part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷))    &   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌))‘((𝑋(2nd ‘𝐹)𝑌)‘𝑅)) = 𝑅)
Theorem	cofid1 49618	Express the object part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    ⇒   ⊢ (𝜑 → (𝐾‘(𝐹‘𝑋)) = 𝑋)
Theorem	cofid2 49619	Express the morphism part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = 𝑅)
Theorem	cofidvala 49620*	The property "𝐹 is a section of 𝐺 " in a category of small categories (in a universe); expressed explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷))    &   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼)    &   ⊢ 𝐻 = (Hom ‘𝐷)    ⇒   ⊢ (𝜑 → (((1st ‘𝐺) ∘ (1st ‘𝐹)) = ( I ↾ 𝐵) ∧ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) = (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))))
Theorem	cofidf2a 49621	If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then the morphism part of 𝐹 is injective, and the morphism part of 𝐺 is surjective in the image of 𝐹. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷))    &   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘𝐹)𝑌):(𝑋𝐻𝑌)–1-1→(((1st ‘𝐹)‘𝑋)𝐽((1st ‘𝐹)‘𝑌)) ∧ (((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌)):(((1st ‘𝐹)‘𝑋)𝐽((1st ‘𝐹)‘𝑌))–onto→(𝑋𝐻𝑌)))
Theorem	cofidf1a 49622	If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then the object part of 𝐹 is injective, and the object part of 𝐺 is surjective. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷))    &   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼)    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → ((1st ‘𝐹):𝐵–1-1→𝐶 ∧ (1st ‘𝐺):𝐶–onto→𝐵))
Theorem	cofidval 49623*	The property "⟨𝐹, 𝐺⟩ is a section of ⟨𝐾, 𝐿⟩ " in a category of small categories (in a universe); expressed explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    &   ⊢ 𝐻 = (Hom ‘𝐷)    ⇒   ⊢ (𝜑 → ((𝐾 ∘ 𝐹) = ( I ↾ 𝐵) ∧ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐿(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦))) = (𝑧 ∈ (𝐵 × 𝐵) ↦ ( I ↾ (𝐻‘𝑧)))))
Theorem	cofidf2 49624	If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then the morphism part of 𝐹 is injective, and the morphism part of 𝐺 is surjective in the image of 𝐹. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋𝐺𝑌):(𝑋𝐻𝑌)–1-1→((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ∧ ((𝐹‘𝑋)𝐿(𝐹‘𝑌)):((𝐹‘𝑋)𝐽(𝐹‘𝑌))–onto→(𝑋𝐻𝑌)))
Theorem	cofidf1 49625	If "⟨𝐹, 𝐺⟩ is a section of ⟨𝐾, 𝐿⟩ " in a category of small categories (in a universe), then 𝐹 is injective, and 𝐾 is surjective. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → (𝐹:𝐵–1-1→𝐶 ∧ 𝐾:𝐶–onto→𝐵))
21.49.15.8  Opposite functors
Syntax	coppf 49626	Extend class notation with the operation generating opposite functors.
class oppFunc
Definition	df-oppf 49627*	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 49645). (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	oppffn 49628	oppFunc is a function on (V × V). (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ oppFunc Fn (V × V)
Theorem	reldmoppf 49629	The domain of oppFunc is a relation. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ Rel dom oppFunc
Theorem	oppfvalg 49630	Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 oppFunc 𝐺) = if((Rel 𝐺 ∧ Rel dom 𝐺), ⟨𝐹, tpos 𝐺⟩, ∅))
Theorem	oppfrcllem 49631	Lemma for oppfrcl 49632. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → 𝐺 ≠ ∅)
Theorem	oppfrcl 49632	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 49633	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 49634	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 49635	Rewrite the opposite functor into its components (eqopi 7971). (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    &   ⊢ 𝐺 = ( oppFunc ‘𝐹)    &   ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → (𝐺 ∈ (V × V) ∧ ((1st ‘𝐺) = 𝐴 ∧ (2nd ‘𝐺) = tpos 𝐵)))
Theorem	2oppf 49636	The double opposite functor is the original functor. Remark 3.42 of [Adamek] p. 39. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    &   ⊢ 𝐺 = ( oppFunc ‘𝐹)    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐺) = 𝐹)
Theorem	eloppf 49637	The pre-image of a non-empty opposite functor is non-empty; and the second component of the pre-image is a relation on triples. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ 𝐺 = ( oppFunc ‘𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (𝐹 ≠ ∅ ∧ (Rel (2nd ‘𝐹) ∧ Rel dom (2nd ‘𝐹))))
Theorem	eloppf2 49638	Both components of a pre-image of a non-empty opposite functor exist; and the second component is a relation on triples. (Contributed by Zhi Wang, 18-Nov-2025.)
⊢ (𝐹 oppFunc 𝐺) = 𝐾    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Rel 𝐺 ∧ Rel dom 𝐺)))
Theorem	oppfvallem 49639	Lemma for oppfval 49640. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (Rel 𝐺 ∧ Rel dom 𝐺))
Theorem	oppfval 49640	Value of the opposite functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 oppFunc 𝐺) = ⟨𝐹, tpos 𝐺⟩)
Theorem	oppfval2 49641	Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → ( oppFunc ‘𝐹) = ⟨(1st ‘𝐹), tpos (2nd ‘𝐹)⟩)
Theorem	oppfval3 49642	Value of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 = ⟨𝐺, 𝐾⟩)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) = ⟨𝐺, tpos 𝐾⟩)
Theorem	oppf1 49643	Value of the object part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (1st ‘( oppFunc ‘𝐹)) = (1st ‘𝐹))
Theorem	oppf2 49644	Value of the morphism part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝑀(2nd ‘( oppFunc ‘𝐹))𝑁) = (𝑁(2nd ‘𝐹)𝑀))
Theorem	oppfoppc 49645	The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (𝐹 oppFunc 𝐺) ∈ (𝑂 Func 𝑃))
Theorem	oppfoppc2 49646	The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Func 𝑃))
Theorem	funcoppc2 49647	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 49648	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 49649	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 49650	The opposite functor of an opposite functor is a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025.) The functor in opposite categories does not have to be an opposite functor. (Revised by Zhi Wang, 17-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑃))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝐶 Func 𝐷))
Theorem	funcoppc3 49651	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 𝐷)𝐺)
Theorem	oppff1 49652	The operation generating opposite functors is injective. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    ⇒   ⊢ ( oppFunc ↾ (𝐶 Func 𝐷)):(𝐶 Func 𝐷)–1-1→(𝑂 Func 𝑃)
Theorem	oppff1o 49653	The operation generating opposite functors is bijective. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ( oppFunc ↾ (𝐶 Func 𝐷)):(𝐶 Func 𝐷)–1-1-onto→(𝑂 Func 𝑃))
Theorem	cofuoppf 49654	Composition of opposite functors. (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (( oppFunc ‘𝐺) ∘func ( oppFunc ‘𝐹)) = ( oppFunc ‘𝐾))
21.49.15.9  Full & faithful functors
Theorem	imasubc 49655*	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 49656*	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 49657*	An image of a functor satisfies the subcategory subset relation. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐽 = (Homf ‘𝐸)    ⇒   ⊢ (𝜑 → 𝐾 ⊆cat 𝐽)
Theorem	imaid 49658*	An image of a functor preserves the identity morphism. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐾𝑋))
Theorem	imaf1co 49659*	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 49660*	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 49661*	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 49662	The inclusion functor is a faithful functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    ⇒   ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 ∈ (𝐷 Faith 𝐸))
Theorem	idemb 49663	The inclusion functor is an embedding. Remark 4.4(1) in [Adamek] p. 49. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    ⇒   ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → (𝐼 ∈ (𝐷 Faith 𝐸) ∧ Fun ◡(1st ‘𝐼)))
Theorem	idsubc 49664	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 49665	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 17902. (Contributed by Zhi Wang, 11-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐸)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝐼 ∈ (𝐷 Full 𝐸) → (𝐵 ⊆ 𝐶 ∧ (𝐽 ↾ (𝐵 × 𝐵)) = 𝐻))
Theorem	cofidfth 49666	If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then 𝐹 is faithful. Combined with cofidf1 49625, this theorem proves that 𝐹 is an embedding (a faithful functor injective on objects, remark 3.28(1) of [Adamek] p. 34). (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    ⇒   ⊢ (𝜑 → 𝐹(𝐷 Faith 𝐸)𝐺)
Theorem	fulloppf 49667	The opposite functor of a full functor is also full. Proposition 3.43(d) in [Adamek] p. 39. (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Full 𝐷))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Full 𝑃))
Theorem	fthoppf 49668	The opposite functor of a faithful functor is also faithful. Proposition 3.43(c) in [Adamek] p. 39. (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Faith 𝐷))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Faith 𝑃))
Theorem	ffthoppf 49669	The opposite functor of a fully faithful functor is also full and faithful. (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷)))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ ((𝑂 Full 𝑃) ∩ (𝑂 Faith 𝑃)))
21.49.15.10  Universal property
Theorem	upciclem1 49670*	Lemma for upcic 49674, upeu 49675, and upeu2 49676. (Contributed by Zhi Wang, 16-Sep-2025.) (Proof shortened by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ (𝑍𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑛 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ∃!𝑙 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑙)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))
Theorem	upciclem2 49671	Lemma for upciclem3 49672 and upeu2 49676. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (((𝑋𝐺𝑍)‘(𝐿(⟨𝑋, 𝑌⟩ · 𝑍)𝐾))(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑍))𝑀) = (((𝑌𝐺𝑍)‘𝐿)(⟨𝑊, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑍))𝑁))
Theorem	upciclem3 49672*	Lemma for upciclem4 49673. (Contributed by Zhi Wang, 17-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑋))    &   ⊢ (𝜑 → 𝑀 = (((𝑌𝐺𝑋)‘𝐿)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑋))𝑁))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (𝐿(⟨𝑋, 𝑌⟩ · 𝑋)𝐾) = ((Id‘𝐷)‘𝑋))
Theorem	upciclem4 49673*	Lemma for upcic 49674 and upeu 49675. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    &   ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐷)𝑌 ∧ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)))
Theorem	upcic 49674*	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 49675*	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 49676*	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 49677	Extend class notation with the class of universal properties.
class UP
Definition	df-up 49678*	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 49699), and can be generated from an existing universal pair by isomorphisms (upeu4 49700). See also oppcup 49711 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 49679	The domain of UP is a relation. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ Rel dom UP
Theorem	upfval 49680*	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 49681*	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 49682*	Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽(𝐹‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑥)⟩𝑂(𝐹‘𝑦))𝑚))})
Theorem	isuplem 49683*	Lemma for isup 49684 and other theorems. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))))
Theorem	isup 49684*	The predicate "is a universal pair". (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)))
Theorem	uppropd 49685	If two categories have the same set of objects, morphisms, and compositions, then they have the same universal pairs. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 UP 𝐶) = (𝐵 UP 𝐷))
Theorem	reldmup2 49686	The domain of (𝐷 UP 𝐸) is a relation. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ Rel dom (𝐷 UP 𝐸)
Theorem	relup 49687	The set of universal pairs is a relation. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ Rel (𝐹(𝐷 UP 𝐸)𝑊)
Theorem	uprcl 49688	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊) → (𝐹 ∈ (𝐷 Func 𝐸) ∧ 𝑊 ∈ 𝐶))
Theorem	up1st2nd 49689	Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)
Theorem	up1st2ndr 49690	Combine separated parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀)
Theorem	up1st2ndb 49691	Combine/separate parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀 ↔ 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀))
Theorem	up1st2nd2 49692	Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊))    ⇒   ⊢ (𝜑 → (1st ‘𝑋)(𝐹(𝐷 UP 𝐸)𝑊)(2nd ‘𝑋))
Theorem	uprcl2 49693	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
Theorem	uprcl3 49694	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝑊 ∈ 𝐶)
Theorem	uprcl4 49695	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    &   ⊢ 𝐵 = (Base‘𝐷)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	uprcl5 49696	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    &   ⊢ 𝐽 = (Hom ‘𝐸)    ⇒   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))
Theorem	uobrcl 49697	Reverse closure for universal object. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (𝑋 ∈ dom (𝐹(𝐷 UP 𝐸)𝑊) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
Theorem	isup2 49698*	The universal property of a universal pair. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))
Theorem	upeu3 49699*	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 49700	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 𝐸)𝑊)𝑁)