![]() |
Metamath
Proof Explorer Theorem List (p. 182 of 483) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30741) |
![]() (30742-32264) |
![]() (32265-48238) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | catcbascl 18101 | An element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 18106. (Contributed by AV, 14-Oct-2024.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑈) | ||
Theorem | catcslotelcl 18102 | A slot entry of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 18106. (Contributed by AV, 14-Oct-2024.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐸 = Slot (𝐸‘ndx) ⇒ ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝑈) | ||
Theorem | catcbaselcl 18103 | The base set of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 18106. (Contributed by AV, 14-Oct-2024.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈) | ||
Theorem | catchomcl 18104 | The Hom-set of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 18106. (Contributed by AV, 14-Oct-2024.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (Hom ‘𝑋) ∈ 𝑈) | ||
Theorem | catcccocl 18105 | The composition operation of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl 18106. (Contributed by AV, 14-Oct-2024.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (comp‘𝑋) ∈ 𝑈) | ||
Theorem | catcoppccl 18106 | The category of categories for a weak universe is closed under taking opposites. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝑋) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑂 ∈ 𝐵) | ||
Theorem | catcoppcclOLD 18107 | Obsolete proof of catcoppccl 18106 as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝑋) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑂 ∈ 𝐵) | ||
Theorem | catcfuccl 18108 | The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑄 = (𝑋 FuncCat 𝑌) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑄 ∈ 𝐵) | ||
Theorem | catcfucclOLD 18109 | Obsolete proof of catcfuccl 18108 as of 14-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑄 = (𝑋 FuncCat 𝑌) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑄 ∈ 𝐵) | ||
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 18113. 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 18115. 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 18111 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 18116, whereas the composition is the ordinary composition of functions, see estrccofval 18119 and estrcco 18120. It is shown that the category of extensible structures ExtStrCat is actually a category, see estrccat 18123 with the identity function as identity arrow, see estrcid 18124. 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 18124): 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 20561 and dfringc2 20590, but with special compositions). With this definitions, however, Theorem rngcresringcat 20602 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 18065, 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 18113. The claimed equivalence is proven by equivestrcsetc 18143. 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 20550 and df-ringc 20579. In the same way, more subcategories could be provided, resulting in the following "inclusion chain" by proving theorems like rngcresringcat 20602, 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 18143. Furthermore, it can be shown that SetCat is embedded into ExtStrCat, see embedsetcestrc 18158. Remark: equivestrcsetc 18143 as well as embedsetcestrc 18158 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 17164), 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 17189. 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) ⊆ Ob(B) and MorA(X,Y) ⊆ 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) ⊆ 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 20178) 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 18110 | 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 18111 | 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 18112 | Extend class notation to include the category ExtStr. |
class ExtStrCat | ||
Definition | df-estrc 18113* | 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 18111 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‘𝑦) ↑m (Base‘𝑥)))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉}) | ||
Theorem | estrcval 18114* | Value of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))) & ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))) ⇒ ⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) | ||
Theorem | estrcbas 18115 | Set of objects of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑈 = (Base‘𝐶)) | ||
Theorem | estrchomfval 18116* | Set of morphisms ("arrows") of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))) | ||
Theorem | estrchom 18117 | The morphisms between extensible structures are mappings between their base sets. (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ 𝐴 = (Base‘𝑋) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝐵 ↑m 𝐴)) | ||
Theorem | elestrchom 18118 | A morphism between extensible structures is a function between their base sets. (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ 𝐴 = (Base‘𝑋) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ↔ 𝐹:𝐴⟶𝐵)) | ||
Theorem | estrccofval 18119* | Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))) | ||
Theorem | estrcco 18120 | Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ 𝐴 = (Base‘𝑋) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐷 = (Base‘𝑍) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐷) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺 ∘ 𝐹)) | ||
Theorem | estrcbasbas 18121 | 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 18122* | Lemma for estrccat 18123. (Contributed by AV, 8-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝑈 ↦ ( I ↾ (Base‘𝑥))))) | ||
Theorem | estrccat 18123 | The category of extensible structures is a category. (Contributed by AV, 8-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) | ||
Theorem | estrcid 18124 | 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 18125 | 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 18126 | 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 18127 | Lemma 1 for estrres 18130. (Contributed by AV, 14-Mar-2020.) (Proof shortened by AV, 28-Oct-2024.) |
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) | ||
Theorem | estrreslem1OLD 18128 | Obsolete version of estrreslem1 18127 as of 28-Oct-2024. Lemma 1 for estrres 18130. (Contributed by AV, 14-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) | ||
Theorem | estrreslem2 18129 | Lemma 2 for estrres 18130. (Contributed by AV, 14-Mar-2020.) |
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → · ∈ 𝑌) ⇒ ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐶) | ||
Theorem | estrres 18130 | 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.) (Revised by AV, 3-Jul-2022.) |
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → · ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((𝐶 ↾s 𝐴) sSet 〈(Hom ‘ndx), 𝐺〉) = {〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉, 〈(comp‘ndx), · 〉}) | ||
Theorem | funcestrcsetclem1 18131* | Lemma 1 for funcestrcsetc 18140. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (Base‘𝑋)) | ||
Theorem | funcestrcsetclem2 18132* | Lemma 2 for funcestrcsetc 18140. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝑈) | ||
Theorem | funcestrcsetclem3 18133* | Lemma 3 for funcestrcsetc 18140. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) | ||
Theorem | funcestrcsetclem4 18134* | Lemma 4 for funcestrcsetc 18140. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) ⇒ ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) | ||
Theorem | funcestrcsetclem5 18135* | Lemma 5 for funcestrcsetc 18140. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) & ⊢ 𝑀 = (Base‘𝑋) & ⊢ 𝑁 = (Base‘𝑌) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌) = ( I ↾ (𝑁 ↑m 𝑀))) | ||
Theorem | funcestrcsetclem6 18136* | Lemma 6 for funcestrcsetc 18140. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) & ⊢ 𝑀 = (Base‘𝑋) & ⊢ 𝑁 = (Base‘𝑌) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐻 ∈ (𝑁 ↑m 𝑀)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻) | ||
Theorem | funcestrcsetclem7 18137* | Lemma 7 for funcestrcsetc 18140. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → ((𝑋𝐺𝑋)‘((Id‘𝐸)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋))) | ||
Theorem | funcestrcsetclem8 18138* | Lemma 8 for funcestrcsetc 18140. (Contributed by AV, 15-Feb-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝐸)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌))) | ||
Theorem | funcestrcsetclem9 18139* | Lemma 9 for funcestrcsetc 18140. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝐻 ∈ (𝑋(Hom ‘𝐸)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝐸)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝐸)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) | ||
Theorem | funcestrcsetc 18140* | 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 18141* | 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 18142* | 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 18143* | 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 18144 | 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 18145* | Lemma 1 for funcsetcestrc 18155. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) = {〈(Base‘ndx), 𝑋〉}) | ||
Theorem | funcsetcestrclem2 18146* | Lemma 2 for funcsetcestrc 18155. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) ∈ 𝑈) | ||
Theorem | funcsetcestrclem3 18147* | Lemma 3 for funcsetcestrc 18155. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) ⇒ ⊢ (𝜑 → 𝐹:𝐶⟶𝐵) | ||
Theorem | embedsetcestrclem 18148* | Lemma for embedsetcestrc 18158. (Contributed by AV, 31-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) ⇒ ⊢ (𝜑 → 𝐹:𝐶–1-1→𝐵) | ||
Theorem | funcsetcestrclem4 18149* | Lemma 4 for funcsetcestrc 18155. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) ⇒ ⊢ (𝜑 → 𝐺 Fn (𝐶 × 𝐶)) | ||
Theorem | funcsetcestrclem5 18150* | Lemma 5 for funcsetcestrc 18155. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌) = ( I ↾ (𝑌 ↑m 𝑋))) | ||
Theorem | funcsetcestrclem6 18151* | Lemma 6 for funcsetcestrc 18155. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝐻 ∈ (𝑌 ↑m 𝑋)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻) | ||
Theorem | funcsetcestrclem7 18152* | Lemma 7 for funcsetcestrc 18155. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑋𝐺𝑋)‘((Id‘𝑆)‘𝑋)) = ((Id‘𝐸)‘(𝐹‘𝑋))) | ||
Theorem | funcsetcestrclem8 18153* | Lemma 8 for funcsetcestrc 18155. (Contributed by AV, 28-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑆)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝐸)(𝐹‘𝑌))) | ||
Theorem | funcsetcestrclem9 18154* | Lemma 9 for funcsetcestrc 18155. (Contributed by AV, 28-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) | ||
Theorem | funcsetcestrc 18155* | 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 18156* | 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 18157* | 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 18158* | 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→𝐵)) | ||
Syntax | cxpc 18159 | Extend class notation with the product of two categories. |
class ×c | ||
Syntax | c1stf 18160 | Extend class notation with the first projection functor. |
class 1stF | ||
Syntax | c2ndf 18161 | Extend class notation with the second projection functor. |
class 2ndF | ||
Syntax | cprf 18162 | Extend class notation with the functor pairing operation. |
class 〈,〉F | ||
Definition | df-xpc 18163* | 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 18164* | 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 18165* | 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 18166* | 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 18167 | The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ ×c Fn (V × V) | ||
Theorem | xpcval 18168* | 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 18169 | Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝑌 = (Base‘𝐷) ⇒ ⊢ (𝑋 × 𝑌) = (Base‘𝑇) | ||
Theorem | xpchomfval 18170* | 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 18171 | 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 18172 | A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ Rel (𝑋𝐾𝑌) | ||
Theorem | xpccofval 18173* | 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 18174 | 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 18175 | 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 18176 | 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 18177 | 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 18178 | 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 18179* | 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 18180 | 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 18181 | The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑇 ∈ Cat) | ||
Theorem | 1stfval 18182* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑃 = (𝐶 1stF 𝐷) ⇒ ⊢ (𝜑 → 𝑃 = 〈(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) | ||
Theorem | 1stf1 18183 | 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 18184 | 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 18185* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐶 2ndF 𝐷) ⇒ ⊢ (𝜑 → 𝑄 = 〈(2nd ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (2nd ↾ (𝑥𝐻𝑦)))〉) | ||
Theorem | 2ndf1 18186 | 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 18187 | 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 18188 | 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 18189 | 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 18190* | Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → 𝑃 = 〈(𝑥 ∈ 𝐵 ↦ 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (ℎ ∈ (𝑥𝐻𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉) | ||
Theorem | prf1 18191 | Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝑃)‘𝑋) = 〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)〉) | ||
Theorem | prf2fval 18192* | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝑃)𝑌) = (ℎ ∈ (𝑋𝐻𝑌) ↦ 〈((𝑋(2nd ‘𝐹)𝑌)‘ℎ), ((𝑋(2nd ‘𝐺)𝑌)‘ℎ)〉)) | ||
Theorem | prf2 18193 | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝑃)𝑌)‘𝐾) = 〈((𝑋(2nd ‘𝐹)𝑌)‘𝐾), ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)〉) | ||
Theorem | prfcl 18194 | The pairing of functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐷 is a functor 〈𝐹, 𝐺〉:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝑇 = (𝐷 ×c 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇)) | ||
Theorem | prf1st 18195 | Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐷 1stF 𝐸) ∘func 𝑃) = 𝐹) | ||
Theorem | prf2nd 18196 | Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺) | ||
Theorem | 1st2ndprf 18197 | 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 18198 | The category of categories for a weak universe is closed under the product category operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑇 = (𝑋 ×c 𝑌) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑇 ∈ 𝐵) | ||
Theorem | catcxpcclOLD 18199 | Obsolete proof of catcxpccl 18198 as of 14-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑇 = (𝑋 ×c 𝑌) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑇 ∈ 𝐵) | ||
Theorem | xpcpropd 18200 | 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 𝐷)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |