Home | Metamath
Proof Explorer Theorem List (p. 174 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | homacd 17301 | The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌) | ||
Theorem | homadmcd 17302 | Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹 = 〈𝑋, 𝑌, (2nd ‘𝐹)〉) | ||
Theorem | arwval 17303 | The set of arrows is the union of all the disjointified hom-sets. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ 𝐴 = ∪ ran 𝐻 | ||
Theorem | arwrcl 17304 | The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝐶 ∈ Cat) | ||
Theorem | arwhoma 17305 | An arrow is contained in the hom-set corresponding to its domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝐹 ∈ ((doma‘𝐹)𝐻(coda‘𝐹))) | ||
Theorem | homarw 17306 | A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝑋𝐻𝑌) ⊆ 𝐴 | ||
Theorem | arwdm 17307 | The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → (doma‘𝐹) ∈ 𝐵) | ||
Theorem | arwcd 17308 | The codomain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → (coda‘𝐹) ∈ 𝐵) | ||
Theorem | dmaf 17309 | The domain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (doma ↾ 𝐴):𝐴⟶𝐵 | ||
Theorem | cdaf 17310 | The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (coda ↾ 𝐴):𝐴⟶𝐵 | ||
Theorem | arwhom 17311 | The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → (2nd ‘𝐹) ∈ ((doma‘𝐹)𝐽(coda‘𝐹))) | ||
Theorem | arwdmcd 17312 | Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝐹 = 〈(doma‘𝐹), (coda‘𝐹), (2nd ‘𝐹)〉) | ||
Syntax | cida 17313 | Extend class notation to include identity for arrows. |
class Ida | ||
Syntax | ccoa 17314 | Extend class notation to include composition for arrows. |
class compa | ||
Definition | df-ida 17315* | Definition of the identity arrow, which is just the identity morphism tagged with its domain and codomain. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
⊢ Ida = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ 〈𝑥, 𝑥, ((Id‘𝑐)‘𝑥)〉)) | ||
Definition | df-coa 17316* | Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a quinary operation like the regular composition in a category comp. Instead, it is a partial binary operation on arrows, which is defined when the domain of the first arrow matches the codomain of the second. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ compa = (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ 〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓), (doma‘𝑔)〉(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))〉)) | ||
Theorem | idafval 17317* | Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵 ↦ 〈𝑥, 𝑥, ( 1 ‘𝑥)〉)) | ||
Theorem | idaval 17318 | Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) = 〈𝑋, 𝑋, ( 1 ‘𝑋)〉) | ||
Theorem | ida2 17319 | Morphism part of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (2nd ‘(𝐼‘𝑋)) = ( 1 ‘𝑋)) | ||
Theorem | idahom 17320 | Domain and codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐻𝑋)) | ||
Theorem | idadm 17321 | Domain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (doma‘(𝐼‘𝑋)) = 𝑋) | ||
Theorem | idacd 17322 | Codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (coda‘(𝐼‘𝑋)) = 𝑋) | ||
Theorem | idaf 17323 | The identity arrow function is a function from objects to arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ (𝜑 → 𝐼:𝐵⟶𝐴) | ||
Theorem | coafval 17324* | The value of the composition of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐴 = (Arrow‘𝐶) & ⊢ ∙ = (comp‘𝐶) ⇒ ⊢ · = (𝑔 ∈ 𝐴, 𝑓 ∈ {ℎ ∈ 𝐴 ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ 〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓), (doma‘𝑔)〉 ∙ (coda‘𝑔))(2nd ‘𝑓))〉) | ||
Theorem | eldmcoa 17325 | A pair 〈𝐺, 𝐹〉 is in the domain of the arrow composition, if the domain of 𝐺 equals the codomain of 𝐹. (In this case we say 𝐺 and 𝐹 are composable.) (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ (𝐺dom · 𝐹 ↔ (𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ (coda‘𝐹) = (doma‘𝐺))) | ||
Theorem | dmcoass 17326 | The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ dom · ⊆ (𝐴 × 𝐴) | ||
Theorem | homdmcoa 17327 | If 𝐹:𝑋⟶𝑌 and 𝐺:𝑌⟶𝑍, then 𝐺 and 𝐹 are composable. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → 𝐺dom · 𝐹) | ||
Theorem | coaval 17328 | Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ ∙ = (comp‘𝐶) ⇒ ⊢ (𝜑 → (𝐺 · 𝐹) = 〈𝑋, 𝑍, ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))〉) | ||
Theorem | coa2 17329 | The morphism part of arrow composition. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ ∙ = (comp‘𝐶) ⇒ ⊢ (𝜑 → (2nd ‘(𝐺 · 𝐹)) = ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))) | ||
Theorem | coahom 17330 | The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → (𝐺 · 𝐹) ∈ (𝑋𝐻𝑍)) | ||
Theorem | coapm 17331 | Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ · ∈ (𝐴 ↑pm (𝐴 × 𝐴)) | ||
Theorem | arwlid 17332 | Left identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ · = (compa‘𝐶) & ⊢ 1 = (Ida‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (( 1 ‘𝑌) · 𝐹) = 𝐹) | ||
Theorem | arwrid 17333 | Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ · = (compa‘𝐶) & ⊢ 1 = (Ida‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (𝐹 · ( 1 ‘𝑋)) = 𝐹) | ||
Theorem | arwass 17334 | Associativity of composition in a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ · = (compa‘𝐶) & ⊢ 1 = (Ida‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑊)) ⇒ ⊢ (𝜑 → ((𝐾 · 𝐺) · 𝐹) = (𝐾 · (𝐺 · 𝐹))) | ||
Syntax | csetc 17335 | Extend class notation to include the category Set. |
class SetCat | ||
Definition | df-setc 17336* | Definition of the category Set, relativized to a subset 𝑢. Example 3.3(1) of [Adamek] p. 22. This is the category of all sets in 𝑢 and functions between these sets. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by FL, 8-Nov-2013.) (Revised by Mario Carneiro, 3-Jan-2017.) |
⊢ SetCat = (𝑢 ∈ V ↦ {〈(Base‘ndx), 𝑢〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ (𝑦 ↑m 𝑥))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉}) | ||
Theorem | setcval 17337* | Value of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ (𝑦 ↑m 𝑥))) & ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) ⇒ ⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) | ||
Theorem | setcbas 17338 | Set of objects of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑈 = (Base‘𝐶)) | ||
Theorem | setchomfval 17339* | Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ (𝑦 ↑m 𝑥))) | ||
Theorem | setchom 17340 | Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑌 ↑m 𝑋)) | ||
Theorem | elsetchom 17341 | A morphism of sets is a function. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ↔ 𝐹:𝑋⟶𝑌)) | ||
Theorem | setccofval 17342* | Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) | ||
Theorem | setcco 17343 | Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑌) & ⊢ (𝜑 → 𝐺:𝑌⟶𝑍) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺 ∘ 𝐹)) | ||
Theorem | setccatid 17344* | Lemma for setccat 17345. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝑈 ↦ ( I ↾ 𝑥)))) | ||
Theorem | setccat 17345 | The category of sets is a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) | ||
Theorem | setcid 17346 | The identity arrow in the category of sets is the identity function. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑋)) | ||
Theorem | setcmon 17347 | A monomorphism of sets is an injection. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ 𝑀 = (Mono‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ 𝐹:𝑋–1-1→𝑌)) | ||
Theorem | setcepi 17348 | An epimorphism of sets is a surjection. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ (𝜑 → 2o ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ 𝐹:𝑋–onto→𝑌)) | ||
Theorem | setcsect 17349 | A section in the category of sets, written out. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹:𝑋⟶𝑌 ∧ 𝐺:𝑌⟶𝑋 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝑋)))) | ||
Theorem | setcinv 17350 | An inverse in the category of sets is the converse operation. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ 𝑁 = (Inv‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹:𝑋–1-1-onto→𝑌 ∧ 𝐺 = ◡𝐹))) | ||
Theorem | setciso 17351 | An isomorphism in the category of sets is a bijection. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹:𝑋–1-1-onto→𝑌)) | ||
Theorem | resssetc 17352 | The restriction of the category of sets to a subset is the category of sets in the subset. Thus, the SetCat‘𝑈 categories for different 𝑈 are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ 𝐷 = (SetCat‘𝑉) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → 𝑉 ⊆ 𝑈) ⇒ ⊢ (𝜑 → ((Homf ‘(𝐶 ↾s 𝑉)) = (Homf ‘𝐷) ∧ (compf‘(𝐶 ↾s 𝑉)) = (compf‘𝐷))) | ||
Theorem | funcsetcres2 17353 | A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ 𝐷 = (SetCat‘𝑉) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → 𝑉 ⊆ 𝑈) ⇒ ⊢ (𝜑 → (𝐸 Func 𝐷) ⊆ (𝐸 Func 𝐶)) | ||
Syntax | ccatc 17354 | Extend class notation to include the category Cat. |
class CatCat | ||
Definition | df-catc 17355* | Definition of the category Cat, which consists of all categories in the universe 𝑢 (i.e. "𝑢-small categories", see definition 3.44. of [Adamek] p. 39), with functors as the morphisms. Definition 3.47 of [Adamek] p. 40. We do not introduce a specific definition for "𝑢 -large categories", which can be expressed as (Cat ∖ 𝑢). (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ CatCat = (𝑢 ∈ V ↦ ⦋(𝑢 ∩ Cat) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))〉}) | ||
Theorem | catcval 17356* | Value of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat)) & ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦))) & ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))) ⇒ ⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) | ||
Theorem | catcbas 17357 | Set of objects of the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat)) | ||
Theorem | catchomfval 17358* | Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦))) | ||
Theorem | catchom 17359 | Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 Func 𝑌)) | ||
Theorem | catccofval 17360* | Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))) | ||
Theorem | catcco 17361 | Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋 Func 𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌 Func 𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺 ∘func 𝐹)) | ||
Theorem | catccatid 17362* | Lemma for catccat 17364. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ (idfunc‘𝑥)))) | ||
Theorem | catcid 17363 | The identity arrow in the category of categories is the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝐼 = (idfunc‘𝑋) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) = 𝐼) | ||
Theorem | catccat 17364 | 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 17365 | 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 17366* | Lemma for catciso 17367. (Contributed by Mario Carneiro, 29-Jan-2017.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑅 = (Base‘𝑋) & ⊢ 𝑆 = (Base‘𝑌) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Inv‘𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ◡((◡𝐹‘𝑥)𝐺(◡𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))𝐺) & ⊢ (𝜑 → 𝐹:𝑅–1-1-onto→𝑆) ⇒ ⊢ (𝜑 → 〈𝐹, 𝐺〉(𝑋𝐼𝑌)〈◡𝐹, 𝐻〉) | ||
Theorem | catciso 17367 | 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 17368 | 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 17369 | 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) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑄 ∈ 𝐵) | ||
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 17373. 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 17375. 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 17371 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 17376, whereas the composition is the ordinary composition of functions, see estrccofval 17379 and estrcco 17380. It is shown that the category of extensible structures ExtStrCat is actually a category, see estrccat 17383 with the identity function as identity arrow, see estrcid 17384. 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 17384): 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 44263 and dfringc2 44309, but with special compositions). With this definitions, however, theorem rngcresringcat 44321 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 17336, 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 17373. The claimed equivalence is proven by equivestrcsetc 17402. 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 44250 and df-ringc 44296. In the same way, more subcategories could be provided, resulting in the following "inclusion chain" by proving theorems like rngcresringcat 44321, 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 17402. Furthermore, it can be shown that SetCat is embedded into ExtStrCat, see embedsetcestrc 17417. Remark: equivestrcsetc 17402 as well as embedsetcestrc 17417 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 16504), 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 16547. 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 19302) 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 17370 | 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 17371 | 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 17372 | Extend class notation to include the category ExtStr. |
class ExtStrCat | ||
Definition | df-estrc 17373* | 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 17371 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 17374* | 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 17375 | Set of objects of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑈 = (Base‘𝐶)) | ||
Theorem | estrchomfval 17376* | 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 17377 | The morphisms between extensible structures are mappings between their base sets. (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ 𝐴 = (Base‘𝑋) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝐵 ↑m 𝐴)) | ||
Theorem | elestrchom 17378 | A morphism between extensible structures is a function between their base sets. (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ 𝐴 = (Base‘𝑋) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) ↔ 𝐹:𝐴⟶𝐵)) | ||
Theorem | estrccofval 17379* | 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 17380 | Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ 𝐴 = (Base‘𝑋) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐷 = (Base‘𝑍) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐷) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺 ∘ 𝐹)) | ||
Theorem | estrcbasbas 17381 | 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 17382* | Lemma for estrccat 17383. (Contributed by AV, 8-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝑈 ↦ ( I ↾ (Base‘𝑥))))) | ||
Theorem | estrccat 17383 | The category of extensible structures is a category. (Contributed by AV, 8-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) | ||
Theorem | estrcid 17384 | 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 17385 | 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 17386 | 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 17387 | Lemma 1 for estrres 17389. (Contributed by AV, 14-Mar-2020.) |
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) | ||
Theorem | estrreslem2 17388 | Lemma 2 for estrres 17389. (Contributed by AV, 14-Mar-2020.) |
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → · ∈ 𝑌) ⇒ ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐶) | ||
Theorem | estrres 17389 | 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 17390* | Lemma 1 for funcestrcsetc 17399. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (Base‘𝑋)) | ||
Theorem | funcestrcsetclem2 17391* | Lemma 2 for funcestrcsetc 17399. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝑈) | ||
Theorem | funcestrcsetclem3 17392* | Lemma 3 for funcestrcsetc 17399. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) | ||
Theorem | funcestrcsetclem4 17393* | Lemma 4 for funcestrcsetc 17399. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) ⇒ ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) | ||
Theorem | funcestrcsetclem5 17394* | Lemma 5 for funcestrcsetc 17399. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) & ⊢ 𝑀 = (Base‘𝑋) & ⊢ 𝑁 = (Base‘𝑌) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌) = ( I ↾ (𝑁 ↑m 𝑀))) | ||
Theorem | funcestrcsetclem6 17395* | Lemma 6 for funcestrcsetc 17399. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) & ⊢ 𝑀 = (Base‘𝑋) & ⊢ 𝑁 = (Base‘𝑌) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐻 ∈ (𝑁 ↑m 𝑀)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻) | ||
Theorem | funcestrcsetclem7 17396* | Lemma 7 for funcestrcsetc 17399. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → ((𝑋𝐺𝑋)‘((Id‘𝐸)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋))) | ||
Theorem | funcestrcsetclem8 17397* | Lemma 8 for funcestrcsetc 17399. (Contributed by AV, 15-Feb-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝐸)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌))) | ||
Theorem | funcestrcsetclem9 17398* | Lemma 9 for funcestrcsetc 17399. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝐻 ∈ (𝑋(Hom ‘𝐸)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝐸)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝐸)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) | ||
Theorem | funcestrcsetc 17399* | 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 17400* | 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 𝑆)𝐺) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |