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	funcestrcsetclem7 18201*	Lemma 7 for funcestrcsetc 18204. (Contributed by AV, 23-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → ((𝑋𝐺𝑋)‘((Id‘𝐸)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋)))
Theorem	funcestrcsetclem8 18202*	Lemma 8 for funcestrcsetc 18204. (Contributed by AV, 15-Feb-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝐸)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌)))
Theorem	funcestrcsetclem9 18203*	Lemma 9 for funcestrcsetc 18204. (Contributed by AV, 23-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝐻 ∈ (𝑋(Hom ‘𝐸)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝐸)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(⟨𝑋, 𝑌⟩(comp‘𝐸)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)))
Theorem	funcestrcsetc 18204*	The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 23-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))    ⇒   ⊢ (𝜑 → 𝐹(𝐸 Func 𝑆)𝐺)
Theorem	fthestrcsetc 18205*	The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is faithful. (Contributed by AV, 2-Apr-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))    ⇒   ⊢ (𝜑 → 𝐹(𝐸 Faith 𝑆)𝐺)
Theorem	fullestrcsetc 18206*	The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is full. (Contributed by AV, 2-Apr-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))    ⇒   ⊢ (𝜑 → 𝐹(𝐸 Full 𝑆)𝐺)
Theorem	equivestrcsetc 18207*	The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is an equivalence. According to definition 3.33 (1) of [Adamek] p. 36, "A functor F : A -> B is called an equivalence provided that it is full, faithful, and isomorphism-dense in the sense that for any B-object B' there exists some A-object A' such that F(A') is isomorphic to B'.". Therefore, the category of sets and the category of extensible structures are equivalent, according to definition 3.33 (2) of [Adamek] p. 36, "Categories A and B are called equivalent provided that there is an equivalence from A to B.". (Contributed by AV, 2-Apr-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))    &   ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐹(𝐸 Faith 𝑆)𝐺 ∧ 𝐹(𝐸 Full 𝑆)𝐺 ∧ ∀𝑏 ∈ 𝐶 ∃𝑎 ∈ 𝐵 ∃𝑖 𝑖:𝑏–1-1-onto→(𝐹‘𝑎)))
Theorem	setc1strwun 18208	A constructed one-slot structure with the objects of the category of sets as base set in a weak universe. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → {⟨(Base‘ndx), 𝑋⟩} ∈ 𝑈)
Theorem	funcsetcestrclem1 18209*	Lemma 1 for funcsetcestrc 18219. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) = {⟨(Base‘ndx), 𝑋⟩})
Theorem	funcsetcestrclem2 18210*	Lemma 2 for funcsetcestrc 18219. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) ∈ 𝑈)
Theorem	funcsetcestrclem3 18211*	Lemma 3 for funcsetcestrc 18219. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐶⟶𝐵)
Theorem	embedsetcestrclem 18212*	Lemma for embedsetcestrc 18222. (Contributed by AV, 31-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐶–1-1→𝐵)
Theorem	funcsetcestrclem4 18213*	Lemma 4 for funcsetcestrc 18219. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 Fn (𝐶 × 𝐶))
Theorem	funcsetcestrclem5 18214*	Lemma 5 for funcsetcestrc 18219. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌) = ( I ↾ (𝑌 ↑m 𝑋)))
Theorem	funcsetcestrclem6 18215*	Lemma 6 for funcsetcestrc 18219. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝐻 ∈ (𝑌 ↑m 𝑋)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻)
Theorem	funcsetcestrclem7 18216*	Lemma 7 for funcsetcestrc 18219. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑋𝐺𝑋)‘((Id‘𝑆)‘𝑋)) = ((Id‘𝐸)‘(𝐹‘𝑋)))
Theorem	funcsetcestrclem8 18217*	Lemma 8 for funcsetcestrc 18219. (Contributed by AV, 28-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑆)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝐸)(𝐹‘𝑌)))
Theorem	funcsetcestrclem9 18218*	Lemma 9 for funcsetcestrc 18219. (Contributed by AV, 28-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(⟨𝑋, 𝑌⟩(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)))
Theorem	funcsetcestrc 18219*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 28-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ (𝜑 → 𝐹(𝑆 Func 𝐸)𝐺)
Theorem	fthsetcestrc 18220*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is faithful. (Contributed by AV, 31-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ (𝜑 → 𝐹(𝑆 Faith 𝐸)𝐺)
Theorem	fullsetcestrc 18221*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is full. (Contributed by AV, 1-Apr-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ (𝜑 → 𝐹(𝑆 Full 𝐸)𝐺)
Theorem	embedsetcestrc 18222*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is an embedding. According to definition 3.27 (1) of [Adamek] p. 34, a functor "F is called an embedding provided that F is injective on morphisms", or according to remark 3.28 (1) in [Adamek] p. 34, "a functor is an embedding if and only if it is faithful and injective on objects". (Contributed by AV, 31-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → (𝐹(𝑆 Faith 𝐸)𝐺 ∧ 𝐹:𝐶–1-1→𝐵))
8.4  Categorical constructions
8.4.1  Product of categories
Syntax	cxpc 18223	Extend class notation with the product of two categories.
class ×c
Syntax	c1stf 18224	Extend class notation with the first projection functor.
class 1stF
Syntax	c2ndf 18225	Extend class notation with the second projection functor.
class 2ndF
Syntax	cprf 18226	Extend class notation with the functor pairing operation.
class ⟨,⟩F
Definition	df-xpc 18227*	Define the binary product of categories, which has objects for each pair of objects of the factors, and morphisms for each pair of morphisms of the factors. Composition is componentwise. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ ×c = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))⟩))⟩})
Definition	df-1stf 18228*	Define the first projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 1stF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)
Definition	df-2ndf 18229*	Define the second projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 2ndF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(2nd ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)
Definition	df-prf 18230*	Define the pairing operation for functors (which takes two functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐸 and produces (𝐹 ⟨,⟩F 𝐺):𝐶⟶(𝐷 ×c 𝐸)). (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ ⟨,⟩F = (𝑓 ∈ V, 𝑔 ∈ V ↦ ⦋dom (1st ‘𝑓) / 𝑏⦌⟨(𝑥 ∈ 𝑏 ↦ ⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (ℎ ∈ dom (𝑥(2nd ‘𝑓)𝑦) ↦ ⟨((𝑥(2nd ‘𝑓)𝑦)‘ℎ), ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)⟩))⟩)
Theorem	fnxpc 18231	The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ ×c Fn (V × V)
Theorem	xpcval 18232*	Value of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝑌 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐶)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 = (𝑋 × 𝑌))    &   ⊢ (𝜑 → 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))))    &   ⊢ (𝜑 → 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩ · (1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩ ∙ (2nd ‘𝑦))(2nd ‘𝑓))⟩)))    ⇒   ⊢ (𝜑 → 𝑇 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐾⟩, ⟨(comp‘ndx), 𝑂⟩})
Theorem	xpcbas 18233	Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝑌 = (Base‘𝐷)    ⇒   ⊢ (𝑋 × 𝑌) = (Base‘𝑇)
Theorem	xpchomfval 18234*	Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (Hom ‘𝑇)    ⇒   ⊢ 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))
Theorem	xpchom 18235	Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 𝐾 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐾𝑌) = (((1st ‘𝑋)𝐻(1st ‘𝑌)) × ((2nd ‘𝑋)𝐽(2nd ‘𝑌))))
Theorem	relxpchom 18236	A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐾 = (Hom ‘𝑇)    ⇒   ⊢ Rel (𝑋𝐾𝑌)
Theorem	xpccofval 18237*	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) (Proof shortened by AV, 2-Mar-2024.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐾 = (Hom ‘𝑇)    &   ⊢ · = (comp‘𝐶)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ 𝑂 = (comp‘𝑇)    ⇒   ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩ · (1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩ ∙ (2nd ‘𝑦))(2nd ‘𝑓))⟩))
Theorem	xpcco 18238	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐾 = (Hom ‘𝑇)    &   ⊢ · = (comp‘𝐶)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ 𝑂 = (comp‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐾𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐾𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = ⟨((1st ‘𝐺)(⟨(1st ‘𝑋), (1st ‘𝑌)⟩ · (1st ‘𝑍))(1st ‘𝐹)), ((2nd ‘𝐺)(⟨(2nd ‘𝑋), (2nd ‘𝑌)⟩ ∙ (2nd ‘𝑍))(2nd ‘𝐹))⟩)
Theorem	xpcco1st 18239	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐾 = (Hom ‘𝑇)    &   ⊢ 𝑂 = (comp‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐾𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐾𝑍))    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → (1st ‘(𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹)) = ((1st ‘𝐺)(⟨(1st ‘𝑋), (1st ‘𝑌)⟩ · (1st ‘𝑍))(1st ‘𝐹)))
Theorem	xpcco2nd 18240	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐾 = (Hom ‘𝑇)    &   ⊢ 𝑂 = (comp‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐾𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐾𝑍))    &   ⊢ · = (comp‘𝐷)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹)) = ((2nd ‘𝐺)(⟨(2nd ‘𝑋), (2nd ‘𝑌)⟩ · (2nd ‘𝑍))(2nd ‘𝐹)))
Theorem	xpchom2 18241	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 18242	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 18243*	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 18244	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 18245	The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑇 ∈ Cat)
Theorem	1stfval 18246*	Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑃 = (𝐶 1stF 𝐷)    ⇒   ⊢ (𝜑 → 𝑃 = ⟨(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))⟩)
Theorem	1stf1 18247	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 18248	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 18249*	Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 2ndF 𝐷)    ⇒   ⊢ (𝜑 → 𝑄 = ⟨(2nd ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (2nd ↾ (𝑥𝐻𝑦)))⟩)
Theorem	2ndf1 18250	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 18251	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 18252	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 18253	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 18254*	Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → 𝑃 = ⟨(𝑥 ∈ 𝐵 ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (ℎ ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))⟩)
Theorem	prf1 18255	Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝑃)‘𝑋) = ⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)⟩)
Theorem	prf2fval 18256*	Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝑃)𝑌) = (ℎ ∈ (𝑋𝐻𝑌) ↦ ⟨((𝑋(2nd ‘𝐹)𝑌)‘ℎ), ((𝑋(2nd ‘𝐺)𝑌)‘ℎ)⟩))
Theorem	prf2 18257	Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘𝑃)𝑌)‘𝐾) = ⟨((𝑋(2nd ‘𝐹)𝑌)‘𝐾), ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)⟩)
Theorem	prfcl 18258	The pairing of functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐷 is a functor ⟨𝐹, 𝐺⟩:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝑇 = (𝐷 ×c 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇))
Theorem	prf1st 18259	Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → ((𝐷 1stF 𝐸) ∘func 𝑃) = 𝐹)
Theorem	prf2nd 18260	Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺)
Theorem	1st2ndprf 18261	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 18262	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	catcxpcclOLD 18263	Obsolete version of catcxpccl 18262 as of 14-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑇 = (𝑋 ×c 𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑇 ∈ 𝐵)
Theorem	xpcpropd 18264	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 18265	Extend class notation with the evaluation functor.
class evalF
Syntax	ccurf 18266	Extend class notation with the currying of a functor.
class curryF
Syntax	cuncf 18267	Extend class notation with the uncurrying of a functor.
class uncurryF
Syntax	cdiag 18268	Extend class notation to include the diagonal functor.
class Δfunc
Definition	df-evlf 18269*	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 18270*	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 18271*	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 18272*	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 18273*	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 18274*	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 18275	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 18276	Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = (𝐶 evalF 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹(1st ‘𝐸)𝑋) = ((1st ‘𝐹)‘𝑋))
Theorem	evlfcllem 18277	Lemma for evlfcl 18278. (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 18278	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 18279*	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 18280*	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 18281*	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 18282	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 18283	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 18284	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 18285*	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 18286	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 18287	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 18288	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 18289	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 18290	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 18291	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 18292	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 18293	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 18294	Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)))    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF 𝐹) = 𝐺)
Theorem	uncfcurf 18295	Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    ⇒   ⊢ (𝜑 → (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺) = 𝐹)
Theorem	diagval 18296	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 18297	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 18298	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 18299	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 18300	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 ‘𝑋))