P. 181 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18001-18100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	yonedalem3a 18001*	Lemma for yoneda 18010. (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 18002*	Lemma for yoneda 18010. (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 18003*	Lemma for yoneda 18010. (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 18004*	Lemma for yoneda 18010. (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 18005	Lemma for yoneda 18010. (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 18006*	Lemma for yoneda 18010. (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 18007*	Lemma for yoneda 18010. (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 18008*	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 18009*	Lemma for yonffth 18011. (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 18010*	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 18011	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 18012*	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 18013	Class function defining dual orders.
class ODual
Definition	df-odu 18014	Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas 18018, oduleval 18016, and oduleg 18017 for its principal properties. EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 18222. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩))
Theorem	oduval 18015	Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ≤ = (le‘𝑂)    ⇒   ⊢ 𝐷 = (𝑂 sSet ⟨(le‘ndx), ◡ ≤ ⟩)
Theorem	oduleval 18016	Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ≤ = (le‘𝑂)    ⇒   ⊢ ◡ ≤ = (le‘𝐷)
Theorem	oduleg 18017	Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ≤ = (le‘𝑂)    &   ⊢ 𝐺 = (le‘𝐷)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝐺𝐵 ↔ 𝐵 ≤ 𝐴))
Theorem	odubas 18018	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 18019	Obsolete proof of odubas 18018 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‘𝐷)
9.2  Preordered sets and directed sets
Syntax	cproset 18020	Extend class notation with the class of all prosets.
class Proset
Syntax	cdrs 18021	Extend class notation with the class of all directed sets.
class Dirset
Definition	df-proset 18022*	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 18023*	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 18024*	Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Proset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	prslem 18025	Lemma for prsref 18026 and prstr 18027. (Contributed by Mario Carneiro, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	prsref 18026	"Less than or equal to" is reflexive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
Theorem	prstr 18027	"Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ≤ 𝑍)
Theorem	isdrs 18028*	Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧)))
Theorem	drsdir 18029*	Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑧 ∈ 𝐵 (𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧))
Theorem	drsprs 18030	A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Proset )
Theorem	drsbn0 18031	The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ (𝐾 ∈ Dirset → 𝐵 ≠ ∅)
Theorem	drsdirfi 18032*	Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 18023 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 18033*	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 18034	Extend class notation with the class of posets.
class Poset
Syntax	cplt 18035	Extend class notation with less-than for posets.
class lt
Syntax	club 18036	Extend class notation with poset least upper bound.
class lub
Syntax	cglb 18037	Extend class notation with poset greatest lower bound.
class glb
Syntax	cjn 18038	Extend class notation with poset join.
class join
Syntax	cmee 18039	Extend class notation with poset meet.
class meet
Definition	df-poset 18040*	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 3484 and related theorems. (Contributed by NM, 18-Oct-2012.)
⊢ Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))}
Theorem	ispos 18041*	The predicate "is a poset". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	ispos2 18042*	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 18043	A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset )
Theorem	posi 18044	Lemma for poset properties. (Contributed by NM, 11-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	posref 18045	A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
Theorem	posasymb 18046	A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))
Theorem	postr 18047	A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
Theorem	0pos 18048	Technical lemma to simplify the statement of ipopos 18263. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 16899) 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 18049	Obsolete proof of 0pos 18048 as of 13-Oct-2024. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∅ ∈ Poset
Theorem	isposd 18050*	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 18051*	Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.)
⊢ 𝐾 ∈ V    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))    ⇒   ⊢ 𝐾 ∈ Poset
Theorem	isposix 18052*	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 18053*	Obsolete proof of isposix 18052 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 18054*	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 18055	Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ Poset → 𝐷 ∈ Poset)
Theorem	oduposb 18056	Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ Poset ↔ 𝐷 ∈ Poset))
Definition	df-plt 18057	Define less-than ordering for posets and related structures. Unlike df-base 16922 and df-ple 16991, 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 18058	Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I ))
Theorem	pltval 18059	Less-than relation. (df-pss 3907 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌)))
Theorem	pltle 18060	"Less than" implies "less than or equal to". (pssss 4031 analog.) (Contributed by NM, 4-Dec-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌))
Theorem	pltne 18061	The "less than" relation is not reflexive. (df-pss 3907 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌))
Theorem	pltirr 18062	The "less than" relation is not reflexive. (pssirr 4036 analog.) (Contributed by NM, 7-Feb-2012.)
⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋 < 𝑋)
Theorem	pleval2i 18063	One direction of pleval2 18064. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌)))
Theorem	pleval2 18064	"Less than or equal to" in terms of "less than". (sspss 4035 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 < 𝑌 ∨ 𝑋 = 𝑌)))
Theorem	pltnle 18065	"Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋)
Theorem	pltval3 18066	Alternate expression for the "less than" relation. (dfpss3 4022 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋)))
Theorem	pltnlt 18067	The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 < 𝑋)
Theorem	pltn2lp 18068	The less-than relation has no 2-cycle loops. (pssn2lp 4037 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ¬ (𝑋 < 𝑌 ∧ 𝑌 < 𝑋))
Theorem	plttr 18069	The less-than relation is transitive. (psstr 4040 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍))
Theorem	pltletr 18070	Transitive law for chained "less than" and "less than or equal to". (psssstr 4042 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍))
Theorem	plelttr 18071	Transitive law for chained "less than or equal to" and "less than". (sspsstr 4041 analog.) (Contributed by NM, 2-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍))
Theorem	pospo 18072	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 18073*	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 18074*	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 18075*	Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by Mario Carneiro, 3-Nov-2015.)
⊢ join = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧})
Definition	df-meet 18076*	Define poset meet. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.)
⊢ meet = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧})
Theorem	lubfval 18077*	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 18078*	Domain of the least upper bound function of a poset. (Contributed by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝑈 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓})
Theorem	lubfun 18079	The LUB is a function. (Contributed by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ Fun 𝑈
Theorem	lubeldm 18080*	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 18081	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 18082*	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 18083*	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 18084	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) ∈ 𝐵)
Theorem	lubprop 18085*	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 18086	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 18087*	Lemma for lublecl 18088 and lubid 18089. (Contributed by NM, 8-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑥 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤)) ↔ 𝑥 = 𝑋))
Theorem	lublecl 18088*	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 18089*	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)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑈‘{𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}) = 𝑋)
Theorem	glbfval 18090*	Value of the greatest lower function of a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐺 = ((𝑠 ∈ 𝒫 𝐵 ↦ (℩𝑥 ∈ 𝐵 𝜓)) ↾ {𝑠 ∣ ∃!𝑥 ∈ 𝐵 𝜓}))
Theorem	glbdm 18091*	Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐺 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓})
Theorem	glbfun 18092	The GLB is a function. (Contributed by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ Fun 𝐺
Theorem	glbeldm 18093*	Member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ (𝑆 ⊆ 𝐵 ∧ ∃!𝑥 ∈ 𝐵 𝜓)))
Theorem	glbelss 18094	A member of the domain of the greatest lower bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
Theorem	glbeu 18095*	Unique existence proper of a member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 𝜓)
Theorem	glbval 18096*	Value of the greatest lower bound function of a poset. Out-of-domain arguments (those not satisfying 𝑆 ∈ dom 𝑈) are allowed for convenience, evaluating to the empty set on both sides of the equality. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	glbcl 18097	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) ∈ 𝐵)
Theorem	glbprop 18098*	Properties of greatest lower bound of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ 𝑆 (𝑈‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝑈‘𝑆))))
Theorem	glble 18099	The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) ≤ 𝑋)
Theorem	joinfval 18100*	Value of join function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove joinfval2 18101 first to reduce net proof size (existence part)?
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∨ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦}𝑈𝑧})