P. 501 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50001-50100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0funcALT 50001	Alternate proof of 0func 50000. (Contributed by Zhi Wang, 7-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → (∅ Func 𝐶) = {⟨∅, ∅⟩})
Theorem	func0g 50002	The source category of a functor to the empty category must be empty as well. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐵 = ∅)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐴 = ∅)
Theorem	func0g2 50003	The source category of a functor to the empty category must be empty as well. (Contributed by Zhi Wang, 19-Oct-2025.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝐵 = ∅)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → 𝐴 = ∅)
Theorem	initc 50004*	Sets with empty base are the only initial objects in the category of small categories. Example 7.2(3) of [Adamek] p. 101. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ ((𝐶 ∈ V ∧ ∅ = (Base‘𝐶)) ↔ ∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝐶 Func 𝑑))
Theorem	cofu1st2nd 50005	Rewrite the functor composition with separated functor parts. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = (⟨(1st ‘𝐺), (2nd ‘𝐺)⟩ ∘func ⟨(1st ‘𝐹), (2nd ‘𝐹)⟩))
Theorem	rescofuf 50006	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	cofu1a 50007	Value of the object part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐾‘(𝐹‘𝑋)) = (𝑀‘𝑋))
Theorem	cofu2a 50008	Value of the morphism part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑋𝑁𝑌)‘𝑅))
Theorem	cofucla 50009	The composition of two functors is a functor. Proposition 3.23 of [Adamek] p. 33. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    ⇒   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) ∈ (𝐶 Func 𝐸))
Theorem	funchomf 50010	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 50011	Reverse closure for an identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ ((idfunc‘𝐶) ∈ (𝐷 Func 𝐸) → 𝐶 ∈ Cat)
Theorem	idfu1stf1o 50012	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 50013	Lemma for idfu1sta 50014. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	idfu1sta 50014	Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → (1st ‘𝐼) = ( I ↾ 𝐵))
Theorem	idfu1a 50015	Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝐼)‘𝑋) = 𝑋)
Theorem	idfu2nda 50016	Value of the morphism part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (𝑋(Hom ‘𝐷)𝑌))    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝐼)𝑌) = ( I ↾ 𝐻))
Theorem	imasubclem1 50017*	Lemma for imasubc 50064. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷) ∈ V)
Theorem	imasubclem2 50018*	Lemma for imasubc 50064. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ 𝐾 = (𝑦 ∈ 𝑋, 𝑧 ∈ 𝑌 ↦ ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷))    ⇒   ⊢ (𝜑 → 𝐾 Fn (𝑋 × 𝑌))
Theorem	imasubclem3 50019*	Lemma for imasubc 50064. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ∪ 𝑧 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐺 “ {𝑦}))((𝐻‘𝐶) “ 𝐷))    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = ∪ 𝑧 ∈ ((◡𝐹 “ {𝑋}) × (◡𝐺 “ {𝑌}))((𝐻‘𝐶) “ 𝐷))
Theorem	imaf1homlem 50020	Lemma for imaf1hom 50021 and other theorems. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ({(◡𝐹‘𝑋)} = (◡𝐹 “ {𝑋}) ∧ (𝐹‘(◡𝐹‘𝑋)) = 𝑋 ∧ (◡𝐹‘𝑋) ∈ 𝐵))
Theorem	imaf1hom 50021*	The hom-set of an image of a functor injective on objects. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = (((◡𝐹‘𝑋)𝐺(◡𝐹‘𝑌)) “ ((◡𝐹‘𝑋)𝐻(◡𝐹‘𝑌))))
Theorem	imaidfu2lem 50022	Lemma for imaidfu2 50024. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → ((1st ‘𝐼) “ (Base‘𝐷)) = (Base‘𝐷))
Theorem	imaidfu 50023*	The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ 𝑆 = ((1st ‘𝐼) “ 𝐴)    ⇒   ⊢ (𝜑 → (𝐽 ↾ (𝑆 × 𝑆)) = 𝐾)
Theorem	imaidfu2 50024*	The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝑆 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → 𝐽 = 𝐾)
Theorem	cofid1a 50025	Express the object part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷))    &   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼)    ⇒   ⊢ (𝜑 → ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑋)) = 𝑋)
Theorem	cofid2a 50026	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 50027	Express the object part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    ⇒   ⊢ (𝜑 → (𝐾‘(𝐹‘𝑋)) = 𝑋)
Theorem	cofid2 50028	Express the morphism part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = 𝑅)
Theorem	cofidvala 50029*	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 50030	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 50031	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 50032*	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 50033	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 50034	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.51.15.8  Opposite functors
Syntax	coppf 50035	Extend class notation with the operation generating opposite functors.
class oppFunc
Definition	df-oppf 50036*	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 50054). (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 50037	oppFunc is a function on (V × V). (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ oppFunc Fn (V × V)
Theorem	reldmoppf 50038	The domain of oppFunc is a relation. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ Rel dom oppFunc
Theorem	oppfvalg 50039	Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 oppFunc 𝐺) = if((Rel 𝐺 ∧ Rel dom 𝐺), ⟨𝐹, tpos 𝐺⟩, ∅))
Theorem	oppfrcllem 50040	Lemma for oppfrcl 50041. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → 𝐺 ≠ ∅)
Theorem	oppfrcl 50041	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 50042	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 50043	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 50044	Rewrite the opposite functor into its components (eqopi 8025). (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    &   ⊢ 𝐺 = ( oppFunc ‘𝐹)    &   ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → (𝐺 ∈ (V × V) ∧ ((1st ‘𝐺) = 𝐴 ∧ (2nd ‘𝐺) = tpos 𝐵)))
Theorem	2oppf 50045	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 50046	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 50047	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 50048	Lemma for oppfval 50049. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (Rel 𝐺 ∧ Rel dom 𝐺))
Theorem	oppfval 50049	Value of the opposite functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 oppFunc 𝐺) = ⟨𝐹, tpos 𝐺⟩)
Theorem	oppfval2 50050	Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → ( oppFunc ‘𝐹) = ⟨(1st ‘𝐹), tpos (2nd ‘𝐹)⟩)
Theorem	oppfval3 50051	Value of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 = ⟨𝐺, 𝐾⟩)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) = ⟨𝐺, tpos 𝐾⟩)
Theorem	oppf1 50052	Value of the object part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (1st ‘( oppFunc ‘𝐹)) = (1st ‘𝐹))
Theorem	oppf2 50053	Value of the morphism part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝑀(2nd ‘( oppFunc ‘𝐹))𝑁) = (𝑁(2nd ‘𝐹)𝑀))
Theorem	oppfoppc 50054	The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (𝐹 oppFunc 𝐺) ∈ (𝑂 Func 𝑃))
Theorem	oppfoppc2 50055	The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Func 𝑃))
Theorem	funcoppc2 50056	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 50057	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 50058	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 50059	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 50060	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 50061	The operation generating opposite functors is injective. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    ⇒   ⊢ ( oppFunc ↾ (𝐶 Func 𝐷)):(𝐶 Func 𝐷)–1-1→(𝑂 Func 𝑃)
Theorem	oppff1o 50062	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 50063	Composition of opposite functors. (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (( oppFunc ‘𝐺) ∘func ( oppFunc ‘𝐹)) = ( oppFunc ‘𝐾))
21.51.15.9  Full & faithful functors
Theorem	imasubc 50064*	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 50065*	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 50066*	An image of a functor satisfies the subcategory subset relation. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐽 = (Homf ‘𝐸)    ⇒   ⊢ (𝜑 → 𝐾 ⊆cat 𝐽)
Theorem	imaid 50067*	An image of a functor preserves the identity morphism. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐾𝑋))
Theorem	imaf1co 50068*	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 50069*	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 50070*	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 50071	The inclusion functor is a faithful functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    ⇒   ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 ∈ (𝐷 Faith 𝐸))
Theorem	idemb 50072	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 50073	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 50074	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 18033. (Contributed by Zhi Wang, 11-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐸)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝐼 ∈ (𝐷 Full 𝐸) → (𝐵 ⊆ 𝐶 ∧ (𝐽 ↾ (𝐵 × 𝐵)) = 𝐻))
Theorem	cofidfth 50075	If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then 𝐹 is faithful. Combined with cofidf1 50034, 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 50076	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 50077	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 50078	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.51.15.10  Universal property
Theorem	upciclem1 50079*	Lemma for upcic 50083, upeu 50084, and upeu2 50085. (Contributed by Zhi Wang, 16-Sep-2025.) (Proof shortened by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ (𝑍𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑛 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ∃!𝑙 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑙)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))
Theorem	upciclem2 50080	Lemma for upciclem3 50081 and upeu2 50085. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (((𝑋𝐺𝑍)‘(𝐿(⟨𝑋, 𝑌⟩ · 𝑍)𝐾))(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑍))𝑀) = (((𝑌𝐺𝑍)‘𝐿)(⟨𝑊, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑍))𝑁))
Theorem	upciclem3 50081*	Lemma for upciclem4 50082. (Contributed by Zhi Wang, 17-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑋))    &   ⊢ (𝜑 → 𝑀 = (((𝑌𝐺𝑋)‘𝐿)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑋))𝑁))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (𝐿(⟨𝑋, 𝑌⟩ · 𝑋)𝐾) = ((Id‘𝐷)‘𝑋))
Theorem	upciclem4 50082*	Lemma for upcic 50083 and upeu 50084. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    &   ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐷)𝑌 ∧ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)))
Theorem	upcic 50083*	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 50084*	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 50085*	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 50086	Extend class notation with the class of universal properties.
class UP
Definition	df-up 50087*	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 50108), and can be generated from an existing universal pair by isomorphisms (upeu4 50109). See also oppcup 50120 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 50088	The domain of UP is a relation. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ Rel dom UP
Theorem	upfval 50089*	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 50090*	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 50091*	Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽(𝐹‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑥)⟩𝑂(𝐹‘𝑦))𝑚))})
Theorem	isuplem 50092*	Lemma for isup 50093 and other theorems. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))))
Theorem	isup 50093*	The predicate "is a universal pair". (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)))
Theorem	uppropd 50094	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 50095	The domain of (𝐷 UP 𝐸) is a relation. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ Rel dom (𝐷 UP 𝐸)
Theorem	relup 50096	The set of universal pairs is a relation. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ Rel (𝐹(𝐷 UP 𝐸)𝑊)
Theorem	uprcl 50097	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊) → (𝐹 ∈ (𝐷 Func 𝐸) ∧ 𝑊 ∈ 𝐶))
Theorem	up1st2nd 50098	Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)
Theorem	up1st2ndr 50099	Combine separated parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀)
Theorem	up1st2ndb 50100	Combine/separate parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀 ↔ 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀))