Home | Metamath
Proof Explorer Theorem List (p. 176 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 | ||
Definition | df-yon 17501 | 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 17502* | 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 17503 | 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 17504 | 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 17505* | 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 17506* | 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 17507 | 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 17508 | Lemma for hofcl 17509. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑊)) & ⊢ (𝜑 → 𝑃 ∈ (𝑆𝐻𝑍)) & ⊢ (𝜑 → 𝑄 ∈ (𝑊𝐻𝑇)) ⇒ ⊢ (𝜑 → ((𝐾(〈𝑆, 𝑍〉(comp‘𝐶)𝑋)𝑃)(〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑆, 𝑇〉)(𝑄(〈𝑌, 𝑊〉(comp‘𝐶)𝑇)𝐿)) = ((𝑃(〈𝑍, 𝑊〉(2nd ‘𝑀)〈𝑆, 𝑇〉)𝑄)(〈(𝑋𝐻𝑌), (𝑍𝐻𝑊)〉(comp‘𝐷)(𝑆𝐻𝑇))(𝐾(〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑍, 𝑊〉)𝐿))) | ||
Theorem | hofcl 17509 | 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 17510 | Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝐶 ×c 𝑂) Func 𝐷)) | ||
Theorem | yonval 17511 | Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ 𝑌 = (Yon‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) ⇒ ⊢ (𝜑 → 𝑌 = (〈𝐶, 𝑂〉 curryF 𝑀)) | ||
Theorem | yoncl 17512 | 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 17513 | 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 17514 | 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 17515 | 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 17516 | Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ 𝑌 = (Yon‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑍)) & ⊢ (𝜑 → 𝐺 ∈ (𝑊𝐻𝑋)) ⇒ ⊢ (𝜑 → ((((𝑋(2nd ‘𝑌)𝑍)‘𝐹)‘𝑊)‘𝐺) = (𝐹(〈𝑊, 𝑋〉 · 𝑍)𝐺)) | ||
Theorem | hofpropd 17517 | 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 17518 | 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 17519 | Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑌 = (Yon‘𝑂) & ⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑌 = (〈𝑂, 𝐶〉 curryF 𝑀)) | ||
Theorem | oyoncl 17520 | 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 17521 | 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 17522 | Lemma for yoneda 17533. (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 17523 | Lemma for yoneda 17533. (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 17524* | Lemma for yoneda 17533. (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 17525* | Lemma for yoneda 17533. (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 17526* | Lemma for yoneda 17533. (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 17527* | Lemma for yoneda 17533. (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 17528 | Lemma for yoneda 17533. (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 17529* | Lemma for yoneda 17533. (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 17530* | Lemma for yoneda 17533. (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 17531* | 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 17532* | Lemma for yonffth 17534. (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 17533* | 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 17534 | 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 17535* | 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 | cproset 17536 | Extend class notation with the class of all prosets. |
class Proset | ||
Syntax | cdrs 17537 | Extend class notation with the class of all directed sets. |
class Dirset | ||
Definition | df-proset 17538* |
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 17539* |
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 17540* | Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Proset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
Theorem | prslem 17541 | Lemma for prsref 17542 and prstr 17543. (Contributed by Mario Carneiro, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
Theorem | prsref 17542 | "Less than or equal to" is reflexive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) | ||
Theorem | prstr 17543 | "Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ≤ 𝑍) | ||
Theorem | isdrs 17544* | Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) | ||
Theorem | drsdir 17545* | Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑧 ∈ 𝐵 (𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧)) | ||
Theorem | drsprs 17546 | A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Proset ) | ||
Theorem | drsbn0 17547 | The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset → 𝐵 ≠ ∅) | ||
Theorem | drsdirfi 17548* | Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 17539 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 17549* | 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 17550 | Extend class notation with the class of posets. |
class Poset | ||
Syntax | cplt 17551 | Extend class notation with less-than for posets. |
class lt | ||
Syntax | club 17552 | Extend class notation with poset least upper bound. |
class lub | ||
Syntax | cglb 17553 | Extend class notation with poset greatest lower bound. |
class glb | ||
Syntax | cjn 17554 | Extend class notation with poset join. |
class join | ||
Syntax | cmee 17555 | Extend class notation with poset meet. |
class meet | ||
Definition | df-poset 17556* |
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 us 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 3544 and related theorems. (Contributed by NM, 18-Oct-2012.) |
⊢ Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))} | ||
Theorem | ispos 17557* | The predicate "is a poset." (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
Theorem | ispos2 17558* |
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 17559 | A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset ) | ||
Theorem | posi 17560 | Lemma for poset properties. (Contributed by NM, 11-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
Theorem | posref 17561 | A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) | ||
Theorem | posasymb 17562 | A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
Theorem | postr 17563 | A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) | ||
Theorem | 0pos 17564 | Technical lemma to simplify the statement of ipopos 17770. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 16535) and any relation partially orders an empty set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ ∅ ∈ Poset | ||
Theorem | isposd 17565* | Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014.) |
⊢ (𝜑 → 𝐾 ∈ V) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → ≤ = (le‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ (𝜑 → 𝐾 ∈ Poset) | ||
Theorem | isposi 17566* | Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.) |
⊢ 𝐾 ∈ V & ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ 𝐾 ∈ Poset | ||
Theorem | isposix 17567* | 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.) |
⊢ 𝐵 ∈ V & ⊢ ≤ ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(le‘ndx), ≤ 〉} & ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ 𝐾 ∈ Poset | ||
Definition | df-plt 17568 | Define less-than ordering for posets and related structures. Unlike df-base 16489 and df-ple 16585, 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 17569 | Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I )) | ||
Theorem | pltval 17570 | Less-than relation. (df-pss 3954 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) | ||
Theorem | pltle 17571 | "Less than" implies "less than or equal to". (pssss 4072 analog.) (Contributed by NM, 4-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌)) | ||
Theorem | pltne 17572 | The "less than" relation is not reflexive. (df-pss 3954 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌)) | ||
Theorem | pltirr 17573 | The "less than" relation is not reflexive. (pssirr 4077 analog.) (Contributed by NM, 7-Feb-2012.) |
⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋 < 𝑋) | ||
Theorem | pleval2i 17574 | One direction of pleval2 17575. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌))) | ||
Theorem | pleval2 17575 | "Less than or equal to" in terms of "less than". (sspss 4076 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 < 𝑌 ∨ 𝑋 = 𝑌))) | ||
Theorem | pltnle 17576 | "Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋) | ||
Theorem | pltval3 17577 | Alternate expression for the "less than" relation. (dfpss3 4063 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋))) | ||
Theorem | pltnlt 17578 | The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 < 𝑋) | ||
Theorem | pltn2lp 17579 | The less-than relation has no 2-cycle loops. (pssn2lp 4078 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ¬ (𝑋 < 𝑌 ∧ 𝑌 < 𝑋)) | ||
Theorem | plttr 17580 | The less-than relation is transitive. (psstr 4081 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍)) | ||
Theorem | pltletr 17581 | Transitive law for chained "less than" and "less than or equal to". (psssstr 4083 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍)) | ||
Theorem | plelttr 17582 | Transitive law for chained "less than or equal to" and "less than". (sspsstr 4082 analog.) (Contributed by NM, 2-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍)) | ||
Theorem | pospo 17583 | Write a poset structure in terms of the proper-class poset predicate (strict less than version). (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ Poset ↔ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ ))) | ||
Definition | df-lub 17584* | Define the least upper bound (LUB) of a set of (poset) elements. The domain is restricted to exclude sets 𝑠 for which the LUB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.) |
⊢ lub = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))})) | ||
Definition | df-glb 17585* | Define the greatest lower bound (GLB) of a set of (poset) elements. The domain is restricted to exclude sets 𝑠 for which the GLB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.) |
⊢ glb = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑧(le‘𝑝)𝑦 → 𝑧(le‘𝑝)𝑥)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑧(le‘𝑝)𝑦 → 𝑧(le‘𝑝)𝑥))})) | ||
Definition | df-join 17586* | Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by Mario Carneiro, 3-Nov-2015.) |
⊢ join = (𝑝 ∈ V ↦ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧}) | ||
Definition | df-meet 17587* | Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.) |
⊢ meet = (𝑝 ∈ V ↦ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧}) | ||
Theorem | lubfval 17588* | Value of the least upper bound function of a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧))) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑈 = ((𝑠 ∈ 𝒫 𝐵 ↦ (℩𝑥 ∈ 𝐵 𝜓)) ↾ {𝑠 ∣ ∃!𝑥 ∈ 𝐵 𝜓})) | ||
Theorem | lubdm 17589* | Domain of the least upper bound function of a poset. (Contributed by NM, 6-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧))) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝑈 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓}) | ||
Theorem | lubfun 17590 | The LUB is a function. (Contributed by NM, 9-Sep-2018.) |
⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ Fun 𝑈 | ||
Theorem | lubeldm 17591* | Member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧))) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ (𝑆 ⊆ 𝐵 ∧ ∃!𝑥 ∈ 𝐵 𝜓))) | ||
Theorem | lubelss 17592 | A member of the domain of the least upper bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ dom 𝑈) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝐵) | ||
Theorem | lubeu 17593* | Unique existence proper of a member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧))) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ dom 𝑈) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 𝜓) | ||
Theorem | lubval 17594* | Value of the least upper bound function of a poset. Out-of-domain arguments (those not satisfying 𝑆 ∈ dom 𝑈) are allowed for convenience, evaluating to the empty set. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧))) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = (℩𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | lubcl 17595 | The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ dom 𝑈) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) ∈ 𝐵) | ||
Theorem | lubprop 17596* | Properties of greatest lower bound of a poset. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ dom 𝑈) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ 𝑆 𝑦 ≤ (𝑈‘𝑆) ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → (𝑈‘𝑆) ≤ 𝑧))) | ||
Theorem | luble 17597 | The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ dom 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑋 ≤ (𝑈‘𝑆)) | ||
Theorem | lublecllem 17598* | Lemma for lublecl 17599 and lubid 17600. (Contributed by NM, 8-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑥 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤)) ↔ 𝑥 = 𝑋)) | ||
Theorem | lublecl 17599* | The set of all elements less than a given element has an LUB. (Contributed by NM, 8-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋} ∈ dom 𝑈) | ||
Theorem | lubid 17600* | The LUB of elements less than or equal to a fixed value equals that value. (Contributed by NM, 19-Oct-2011.) (Revised by NM, 7-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑈‘{𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}) = 𝑋) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |