HomeTheorem List (p. 184 of 491)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 184 of 491) | < 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-30946) |
Hilbert Space Explorer
(30947-32469) |
Users' Mathboxes
(32470-49035) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | diag2 18301 | Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = (𝐵 × {𝐹})) | ||
| Theorem | diag2cl 18302 | The diagonal functor at a morphism is a natural transformation between constant functors. (Contributed by Mario Carneiro, 7-Jan-2017.) |
| ⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ 𝑁 = (𝐷 Nat 𝐶) ⇒ ⊢ (𝜑 → (𝐵 × {𝐹}) ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌))) | ||
| Theorem | curf2ndf 18303 | As shown in diagval 18296, the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is 𝑥 ∈ 𝐶 ↦ (𝑦 ∈ 𝐷 ↦ 𝑦), which is a constant functor of the identity functor at 𝐷. (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑄 = (𝐷 FuncCat 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) | ||
| Syntax | chof 18304 | Extend class notation with the Hom functor. |
| class HomF | ||
| Syntax | cyon 18305 | Extend class notation with the Yoneda embedding. |
| class Yon | ||
| Definition | df-hof 18306* | Define the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat‘𝐶) × 𝐶 to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017.) |
| ⊢ HomF = (𝑐 ∈ Cat ↦ ⟨(Homf ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓))))⟩) | ||
| Definition | df-yon 18307 | Define the Yoneda embedding, which is the currying of the (opposite) Hom functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
| ⊢ Yon = (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐)))) | ||
| Theorem | hofval 18308* | Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat‘𝐶) × 𝐶 to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → 𝑀 = ⟨(Homf ‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩ · (2nd ‘𝑦))𝑓))))⟩) | ||
| Theorem | hof1fval 18309 | The object part of the Hom functor is the Homf operation, which is just a functionalized version of Hom. That is, it is a two argument function, which maps 𝑋, 𝑌 to the set of morphisms from 𝑋 to 𝑌. (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → (1st ‘𝑀) = (Homf ‘𝐶)) | ||
| Theorem | hof1 18310 | The object part of the Hom functor maps 𝑋, 𝑌 to the set of morphisms from 𝑋 to 𝑌. (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(1st ‘𝑀)𝑌) = (𝑋𝐻𝑌)) | ||
| Theorem | hof2fval 18311* | The morphism part of the Hom functor, for morphisms ⟨𝑓, 𝑔⟩:⟨𝑋, 𝑌⟩⟶⟨𝑍, 𝑊⟩ (which since the first argument is contravariant means morphisms 𝑓:𝑍⟶𝑋 and 𝑔:𝑌⟶𝑊), yields a function (a morphism of SetCat) mapping ℎ:𝑋⟶𝑌 to 𝑔 ∘ ℎ ∘ 𝑓:𝑍⟶𝑊. (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → (⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩) = (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (𝑌𝐻𝑊) ↦ (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝑔(⟨𝑋, 𝑌⟩ · 𝑊)ℎ)(⟨𝑍, 𝑋⟩ · 𝑊)𝑓)))) | ||
| Theorem | hof2val 18312* | The morphism part of the Hom functor, for morphisms ⟨𝑓, 𝑔⟩:⟨𝑋, 𝑌⟩⟶⟨𝑍, 𝑊⟩ (which since the first argument is contravariant means morphisms 𝑓:𝑍⟶𝑋 and 𝑔:𝑌⟶𝑊), yields a function (a morphism of SetCat) mapping ℎ:𝑋⟶𝑌 to 𝑔 ∘ ℎ ∘ 𝑓:𝑍⟶𝑊. (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑊)) ⇒ ⊢ (𝜑 → (𝐹(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩)𝐺) = (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝐺(⟨𝑋, 𝑌⟩ · 𝑊)ℎ)(⟨𝑍, 𝑋⟩ · 𝑊)𝐹))) | ||
| Theorem | hof2 18313 | The morphism part of the Hom functor, for morphisms ⟨𝑓, 𝑔⟩:⟨𝑋, 𝑌⟩⟶⟨𝑍, 𝑊⟩ (which since the first argument is contravariant means morphisms 𝑓:𝑍⟶𝑋 and 𝑔:𝑌⟶𝑊), yields a function (a morphism of SetCat) mapping ℎ:𝑋⟶𝑌 to 𝑔 ∘ ℎ ∘ 𝑓:𝑍⟶𝑊. (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑊)) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝐹(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩)𝐺)‘𝐾) = ((𝐺(⟨𝑋, 𝑌⟩ · 𝑊)𝐾)(⟨𝑍, 𝑋⟩ · 𝑊)𝐹)) | ||
| Theorem | hofcllem 18314 | Lemma for hofcl 18315. (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑀 = (HomF‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑊)) & ⊢ (𝜑 → 𝑃 ∈ (𝑆𝐻𝑍)) & ⊢ (𝜑 → 𝑄 ∈ (𝑊𝐻𝑇)) ⇒ ⊢ (𝜑 → ((𝐾(⟨𝑆, 𝑍⟩(comp‘𝐶)𝑋)𝑃)(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑆, 𝑇⟩)(𝑄(⟨𝑌, 𝑊⟩(comp‘𝐶)𝑇)𝐿)) = ((𝑃(⟨𝑍, 𝑊⟩(2nd ‘𝑀)⟨𝑆, 𝑇⟩)𝑄)(⟨(𝑋𝐻𝑌), (𝑍𝐻𝑊)⟩(comp‘𝐷)(𝑆𝐻𝑇))(𝐾(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩)𝐿))) | ||
| Theorem | hofcl 18315 | Closure of the Hom functor. Note that the codomain is the category SetCat‘𝑈 for any universe 𝑈 which contains each Hom-set. This corresponds to the assertion that 𝐶 be locally small (with respect to 𝑈). (Contributed by Mario Carneiro, 15-Jan-2017.) |
| ⊢ 𝑀 = (HomF‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝑂 ×c 𝐶) Func 𝐷)) | ||
| Theorem | oppchofcl 18316 | Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝐶 ×c 𝑂) Func 𝐷)) | ||
| Theorem | yonval 18317 | Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) ⇒ ⊢ (𝜑 → 𝑌 = (⟨𝐶, 𝑂⟩ curryF 𝑀)) | ||
| Theorem | yoncl 18318 | The Yoneda embedding is a functor from the category to the category 𝑄 of presheaves on 𝐶. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄)) | ||
| Theorem | yon1cl 18319 | The Yoneda embedding at an object of 𝐶 is a presheaf on 𝐶, also known as the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → ((1st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) | ||
| Theorem | yon11 18320 | Value of the Yoneda embedding at an object. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘((1st ‘𝑌)‘𝑋))‘𝑍) = (𝑍𝐻𝑋)) | ||
| Theorem | yon12 18321 | Value of the Yoneda embedding at a morphism. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑊𝐻𝑍)) & ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑋)) ⇒ ⊢ (𝜑 → (((𝑍(2nd ‘((1st ‘𝑌)‘𝑋))𝑊)‘𝐹)‘𝐺) = (𝐺(⟨𝑊, 𝑍⟩ · 𝑋)𝐹)) | ||
| Theorem | yon2 18322 | Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑍)) & ⊢ (𝜑 → 𝐺 ∈ (𝑊𝐻𝑋)) ⇒ ⊢ (𝜑 → ((((𝑋(2nd ‘𝑌)𝑍)‘𝐹)‘𝑊)‘𝐺) = (𝐹(⟨𝑊, 𝑋⟩ · 𝑍)𝐺)) | ||
| Theorem | hofpropd 18323 | If two categories have the same set of objects, morphisms, and compositions, then they have the same Hom functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (HomF‘𝐶) = (HomF‘𝐷)) | ||
| Theorem | yonpropd 18324 | If two categories have the same set of objects, morphisms, and compositions, then they have the same Yoneda functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (Yon‘𝐶) = (Yon‘𝐷)) | ||
| Theorem | oppcyon 18325 | Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑌 = (Yon‘𝑂) & ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑌 = (⟨𝑂, 𝐶⟩ curryF 𝑀)) | ||
| Theorem | oyoncl 18326 | The opposite Yoneda embedding is a functor from oppCat‘𝐶 to the functor category 𝐶 → SetCat. (Contributed by Mario Carneiro, 26-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑌 = (Yon‘𝑂) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ 𝑄 = (𝐶 FuncCat 𝑆) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝑂 Func 𝑄)) | ||
| Theorem | oyon1cl 18327 | The opposite Yoneda embedding at an object of 𝐶 is a functor from 𝐶 to Set, also known as the covariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑌 = (Yon‘𝑂) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝑌)‘𝑋) ∈ (𝐶 Func 𝑆)) | ||
| Theorem | yonedalem1 18328 | Lemma for yoneda 18339. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))) | ||
| Theorem | yonedalem21 18329 | Lemma for yoneda 18339. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹(1st ‘𝑍)𝑋) = (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) | ||
| Theorem | yonedalem3a 18330* | Lemma for yoneda 18339. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) ⇒ ⊢ (𝜑 → ((𝐹𝑀𝑋) = (𝑎 ∈ (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) ∧ (𝐹𝑀𝑋):(𝐹(1st ‘𝑍)𝑋)⟶(𝐹(1st ‘𝐸)𝑋))) | ||
| Theorem | yonedalem4a 18331* | Lemma for yoneda 18339. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))))) & ⊢ (𝜑 → 𝐴 ∈ ((1st ‘𝐹)‘𝑋)) ⇒ ⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑦)‘𝑔)‘𝐴)))) | ||
| Theorem | yonedalem4b 18332* | Lemma for yoneda 18339. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))))) & ⊢ (𝜑 → 𝐴 ∈ ((1st ‘𝐹)‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ (𝑃(Hom ‘𝐶)𝑋)) ⇒ ⊢ (𝜑 → ((((𝐹𝑁𝑋)‘𝐴)‘𝑃)‘𝐺) = (((𝑋(2nd ‘𝐹)𝑃)‘𝐺)‘𝐴)) | ||
| Theorem | yonedalem4c 18333* | Lemma for yoneda 18339. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))))) & ⊢ (𝜑 → 𝐴 ∈ ((1st ‘𝐹)‘𝑋)) ⇒ ⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) ∈ (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) | ||
| Theorem | yonedalem22 18334 | Lemma for yoneda 18339. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) ⇒ ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2nd ‘𝑌)𝑋)‘𝐾)(⟨((1st ‘𝑌)‘𝑋), 𝐹⟩(2nd ‘𝐻)⟨((1st ‘𝑌)‘𝑃), 𝐺⟩)𝐴)) | ||
| Theorem | yonedalem3b 18335* | Lemma for yoneda 18339. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) & ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) ⇒ ⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1st ‘𝑍)𝑋), (𝐺(1st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1st ‘𝑍)𝑋), (𝐹(1st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1st ‘𝐸)𝑃))(𝐹𝑀𝑋))) | ||
| Theorem | yonedalem3 18336* | Lemma for yoneda 18339. (Contributed by Mario Carneiro, 28-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸)) | ||
| Theorem | yonedainv 18337* | The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) & ⊢ 𝐼 = (Inv‘𝑅) & ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))))) ⇒ ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁) | ||
| Theorem | yonffthlem 18338* | Lemma for yonffth 18340. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) & ⊢ 𝐼 = (Inv‘𝑅) & ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))))) ⇒ ⊢ (𝜑 → 𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))) | ||
| Theorem | yoneda 18339* | The Yoneda Lemma. There is a natural isomorphism between the functors 𝑍 and 𝐸, where 𝑍(𝐹, 𝑋) is the natural transformations from Yon(𝑋) = Hom ( − , 𝑋) to 𝐹, and 𝐸(𝐹, 𝑋) = 𝐹(𝑋) is the evaluation functor. Here we need two universes to state the claim: the smaller universe 𝑈 is used for forming the functor category 𝑄 = 𝐶 op → SetCat(𝑈), which itself does not (necessarily) live in 𝑈 but instead is an element of the larger universe 𝑉. (If 𝑈 is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set 𝑈 = 𝑉 in this case.) (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑇 = (SetCat‘𝑉) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐻 = (HomF‘𝑄) & ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) & ⊢ 𝐸 = (𝑂 evalF 𝑆) & ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) & ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) & ⊢ 𝐼 = (Iso‘𝑅) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐼𝐸)) | ||
| Theorem | yonffth 18340 | The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category 𝐶 as a full subcategory of the category 𝑄 of presheaves on 𝐶. (Contributed by Mario Carneiro, 29-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))) | ||
| Theorem | yoniso 18341* | If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from 𝐶 into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017.) |
| ⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐷 = (CatCat‘𝑉) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐼 = (Iso‘𝐷) & ⊢ 𝑄 = (𝑂 FuncCat 𝑆) & ⊢ 𝐸 = (𝑄 ↾s ran (1st ‘𝑌)) & ⊢ (𝜑 → 𝑉 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝐹‘(𝑥(Hom ‘𝐶)𝑦)) = 𝑦) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝐶𝐼𝐸)) | ||
| Syntax | codu 18342 | Class function defining dual orders. |
| class ODual | ||
| Definition | df-odu 18343 |
Define the dual of an ordered structure, which replaces the order
component of the structure with its reverse. See odubas 18347, oduleval 18345,
and oduleg 18346 for its principal properties.
EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 18552. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩)) | ||
| Theorem | oduval 18344 | Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ 𝐷 = (𝑂 sSet ⟨(le‘ndx), ◡ ≤ ⟩) | ||
| Theorem | oduleval 18345 | Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ ◡ ≤ = (le‘𝐷) | ||
| Theorem | oduleg 18346 | Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) & ⊢ 𝐺 = (le‘𝐷) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝐺𝐵 ↔ 𝐵 ≤ 𝐴)) | ||
| Theorem | odubas 18347 | Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Proof shortened by AV, 12-Nov-2024.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ 𝐵 = (Base‘𝑂) ⇒ ⊢ 𝐵 = (Base‘𝐷) | ||
| Theorem | odubasOLD 18348 | Obsolete version of odubas 18347 as of 12-Nov-2024. Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ODual‘𝑂) & ⊢ 𝐵 = (Base‘𝑂) ⇒ ⊢ 𝐵 = (Base‘𝐷) | ||
| Syntax | cproset 18349 | Extend class notation with the class of all prosets. |
| class Proset | ||
| Syntax | cdrs 18350 | Extend class notation with the class of all directed sets. |
| class Dirset | ||
| Definition | df-proset 18351* |
Define the class of preordered sets, or prosets. A proset is a set
equipped with a preorder, that is, a transitive and reflexive relation.
Preorders are a natural generalization of partial orders which need not be antisymmetric: there may be pairs of elements such that each is "less than or equal to" the other, so that both elements have the same order-theoretic properties (in some sense, there is a "tie" among them). If a preorder is required to be antisymmetric, that is, there is no such "tie", then one obtains a partial order. If a preorder is required to be symmetric, that is, all comparable elements are tied, then one obtains an equivalence relation. Every preorder naturally factors into these two notions: the "tie" relation on a proset is an equivalence relation, and the quotient under that equivalence relation is a partial order. (Contributed by FL, 17-Nov-2014.) (Revised by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ Proset = {𝑓 ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))} | ||
| Definition | df-drs 18352* |
Define the class of directed sets. A directed set is a nonempty
preordered set where every pair of elements have some upper bound. Note
that it is not required that there exist a least upper bound.
There is no consensus in the literature over whether directed sets are allowed to be empty. It is slightly more convenient for us if they are not. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ Dirset = {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))} | ||
| Theorem | isprs 18353* | Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Proset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
| Theorem | prslem 18354 | Lemma for prsref 18355 and prstr 18356. (Contributed by Mario Carneiro, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
| Theorem | prsref 18355 | "Less than or equal to" is reflexive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) | ||
| Theorem | prstr 18356 | "Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ≤ 𝑍) | ||
| Theorem | oduprs 18357 | Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ Proset → 𝐷 ∈ Proset ) | ||
| Theorem | isdrs 18358* | Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) | ||
| Theorem | drsdir 18359* | Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑧 ∈ 𝐵 (𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧)) | ||
| Theorem | drsprs 18360 | A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Proset ) | ||
| Theorem | drsbn0 18361 | The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset → 𝐵 ≠ ∅) | ||
| Theorem | drsdirfi 18362* | Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 18352 first comes into play; without it we would need an additional constraint that 𝑋 not be empty. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ⊆ 𝐵 ∧ 𝑋 ∈ Fin) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑦) | ||
| Theorem | isdrs2 18363* | Directed sets may be defined in terms of finite subsets. Again, without nonemptiness we would need to restrict to nonempty subsets here. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ ∀𝑥 ∈ (𝒫 𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦)) | ||
| Syntax | cpo 18364 | Extend class notation with the class of posets. |
| class Poset | ||
| Syntax | cplt 18365 | Extend class notation with less-than for posets. |
| class lt | ||
| Syntax | club 18366 | Extend class notation with poset least upper bound. |
| class lub | ||
| Syntax | cglb 18367 | Extend class notation with poset greatest lower bound. |
| class glb | ||
| Syntax | cjn 18368 | Extend class notation with poset join. |
| class join | ||
| Syntax | cmee 18369 | Extend class notation with poset meet. |
| class meet | ||
| Definition | df-poset 18370* |
Define the class of partially ordered sets (posets). A poset is a set
equipped with a partial order, that is, a binary relation which is
reflexive, antisymmetric, and transitive. Unlike a total order, in a
partial order there may be pairs of elements where neither precedes the
other. Definition of poset in [Crawley] p. 1. Note that
Crawley-Dilworth require that a poset base set be nonempty, but we
follow the convention of most authors who don't make this a requirement.
In our formalism of extensible structures, the base set of a poset 𝑓 is denoted by (Base‘𝑓) and its partial order by (le‘𝑓) (for "less than or equal to"). The quantifiers ∃𝑏∃𝑟 provide a notational shorthand to allow to refer to the base and ordering relation as 𝑏 and 𝑟 in the definition rather than having to repeat (Base‘𝑓) and (le‘𝑓) throughout. These quantifiers can be eliminated with ceqsex2v 3535 and related theorems. (Contributed by NM, 18-Oct-2012.) |
| ⊢ Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))} | ||
| Theorem | ispos 18371* | The predicate "is a poset". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
| Theorem | ispos2 18372* |
A poset is an antisymmetric proset.
EDITORIAL: could become the definition of poset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ Proset ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))) | ||
| Theorem | posprs 18373 | A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset ) | ||
| Theorem | posi 18374 | Lemma for poset properties. (Contributed by NM, 11-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
| Theorem | posref 18375 | A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) | ||
| Theorem | posasymb 18376 | A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
| Theorem | postr 18377 | A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) | ||
| Theorem | 0pos 18378 | Technical lemma to simplify the statement of ipopos 18593. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 17222) and any relation partially orders an empty set. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Proof shortened by AV, 13-Oct-2024.) |
| ⊢ ∅ ∈ Poset | ||
| Theorem | 0posOLD 18379 | Obsolete version of 0pos 18378 as of 13-Oct-2024. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ∅ ∈ Poset | ||
| Theorem | isposd 18380* | Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by AV, 26-Apr-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → ≤ = (le‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ (𝜑 → 𝐾 ∈ Poset) | ||
| Theorem | isposi 18381* | Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.) |
| ⊢ 𝐾 ∈ V & ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ 𝐾 ∈ Poset | ||
| Theorem | isposix 18382* | Properties that determine a poset (explicit structure version). Note that the numeric indices of the structure components are not mentioned explicitly in either the theorem or its proof. (Contributed by NM, 9-Nov-2012.) (Proof shortened by AV, 30-Oct-2024.) |
| ⊢ 𝐵 ∈ V & ⊢ ≤ ∈ V & ⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ≤ ⟩} & ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ 𝐾 ∈ Poset | ||
| Theorem | isposixOLD 18383* | Obsolete version of isposix 18382 as of 30-Oct-2024. Properties that determine a poset (explicit structure version). Note that the numeric indices of the structure components are not mentioned explicitly in either the theorem or its proof (Remark: That is not true - it becomes true with the new proof!). (Contributed by NM, 9-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ V & ⊢ ≤ ∈ V & ⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ≤ ⟩} & ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ 𝐾 ∈ Poset | ||
| Theorem | pospropd 18384* | Posethood is determined only by structure components and only by the value of the relation within the base set. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝐿 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(le‘𝐾)𝑦 ↔ 𝑥(le‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐿 ∈ Poset)) | ||
| Theorem | odupos 18385 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ Poset → 𝐷 ∈ Poset) | ||
| Theorem | oduposb 18386 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ Poset ↔ 𝐷 ∈ Poset)) | ||
| Definition | df-plt 18387 | Define less-than ordering for posets and related structures. Unlike df-base 17245 and df-ple 17317, this is a derived component extractor and not an extensible structure component extractor that defines the poset. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.) |
| ⊢ lt = (𝑝 ∈ V ↦ ((le‘𝑝) ∖ I )) | ||
| Theorem | pltfval 18388 | Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I )) | ||
| Theorem | pltval 18389 | Less-than relation. (df-pss 3982 analog.) (Contributed by NM, 12-Oct-2011.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) | ||
| Theorem | pltle 18390 | "Less than" implies "less than or equal to". (pssss 4107 analog.) (Contributed by NM, 4-Dec-2011.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌)) | ||
| Theorem | pltne 18391 | The "less than" relation is not reflexive. (df-pss 3982 analog.) (Contributed by NM, 2-Dec-2011.) |
| ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌)) | ||
| Theorem | pltirr 18392 | The "less than" relation is not reflexive. (pssirr 4112 analog.) (Contributed by NM, 7-Feb-2012.) |
| ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋 < 𝑋) | ||
| Theorem | pleval2i 18393 | One direction of pleval2 18394. (Contributed by Mario Carneiro, 8-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌))) | ||
| Theorem | pleval2 18394 | "Less than or equal to" in terms of "less than". (sspss 4111 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 < 𝑌 ∨ 𝑋 = 𝑌))) | ||
| Theorem | pltnle 18395 | "Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋) | ||
| Theorem | pltval3 18396 | Alternate expression for the "less than" relation. (dfpss3 4098 analog.) (Contributed by NM, 4-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋))) | ||
| Theorem | pltnlt 18397 | The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 < 𝑋) | ||
| Theorem | pltn2lp 18398 | The less-than relation has no 2-cycle loops. (pssn2lp 4113 analog.) (Contributed by NM, 2-Dec-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ¬ (𝑋 < 𝑌 ∧ 𝑌 < 𝑋)) | ||
| Theorem | plttr 18399 | The less-than relation is transitive. (psstr 4116 analog.) (Contributed by NM, 2-Dec-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍)) | ||
| Theorem | pltletr 18400 | Transitive law for chained "less than" and "less than or equal to". (psssstr 4118 analog.) (Contributed by NM, 2-Dec-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |