P. 184 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18301-18400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	diagcl 18301	The diagonal functor is a functor from the base category to the functor category. Another way of saying this is that the constant functor (𝑦 ∈ 𝐷 ↦ 𝑋) is a construction that is natural in 𝑋 (and covariant). (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝑄 = (𝐷 FuncCat 𝐶)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐶 Func 𝑄))
Theorem	diag1cl 18302	The constant functor of 𝑋 is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐶))
Theorem	diag11 18303	Value of the constant functor at an object. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((1st ‘𝐾)‘𝑌) = 𝑋)
Theorem	diag12 18304	Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑌𝐽𝑍))    ⇒   ⊢ (𝜑 → ((𝑌(2nd ‘𝐾)𝑍)‘𝐹) = ( 1 ‘𝑋))
Theorem	diag2 18305	Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝐷 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = (𝐵 × {𝐹}))
Theorem	diag2cl 18306	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 18307	As shown in diagval 18300, 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‘𝐷)))
8.4.3  Hom functor
Syntax	chof 18308	Extend class notation with the Hom functor.
class HomF
Syntax	cyon 18309	Extend class notation with the Yoneda embedding.
class Yon
Definition	df-hof 18310*	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 18311	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 18312*	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 18313	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 18314	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 18315*	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 18316*	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 18317	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 18318	Lemma for hofcl 18319. (Contributed by Mario Carneiro, 15-Jan-2017.)
⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐷 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑊))    &   ⊢ (𝜑 → 𝑃 ∈ (𝑆𝐻𝑍))    &   ⊢ (𝜑 → 𝑄 ∈ (𝑊𝐻𝑇))    ⇒   ⊢ (𝜑 → ((𝐾(⟨𝑆, 𝑍⟩(comp‘𝐶)𝑋)𝑃)(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑆, 𝑇⟩)(𝑄(⟨𝑌, 𝑊⟩(comp‘𝐶)𝑇)𝐿)) = ((𝑃(⟨𝑍, 𝑊⟩(2nd ‘𝑀)⟨𝑆, 𝑇⟩)𝑄)(⟨(𝑋𝐻𝑌), (𝑍𝐻𝑊)⟩(comp‘𝐷)(𝑆𝐻𝑇))(𝐾(⟨𝑋, 𝑌⟩(2nd ‘𝑀)⟨𝑍, 𝑊⟩)𝐿)))
Theorem	hofcl 18319	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 18320	Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑀 = (HomF‘𝑂)    &   ⊢ 𝐷 = (SetCat‘𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑀 ∈ ((𝐶 ×c 𝑂) Func 𝐷))
Theorem	yonval 18321	Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑀 = (HomF‘𝑂)    ⇒   ⊢ (𝜑 → 𝑌 = (⟨𝐶, 𝑂⟩ curryF 𝑀))
Theorem	yoncl 18322	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 18323	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 18324	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 18325	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 18326	Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑍))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑊𝐻𝑋))    ⇒   ⊢ (𝜑 → ((((𝑋(2nd ‘𝑌)𝑍)‘𝐹)‘𝑊)‘𝐺) = (𝐹(⟨𝑊, 𝑋⟩ · 𝑍)𝐺))
Theorem	hofpropd 18327	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 18328	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 18329	Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑌 = (Yon‘𝑂)    &   ⊢ 𝑀 = (HomF‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑌 = (⟨𝑂, 𝐶⟩ curryF 𝑀))
Theorem	oyoncl 18330	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 18331	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 18332	Lemma for yoneda 18343. (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 18333	Lemma for yoneda 18343. (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 18334*	Lemma for yoneda 18343. (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 18335*	Lemma for yoneda 18343. (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 18336*	Lemma for yoneda 18343. (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 18337*	Lemma for yoneda 18343. (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 18338	Lemma for yoneda 18343. (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 18339*	Lemma for yoneda 18343. (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 18340*	Lemma for yoneda 18343. (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 18341*	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 18342*	Lemma for yonffth 18344. (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 18343*	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 18344	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 18345*	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 ‘𝐶)𝑦)) = 𝑦)    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝐶𝐼𝐸))
PART 9  BASIC ORDER THEORY
9.1  Dual of an order structure
Syntax	codu 18346	Class function defining dual orders.
class ODual
Definition	df-odu 18347	Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas 18351, oduleval 18349, and oduleg 18350 for its principal properties. EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 18555. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩))
Theorem	oduval 18348	Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ≤ = (le‘𝑂)    ⇒   ⊢ 𝐷 = (𝑂 sSet ⟨(le‘ndx), ◡ ≤ ⟩)
Theorem	oduleval 18349	Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ≤ = (le‘𝑂)    ⇒   ⊢ ◡ ≤ = (le‘𝐷)
Theorem	oduleg 18350	Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ≤ = (le‘𝑂)    &   ⊢ 𝐺 = (le‘𝐷)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝐺𝐵 ↔ 𝐵 ≤ 𝐴))
Theorem	odubas 18351	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‘𝐷)
9.2  Preordered sets and directed sets
Syntax	cproset 18352	Extend class notation with the class of all prosets.
class Proset
Syntax	cdrs 18353	Extend class notation with the class of all directed sets.
class Dirset
Definition	df-proset 18354*	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 18355*	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 18356*	Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Proset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	prslem 18357	Lemma for prsref 18358 and prstr 18359. (Contributed by Mario Carneiro, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	prsref 18358	"Less than or equal to" is reflexive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
Theorem	prstr 18359	"Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ≤ 𝑍)
Theorem	oduprs 18360	Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐷 = (ODual‘𝐾)    ⇒   ⊢ (𝐾 ∈ Proset → 𝐷 ∈ Proset )
Theorem	isdrs 18361*	Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧)))
Theorem	drsdir 18362*	Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑧 ∈ 𝐵 (𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧))
Theorem	drsprs 18363	A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Proset )
Theorem	drsbn0 18364	The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ (𝐾 ∈ Dirset → 𝐵 ≠ ∅)
Theorem	drsdirfi 18365*	Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 18355 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 18366*	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)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦))
9.3  Partially ordered sets (posets)
Syntax	cpo 18367	Extend class notation with the class of posets.
class Poset
Syntax	cplt 18368	Extend class notation with less-than for posets.
class lt
Syntax	club 18369	Extend class notation with poset least upper bound.
class lub
Syntax	cglb 18370	Extend class notation with poset greatest lower bound.
class glb
Syntax	cjn 18371	Extend class notation with poset join.
class join
Syntax	cmee 18372	Extend class notation with poset meet.
class meet
Definition	df-poset 18373*	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 3505 and related theorems. (Contributed by NM, 18-Oct-2012.)
⊢ Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))}
Theorem	ispos 18374*	The predicate "is a poset". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	ispos2 18375*	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 18376	A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset )
Theorem	posi 18377	Lemma for poset properties. (Contributed by NM, 11-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	posref 18378	A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
Theorem	posasymb 18379	A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))
Theorem	postr 18380	A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
Theorem	0pos 18381	Technical lemma to simplify the statement of ipopos 18596. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 17253) 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	isposd 18382*	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 18383*	Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.)
⊢ 𝐾 ∈ V    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))    ⇒   ⊢ 𝐾 ∈ Poset
Theorem	isposix 18384*	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	pospropd 18385*	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 18386	Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ Poset → 𝐷 ∈ Poset)
Theorem	oduposb 18387	Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ Poset ↔ 𝐷 ∈ Poset))
Definition	df-plt 18388	Define less-than ordering for posets and related structures. Unlike df-base 17274 and df-ple 17334, 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 18389	Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I ))
Theorem	pltval 18390	Less-than relation. (df-pss 3924 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌)))
Theorem	pltle 18391	"Less than" implies "less than or equal to". (pssss 4051 analog.) (Contributed by NM, 4-Dec-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌))
Theorem	pltne 18392	The "less than" relation is not reflexive. (df-pss 3924 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌))
Theorem	pltirr 18393	The "less than" relation is not reflexive. (pssirr 4056 analog.) (Contributed by NM, 7-Feb-2012.)
⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋 < 𝑋)
Theorem	pleval2i 18394	One direction of pleval2 18395. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌)))
Theorem	pleval2 18395	"Less than or equal to" in terms of "less than". (sspss 4055 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 < 𝑌 ∨ 𝑋 = 𝑌)))
Theorem	pltnle 18396	"Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋)
Theorem	pltval3 18397	Alternate expression for the "less than" relation. (dfpss3 4042 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋)))
Theorem	pltnlt 18398	The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 < 𝑋)
Theorem	pltn2lp 18399	The less-than relation has no 2-cycle loops. (pssn2lp 4058 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ¬ (𝑋 < 𝑌 ∧ 𝑌 < 𝑋))
Theorem	plttr 18400	The less-than relation is transitive. (psstr 4061 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍))