P. 177 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17601-17700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	idfu2nd 17601	Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝐼)𝑌) = ( I ↾ (𝑋𝐻𝑌)))
Theorem	idfu2 17602	Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘𝐼)𝑌)‘𝐹) = 𝐹)
Theorem	idfu1st 17603	Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → (1st ‘𝐼) = ( I ↾ 𝐵))
Theorem	idfu1 17604	Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐼 = (idfunc‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝐼)‘𝑋) = 𝑋)
Theorem	idfucl 17605	The identity functor is a functor. Example 3.20(1) of [Adamek] p. 30. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐼 = (idfunc‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → 𝐼 ∈ (𝐶 Func 𝐶))
Theorem	cofuval 17606*	Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) = ⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩)
Theorem	cofu1st 17607	Value of the object part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹)) = ((1st ‘𝐺) ∘ (1st ‘𝐹)))
Theorem	cofu1 17608	Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘(𝐺 ∘func 𝐹))‘𝑋) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑋)))
Theorem	cofu2nd 17609	Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘(𝐺 ∘func 𝐹))𝑌) = ((((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌)) ∘ (𝑋(2nd ‘𝐹)𝑌)))
Theorem	cofu2 17610	Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘(𝐺 ∘func 𝐹))𝑌)‘𝑅) = ((((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌))‘((𝑋(2nd ‘𝐹)𝑌)‘𝑅)))
Theorem	cofuval2 17611*	Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐻(𝐷 Func 𝐸)𝐾)    ⇒   ⊢ (𝜑 → (⟨𝐻, 𝐾⟩ ∘func ⟨𝐹, 𝐺⟩) = ⟨(𝐻 ∘ 𝐹), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐾(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))⟩)
Theorem	cofucl 17612	The composition of two functors is a functor. Proposition 3.23 of [Adamek] p. 33. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸))
Theorem	cofuass 17613	Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐾 ∈ (𝐸 Func 𝐹))    ⇒   ⊢ (𝜑 → ((𝐾 ∘func 𝐻) ∘func 𝐺) = (𝐾 ∘func (𝐻 ∘func 𝐺)))
Theorem	cofulid 17614	The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ 𝐼 = (idfunc‘𝐷)    ⇒   ⊢ (𝜑 → (𝐼 ∘func 𝐹) = 𝐹)
Theorem	cofurid 17615	The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ 𝐼 = (idfunc‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘func 𝐼) = 𝐹)
Theorem	resfval 17616*	Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 ↾f 𝐻) = ⟨((1st ‘𝐹) ↾ dom dom 𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))⟩)
Theorem	resfval2 17617*	Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    ⇒   ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ↾f 𝐻) = ⟨(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))⟩)
Theorem	resf1st 17618	Value of the functor restriction operator on objects. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    ⇒   ⊢ (𝜑 → (1st ‘(𝐹 ↾f 𝐻)) = ((1st ‘𝐹) ↾ 𝑆))
Theorem	resf2nd 17619	Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘(𝐹 ↾f 𝐻))𝑌) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌)))
Theorem	funcres 17620	A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶))    ⇒   ⊢ (𝜑 → (𝐹 ↾f 𝐻) ∈ ((𝐶 ↾cat 𝐻) Func 𝐷))
Theorem	funcres2b 17621*	Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (Subcat‘𝐷))    &   ⊢ (𝜑 → 𝑅 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺))
Theorem	funcres2 17622	A functor into a restricted category is also a functor into the whole category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝑅 ∈ (Subcat‘𝐷) → (𝐶 Func (𝐷 ↾cat 𝑅)) ⊆ (𝐶 Func 𝐷))
Theorem	wunfunc 17623	A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈)
Theorem	wunfuncOLD 17624	Obsolete proof of wunfunc 17623 as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈)
Theorem	funcpropd 17625	If two categories have the same set of objects, morphisms, and compositions, then they have the same functors. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷))
Theorem	funcres2c 17626	Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐸 = (𝐷 ↾s 𝑆)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func 𝐸)𝐺))
8.1.8  Full & faithful functors
Syntax	cful 17627	Extend class notation with the class of all full functors.
class Full
Syntax	cfth 17628	Extend class notation with the class of all faithful functors.
class Faith
Definition	df-full 17629*	Function returning all the full functors from a category 𝐶 to a category 𝐷. A full functor is a functor in which all the morphism maps 𝐺(𝑋, 𝑌) between objects 𝑋, 𝑌 ∈ 𝐶 are surjections. Definition 3.27(3) in [Adamek] p. 34. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ Full = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})
Definition	df-fth 17630*	Function returning all the faithful functors from a category 𝐶 to a category 𝐷. A faithful functor is a functor in which all the morphism maps 𝐺(𝑋, 𝑌) between objects 𝑋, 𝑌 ∈ 𝐶 are injections. Definition 3.27(2) in [Adamek] p. 34. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ Faith = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦))})
Theorem	fullfunc 17631	A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷)
Theorem	fthfunc 17632	A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷)
Theorem	relfull 17633	The set of full functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ Rel (𝐶 Full 𝐷)
Theorem	relfth 17634	The set of faithful functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ Rel (𝐶 Faith 𝐷)
Theorem	isfull 17635*	Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    ⇒   ⊢ (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ran (𝑥𝐺𝑦) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
Theorem	isfull2 17636*	Equivalent condition for a full functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–onto→((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
Theorem	fullfo 17637	The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–onto→((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	fulli 17638*	The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ (𝑋𝐻𝑌)𝑅 = ((𝑋𝐺𝑌)‘𝑓))
Theorem	isfth 17639*	Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦)))
Theorem	isfth2 17640*	Equivalent condition for a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    ⇒   ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–1-1→((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
Theorem	isffth2 17641*	A fully faithful functor is a functor which is bijective on hom-sets. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    ⇒   ⊢ (𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)–1-1-onto→((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
Theorem	fthf1 17642	The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–1-1→((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	fthi 17643	The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (((𝑋𝐺𝑌)‘𝑅) = ((𝑋𝐺𝑌)‘𝑆) ↔ 𝑅 = 𝑆))
Theorem	ffthf1o 17644	The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–1-1-onto→((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
Theorem	fullpropd 17645	If two categories have the same set of objects, morphisms, and compositions, then they have the same full functors. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 Full 𝐶) = (𝐵 Full 𝐷))
Theorem	fthpropd 17646	If two categories have the same set of objects, morphisms, and compositions, then they have the same faithful functors. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 Faith 𝐶) = (𝐵 Faith 𝐷))
Theorem	fulloppc 17647	The opposite functor of a full functor is also full. Proposition 3.43(d) in [Adamek] p. 39. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝑂 Full 𝑃)tpos 𝐺)
Theorem	fthoppc 17648	The opposite functor of a faithful functor is also faithful. Proposition 3.43(c) in [Adamek] p. 39. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝑂 Faith 𝑃)tpos 𝐺)
Theorem	ffthoppc 17649	The opposite functor of a fully faithful functor is also full and faithful. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ (𝜑 → 𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺)    ⇒   ⊢ (𝜑 → 𝐹((𝑂 Full 𝑃) ∩ (𝑂 Faith 𝑃))tpos 𝐺)
Theorem	fthsect 17650	A faithful functor reflects sections. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑋))    &   ⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ 𝑇 = (Sect‘𝐷)    ⇒   ⊢ (𝜑 → (𝑀(𝑋𝑆𝑌)𝑁 ↔ ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝑇(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁)))
Theorem	fthinv 17651	A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑋))    &   ⊢ 𝐼 = (Inv‘𝐶)    &   ⊢ 𝐽 = (Inv‘𝐷)    ⇒   ⊢ (𝜑 → (𝑀(𝑋𝐼𝑌)𝑁 ↔ ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝐽(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁)))
Theorem	fthmon 17652	A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ 𝑁 = (Mono‘𝐷)    &   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑁(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝑀𝑌))
Theorem	fthepi 17653	A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐸 = (Epi‘𝐶)    &   ⊢ 𝑃 = (Epi‘𝐷)    &   ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑃(𝐹‘𝑌)))    ⇒   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐸𝑌))
Theorem	ffthiso 17654	A fully faithful functor reflects isomorphisms. Corollary 3.32 of [Adamek] p. 35. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺)    &   ⊢ 𝐼 = (Iso‘𝐶)    &   ⊢ 𝐽 = (Iso‘𝐷)    ⇒   ⊢ (𝜑 → (𝑅 ∈ (𝑋𝐼𝑌) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))))
Theorem	fthres2b 17655*	Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (Subcat‘𝐷))    &   ⊢ (𝜑 → 𝑅 Fn (𝑆 × 𝑆))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ 𝐹(𝐶 Faith (𝐷 ↾cat 𝑅))𝐺))
Theorem	fthres2c 17656	Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐸 = (𝐷 ↾s 𝑆)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ 𝐹(𝐶 Faith 𝐸)𝐺))
Theorem	fthres2 17657	A faithful functor into a restricted category is also a faithful functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝑅 ∈ (Subcat‘𝐷) → (𝐶 Faith (𝐷 ↾cat 𝑅)) ⊆ (𝐶 Faith 𝐷))
Theorem	idffth 17658	The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐼 = (idfunc‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → 𝐼 ∈ ((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶)))
Theorem	cofull 17659	The composition of two full functors is full. Proposition 3.30(d) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Full 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Full 𝐸))    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Full 𝐸))
Theorem	cofth 17660	The composition of two faithful functors is faithful. Proposition 3.30(c) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ (𝐶 Faith 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Faith 𝐸))    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Faith 𝐸))
Theorem	coffth 17661	The composition of two fully faithful functors is fully faithful. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ ((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷)))    &   ⊢ (𝜑 → 𝐺 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸)))    ⇒   ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ ((𝐶 Full 𝐸) ∩ (𝐶 Faith 𝐸)))
Theorem	rescfth 17662	The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾cat 𝐽)    &   ⊢ 𝐼 = (idfunc‘𝐷)    ⇒   ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 ∈ (𝐷 Faith 𝐶))
Theorem	ressffth 17663	The inclusion functor from a full subcategory is a full and faithful functor, see also remark 4.4(2) in [Adamek] p. 49. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾s 𝑆)    &   ⊢ 𝐼 = (idfunc‘𝐷)    ⇒   ⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶)))
Theorem	fullres2c 17664	Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐸 = (𝐷 ↾s 𝑆)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    ⇒   ⊢ (𝜑 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ 𝐹(𝐶 Full 𝐸)𝐺))
Theorem	ffthres2c 17665	Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐸 = (𝐷 ↾s 𝑆)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    ⇒   ⊢ (𝜑 → (𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺 ↔ 𝐹((𝐶 Full 𝐸) ∩ (𝐶 Faith 𝐸))𝐺))
8.1.9  Natural transformations and the functor category
Syntax	cnat 17666	Extend class notation to include the collection of natural transformations.
class Nat
Syntax	cfuc 17667	Extend class notation to include the functor category.
class FuncCat
Definition	df-nat 17668*	Definition of a natural transformation between two functors. A natural transformation 𝐴:𝐹⟶𝐺 is a collection of arrows 𝐴(𝑥):𝐹(𝑥)⟶𝐺(𝑥), such that 𝐴(𝑦) ∘ 𝐹(ℎ) = 𝐺(ℎ) ∘ 𝐴(𝑥) for each morphism ℎ:𝑥⟶𝑦. Definition 6.1 in [Adamek] p. 83, and definition in [Lang] p. 65. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ Nat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))}))
Definition	df-fuc 17669*	Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ FuncCat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩})
Theorem	fnfuc 17670	The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ FuncCat Fn (Cat × Cat)
Theorem	natfval 17671*	Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐷)    ⇒   ⊢ 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩ · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩ · (𝑠‘𝑦))(𝑎‘𝑥))})
Theorem	isnat 17672*	Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)    &   ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿)    ⇒   ⊢ (𝜑 → (𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(⟨(𝐹‘𝑥), (𝐾‘𝑥)⟩ · (𝐾‘𝑦))(𝐴‘𝑥)))))
Theorem	isnat2 17673*	Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐹𝑁𝐺) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩ · ((1st ‘𝐺)‘𝑦))((𝑥(2nd ‘𝐹)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝐺)𝑦)‘ℎ)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ · ((1st ‘𝐺)‘𝑦))(𝐴‘𝑥)))))
Theorem	natffn 17674	The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    ⇒   ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷))
Theorem	natrcl 17675	Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    ⇒   ⊢ (𝐴 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)))
Theorem	nat1st2nd 17676	Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (⟨(1st ‘𝐹), (2nd ‘𝐹)⟩𝑁⟨(1st ‘𝐺), (2nd ‘𝐺)⟩))
Theorem	natixp 17677*	A natural transformation is a function from the objects of 𝐶 to homomorphisms from 𝐹(𝑥) to 𝐺(𝑥). (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    ⇒   ⊢ (𝜑 → 𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)))
Theorem	natcl 17678	A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴‘𝑋) ∈ ((𝐹‘𝑋)𝐽(𝐾‘𝑋)))
Theorem	natfn 17679	A natural transformation is a function on the objects of 𝐶. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → 𝐴 Fn 𝐵)
Theorem	nati 17680	Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝐴‘𝑌)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩ · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹‘𝑋), (𝐾‘𝑋)⟩ · (𝐾‘𝑌))(𝐴‘𝑋)))
Theorem	wunnat 17681	A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈)
Theorem	wunnatOLD 17682	Obsolete proof of wunnat 17681 as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈)
Theorem	catstr 17683	A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ {⟨(Base‘ndx), 𝑈⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} Struct ⟨1, ;15⟩
Theorem	fucval 17684*	Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐵 = (𝐶 Func 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩ · ((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))))    ⇒   ⊢ (𝜑 → 𝑄 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), ∙ ⟩})
Theorem	fuccofval 17685*	Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐵 = (𝐶 Func 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ ∙ = (comp‘𝑄)    ⇒   ⊢ (𝜑 → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩ · ((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))))
Theorem	fucbas 17686	The objects of the functor category are functors from 𝐶 to 𝐷. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    ⇒   ⊢ (𝐶 Func 𝐷) = (Base‘𝑄)
Theorem	fuchom 17687	The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    ⇒   ⊢ 𝑁 = (Hom ‘𝑄)
Theorem	fuchomOLD 17688	Obsolete proof of fuchom 17687 as of 14-Oct-2024. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    ⇒   ⊢ 𝑁 = (Hom ‘𝑄)
Theorem	fucco 17689*	Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻))    ⇒   ⊢ (𝜑 → (𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅) = (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ · ((1st ‘𝐻)‘𝑥))(𝑅‘𝑥))))
Theorem	fuccoval 17690	Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅)‘𝑋) = ((𝑆‘𝑋)(⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)⟩ · ((1st ‘𝐻)‘𝑋))(𝑅‘𝑋)))
Theorem	fuccocl 17691	The composition of two natural transformations is a natural transformation. Remark 6.14(a) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻))    ⇒   ⊢ (𝜑 → (𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅) ∈ (𝐹𝑁𝐻))
Theorem	fucidcl 17692	The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → ( 1 ∘ (1st ‘𝐹)) ∈ (𝐹𝑁𝐹))
Theorem	fuclid 17693	Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    ⇒   ⊢ (𝜑 → (( 1 ∘ (1st ‘𝐺))(⟨𝐹, 𝐺⟩ ∙ 𝐺)𝑅) = 𝑅)
Theorem	fucrid 17694	Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    ⇒   ⊢ (𝜑 → (𝑅(⟨𝐹, 𝐹⟩ ∙ 𝐺)( 1 ∘ (1st ‘𝐹))) = 𝑅)
Theorem	fucass 17695	Associativity of natural transformation composition. Remark 6.14(b) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ ∙ = (comp‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺))    &   ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ (𝐻𝑁𝐾))    ⇒   ⊢ (𝜑 → ((𝑇(⟨𝐺, 𝐻⟩ ∙ 𝐾)𝑆)(⟨𝐹, 𝐺⟩ ∙ 𝐾)𝑅) = (𝑇(⟨𝐹, 𝐻⟩ ∙ 𝐾)(𝑆(⟨𝐹, 𝐺⟩ ∙ 𝐻)𝑅)))
Theorem	fuccatid 17696*	The functor category is a category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 1 = (Id‘𝐷)    ⇒   ⊢ (𝜑 → (𝑄 ∈ Cat ∧ (Id‘𝑄) = (𝑓 ∈ (𝐶 Func 𝐷) ↦ ( 1 ∘ (1st ‘𝑓)))))
Theorem	fuccat 17697	The functor category is a category. Remark 6.16 in [Adamek] p. 88. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑄 ∈ Cat)
Theorem	fucid 17698	The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐼 = (Id‘𝑄)    &   ⊢ 1 = (Id‘𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐼‘𝐹) = ( 1 ∘ (1st ‘𝐹)))
Theorem	fucsect 17699*	Two natural transformations are in a section iff all the components are in a section relation. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    &   ⊢ 𝑆 = (Sect‘𝑄)    &   ⊢ 𝑇 = (Sect‘𝐷)    ⇒   ⊢ (𝜑 → (𝑈(𝐹𝑆𝐺)𝑉 ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ 𝑉 ∈ (𝐺𝑁𝐹) ∧ ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝑇((1st ‘𝐺)‘𝑥))(𝑉‘𝑥))))
Theorem	fucinv 17700*	Two natural transformations are inverses of each other iff all the components are inverse. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝑄 = (𝐶 FuncCat 𝐷)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐶 Nat 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))    &   ⊢ 𝐼 = (Inv‘𝑄)    &   ⊢ 𝐽 = (Inv‘𝐷)    ⇒   ⊢ (𝜑 → (𝑈(𝐹𝐼𝐺)𝑉 ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ 𝑉 ∈ (𝐺𝑁𝐹) ∧ ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))(𝑉‘𝑥))))