P. 184 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18301-18400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	funcestrcsetclem8 18301*	Lemma 8 for funcestrcsetc 18303. (Contributed by AV, 15-Feb-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝐸)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌)))
Theorem	funcestrcsetclem9 18302*	Lemma 9 for funcestrcsetc 18303. (Contributed by AV, 23-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝐻 ∈ (𝑋(Hom ‘𝐸)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝐸)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(⟨𝑋, 𝑌⟩(comp‘𝐸)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)))
Theorem	funcestrcsetc 18303*	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 18304*	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 18305*	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 18306*	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 18307	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 18308*	Lemma 1 for funcsetcestrc 18318. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) = {⟨(Base‘ndx), 𝑋⟩})
Theorem	funcsetcestrclem2 18309*	Lemma 2 for funcsetcestrc 18318. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) ∈ 𝑈)
Theorem	funcsetcestrclem3 18310*	Lemma 3 for funcsetcestrc 18318. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐶⟶𝐵)
Theorem	embedsetcestrclem 18311*	Lemma for embedsetcestrc 18321. (Contributed by AV, 31-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐶–1-1→𝐵)
Theorem	funcsetcestrclem4 18312*	Lemma 4 for funcsetcestrc 18318. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 Fn (𝐶 × 𝐶))
Theorem	funcsetcestrclem5 18313*	Lemma 5 for funcsetcestrc 18318. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌) = ( I ↾ (𝑌 ↑m 𝑋)))
Theorem	funcsetcestrclem6 18314*	Lemma 6 for funcsetcestrc 18318. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝐻 ∈ (𝑌 ↑m 𝑋)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻)
Theorem	funcsetcestrclem7 18315*	Lemma 7 for funcsetcestrc 18318. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑋𝐺𝑋)‘((Id‘𝑆)‘𝑋)) = ((Id‘𝐸)‘(𝐹‘𝑋)))
Theorem	funcsetcestrclem8 18316*	Lemma 8 for funcsetcestrc 18318. (Contributed by AV, 28-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑆)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝐸)(𝐹‘𝑌)))
Theorem	funcsetcestrclem9 18317*	Lemma 9 for funcsetcestrc 18318. (Contributed by AV, 28-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(⟨𝑋, 𝑌⟩(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)))
Theorem	funcsetcestrc 18318*	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 18319*	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 18320*	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 18321*	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 18322	Extend class notation with the product of two categories.
class ×c
Syntax	c1stf 18323	Extend class notation with the first projection functor.
class 1stF
Syntax	c2ndf 18324	Extend class notation with the second projection functor.
class 2ndF
Syntax	cprf 18325	Extend class notation with the functor pairing operation.
class ⟨,⟩F
Definition	df-xpc 18326*	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 18327*	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 18328*	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 18329*	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 18330	The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ ×c Fn (V × V)
Theorem	xpcval 18331*	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 18332	Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝑌 = (Base‘𝐷)    ⇒   ⊢ (𝑋 × 𝑌) = (Base‘𝑇)
Theorem	xpchomfval 18333*	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 18334	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 18335	A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐾 = (Hom ‘𝑇)    ⇒   ⊢ Rel (𝑋𝐾𝑌)
Theorem	xpccofval 18336*	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 18337	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 18338	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 18339	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 18340	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 18341	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 18342*	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 18343	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 18344	The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑇 ∈ Cat)
Theorem	1stfval 18345*	Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑃 = (𝐶 1stF 𝐷)    ⇒   ⊢ (𝜑 → 𝑃 = ⟨(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))⟩)
Theorem	1stf1 18346	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 18347	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 18348*	Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 2ndF 𝐷)    ⇒   ⊢ (𝜑 → 𝑄 = ⟨(2nd ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (2nd ↾ (𝑥𝐻𝑦)))⟩)
Theorem	2ndf1 18349	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 18350	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 18351	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 18352	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 18353*	Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → 𝑃 = ⟨(𝑥 ∈ 𝐵 ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (ℎ ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))⟩)
Theorem	prf1 18354	Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝑃)‘𝑋) = ⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)⟩)
Theorem	prf2fval 18355*	Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝑃)𝑌) = (ℎ ∈ (𝑋𝐻𝑌) ↦ ⟨((𝑋(2nd ‘𝐹)𝑌)‘ℎ), ((𝑋(2nd ‘𝐺)𝑌)‘ℎ)⟩))
Theorem	prf2 18356	Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘𝑃)𝑌)‘𝐾) = ⟨((𝑋(2nd ‘𝐹)𝑌)‘𝐾), ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)⟩)
Theorem	prfcl 18357	The pairing of functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐷 is a functor ⟨𝐹, 𝐺⟩:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝑇 = (𝐷 ×c 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇))
Theorem	prf1st 18358	Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → ((𝐷 1stF 𝐸) ∘func 𝑃) = 𝐹)
Theorem	prf2nd 18359	Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺)
Theorem	1st2ndprf 18360	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 18361	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 18362	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 18363	Extend class notation with the evaluation functor.
class evalF
Syntax	ccurf 18364	Extend class notation with the currying of a functor.
class curryF
Syntax	cuncf 18365	Extend class notation with the uncurrying of a functor.
class uncurryF
Syntax	cdiag 18366	Extend class notation to include the diagonal functor.
class Δfunc
Definition	df-evlf 18367*	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 18368*	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 18369*	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 18370*	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 18371*	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 18372*	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 18373	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 18374	Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = (𝐶 evalF 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹(1st ‘𝐸)𝑋) = ((1st ‘𝐹)‘𝑋))
Theorem	evlfcllem 18375	Lemma for evlfcl 18376. (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 18376	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 18377*	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 18378*	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 18379*	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 18380	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 18381	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 18382	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 18383*	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 18384	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 18385	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 18386	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 18387	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 18388	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 18389	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 18390	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 18391	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 18392	Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐸 ∈ Cat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)))    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF 𝐹) = 𝐺)
Theorem	uncfcurf 18393	Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))    ⇒   ⊢ (𝜑 → (⟨“𝐶𝐷𝐸”⟩ uncurryF 𝐺) = 𝐹)
Theorem	diagval 18394	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 18395	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 18396	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 18397	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 18398	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 18399	Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = (𝐵 × {𝐹}))
Theorem	diag2cl 18400	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 ‘𝐿)‘𝑌)))