P. 183 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18201-18300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xpchom2 18201	Value of the set of morphisms in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝑌 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑌)    &   ⊢ 𝐾 = (Hom ‘𝑇)    ⇒   ⊢ (𝜑 → (⟨𝑀, 𝑁⟩𝐾⟨𝑃, 𝑄⟩) = ((𝑀𝐻𝑃) × (𝑁𝐽𝑄)))
Theorem	xpcco2 18202	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝑌 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑌)    &   ⊢ · = (comp‘𝐶)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ 𝑂 = (comp‘𝑇)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀𝐻𝑃))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑁𝐽𝑄))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃𝐻𝑅))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑄𝐽𝑆))    ⇒   ⊢ (𝜑 → (⟨𝐾, 𝐿⟩(⟨⟨𝑀, 𝑁⟩, ⟨𝑃, 𝑄⟩⟩𝑂⟨𝑅, 𝑆⟩)⟨𝐹, 𝐺⟩) = ⟨(𝐾(⟨𝑀, 𝑃⟩ · 𝑅)𝐹), (𝐿(⟨𝑁, 𝑄⟩ ∙ 𝑆)𝐺)⟩)
Theorem	xpccatid 18203*	The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝑌 = (Base‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ 𝐽 = (Id‘𝐷)    ⇒   ⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩)))
Theorem	xpcid 18204	The identity morphism in the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝑌 = (Base‘𝐷)    &   ⊢ 𝐼 = (Id‘𝐶)    &   ⊢ 𝐽 = (Id‘𝐷)    &   ⊢ 1 = (Id‘𝑇)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    ⇒   ⊢ (𝜑 → ( 1 ‘⟨𝑅, 𝑆⟩) = ⟨(𝐼‘𝑅), (𝐽‘𝑆)⟩)
Theorem	xpccat 18205	The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑇 ∈ Cat)
Theorem	1stfval 18206*	Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑃 = (𝐶 1stF 𝐷)    ⇒   ⊢ (𝜑 → 𝑃 = ⟨(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))⟩)
Theorem	1stf1 18207	Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑃 = (𝐶 1stF 𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝑃)‘𝑅) = (1st ‘𝑅))
Theorem	1stf2 18208	Value of the first projection on a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑃 = (𝐶 1stF 𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑅(2nd ‘𝑃)𝑆) = (1st ↾ (𝑅𝐻𝑆)))
Theorem	2ndfval 18209*	Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 2ndF 𝐷)    ⇒   ⊢ (𝜑 → 𝑄 = ⟨(2nd ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (2nd ↾ (𝑥𝐻𝑦)))⟩)
Theorem	2ndf1 18210	Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 2ndF 𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝑄)‘𝑅) = (2nd ‘𝑅))
Theorem	2ndf2 18211	Value of the first projection on a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 2ndF 𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑅(2nd ‘𝑄)𝑆) = (2nd ↾ (𝑅𝐻𝑆)))
Theorem	1stfcl 18212	The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑃 = (𝐶 1stF 𝐷)    ⇒   ⊢ (𝜑 → 𝑃 ∈ (𝑇 Func 𝐶))
Theorem	2ndfcl 18213	The second projection functor is a functor onto the right argument. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 2ndF 𝐷)    ⇒   ⊢ (𝜑 → 𝑄 ∈ (𝑇 Func 𝐷))
Theorem	prfval 18214*	Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → 𝑃 = ⟨(𝑥 ∈ 𝐵 ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (ℎ ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))⟩)
Theorem	prf1 18215	Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝑃)‘𝑋) = ⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)⟩)
Theorem	prf2fval 18216*	Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝑃)𝑌) = (ℎ ∈ (𝑋𝐻𝑌) ↦ ⟨((𝑋(2nd ‘𝐹)𝑌)‘ℎ), ((𝑋(2nd ‘𝐺)𝑌)‘ℎ)⟩))
Theorem	prf2 18217	Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘𝑃)𝑌)‘𝐾) = ⟨((𝑋(2nd ‘𝐹)𝑌)‘𝐾), ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)⟩)
Theorem	prfcl 18218	The pairing of functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐷 is a functor ⟨𝐹, 𝐺⟩:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝑇 = (𝐷 ×c 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇))
Theorem	prf1st 18219	Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → ((𝐷 1stF 𝐸) ∘func 𝑃) = 𝐹)
Theorem	prf2nd 18220	Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺)
Theorem	1st2ndprf 18221	Break a functor into a product category into first and second projections. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑇 = (𝐷 ×c 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝑇))    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐹 = (((𝐷 1stF 𝐸) ∘func 𝐹) ⟨,⟩F ((𝐷 2ndF 𝐸) ∘func 𝐹)))
Theorem	catcxpccl 18222	The category of categories for a weak universe is closed under the product category operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑇 = (𝑋 ×c 𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑇 ∈ 𝐵)
Theorem	xpcpropd 18223	If two categories have the same set of objects, morphisms, and compositions, then they have the same product category. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 ×c 𝐶) = (𝐵 ×c 𝐷))
8.4.2  Functor evaluation
Syntax	cevlf 18224	Extend class notation with the evaluation functor.
class evalF
Syntax	ccurf 18225	Extend class notation with the currying of a functor.
class curryF
Syntax	cuncf 18226	Extend class notation with the uncurrying of a functor.
class uncurryF
Syntax	cdiag 18227	Extend class notation to include the diagonal functor.
class Δfunc
Definition	df-evlf 18228*	Define the evaluation functor, which is the extension of the evaluation map 𝑓, 𝑥 ↦ (𝑓‘𝑥) of functors, to a functor (𝐶⟶𝐷) × 𝐶⟶𝐷. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ evalF = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ ⟨(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝑑)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩)
Definition	df-curf 18229*	Define the curry functor, which maps a functor 𝐹:𝐶 × 𝐷⟶𝐸 to curryF (𝐹):𝐶⟶(𝐷⟶𝐸). (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ curryF = (𝑒 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑒) / 𝑐⦌⦋(2nd ‘𝑒) / 𝑑⦌⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩)
Definition	df-uncf 18230*	Define the uncurry functor, which can be defined equationally using evalF. Strictly speaking, the third category argument is not needed, since the resulting functor is extensionally equal regardless, but it is used in the equational definition and is too much work to remove. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))
Definition	df-diag 18231*	Define the diagonal functor, which is the functor 𝐶⟶(𝐷 Func 𝐶) whose object part is 𝑥 ∈ 𝐶 ↦ (𝑦 ∈ 𝐷 ↦ 𝑥). The value of the functor at an object 𝑥 is the constant functor which maps all objects in 𝐷 to 𝑥 and all morphisms to 1(𝑥). The morphism part is a natural transformation between these functors, which takes 𝑓:𝑥⟶𝑦 to the natural transformation with every component equal to 𝑓. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ Δfunc = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ (⟨𝑐, 𝑑⟩ curryF (𝑐 1stF 𝑑)))
Theorem	evlfval 18232*	Value of the evaluation functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = (𝐶 evalF 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    ⇒   ⊢ (𝜑 → 𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩ · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩)
Theorem	evlf2 18233*	Value of the evaluation functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = (𝐶 evalF 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐿 = (⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)    ⇒   ⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))))
Theorem	evlf2val 18234	Value of the evaluation natural transformation at an object. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = (𝐶 evalF 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐿 = (⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (𝐴𝐿𝐾) = ((𝐴‘𝑌)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝐾)))
Theorem	evlf1 18235	Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = (𝐶 evalF 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹(1st ‘𝐸)𝑋) = ((1st ‘𝐹)‘𝑋))
Theorem	evlfcllem 18236	Lemma for evlfcl 18237. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = (𝐶 evalF 𝐷)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (Base‘𝐶)))    &   ⊢ (𝜑 → (𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ (Base‘𝐶)))    &   ⊢ (𝜑 → (𝐻 ∈ (𝐶 Func 𝐷) ∧ 𝑍 ∈ (Base‘𝐶)))    &   ⊢ (𝜑 → (𝐴 ∈ (𝐹𝑁𝐺) ∧ 𝐾 ∈ (𝑋(Hom ‘𝐶)𝑌)))    &   ⊢ (𝜑 → (𝐵 ∈ (𝐺𝑁𝐻) ∧ 𝐿 ∈ (𝑌(Hom ‘𝐶)𝑍)))    ⇒   ⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘(⟨𝐵, 𝐿⟩(⟨⟨𝐹, 𝑋⟩, ⟨𝐺, 𝑌⟩⟩(comp‘(𝑄 ×c 𝐶))⟨𝐻, 𝑍⟩)⟨𝐴, 𝐾⟩)) = (((⟨𝐺, 𝑌⟩(2nd ‘𝐸)⟨𝐻, 𝑍⟩)‘⟨𝐵, 𝐿⟩)(⟨((1st ‘𝐸)‘⟨𝐹, 𝑋⟩), ((1st ‘𝐸)‘⟨𝐺, 𝑌⟩)⟩(comp‘𝐷)((1st ‘𝐸)‘⟨𝐻, 𝑍⟩))((⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑌⟩)‘⟨𝐴, 𝐾⟩)))
Theorem	evlfcl 18237	The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors 𝐶⟶𝐷, and the second parameter in 𝐷. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = (𝐶 evalF 𝐷)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝐶) Func 𝐷))
Theorem	curfval 18238*	Value of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐷)    ⇒   ⊢ (𝜑 → 𝐺 = ⟨(𝑥 ∈ 𝐴 ↦ ⟨(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)(𝐼‘𝑧)))))⟩)
Theorem	curf1fval 18239*	Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → (1st ‘𝐺) = (𝑥 ∈ 𝐴 ↦ ⟨(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩))
Theorem	curf1 18240*	Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
Theorem	curf11 18241	Value of the double evaluated curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝐾)‘𝑌) = (𝑋(1st ‘𝐹)𝑌))
Theorem	curf12 18242	The partially evaluated curry functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑌𝐽𝑍))    ⇒   ⊢ (𝜑 → ((𝑌(2nd ‘𝐾)𝑍)‘𝐻) = (( 1 ‘𝑋)(⟨𝑋, 𝑌⟩(2nd ‘𝐹)⟨𝑋, 𝑍⟩)𝐻))
Theorem	curf1cl 18243	The partially evaluated curry functor is a functor. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))
Theorem	curf2 18244*	Value of the curry functor at a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)    ⇒   ⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))))
Theorem	curf2val 18245	Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐿‘𝑍) = (𝐾(⟨𝑋, 𝑍⟩(2nd ‘𝐹)⟨𝑌, 𝑍⟩)(𝐼‘𝑍)))
Theorem	curf2cl 18246	The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐼 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)    &   ⊢ 𝑁 = (𝐷 Nat 𝐸)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌)))
Theorem	curfcl 18247	The curry functor of a functor 𝐹:𝐶 × 𝐷⟶𝐸 is a functor curryF (𝐹):𝐶⟶(𝐷⟶𝐸). (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝑄))
Theorem	curfpropd 18248	If two categories have the same set of objects, morphisms, and compositions, then they curry the same functor to the same result. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ Cat)    &   ⊢ (𝜑 → 𝐵 ∈ Cat)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴 ×c 𝐶) Func 𝐸))    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐶⟩ curryF 𝐹) = (⟨𝐵, 𝐷⟩ curryF 𝐹))
Theorem	uncfval 18249	Value of the uncurry functor, which is the reverse of the curry functor, taking 𝐺:𝐶⟶(𝐷⟶𝐸) to uncurryF (𝐺):𝐶 × 𝐷⟶𝐸. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)))    ⇒   ⊢ (𝜑 → 𝐹 = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func (𝐶 1stF 𝐷)) ⟨,⟩F (𝐶 2ndF 𝐷))))
Theorem	uncfcl 18250	The uncurry operation takes a functor 𝐹:𝐶⟶(𝐷⟶𝐸) to a functor uncurryF (𝐹):𝐶 × 𝐷⟶𝐸. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
Theorem	uncf1 18251	Value of the uncurry functor on an object. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(1st ‘𝐹)𝑌) = ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑌))
Theorem	uncf2 18252	Value of the uncurry functor on a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)))    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑍))    &   ⊢ (𝜑 → 𝑆 ∈ (𝑌𝐽𝑊))    ⇒   ⊢ (𝜑 → (𝑅(⟨𝑋, 𝑌⟩(2nd ‘𝐹)⟨𝑍, 𝑊⟩)𝑆) = ((((𝑋(2nd ‘𝐺)𝑍)‘𝑅)‘𝑊)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑌), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑊)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑍))‘𝑊))((𝑌(2nd ‘((1st ‘𝐺)‘𝑋))𝑊)‘𝑆)))
Theorem	curfuncf 18253	Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)))    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF 𝐹) = 𝐺)
Theorem	uncfcurf 18254	Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    ⇒   ⊢ (𝜑 → (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺) = 𝐹)
Theorem	diagval 18255	Define the diagonal functor, which is the functor 𝐶⟶(𝐷 Func 𝐶) whose object part is 𝑥 ∈ 𝐶 ↦ (𝑦 ∈ 𝐷 ↦ 𝑥). We can define this equationally as the currying of the first projection functor, and by expressing it this way we get a quick proof of functoriality. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝐿 = (⟨𝐶, 𝐷⟩ curryF (𝐶 1stF 𝐷)))
Theorem	diagcl 18256	The diagonal functor is a functor from the base category to the functor category. Another way of saying this is that the constant functor (𝑦 ∈ 𝐷 ↦ 𝑋) is a construction that is natural in 𝑋 (and covariant). (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐶)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐶 Func 𝑄))
Theorem	diag1cl 18257	The constant functor of 𝑋 is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐶))
Theorem	diag11 18258	Value of the constant functor at an object. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝐾)‘𝑌) = 𝑋)
Theorem	diag12 18259	Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑌𝐽𝑍))    ⇒   ⊢ (𝜑 → ((𝑌(2nd ‘𝐾)𝑍)‘𝐹) = ( 1 ‘𝑋))
Theorem	diag2 18260	Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = (𝐵 × {𝐹}))
Theorem	diag2cl 18261	The diagonal functor at a morphism is a natural transformation between constant functors. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 × {𝐹}) ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌)))
Theorem	curf2ndf 18262	As shown in diagval 18255, the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is 𝑥 ∈ 𝐶 ↦ (𝑦 ∈ 𝐷 ↦ 𝑦), which is a constant functor of the identity functor at 𝐷. (Contributed by Mario Carneiro, 15-Jan-2017.)
⊢ 𝑄 = (𝐷 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))
8.4.3  Hom functor
Syntax	chof 18263	Extend class notation with the Hom functor.
class HomF
Syntax	cyon 18264	Extend class notation with the Yoneda embedding.
class Yon
Definition	df-hof 18265*	Define the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat‘𝐶) × 𝐶 to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ HomF = (𝑐 ∈ Cat ↦ ⟨(Homf ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓))))⟩)
Definition	df-yon 18266	Define the Yoneda embedding, which is the currying of the (opposite) Hom functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ Yon = (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐))))
Theorem	hofval 18267*	Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat‘𝐶) × 𝐶 to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017.)
⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → 𝑀 = ⟨(Homf ‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩ · (2nd ‘𝑦))𝑓))))⟩)
Theorem	hof1fval 18268	The object part of the Hom functor is the Homf operation, which is just a functionalized version of Hom. That is, it is a two argument function, which maps 𝑋, 𝑌 to the set of morphisms from 𝑋 to 𝑌. (Contributed by Mario Carneiro, 15-Jan-2017.)
⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → (1st ‘𝑀) = (Homf ‘𝐶))
Theorem	hof1 18269	The object part of the Hom functor maps 𝑋, 𝑌 to the set of morphisms from 𝑋 to 𝑌. (Contributed by Mario Carneiro, 15-Jan-2017.)
⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(1st ‘𝑀)𝑌) = (𝑋𝐻𝑌))
Theorem	hof2fval 18270*	The morphism part of the Hom functor, for morphisms ⟨𝑓, 𝑔⟩:⟨𝑋, 𝑌⟩⟶⟨𝑍, 𝑊⟩ (which since the first argument is contravariant means morphisms 𝑓:𝑍⟶𝑋 and 𝑔:𝑌⟶𝑊), yields a function (a morphism of SetCat) mapping ℎ:𝑋⟶𝑌 to 𝑔 ∘ ℎ ∘ 𝑓:𝑍⟶𝑊. (Contributed by Mario Carneiro, 15-Jan-2017.)
⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩) = (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (𝑌𝐻𝑊) ↦ (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝑔(⟨𝑋, 𝑌⟩ · 𝑊)ℎ)(⟨𝑍, 𝑋⟩ · 𝑊)𝑓))))
Theorem	hof2val 18271*	The morphism part of the Hom functor, for morphisms ⟨𝑓, 𝑔⟩:⟨𝑋, 𝑌⟩⟶⟨𝑍, 𝑊⟩ (which since the first argument is contravariant means morphisms 𝑓:𝑍⟶𝑋 and 𝑔:𝑌⟶𝑊), yields a function (a morphism of SetCat) mapping ℎ:𝑋⟶𝑌 to 𝑔 ∘ ℎ ∘ 𝑓:𝑍⟶𝑊. (Contributed by Mario Carneiro, 15-Jan-2017.)
⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑍𝐻𝑋))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑊))    ⇒   ⊢ (𝜑 → (𝐹(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩)𝐺) = (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝐺(⟨𝑋, 𝑌⟩ · 𝑊)ℎ)(⟨𝑍, 𝑋⟩ · 𝑊)𝐹)))
Theorem	hof2 18272	The morphism part of the Hom functor, for morphisms ⟨𝑓, 𝑔⟩:⟨𝑋, 𝑌⟩⟶⟨𝑍, 𝑊⟩ (which since the first argument is contravariant means morphisms 𝑓:𝑍⟶𝑋 and 𝑔:𝑌⟶𝑊), yields a function (a morphism of SetCat) mapping ℎ:𝑋⟶𝑌 to 𝑔 ∘ ℎ ∘ 𝑓:𝑍⟶𝑊. (Contributed by Mario Carneiro, 15-Jan-2017.)
⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑍𝐻𝑋))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑊))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝐹(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩)𝐺)‘𝐾) = ((𝐺(⟨𝑋, 𝑌⟩ · 𝑊)𝐾)(⟨𝑍, 𝑋⟩ · 𝑊)𝐹))
Theorem	hofcllem 18273	Lemma for hofcl 18274. (Contributed by Mario Carneiro, 15-Jan-2017.)
⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐷 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑊))    &   ⊢ (𝜑 → 𝑃 ∈ (𝑆𝐻𝑍))    &   ⊢ (𝜑 → 𝑄 ∈ (𝑊𝐻𝑇))    ⇒   ⊢ (𝜑 → ((𝐾(⟨𝑆, 𝑍⟩(comp‘𝐶)𝑋)𝑃)(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑆, 𝑇⟩)(𝑄(⟨𝑌, 𝑊⟩(comp‘𝐶)𝑇)𝐿)) = ((𝑃(⟨𝑍, 𝑊⟩(2nd ‘𝑀)⟨𝑆, 𝑇⟩)𝑄)(⟨(𝑋𝐻𝑌), (𝑍𝐻𝑊)⟩(comp‘𝐷)(𝑆𝐻𝑇))(𝐾(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩)𝐿)))
Theorem	hofcl 18274	Closure of the Hom functor. Note that the codomain is the category SetCat‘𝑈 for any universe 𝑈 which contains each Hom-set. This corresponds to the assertion that 𝐶 be locally small (with respect to 𝑈). (Contributed by Mario Carneiro, 15-Jan-2017.)
⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐷 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑀 ∈ ((𝑂 ×c 𝐶) Func 𝐷))
Theorem	oppchofcl 18275	Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑀 = (HomF‘𝑂)    &   ⊢ 𝐷 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑀 ∈ ((𝐶 ×c 𝑂) Func 𝐷))
Theorem	yonval 18276	Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑀 = (HomF‘𝑂)    ⇒   ⊢ (𝜑 → 𝑌 = (⟨𝐶, 𝑂⟩ curryF 𝑀))
Theorem	yoncl 18277	The Yoneda embedding is a functor from the category to the category 𝑄 of presheaves on 𝐶. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
Theorem	yon1cl 18278	The Yoneda embedding at an object of 𝐶 is a presheaf on 𝐶, also known as the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ((1st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆))
Theorem	yon11 18279	Value of the Yoneda embedding at an object. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘((1st ‘𝑌)‘𝑋))‘𝑍) = (𝑍𝐻𝑋))
Theorem	yon12 18280	Value of the Yoneda embedding at a morphism. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑊𝐻𝑍))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑋))    ⇒   ⊢ (𝜑 → (((𝑍(2nd ‘((1st ‘𝑌)‘𝑋))𝑊)‘𝐹)‘𝐺) = (𝐺(⟨𝑊, 𝑍⟩ · 𝑋)𝐹))
Theorem	yon2 18281	Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑍))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑊𝐻𝑋))    ⇒   ⊢ (𝜑 → ((((𝑋(2nd ‘𝑌)𝑍)‘𝐹)‘𝑊)‘𝐺) = (𝐹(⟨𝑊, 𝑋⟩ · 𝑍)𝐺))
Theorem	hofpropd 18282	If two categories have the same set of objects, morphisms, and compositions, then they have the same Hom functor. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → (HomF‘𝐶) = (HomF‘𝐷))
Theorem	yonpropd 18283	If two categories have the same set of objects, morphisms, and compositions, then they have the same Yoneda functor. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → (Yon‘𝐶) = (Yon‘𝐷))
Theorem	oppcyon 18284	Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑌 = (Yon‘𝑂)    &   ⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑌 = (⟨𝑂, 𝐶⟩ curryF 𝑀))
Theorem	oyoncl 18285	The opposite Yoneda embedding is a functor from oppCat‘𝐶 to the functor category 𝐶 → SetCat. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑌 = (Yon‘𝑂)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ 𝑄 = (𝐶 FuncCat 𝑆)    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝑂 Func 𝑄))
Theorem	oyon1cl 18286	The opposite Yoneda embedding at an object of 𝐶 is a functor from 𝐶 to Set, also known as the covariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑌 = (Yon‘𝑂)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝑌)‘𝑋) ∈ (𝐶 Func 𝑆))
Theorem	yonedalem1 18287	Lemma for yoneda 18298. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
Theorem	yonedalem21 18288	Lemma for yoneda 18298. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹(1st ‘𝑍)𝑋) = (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
Theorem	yonedalem3a 18289*	Lemma for yoneda 18298. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    ⇒   ⊢ (𝜑 → ((𝐹𝑀𝑋) = (𝑎 ∈ (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) ∧ (𝐹𝑀𝑋):(𝐹(1st ‘𝑍)𝑋)⟶(𝐹(1st ‘𝐸)𝑋)))
Theorem	yonedalem4a 18290*	Lemma for yoneda 18298. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))    &   ⊢ (𝜑 → 𝐴 ∈ ((1st ‘𝐹)‘𝑋))    ⇒   ⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑦)‘𝑔)‘𝐴))))
Theorem	yonedalem4b 18291*	Lemma for yoneda 18298. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))    &   ⊢ (𝜑 → 𝐴 ∈ ((1st ‘𝐹)‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑃(Hom ‘𝐶)𝑋))    ⇒   ⊢ (𝜑 → ((((𝐹𝑁𝑋)‘𝐴)‘𝑃)‘𝐺) = (((𝑋(2nd ‘𝐹)𝑃)‘𝐺)‘𝐴))
Theorem	yonedalem4c 18292*	Lemma for yoneda 18298. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))    &   ⊢ (𝜑 → 𝐴 ∈ ((1st ‘𝐹)‘𝑋))    ⇒   ⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) ∈ (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
Theorem	yonedalem22 18293	Lemma for yoneda 18298. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))    ⇒   ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2nd ‘𝑌)𝑋)‘𝐾)(⟨((1st ‘𝑌)‘𝑋), 𝐹⟩(2nd ‘𝐻)⟨((1st ‘𝑌)‘𝑃), 𝐺⟩)𝐴))
Theorem	yonedalem3b 18294*	Lemma for yoneda 18298. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    ⇒   ⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1st ‘𝑍)𝑋), (𝐺(1st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1st ‘𝑍)𝑋), (𝐹(1st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1st ‘𝐸)𝑃))(𝐹𝑀𝑋)))
Theorem	yonedalem3 18295*	Lemma for yoneda 18298. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    ⇒   ⊢ (𝜑 → 𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸))
Theorem	yonedainv 18296*	The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    &   ⊢ 𝐼 = (Inv‘𝑅)    &   ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))    ⇒   ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁)
Theorem	yonffthlem 18297*	Lemma for yonffth 18299. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    &   ⊢ 𝐼 = (Inv‘𝑅)    &   ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))    ⇒   ⊢ (𝜑 → 𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))
Theorem	yoneda 18298*	The Yoneda Lemma. There is a natural isomorphism between the functors 𝑍 and 𝐸, where 𝑍(𝐹, 𝑋) is the natural transformations from Yon(𝑋) = Hom ( − , 𝑋) to 𝐹, and 𝐸(𝐹, 𝑋) = 𝐹(𝑋) is the evaluation functor. Here we need two universes to state the claim: the smaller universe 𝑈 is used for forming the functor category 𝑄 = 𝐶 op → SetCat(𝑈), which itself does not (necessarily) live in 𝑈 but instead is an element of the larger universe 𝑉. (If 𝑈 is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set 𝑈 = 𝑉 in this case.) (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    &   ⊢ 𝐼 = (Iso‘𝑅)    ⇒   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐼𝐸))
Theorem	yonffth 18299	The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category 𝐶 as a full subcategory of the category 𝑄 of presheaves on 𝐶. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))
Theorem	yoniso 18300*	If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from 𝐶 into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐷 = (CatCat‘𝑉)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐼 = (Iso‘𝐷)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐸 = (𝑄 ↾s ran (1st ‘𝑌))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝐹‘(𝑥(Hom ‘𝐶)𝑦)) = 𝑦)    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝐶𝐼𝐸))