P. 492 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49101-49200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	func0g2 49101	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 49102*	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 49103	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 49104	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 49105	Value of the object part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐾‘(𝐹‘𝑋)) = (𝑀‘𝑋))
Theorem	cofu2a 49106	Value of the morphism part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑋𝑁𝑌)‘𝑅))
Theorem	cofucla 49107	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 49108	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 49109	Reverse closure for an identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ ((idfunc‘𝐶) ∈ (𝐷 Func 𝐸) → 𝐶 ∈ Cat)
Theorem	idfu1stf1o 49110	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 49111	Lemma for idfu1sta 49112. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	idfu1sta 49112	Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → (1st ‘𝐼) = ( I ↾ 𝐵))
Theorem	idfu1a 49113	Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝐼)‘𝑋) = 𝑋)
Theorem	idfu2nda 49114	Value of the morphism part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (𝑋(Hom ‘𝐷)𝑌))    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝐼)𝑌) = ( I ↾ 𝐻))
Theorem	imasubclem1 49115*	Lemma for imasubc 49162. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷) ∈ V)
Theorem	imasubclem2 49116*	Lemma for imasubc 49162. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ 𝐾 = (𝑦 ∈ 𝑋, 𝑧 ∈ 𝑌 ↦ ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷))    ⇒   ⊢ (𝜑 → 𝐾 Fn (𝑋 × 𝑌))
Theorem	imasubclem3 49117*	Lemma for imasubc 49162. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ∪ 𝑧 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐺 “ {𝑦}))((𝐻‘𝐶) “ 𝐷))    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = ∪ 𝑧 ∈ ((◡𝐹 “ {𝑋}) × (◡𝐺 “ {𝑌}))((𝐻‘𝐶) “ 𝐷))
Theorem	imaf1homlem 49118	Lemma for imaf1hom 49119 and other theorems. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ({(◡𝐹‘𝑋)} = (◡𝐹 “ {𝑋}) ∧ (𝐹‘(◡𝐹‘𝑋)) = 𝑋 ∧ (◡𝐹‘𝑋) ∈ 𝐵))
Theorem	imaf1hom 49119*	The hom-set of an image of a functor injective on objects. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = (((◡𝐹‘𝑋)𝐺(◡𝐹‘𝑌)) “ ((◡𝐹‘𝑋)𝐻(◡𝐹‘𝑌))))
Theorem	imaidfu2lem 49120	Lemma for imaidfu2 49122. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → ((1st ‘𝐼) “ (Base‘𝐷)) = (Base‘𝐷))
Theorem	imaidfu 49121*	The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ 𝑆 = ((1st ‘𝐼) “ 𝐴)    ⇒   ⊢ (𝜑 → (𝐽 ↾ (𝑆 × 𝑆)) = 𝐾)
Theorem	imaidfu2 49122*	The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝑆 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → 𝐽 = 𝐾)
Theorem	cofid1a 49123	Express the object part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷))    &   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼)    ⇒   ⊢ (𝜑 → ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑋)) = 𝑋)
Theorem	cofid2a 49124	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 49125	Express the object part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    ⇒   ⊢ (𝜑 → (𝐾‘(𝐹‘𝑋)) = 𝑋)
Theorem	cofid2 49126	Express the morphism part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = 𝑅)
Theorem	cofidvala 49127*	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 49128	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 49129	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 49130*	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 49131	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 49132	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 49133	Extend class notation with the operation generating opposite functors.
class oppFunc
Definition	df-oppf 49134*	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 49152). (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 49135	oppFunc is a function on (V × V). (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ oppFunc Fn (V × V)
Theorem	reldmoppf 49136	The domain of oppFunc is a relation. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ Rel dom oppFunc
Theorem	oppfvalg 49137	Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 oppFunc 𝐺) = if((Rel 𝐺 ∧ Rel dom 𝐺), ⟨𝐹, tpos 𝐺⟩, ∅))
Theorem	oppfrcllem 49138	Lemma for oppfrcl 49139. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → 𝐺 ≠ ∅)
Theorem	oppfrcl 49139	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 49140	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 49141	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 49142	Rewrite the opposite functor into its components (eqopi 7952). (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    &   ⊢ 𝐺 = ( oppFunc ‘𝐹)    &   ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → (𝐺 ∈ (V × V) ∧ ((1st ‘𝐺) = 𝐴 ∧ (2nd ‘𝐺) = tpos 𝐵)))
Theorem	2oppf 49143	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 49144	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 49145	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 49146	Lemma for oppfval 49147. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (Rel 𝐺 ∧ Rel dom 𝐺))
Theorem	oppfval 49147	Value of the opposite functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 oppFunc 𝐺) = ⟨𝐹, tpos 𝐺⟩)
Theorem	oppfval2 49148	Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → ( oppFunc ‘𝐹) = ⟨(1st ‘𝐹), tpos (2nd ‘𝐹)⟩)
Theorem	oppfval3 49149	Value of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 = ⟨𝐺, 𝐾⟩)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) = ⟨𝐺, tpos 𝐾⟩)
Theorem	oppf1 49150	Value of the object part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (1st ‘( oppFunc ‘𝐹)) = (1st ‘𝐹))
Theorem	oppf2 49151	Value of the morphism part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝑀(2nd ‘( oppFunc ‘𝐹))𝑁) = (𝑁(2nd ‘𝐹)𝑀))
Theorem	oppfoppc 49152	The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (𝐹 oppFunc 𝐺) ∈ (𝑂 Func 𝑃))
Theorem	oppfoppc2 49153	The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Func 𝑃))
Theorem	funcoppc2 49154	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 49155	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 49156	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 49157	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 49158	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 49159	The operation generating opposite functors is injective. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    ⇒   ⊢ ( oppFunc ↾ (𝐶 Func 𝐷)):(𝐶 Func 𝐷)–1-1→(𝑂 Func 𝑃)
Theorem	oppff1o 49160	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 49161	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 49162*	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 49163*	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 49164*	An image of a functor satisfies the subcategory subset relation. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐽 = (Homf ‘𝐸)    ⇒   ⊢ (𝜑 → 𝐾 ⊆cat 𝐽)
Theorem	imaid 49165*	An image of a functor preserves the identity morphism. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐾𝑋))
Theorem	imaf1co 49166*	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 49167*	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 49168*	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 49169	The inclusion functor is a faithful functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    ⇒   ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 ∈ (𝐷 Faith 𝐸))
Theorem	idemb 49170	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 49171	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 49172	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 17839. (Contributed by Zhi Wang, 11-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐸)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝐼 ∈ (𝐷 Full 𝐸) → (𝐵 ⊆ 𝐶 ∧ (𝐽 ↾ (𝐵 × 𝐵)) = 𝐻))
Theorem	cofidfth 49173	If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then 𝐹 is faithful. Combined with cofidf1 49132, 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 49174	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 49175	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 49176	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 49177*	Lemma for upcic 49181, upeu 49182, and upeu2 49183. (Contributed by Zhi Wang, 16-Sep-2025.) (Proof shortened by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ (𝑍𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑛 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ∃!𝑙 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑙)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))
Theorem	upciclem2 49178	Lemma for upciclem3 49179 and upeu2 49183. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (((𝑋𝐺𝑍)‘(𝐿(⟨𝑋, 𝑌⟩ · 𝑍)𝐾))(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑍))𝑀) = (((𝑌𝐺𝑍)‘𝐿)(⟨𝑊, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑍))𝑁))
Theorem	upciclem3 49179*	Lemma for upciclem4 49180. (Contributed by Zhi Wang, 17-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑋))    &   ⊢ (𝜑 → 𝑀 = (((𝑌𝐺𝑋)‘𝐿)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑋))𝑁))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (𝐿(⟨𝑋, 𝑌⟩ · 𝑋)𝐾) = ((Id‘𝐷)‘𝑋))
Theorem	upciclem4 49180*	Lemma for upcic 49181 and upeu 49182. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    &   ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐷)𝑌 ∧ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)))
Theorem	upcic 49181*	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 49182*	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 49183*	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 49184	Extend class notation with the class of universal properties.
class UP
Definition	df-up 49185*	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 49206), and can be generated from an existing universal pair by isomorphisms (upeu4 49207). See also oppcup 49218 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 49186	The domain of UP is a relation. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ Rel dom UP
Theorem	upfval 49187*	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 49188*	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 49189*	Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽(𝐹‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑥)⟩𝑂(𝐹‘𝑦))𝑚))})
Theorem	isuplem 49190*	Lemma for isup 49191 and other theorems. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))))
Theorem	isup 49191*	The predicate "is a universal pair". (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)))
Theorem	uppropd 49192	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 49193	The domain of (𝐷 UP 𝐸) is a relation. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ Rel dom (𝐷 UP 𝐸)
Theorem	relup 49194	The set of universal pairs is a relation. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ Rel (𝐹(𝐷 UP 𝐸)𝑊)
Theorem	uprcl 49195	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊) → (𝐹 ∈ (𝐷 Func 𝐸) ∧ 𝑊 ∈ 𝐶))
Theorem	up1st2nd 49196	Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)
Theorem	up1st2ndr 49197	Combine separated parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀)
Theorem	up1st2ndb 49198	Combine/separate parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀 ↔ 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀))
Theorem	up1st2nd2 49199	Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊))    ⇒   ⊢ (𝜑 → (1st ‘𝑋)(𝐹(𝐷 UP 𝐸)𝑊)(2nd ‘𝑋))
Theorem	uprcl2 49200	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)