P. 493 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49201-49300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	func0g2 49201	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 49202*	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 49203	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 49204	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 49205	Value of the object part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐾‘(𝐹‘𝑋)) = (𝑀‘𝑋))
Theorem	cofu2a 49206	Value of the morphism part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑋𝑁𝑌)‘𝑅))
Theorem	cofucla 49207	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 49208	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 49209	Reverse closure for an identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ ((idfunc‘𝐶) ∈ (𝐷 Func 𝐸) → 𝐶 ∈ Cat)
Theorem	idfu1stf1o 49210	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 49211	Lemma for idfu1sta 49212. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	idfu1sta 49212	Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → (1st ‘𝐼) = ( I ↾ 𝐵))
Theorem	idfu1a 49213	Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝐼)‘𝑋) = 𝑋)
Theorem	idfu2nda 49214	Value of the morphism part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 = (𝑋(Hom ‘𝐷)𝑌))    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝐼)𝑌) = ( I ↾ 𝐻))
Theorem	imasubclem1 49215*	Lemma for imasubc 49262. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷) ∈ V)
Theorem	imasubclem2 49216*	Lemma for imasubc 49262. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ 𝐾 = (𝑦 ∈ 𝑋, 𝑧 ∈ 𝑌 ↦ ∪ 𝑥 ∈ ((◡𝐹 “ 𝐴) × (◡𝐺 “ 𝐵))((𝐻‘𝐶) “ 𝐷))    ⇒   ⊢ (𝜑 → 𝐾 Fn (𝑋 × 𝑌))
Theorem	imasubclem3 49217*	Lemma for imasubc 49262. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐾 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ∪ 𝑧 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐺 “ {𝑦}))((𝐻‘𝐶) “ 𝐷))    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = ∪ 𝑧 ∈ ((◡𝐹 “ {𝑋}) × (◡𝐺 “ {𝑌}))((𝐻‘𝐶) “ 𝐷))
Theorem	imaf1homlem 49218	Lemma for imaf1hom 49219 and other theorems. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ({(◡𝐹‘𝑋)} = (◡𝐹 “ {𝑋}) ∧ (𝐹‘(◡𝐹‘𝑋)) = 𝑋 ∧ (◡𝐹‘𝑋) ∈ 𝐵))
Theorem	imaf1hom 49219*	The hom-set of an image of a functor injective on objects. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = (((◡𝐹‘𝑋)𝐺(◡𝐹‘𝑌)) “ ((◡𝐹‘𝑋)𝐻(◡𝐹‘𝑌))))
Theorem	imaidfu2lem 49220	Lemma for imaidfu2 49222. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → ((1st ‘𝐼) “ (Base‘𝐷)) = (Base‘𝐷))
Theorem	imaidfu 49221*	The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ 𝑆 = ((1st ‘𝐼) “ 𝐴)    ⇒   ⊢ (𝜑 → (𝐽 ↾ (𝑆 × 𝑆)) = 𝐾)
Theorem	imaidfu2 49222*	The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 Func 𝐸))    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡(1st ‘𝐼) “ {𝑥}) × (◡(1st ‘𝐼) “ {𝑦}))(((2nd ‘𝐼)‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝑆 = (Base‘𝐷))    ⇒   ⊢ (𝜑 → 𝐽 = 𝐾)
Theorem	cofid1a 49223	Express the object part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐸 Func 𝐷))    &   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = 𝐼)    ⇒   ⊢ (𝜑 → ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑋)) = 𝑋)
Theorem	cofid2a 49224	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 49225	Express the object part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    ⇒   ⊢ (𝜑 → (𝐾‘(𝐹‘𝑋)) = 𝑋)
Theorem	cofid2 49226	Express the morphism part of (𝐺 ∘func 𝐹) = 𝐼 explicitly. (Contributed by Zhi Wang, 15-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐸 Func 𝐷)𝐿)    &   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩ ∘func ⟨𝐹, 𝐺⟩) = 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = 𝑅)
Theorem	cofidvala 49227*	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 49228	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 49229	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 49230*	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 49231	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 49232	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 49233	Extend class notation with the operation generating opposite functors.
class oppFunc
Definition	df-oppf 49234*	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 49252). (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 49235	oppFunc is a function on (V × V). (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ oppFunc Fn (V × V)
Theorem	reldmoppf 49236	The domain of oppFunc is a relation. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ Rel dom oppFunc
Theorem	oppfvalg 49237	Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 oppFunc 𝐺) = if((Rel 𝐺 ∧ Rel dom 𝐺), ⟨𝐹, tpos 𝐺⟩, ∅))
Theorem	oppfrcllem 49238	Lemma for oppfrcl 49239. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    ⇒   ⊢ (𝜑 → 𝐺 ≠ ∅)
Theorem	oppfrcl 49239	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 49240	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 49241	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 49242	Rewrite the opposite functor into its components (eqopi 7957). (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑅)    &   ⊢ Rel 𝑅    &   ⊢ 𝐺 = ( oppFunc ‘𝐹)    &   ⊢ (𝜑 → 𝐹 = ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → (𝐺 ∈ (V × V) ∧ ((1st ‘𝐺) = 𝐴 ∧ (2nd ‘𝐺) = tpos 𝐵)))
Theorem	2oppf 49243	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 49244	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 49245	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 49246	Lemma for oppfval 49247. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (Rel 𝐺 ∧ Rel dom 𝐺))
Theorem	oppfval 49247	Value of the opposite functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 oppFunc 𝐺) = ⟨𝐹, tpos 𝐺⟩)
Theorem	oppfval2 49248	Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → ( oppFunc ‘𝐹) = ⟨(1st ‘𝐹), tpos (2nd ‘𝐹)⟩)
Theorem	oppfval3 49249	Value of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 = ⟨𝐺, 𝐾⟩)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) = ⟨𝐺, tpos 𝐾⟩)
Theorem	oppf1 49250	Value of the object part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (1st ‘( oppFunc ‘𝐹)) = (1st ‘𝐹))
Theorem	oppf2 49251	Value of the morphism part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝑀(2nd ‘( oppFunc ‘𝐹))𝑁) = (𝑁(2nd ‘𝐹)𝑀))
Theorem	oppfoppc 49252	The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    ⇒   ⊢ (𝜑 → (𝐹 oppFunc 𝐺) ∈ (𝑂 Func 𝑃))
Theorem	oppfoppc2 49253	The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( oppFunc ‘𝐹) ∈ (𝑂 Func 𝑃))
Theorem	funcoppc2 49254	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 49255	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 49256	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 49257	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 49258	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 49259	The operation generating opposite functors is injective. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    ⇒   ⊢ ( oppFunc ↾ (𝐶 Func 𝐷)):(𝐶 Func 𝐷)–1-1→(𝑂 Func 𝑃)
Theorem	oppff1o 49260	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 49261	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 49262*	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 49263*	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 49264*	An image of a functor satisfies the subcategory subset relation. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐽 = (Homf ‘𝐸)    ⇒   ⊢ (𝜑 → 𝐾 ⊆cat 𝐽)
Theorem	imaid 49265*	An image of a functor preserves the identity morphism. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ 𝑆 = (𝐹 “ 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ((◡𝐹 “ {𝑥}) × (◡𝐹 “ {𝑦}))((𝐺‘𝑝) “ (𝐻‘𝑝)))    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ 𝐼 = (Id‘𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐾𝑋))
Theorem	imaf1co 49266*	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 49267*	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 49268*	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 49269	The inclusion functor is a faithful functor. (Contributed by Zhi Wang, 10-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    ⇒   ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 ∈ (𝐷 Faith 𝐸))
Theorem	idemb 49270	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 49271	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 49272	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 17847. (Contributed by Zhi Wang, 11-Nov-2025.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐷)    &   ⊢ 𝐽 = (Homf ‘𝐸)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝐼 ∈ (𝐷 Full 𝐸) → (𝐵 ⊆ 𝐶 ∧ (𝐽 ↾ (𝐵 × 𝐵)) = 𝐻))
Theorem	cofidfth 49273	If "𝐹 is a section of 𝐺 " in a category of small categories (in a universe), then 𝐹 is faithful. Combined with cofidf1 49232, 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 49274	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 49275	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 49276	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 49277*	Lemma for upcic 49281, upeu 49282, and upeu2 49283. (Contributed by Zhi Wang, 16-Sep-2025.) (Proof shortened by Zhi Wang, 5-Nov-2025.)
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ (𝑍𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑛 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ∃!𝑙 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑙)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))
Theorem	upciclem2 49278	Lemma for upciclem3 49279 and upeu2 49283. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (((𝑋𝐺𝑍)‘(𝐿(⟨𝑋, 𝑌⟩ · 𝑍)𝐾))(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑍))𝑀) = (((𝑌𝐺𝑍)‘𝐿)(⟨𝑊, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑍))𝑁))
Theorem	upciclem3 49279*	Lemma for upciclem4 49280. (Contributed by Zhi Wang, 17-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑋))    &   ⊢ (𝜑 → 𝑀 = (((𝑌𝐺𝑋)‘𝐿)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑋))𝑁))    &   ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))    ⇒   ⊢ (𝜑 → (𝐿(⟨𝑋, 𝑌⟩ · 𝑋)𝐾) = ((Id‘𝐷)‘𝑋))
Theorem	upciclem4 49280*	Lemma for upcic 49281 and upeu 49282. (Contributed by Zhi Wang, 19-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))    &   ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))    ⇒   ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐷)𝑌 ∧ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)))
Theorem	upcic 49281*	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 49282*	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 49283*	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 49284	Extend class notation with the class of universal properties.
class UP
Definition	df-up 49285*	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 49306), and can be generated from an existing universal pair by isomorphisms (upeu4 49307). See also oppcup 49318 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 49286	The domain of UP is a relation. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ Rel dom UP
Theorem	upfval 49287*	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 49288*	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 49289*	Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽(𝐹‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑥)⟩𝑂(𝐹‘𝑦))𝑚))})
Theorem	isuplem 49290*	Lemma for isup 49291 and other theorems. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))))
Theorem	isup 49291*	The predicate "is a universal pair". (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐶 = (Base‘𝐸)    &   ⊢ 𝐻 = (Hom ‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐸)    &   ⊢ 𝑂 = (comp‘𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋)))    ⇒   ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)))
Theorem	uppropd 49292	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 49293	The domain of (𝐷 UP 𝐸) is a relation. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ Rel dom (𝐷 UP 𝐸)
Theorem	relup 49294	The set of universal pairs is a relation. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ Rel (𝐹(𝐷 UP 𝐸)𝑊)
Theorem	uprcl 49295	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊) → (𝐹 ∈ (𝐷 Func 𝐸) ∧ 𝑊 ∈ 𝐶))
Theorem	up1st2nd 49296	Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)
Theorem	up1st2ndr 49297	Combine separated parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀)
Theorem	up1st2ndb 49298	Combine/separate parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀 ↔ 𝑋(⟨(1st ‘𝐹), (2nd ‘𝐹)⟩(𝐷 UP 𝐸)𝑊)𝑀))
Theorem	up1st2nd2 49299	Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ (𝐹(𝐷 UP 𝐸)𝑊))    ⇒   ⊢ (𝜑 → (1st ‘𝑋)(𝐹(𝐷 UP 𝐸)𝑊)(2nd ‘𝑋))
Theorem	uprcl2 49300	Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.)
⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷 UP 𝐸)𝑊)𝑀)    ⇒   ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)