Home | Metamath
Proof Explorer Theorem List (p. 167 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | estrreslem2 16601 | Lemma 2 for estrres 16602. (Contributed by AV, 14-Mar-2020.) |
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → · ∈ 𝑌) ⇒ ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐶) | ||
Theorem | estrres 16602 | 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 16603* | Lemma 1 for funcestrcsetc 16612. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (Base‘𝑋)) | ||
Theorem | funcestrcsetclem2 16604* | Lemma 2 for funcestrcsetc 16612. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝑈) | ||
Theorem | funcestrcsetclem3 16605* | Lemma 3 for funcestrcsetc 16612. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) | ||
Theorem | funcestrcsetclem4 16606* | Lemma 4 for funcestrcsetc 16612. (Contributed by AV, 22-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))) ⇒ ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) | ||
Theorem | funcestrcsetclem5 16607* | Lemma 5 for funcestrcsetc 16612. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))) & ⊢ 𝑀 = (Base‘𝑋) & ⊢ 𝑁 = (Base‘𝑌) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌) = ( I ↾ (𝑁 ↑𝑚 𝑀))) | ||
Theorem | funcestrcsetclem6 16608* | Lemma 6 for funcestrcsetc 16612. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))) & ⊢ 𝑀 = (Base‘𝑋) & ⊢ 𝑁 = (Base‘𝑌) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐻 ∈ (𝑁 ↑𝑚 𝑀)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻) | ||
Theorem | funcestrcsetclem7 16609* | Lemma 7 for funcestrcsetc 16612. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → ((𝑋𝐺𝑋)‘((Id‘𝐸)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋))) | ||
Theorem | funcestrcsetclem8 16610* | Lemma 8 for funcestrcsetc 16612. (Contributed by AV, 15-Feb-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝐸)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌))) | ||
Theorem | funcestrcsetclem9 16611* | Lemma 9 for funcestrcsetc 16612. (Contributed by AV, 23-Mar-2020.) |
⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝐻 ∈ (𝑋(Hom ‘𝐸)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝐸)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝐸)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) | ||
Theorem | funcestrcsetc 16612* | 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 16613* | 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 16614* | 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 16615* | 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 16616 | 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 16617* | Lemma 1 for funcsetcestrc 16627. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) = {〈(Base‘ndx), 𝑋〉}) | ||
Theorem | funcsetcestrclem2 16618* | Lemma 2 for funcsetcestrc 16627. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) ∈ 𝑈) | ||
Theorem | funcsetcestrclem3 16619* | Lemma 3 for funcsetcestrc 16627. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) ⇒ ⊢ (𝜑 → 𝐹:𝐶⟶𝐵) | ||
Theorem | embedsetcestrclem 16620* | Lemma for embedsetcestrc 16630. (Contributed by AV, 31-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) ⇒ ⊢ (𝜑 → 𝐹:𝐶–1-1→𝐵) | ||
Theorem | funcsetcestrclem4 16621* | Lemma 4 for funcsetcestrc 16627. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) ⇒ ⊢ (𝜑 → 𝐺 Fn (𝐶 × 𝐶)) | ||
Theorem | funcsetcestrclem5 16622* | Lemma 5 for funcsetcestrc 16627. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌) = ( I ↾ (𝑌 ↑𝑚 𝑋))) | ||
Theorem | funcsetcestrclem6 16623* | Lemma 6 for funcsetcestrc 16627. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝐻 ∈ (𝑌 ↑𝑚 𝑋)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻) | ||
Theorem | funcsetcestrclem7 16624* | Lemma 7 for funcsetcestrc 16627. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑋𝐺𝑋)‘((Id‘𝑆)‘𝑋)) = ((Id‘𝐸)‘(𝐹‘𝑋))) | ||
Theorem | funcsetcestrclem8 16625* | Lemma 8 for funcsetcestrc 16627. (Contributed by AV, 28-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑆)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝐸)(𝐹‘𝑌))) | ||
Theorem | funcsetcestrclem9 16626* | Lemma 9 for funcsetcestrc 16627. (Contributed by AV, 28-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) | ||
Theorem | funcsetcestrc 16627* | 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 16628* | 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 16629* | 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 16630* | 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→𝐵)) | ||
Syntax | cxpc 16631 | Extend class notation with the product of two categories. |
class ×c | ||
Syntax | c1stf 16632 | Extend class notation with the first projection functor. |
class 1stF | ||
Syntax | c2ndf 16633 | Extend class notation with the second projection functor. |
class 2ndF | ||
Syntax | cprf 16634 | Extend class notation with the functor pairing operation. |
class 〈,〉F | ||
Definition | df-xpc 16635* | 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 16636* | 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 16637* | 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 16638* | 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 16639 | The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ ×c Fn (V × V) | ||
Theorem | xpcval 16640* | 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 16641 | Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝑌 = (Base‘𝐷) ⇒ ⊢ (𝑋 × 𝑌) = (Base‘𝑇) | ||
Theorem | xpchomfval 16642* | 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 16643 | 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 16644 | A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ Rel (𝑋𝐾𝑌) | ||
Theorem | xpccofval 16645* | 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 16646 | 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 16647 | 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 16648 | 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 16649 | 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 16650 | 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 16651* | 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 16652 | 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 16653 | The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑇 ∈ Cat) | ||
Theorem | 1stfval 16654* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑃 = (𝐶 1stF 𝐷) ⇒ ⊢ (𝜑 → 𝑃 = 〈(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) | ||
Theorem | 1stf1 16655 | 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 16656 | 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 16657* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐶 2ndF 𝐷) ⇒ ⊢ (𝜑 → 𝑄 = 〈(2nd ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (2nd ↾ (𝑥𝐻𝑦)))〉) | ||
Theorem | 2ndf1 16658 | 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 16659 | 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 16660 | 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 16661 | 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 16662* | Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → 𝑃 = 〈(𝑥 ∈ 𝐵 ↦ 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (ℎ ∈ (𝑥𝐻𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉) | ||
Theorem | prf1 16663 | Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝑃)‘𝑋) = 〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)〉) | ||
Theorem | prf2fval 16664* | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝑃)𝑌) = (ℎ ∈ (𝑋𝐻𝑌) ↦ 〈((𝑋(2nd ‘𝐹)𝑌)‘ℎ), ((𝑋(2nd ‘𝐺)𝑌)‘ℎ)〉)) | ||
Theorem | prf2 16665 | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝑃)𝑌)‘𝐾) = 〈((𝑋(2nd ‘𝐹)𝑌)‘𝐾), ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)〉) | ||
Theorem | prfcl 16666 | The pairing of functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐷 is a functor 〈𝐹, 𝐺〉:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝑇 = (𝐷 ×c 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇)) | ||
Theorem | prf1st 16667 | Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐷 1stF 𝐸) ∘func 𝑃) = 𝐹) | ||
Theorem | prf2nd 16668 | Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺) | ||
Theorem | 1st2ndprf 16669 | 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 16670 | 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 16671 | 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 𝐷)) | ||
Syntax | cevlf 16672 | Extend class notation with the evaluation functor. |
class evalF | ||
Syntax | ccurf 16673 | Extend class notation with the currying of a functor. |
class curryF | ||
Syntax | cuncf 16674 | Extend class notation with the uncurrying of a functor. |
class uncurryF | ||
Syntax | cdiag 16675 | Extend class notation to include the diagonal functor. |
class Δfunc | ||
Definition | df-evlf 16676* | Define the evaluation functor, which is the extension of the evaluation map 𝑓, 𝑥 ↦ (𝑓‘𝑥) of functors, to a functor (𝐶⟶𝐷) × 𝐶⟶𝐷. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ evalF = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ 〈(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉) | ||
Definition | df-curf 16677* | Define the curry functor, which maps a functor 𝐹:𝐶 × 𝐷⟶𝐸 to curryF (𝐹):𝐶⟶(𝐷⟶𝐸). (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ curryF = (𝑒 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑒) / 𝑐⦌⦋(2nd ‘𝑒) / 𝑑⦌〈(𝑥 ∈ (Base‘𝑐) ↦ 〈(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧)))))〉) | ||
Definition | df-uncf 16678* | Define the uncurry functor, which can be defined equationally using evalF. Strictly speaking, the third category argument is not needed, since the resulting functor is extensionally equal regardless, but it is used in the equational definition and is too much work to remove. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) 〈,〉F ((𝑐‘0) 2ndF (𝑐‘1))))) | ||
Definition | df-diag 16679* | Define the diagonal functor, which is the functor 𝐶⟶(𝐷 Func 𝐶) whose object part is 𝑥 ∈ 𝐶 ↦ (𝑦 ∈ 𝐷 ↦ 𝑥). The value of the functor at an object 𝑥 is the constant functor which maps all objects in 𝐷 to 𝑥 and all morphisms to 1(𝑥). The morphism part is a natural transformation between these functors, which takes 𝑓:𝑥⟶𝑦 to the natural transformation with every component equal to 𝑓. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ Δfunc = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ (〈𝑐, 𝑑〉 curryF (𝑐 1stF 𝑑))) | ||
Theorem | evlfval 16680* | Value of the evaluation functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ (𝜑 → 𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))〉 · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉) | ||
Theorem | evlf2 16681* | Value of the evaluation functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐿 = (〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉) ⇒ ⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) | ||
Theorem | evlf2val 16682 | Value of the evaluation natural transformation at an object. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐿 = (〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (𝐴𝐿𝐾) = ((𝐴‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝐾))) | ||
Theorem | evlf1 16683 | Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹(1st ‘𝐸)𝑋) = ((1st ‘𝐹)‘𝑋)) | ||
Theorem | evlfcllem 16684 | Lemma for evlfcl 16685. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (Base‘𝐶))) & ⊢ (𝜑 → (𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ (Base‘𝐶))) & ⊢ (𝜑 → (𝐻 ∈ (𝐶 Func 𝐷) ∧ 𝑍 ∈ (Base‘𝐶))) & ⊢ (𝜑 → (𝐴 ∈ (𝐹𝑁𝐺) ∧ 𝐾 ∈ (𝑋(Hom ‘𝐶)𝑌))) & ⊢ (𝜑 → (𝐵 ∈ (𝐺𝑁𝐻) ∧ 𝐿 ∈ (𝑌(Hom ‘𝐶)𝑍))) ⇒ ⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐻, 𝑍〉)‘(〈𝐵, 𝐿〉(〈〈𝐹, 𝑋〉, 〈𝐺, 𝑌〉〉(comp‘(𝑄 ×c 𝐶))〈𝐻, 𝑍〉)〈𝐴, 𝐾〉)) = (((〈𝐺, 𝑌〉(2nd ‘𝐸)〈𝐻, 𝑍〉)‘〈𝐵, 𝐿〉)(〈((1st ‘𝐸)‘〈𝐹, 𝑋〉), ((1st ‘𝐸)‘〈𝐺, 𝑌〉)〉(comp‘𝐷)((1st ‘𝐸)‘〈𝐻, 𝑍〉))((〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉)‘〈𝐴, 𝐾〉))) | ||
Theorem | evlfcl 16685 | The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors 𝐶⟶𝐷, and the second parameter in 𝐷. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝐶) Func 𝐷)) | ||
Theorem | curfval 16686* | Value of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) ⇒ ⊢ (𝜑 → 𝐺 = 〈(𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))〉) | ||
Theorem | curf1fval 16687* | Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → (1st ‘𝐺) = (𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉)) | ||
Theorem | curf1 16688* | Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 𝐾 = 〈(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉) | ||
Theorem | curf11 16689 | Value of the double evaluated curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝐾)‘𝑌) = (𝑋(1st ‘𝐹)𝑌)) | ||
Theorem | curf12 16690 | The partially evaluated curry functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 ∈ (𝑌𝐽𝑍)) ⇒ ⊢ (𝜑 → ((𝑌(2nd ‘𝐾)𝑍)‘𝐻) = (( 1 ‘𝑋)(〈𝑋, 𝑌〉(2nd ‘𝐹)〈𝑋, 𝑍〉)𝐻)) | ||
Theorem | curf1cl 16691 | The partially evaluated curry functor is a functor. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸)) | ||
Theorem | curf2 16692* | Value of the curry functor at a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) ⇒ ⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) | ||
Theorem | curf2val 16693 | Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐿‘𝑍) = (𝐾(〈𝑋, 𝑍〉(2nd ‘𝐹)〈𝑌, 𝑍〉)(𝐼‘𝑍))) | ||
Theorem | curf2cl 16694 | The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) & ⊢ 𝑁 = (𝐷 Nat 𝐸) ⇒ ⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌))) | ||
Theorem | curfcl 16695 | The curry functor of a functor 𝐹:𝐶 × 𝐷⟶𝐸 is a functor curryF (𝐹):𝐶⟶(𝐷⟶𝐸). (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝑄 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝑄)) | ||
Theorem | curfpropd 16696 | If two categories have the same set of objects, morphisms, and compositions, then they curry the same functor to the same result. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ Cat) & ⊢ (𝜑 → 𝐵 ∈ Cat) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴 ×c 𝐶) Func 𝐸)) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐶〉 curryF 𝐹) = (〈𝐵, 𝐷〉 curryF 𝐹)) | ||
Theorem | uncfval 16697 | Value of the uncurry functor, which is the reverse of the curry functor, taking 𝐺:𝐶⟶(𝐷⟶𝐸) to uncurryF (𝐺):𝐶 × 𝐷⟶𝐸. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) ⇒ ⊢ (𝜑 → 𝐹 = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func (𝐶 1stF 𝐷)) 〈,〉F (𝐶 2ndF 𝐷)))) | ||
Theorem | uncfcl 16698 | The uncurry operation takes a functor 𝐹:𝐶⟶(𝐷⟶𝐸) to a functor uncurryF (𝐹):𝐶 × 𝐷⟶𝐸. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) | ||
Theorem | uncf1 16699 | Value of the uncurry functor on an object. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(1st ‘𝐹)𝑌) = ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑌)) | ||
Theorem | uncf2 16700 | Value of the uncurry functor on a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑍)) & ⊢ (𝜑 → 𝑆 ∈ (𝑌𝐽𝑊)) ⇒ ⊢ (𝜑 → (𝑅(〈𝑋, 𝑌〉(2nd ‘𝐹)〈𝑍, 𝑊〉)𝑆) = ((((𝑋(2nd ‘𝐺)𝑍)‘𝑅)‘𝑊)(〈((1st ‘((1st ‘𝐺)‘𝑋))‘𝑌), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑊)〉(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑍))‘𝑊))((𝑌(2nd ‘((1st ‘𝐺)‘𝑋))𝑊)‘𝑆))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |