P. 169 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16801-16900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	catccat 16801	The category of categories is a category, see remark 3.48 in [Adamek] p. 40. (Clearly it cannot be an element of itself, hence it is "𝑈 -large".) (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	resscatc 16802	The restriction of the category of categories to a subset is the category of categories in the subset. Thus, the CatCat‘𝑈 categories for different 𝑈 are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐷 = (CatCat‘𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ((Homf ‘(𝐶 ↾s 𝑉)) = (Homf ‘𝐷) ∧ (compf‘(𝐶 ↾s 𝑉)) = (compf‘𝐷)))
Theorem	catcisolem 16803*	Lemma for catciso 16804. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Inv‘𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ◡((◡𝐹‘𝑥)𝐺(◡𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺)    &   ⊢ (𝜑 → 𝐹:𝑅–1-1-onto→𝑆)    ⇒   ⊢ (𝜑 → ⟨𝐹, 𝐺⟩(𝑋𝐼𝑌)⟨◡𝐹, 𝐻⟩)
Theorem	catciso 16804	A functor is an isomorphism of categories if and only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in [Adamek] p. 34. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑅 = (Base‘𝑋)    &   ⊢ 𝑆 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)))
Theorem	catcoppccl 16805	The category of categories for a weak universe is closed under taking opposites. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑂 ∈ 𝐵)
Theorem	catcfuccl 16806	The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑄 = (𝑋 FuncCat 𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑄 ∈ 𝐵)
8.3.3  The category of extensible structures The "category of extensible structures" ExtStrCat is the category of all sets in a universe regarded as extensible structures and the functions between their base sets, see df-estrc 16810. Since we consider only "small categories" (i.e. categories whose objects and morphisms are actually sets and not proper classes), the objects of the category (i.e. the base set of the category regarded as extensible structure) are all sets in a universe 𝑢, which can be an arbitrary set, see estrcbas 16812. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. If a set is not a real extensible structure, it is regarded as extensible structure with an empty base set. Because of bascnvimaeqv 16808 we do not need to restrict the universe to sets which "have a base". The morphisms (or arrows) between two objects, i.e. sets from the universe, are the mappings between their base sets, see estrchomfval 16813, whereas the composition is the ordinary composition of functions, see estrccofval 16816 and estrcco 16817. It is shown that the category of extensible structures ExtStrCat is actually a category, see estrccat 16820 with the identity function as identity arrow, see estrcid 16821. In the following, some background information about the category of extensible structures is given, taken from the discussion in Github issue #1507 (see https://github.com/metamath/set.mm/issues/1507): At the beginning, the categories of non-unital rings RngCat and unital rings RingCat were defined separately (as unordered triples of ordereds pairs, see dfrngc2 42297 and dfringc2 42343, but with special compositions). With this definitions, however, theorem rngcresringcat 42355 could not be proven, because the compositions were not compatible. Unfortunately, no precise definition of the composition within the category of rings could be found in the literature. In section 3.3 EXAMPLES, paragraph (2) of [Adamek] p. 22, however, a definition is given for "Grp", the category of groups: "The following constructs; i.e., categories of structured sets and structure-preserving functions between them (o will always be the composition of functions and idA will always be the identity function on A): ... (b) Grp with objects all groups and morphisms all homomorphisms between them." Therefore, the compositions should have been harmonized by using the composition of the category of sets SetCat, see df-setc 16773, which is the ordinary composition of functions. Analogously, categories of Rngs (and Rings) could have been shown to be restrictions resp. subcategories of the category of sets. BJ and MC observed, however, that "... ↾cat [cannot be used] to restrict the category Set to Ring, because the homs are different. Although Ring is a concrete category, a hom between rings R and S is a function (Base`R) --> (Base`S) with certain properties, unlike in Set where it is a function R --> S.". Therefore, MC suggested that "we could have an alternative version of the Set category consisting of extensible structures (in U) together with (A Hom B) := (Base`A) --> (Base`B). This category is not isomorphic to Set because different extensible structures can have the same base set, but it is equivalent to Set; the relevant functors are (U`A) = (Base`A), the forgetful functor, and (F`A) = { <. (Base`ndx), A >. }". This led to the current definition of ExtStrCat, see df-estrc 16810. The claimed equivalence is proven by equivestrcsetc 16839. Having a definition of a category of extensible structures, the categories of non-unital and unital rings can be defined as appropriate restrictions of the category of extensible structures, see df-rngc 42284 and df-ringc 42330. In the same way, more subcategories could be provided, resulting in the following "inclusion chain" by proving theorems like rngcresringcat 42355, although the morphisms of the shown categories are different ( "->" means "is subcategory of"): RingCat-> RngCat-> GrpCat -> MndCat -> MgmCat -> ExtStrCat According to MC, "If we generalize from subcategories to embeddings, then we can even fit SetCat into the chain, equivalent to ExtStrCat at the end." As mentioned before, the equivalence of SetCat and ExtStrCat is proven by equivestrcsetc 16839. Furthermore, it can be shown that SetCat is embedded into ExtStrCat, see embedsetcestrc 16854. Remark: equivestrcsetc 16839 as well as embedsetcestrc 16854 require that the index of the base set extractor is contained within the considered universe. This is ensured by assuming that the natural numbers are contained within the considered universe: ω ∈ 𝑈 (see wunndx 15925), but it would be currently sufficient to assume that 1 ∈ 𝑈, because the index value of the base set extractor is hard-coded as 1, see basendx 15970. Some people, however, feel uncomfortable to say that a ring "is a" group (without mentioning the restriction to the addition, which is usually found in the literature, e.g. the definition of a ring in [Herstein] p. 126: "... Note that so far all we have said is that R is an abelian group under +.". The main argument against a ring being a group is the number of components/slots: usually, a group consists of (exactly!) two components (a base set and an operation), whereas a ring consists of (exactly!) three components (a base set and two operations). According to this "definition", a ring cannot be a group. This is also an (unfortunately informal) argument for the category of rings not being a subcategory of the category of abelian groups in "Categories and Functors", Bodo Pareigis, Academic Press, New York, London, 1970: "A category A is called a subcategory of a category B if Ob(A) C_ Ob(B) and MorA(X,Y) C_ MorB(X,Y) for all X,Y e. Ob(A), if the composition of morphisms in A coincides with the composition of the same morphisms in B and if the identity of an object in A is also the identity of the same object viewed as an object in B. Then there is a forgetful functor from A to B. We note that Ri [the category of rings] is not a subcategory of Ab [the category of abelian groups]. In fact, Ob(Ri) C_ Ob(Ab) is not true, although every ring can also be regarded as an abelian group. The corresponding abelian groups of two rings may coincide even if the rings do not coincide. The multiplication may be defined differently.". As long as we define Rings, Groups, etc. in a way that 𝐴 ∈ Ring → 𝐴 ∈ Grp is valid (see ringgrp 18598) the corresponding categories are in a subcategory relation. If we do not want Rings to be Groups (then the category of rings would not be a subcategory of the category of groups, as observed by Pareigis), we would have to change the definitions of Magmas, Monoids, Groups, Rings etc. to restrict them to have exactly the required number of slots, so that the following holds 𝑔 ∈ Grp → 𝑔 Struct ⟨(Base‘ndx), (+g‘ndx)⟩ 𝑟 ∈ Ring → 𝑟 Struct ⟨(Base‘ndx), (+g‘ndx), (.r‘ndx)⟩
Theorem	fncnvimaeqv 16807	The inverse images of the universal class V under functions on the universal class V are the universal class V itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020.)
⊢ (𝐹 Fn V → (◡𝐹 “ V) = V)
Theorem	bascnvimaeqv 16808	The inverse image of the universal class V under the base function is the universal class V itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020.)
⊢ (◡Base “ V) = V
Syntax	cestrc 16809	Extend class notation to include the category ExtStr.
class ExtStrCat
Definition	df-estrc 16810*	Definition of the category ExtStr of extensible structures. This is the category whose objects are all sets in a universe 𝑢 regarded as extensible structures and whose morphisms are the functions between their base sets. If a set is not a real extensible structure, it is regarded as extensible structure with an empty base set. Because of bascnvimaeqv 16808 we do not need to restrict the universe to sets which "have a base". Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Proposed by Mario Carneiro, 5-Mar-2020.) (Contributed by AV, 7-Mar-2020.)
⊢ ExtStrCat = (𝑢 ∈ V ↦ {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚 (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))⟩})
Theorem	estrcval 16811*	Value of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))    &   ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚 (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓))))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝑈⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	estrcbas 16812	Set of objects of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
Theorem	estrchomfval 16813*	Set of morphisms ("arrows") of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))
Theorem	estrchom 16814	The morphisms between extensible structures are mappings between their base sets. (Contributed by AV, 7-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝐴 = (Base‘𝑋)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝐵 ↑𝑚 𝐴))
Theorem	elestrchom 16815	A morphism between extensible structures is a function between their base sets. (Contributed by AV, 7-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ 𝐴 = (Base‘𝑋)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ↔ 𝐹:𝐴⟶𝐵))
Theorem	estrccofval 16816*	Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚 (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓))))
Theorem	estrcco 16817	Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ 𝐴 = (Base‘𝑋)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐷 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐷)    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘ 𝐹))
Theorem	estrcbasbas 16818	An element of the base set of the base set of the category of extensible structures (i.e. the base set of an extensible structure) belongs to the considered weak universe. (Contributed by AV, 22-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ ((𝜑 ∧ 𝐸 ∈ 𝐵) → (Base‘𝐸) ∈ 𝑈)
Theorem	estrccatid 16819*	Lemma for estrccat 16820. (Contributed by AV, 8-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝑈 ↦ ( I ↾ (Base‘𝑥)))))
Theorem	estrccat 16820	The category of extensible structures is a category. (Contributed by AV, 8-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	estrcid 16821	The identity arrow in the category of extensible structures is the identity function of base sets. (Contributed by AV, 8-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ (Base‘𝑋)))
Theorem	estrchomfn 16822	The Hom-set operation in the category of extensible structures (in a universe) is a function. (Contributed by AV, 8-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝑈 × 𝑈))
Theorem	estrchomfeqhom 16823	The functionalized Hom-set operation equals the Hom-set operation in the category of extensible structures (in a universe). (Contributed by AV, 8-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → (Homf ‘𝐶) = 𝐻)
Theorem	estrreslem1 16824	Lemma 1 for estrres 16826. (Contributed by AV, 14-Mar-2020.)
⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
Theorem	estrreslem2 16825	Lemma 2 for estrres 16826. (Contributed by AV, 14-Mar-2020.)
⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → · ∈ 𝑌)    ⇒   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐶)
Theorem	estrres 16826	Any restriction of a category (as an extensible structure which is an unordered triple of ordered pairs) is an unordered triple of ordered pairs. (Contributed by AV, 15-Mar-2020.)
⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → · ∈ 𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐶 ↾s 𝐴) sSet ⟨(Hom ‘ndx), 𝐺⟩) = {⟨(Base‘ndx), 𝐴⟩, ⟨(Hom ‘ndx), 𝐺⟩, ⟨(comp‘ndx), · ⟩})
Theorem	funcestrcsetclem1 16827*	Lemma 1 for funcestrcsetc 16836. (Contributed by AV, 22-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (Base‘𝑋))
Theorem	funcestrcsetclem2 16828*	Lemma 2 for funcestrcsetc 16836. (Contributed by AV, 22-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝑈)
Theorem	funcestrcsetclem3 16829*	Lemma 3 for funcestrcsetc 16836. (Contributed by AV, 22-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    ⇒   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
Theorem	funcestrcsetclem4 16830*	Lemma 4 for funcestrcsetc 16836. (Contributed by AV, 22-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))))    ⇒   ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵))
Theorem	funcestrcsetclem5 16831*	Lemma 5 for funcestrcsetc 16836. (Contributed by AV, 23-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))))    &   ⊢ 𝑀 = (Base‘𝑋)    &   ⊢ 𝑁 = (Base‘𝑌)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌) = ( I ↾ (𝑁 ↑𝑚 𝑀)))
Theorem	funcestrcsetclem6 16832*	Lemma 6 for funcestrcsetc 16836. (Contributed by AV, 23-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))))    &   ⊢ 𝑀 = (Base‘𝑋)    &   ⊢ 𝑁 = (Base‘𝑌)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐻 ∈ (𝑁 ↑𝑚 𝑀)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻)
Theorem	funcestrcsetclem7 16833*	Lemma 7 for funcestrcsetc 16836. (Contributed by AV, 23-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → ((𝑋𝐺𝑋)‘((Id‘𝐸)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋)))
Theorem	funcestrcsetclem8 16834*	Lemma 8 for funcestrcsetc 16836. (Contributed by AV, 15-Feb-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝐸)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌)))
Theorem	funcestrcsetclem9 16835*	Lemma 9 for funcestrcsetc 16836. (Contributed by AV, 23-Mar-2020.)
⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝐻 ∈ (𝑋(Hom ‘𝐸)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝐸)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(⟨𝑋, 𝑌⟩(comp‘𝐸)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)))
Theorem	funcestrcsetc 16836*	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‘𝑦) ↑𝑚 (Base‘𝑥)))))    ⇒   ⊢ (𝜑 → 𝐹(𝐸 Func 𝑆)𝐺)
Theorem	fthestrcsetc 16837*	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‘𝑦) ↑𝑚 (Base‘𝑥)))))    ⇒   ⊢ (𝜑 → 𝐹(𝐸 Faith 𝑆)𝐺)
Theorem	fullestrcsetc 16838*	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‘𝑦) ↑𝑚 (Base‘𝑥)))))    ⇒   ⊢ (𝜑 → 𝐹(𝐸 Full 𝑆)𝐺)
Theorem	equivestrcsetc 16839*	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‘𝑦) ↑𝑚 (Base‘𝑥)))))    &   ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐹(𝐸 Faith 𝑆)𝐺 ∧ 𝐹(𝐸 Full 𝑆)𝐺 ∧ ∀𝑏 ∈ 𝐶 ∃𝑎 ∈ 𝐵 ∃𝑖 𝑖:𝑏–1-1-onto→(𝐹‘𝑎)))
Theorem	setc1strwun 16840	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 16841*	Lemma 1 for funcsetcestrc 16851. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) = {⟨(Base‘ndx), 𝑋⟩})
Theorem	funcsetcestrclem2 16842*	Lemma 2 for funcsetcestrc 16851. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) ∈ 𝑈)
Theorem	funcsetcestrclem3 16843*	Lemma 3 for funcsetcestrc 16851. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐶⟶𝐵)
Theorem	embedsetcestrclem 16844*	Lemma for embedsetcestrc 16854. (Contributed by AV, 31-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐶–1-1→𝐵)
Theorem	funcsetcestrclem4 16845*	Lemma 4 for funcsetcestrc 16851. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 Fn (𝐶 × 𝐶))
Theorem	funcsetcestrclem5 16846*	Lemma 5 for funcsetcestrc 16851. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌) = ( I ↾ (𝑌 ↑𝑚 𝑋)))
Theorem	funcsetcestrclem6 16847*	Lemma 6 for funcsetcestrc 16851. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝐻 ∈ (𝑌 ↑𝑚 𝑋)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻)
Theorem	funcsetcestrclem7 16848*	Lemma 7 for funcsetcestrc 16851. (Contributed by AV, 27-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑋𝐺𝑋)‘((Id‘𝑆)‘𝑋)) = ((Id‘𝐸)‘(𝐹‘𝑋)))
Theorem	funcsetcestrclem8 16849*	Lemma 8 for funcsetcestrc 16851. (Contributed by AV, 28-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑆)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝐸)(𝐹‘𝑌)))
Theorem	funcsetcestrclem9 16850*	Lemma 9 for funcsetcestrc 16851. (Contributed by AV, 28-Mar-2020.)
⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(⟨𝑋, 𝑌⟩(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)))
Theorem	funcsetcestrc 16851*	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 ↾ (𝑦 ↑𝑚 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ (𝜑 → 𝐹(𝑆 Func 𝐸)𝐺)
Theorem	fthsetcestrc 16852*	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 ↾ (𝑦 ↑𝑚 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ (𝜑 → 𝐹(𝑆 Faith 𝐸)𝐺)
Theorem	fullsetcestrc 16853*	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 ↾ (𝑦 ↑𝑚 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    ⇒   ⊢ (𝜑 → 𝐹(𝑆 Full 𝐸)𝐺)
Theorem	embedsetcestrc 16854*	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 ↾ (𝑦 ↑𝑚 𝑥))))    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → (𝐹(𝑆 Faith 𝐸)𝐺 ∧ 𝐹:𝐶–1-1→𝐵))
8.4  Categorical constructions
8.4.1  Product of categories
Syntax	cxpc 16855	Extend class notation with the product of two categories.
class ×c
Syntax	c1stf 16856	Extend class notation with the first projection functor.
class 1stF
Syntax	c2ndf 16857	Extend class notation with the second projection functor.
class 2ndF
Syntax	cprf 16858	Extend class notation with the functor pairing operation.
class ⟨,⟩F
Definition	df-xpc 16859*	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 16860*	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 16861*	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 16862*	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 16863	The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ ×c Fn (V × V)
Theorem	xpcval 16864*	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 16865	Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝑋 = (Base‘𝐶)    &   ⊢ 𝑌 = (Base‘𝐷)    ⇒   ⊢ (𝑋 × 𝑌) = (Base‘𝑇)
Theorem	xpchomfval 16866*	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	xpchom 16867	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 16868	A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐾 = (Hom ‘𝑇)    ⇒   ⊢ Rel (𝑋𝐾𝑌)
Theorem	xpccofval 16869*	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐾 = (Hom ‘𝑇)    &   ⊢ · = (comp‘𝐶)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ 𝑂 = (comp‘𝑇)    ⇒   ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩ · (1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩ ∙ (2nd ‘𝑦))(2nd ‘𝑓))⟩))
Theorem	xpcco 16870	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 16871	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 16872	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 16873	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 16874	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 16875*	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 16876	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 16877	The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑇 ∈ Cat)
Theorem	1stfval 16878*	Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑃 = (𝐶 1stF 𝐷)    ⇒   ⊢ (𝜑 → 𝑃 = ⟨(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))⟩)
Theorem	1stf1 16879	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 16880	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 16881*	Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ 𝑇 = (𝐶 ×c 𝐷)    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ 𝐻 = (Hom ‘𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐶 2ndF 𝐷)    ⇒   ⊢ (𝜑 → 𝑄 = ⟨(2nd ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (2nd ↾ (𝑥𝐻𝑦)))⟩)
Theorem	2ndf1 16882	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 16883	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 16884	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 16885	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 16886*	Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → 𝑃 = ⟨(𝑥 ∈ 𝐵 ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (ℎ ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))⟩)
Theorem	prf1 16887	Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝑃)‘𝑋) = ⟨((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)⟩)
Theorem	prf2fval 16888*	Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋(2nd ‘𝑃)𝑌) = (ℎ ∈ (𝑋𝐻𝑌) ↦ ⟨((𝑋(2nd ‘𝐹)𝑌)‘ℎ), ((𝑋(2nd ‘𝐺)𝑌)‘ℎ)⟩))
Theorem	prf2 16889	Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘𝑃)𝑌)‘𝐾) = ⟨((𝑋(2nd ‘𝐹)𝑌)‘𝐾), ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)⟩)
Theorem	prfcl 16890	The pairing of functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐷 is a functor ⟨𝐹, 𝐺⟩:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ 𝑇 = (𝐷 ×c 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇))
Theorem	prf1st 16891	Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → ((𝐷 1stF 𝐸) ∘func 𝑃) = 𝐹)
Theorem	prf2nd 16892	Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝑃 = (𝐹 ⟨,⟩F 𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))    ⇒   ⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺)
Theorem	1st2ndprf 16893	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 16894	The category of categories for a weak universe is closed under the product category operation. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐶 = (CatCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝑇 = (𝑋 ×c 𝑌)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑇 ∈ 𝐵)
Theorem	xpcpropd 16895	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 16896	Extend class notation with the evaluation functor.
class evalF
Syntax	ccurf 16897	Extend class notation with the currying of a functor.
class curryF
Syntax	cuncf 16898	Extend class notation with the uncurrying of a functor.
class uncurryF
Syntax	cdiag 16899	Extend class notation to include the diagonal functor.
class Δfunc
Definition	df-evlf 16900*	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 ‘𝑦))‘𝑔))))⟩)