P. 508 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50701-50800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	relran 50701	The set of right Kan extensions is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel (𝐹(𝑃 Ran 𝐸)𝑋)
Theorem	islan 50702	A left Kan extension is a universal pair. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) → 𝐿 ∈ (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	islan2 50703	A left Kan extension is a universal pair. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴 → 𝐿(𝐾(𝑅 UP 𝑆)𝑋)𝐴)
Theorem	lanval2 50704	The set of left Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by isup2 50271 and upciclem1 50243. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) = (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	isran 50705	A right Kan extension is a universal pair. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑃 = (oppCat‘(𝐶 FuncCat 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐽, 𝐾⟩)    &   ⊢ (𝜑 → 𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋))    ⇒   ⊢ (𝜑 → 𝐿 ∈ (⟨𝐽, tpos 𝐾⟩(𝑂 UP 𝑃)𝑋))
Theorem	isran2 50706	A right Kan extension is a universal pair. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑃 = (oppCat‘(𝐶 FuncCat 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐽, 𝐾⟩)    &   ⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐿(⟨𝐽, tpos 𝐾⟩(𝑂 UP 𝑃)𝑋)𝐴)
Theorem	ranval2 50707	The set of right Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by oppcup2 50285 and oppcup3lem 50283. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑃 = (oppCat‘(𝐶 FuncCat 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐽, 𝐾⟩)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) = (⟨𝐽, tpos 𝐾⟩(𝑂 UP 𝑃)𝑋))
Theorem	ranval3 50708	The set of right Kan extensions is the set of universal pairs. (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ 𝑂 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑃 = (oppCat‘(𝐶 FuncCat 𝐸))    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) = (( oppFunc ‘𝐾)(𝑂 UP 𝑃)𝑋))
Theorem	lanrcl2 50709	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
Theorem	lanrcl3 50710	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))
Theorem	lanrcl4 50711	The first component of a left Kan extension is a functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))
Theorem	lanrcl5 50712	The second component of a left Kan extension is a natural transformation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝑁(𝐿 ∘func 𝐹)))
Theorem	ranrcl2 50713	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
Theorem	ranrcl3 50714	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))
Theorem	ranrcl4lem 50715	Lemma for ranrcl4 50716 and ranrcl5 50717. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨(1st ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)), (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹))⟩)
Theorem	ranrcl4 50716	The first component of a right Kan extension is a functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))
Theorem	ranrcl5 50717	The second component of a right Kan extension is a natural transformation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ((𝐿 ∘func 𝐹)𝑁𝑋))
Theorem	lanup 50718*	The universal property of the left Kan extension; expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝑀 = (𝐷 Nat 𝐸)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    &   ⊢ ∙ = (comp‘𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝑁(𝐿 ∘func 𝐹)))    ⇒   ⊢ (𝜑 → (𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴 ↔ ∀𝑙 ∈ (𝐷 Func 𝐸)∀𝑎 ∈ (𝑋𝑁(𝑙 ∘func 𝐹))∃!𝑏 ∈ (𝐿𝑀𝑙)𝑎 = ((𝑏 ∘ (1st ‘𝐹))(⟨𝑋, (𝐿 ∘func 𝐹)⟩ ∙ (𝑙 ∘func 𝐹))𝐴)))
Theorem	ranup 50719*	The universal property of the right Kan extension; expressed explicitly. (Contributed by Zhi Wang, 5-Nov-2025.)
⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝑀 = (𝐷 Nat 𝐸)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    &   ⊢ ∙ = (comp‘𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ ((𝐿 ∘func 𝐹)𝑁𝑋))    ⇒   ⊢ (𝜑 → (𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴 ↔ ∀𝑙 ∈ (𝐷 Func 𝐸)∀𝑎 ∈ ((𝑙 ∘func 𝐹)𝑁𝑋)∃!𝑏 ∈ (𝑙𝑀𝐿)𝑎 = (𝐴(⟨(𝑙 ∘func 𝐹), (𝐿 ∘func 𝐹)⟩ ∙ 𝑋)(𝑏 ∘ (1st ‘𝐹)))))
21.51.17.2  Limits and colimits
Syntax	clmd 50720	Class function defining the limit of a diagram.
class Limit
Syntax	ccmd 50721	Class function defining the colimit of a diagram.
class Colimit
Definition	df-lmd 50722*	A diagram of type 𝐷 or a 𝐷-shaped diagram in a category 𝐶, is a functor 𝐹:𝐷⟶𝐶 where the source category 𝐷, usually small or even finite, is called the index category or the scheme of the diagram. The actual objects and morphisms in 𝐷 are largely irrelevant; only the way in which they are interrelated matters. The diagram is thought of as indexing a collection of objects and morphisms in 𝐶 patterned on 𝐷. Definition 11.1(1) of [Adamek] p. 193. A cone to a diagram, or a natural source for a diagram in a category 𝐶 is a pair of an object 𝑋 in 𝐶 and a natural transformation from the constant functor (or constant diagram) of the object 𝑋 to the diagram. The second component associates each object in the index category with a morphism in 𝐶 whose domain is 𝑋 (concl 50738). The naturality guarantees that the combination of the diagram with the cone must commute (concom 50740). Definition 11.3(1) of [Adamek] p. 193. A limit of a diagram 𝐹:𝐷⟶𝐶 of type 𝐷 in category 𝐶 is a universal pair from the diagonal functor (𝐶Δfunc𝐷) to the diagram. The universal pair is a cone to the diagram satisfying the universal property, that each cone to the diagram uniquely factors through the limit (islmd 50742). Definition 11.3(2) of [Adamek] p. 194. Terminal objects (termolmd 50747), products, equalizers, pullbacks, and inverse limits can be considered as limits of some diagram; limits can be further generalized as right Kan extensions (lmdran 50748). "lmd" is short for "limit of a diagram". See df-cmd 50723 for the dual concept (lmddu 50744, cmddu 50745). (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Limit = (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ (( oppFunc ‘(𝑐Δfunc𝑑))((oppCat‘𝑐) UP (oppCat‘(𝑑 FuncCat 𝑐)))𝑓)))
Definition	df-cmd 50723*	A co-cone (or cocone) to a diagram (see df-lmd 50722 for definition), or a natural sink for a diagram in a category 𝐶 is a pair of an object 𝑋 in 𝐶 and a natural transformation from the diagram to the constant functor (or constant diagram) of the object 𝑋. The second component associates each object in the index category with a morphism in 𝐶 whose codomain is 𝑋 (coccl 50739). The naturality guarantees that the combination of the diagram with the co-cone must commute (coccom 50741). Definition 11.27(1) of [Adamek] p. 202. A colimit of a diagram 𝐹:𝐷⟶𝐶 of type 𝐷 in category 𝐶 is a universal pair from the diagram to the diagonal functor (𝐶Δfunc𝐷). The universal pair is a co-cone to the diagram satisfying the universal property, that each co-cone to the diagram uniquely factors through the colimit. (iscmd 50743). Definition 11.27(2) of [Adamek] p. 202. Initial objects (initocmd 50746), coproducts, coequalizers, pushouts, and direct limits can be considered as colimits of some diagram; colimits can be further generalized as left Kan extensions (cmdlan 50749). "cmd" is short for "colimit of a diagram". See df-lmd 50722 for the dual concept (lmddu 50744, cmddu 50745). (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Colimit = (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((𝑐Δfunc𝑑)(𝑐 UP (𝑑 FuncCat 𝑐))𝑓)))
Theorem	reldmlmd 50724	The domain of Limit is a relation. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Rel dom Limit
Theorem	reldmcmd 50725	The domain of Colimit is a relation. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Rel dom Colimit
Theorem	lmdfval 50726*	Function value of Limit. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝐶 Limit 𝐷) = (𝑓 ∈ (𝐷 Func 𝐶) ↦ (( oppFunc ‘(𝐶Δfunc𝐷))((oppCat‘𝐶) UP (oppCat‘(𝐷 FuncCat 𝐶)))𝑓))
Theorem	cmdfval 50727*	Function value of Colimit. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ (𝐶 Colimit 𝐷) = (𝑓 ∈ (𝐷 Func 𝐶) ↦ ((𝐶Δfunc𝐷)(𝐶 UP (𝐷 FuncCat 𝐶))𝑓))
Theorem	lmdrcl 50728	Reverse closure for a limit of a diagram. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝑋 ∈ ((𝐶 Limit 𝐷)‘𝐹) → 𝐹 ∈ (𝐷 Func 𝐶))
Theorem	cmdrcl 50729	Reverse closure for a colimit of a diagram. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝑋 ∈ ((𝐶 Colimit 𝐷)‘𝐹) → 𝐹 ∈ (𝐷 Func 𝐶))
Theorem	reldmlmd2 50730	The domain of (𝐶 Limit 𝐷) is a relation. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ Rel dom (𝐶 Limit 𝐷)
Theorem	reldmcmd2 50731	The domain of (𝐶 Colimit 𝐷) is a relation. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ Rel dom (𝐶 Colimit 𝐷)
Theorem	lmdfval2 50732	The set of limits of a diagram. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ ((𝐶 Limit 𝐷)‘𝐹) = (( oppFunc ‘(𝐶Δfunc𝐷))((oppCat‘𝐶) UP (oppCat‘(𝐷 FuncCat 𝐶)))𝐹)
Theorem	cmdfval2 50733	The set of colimits of a diagram. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ ((𝐶 Colimit 𝐷)‘𝐹) = ((𝐶Δfunc𝐷)(𝐶 UP (𝐷 FuncCat 𝐶))𝐹)
Theorem	lmdpropd 50734	If the categories have the same set of objects, morphisms, and compositions, then they have the same limits. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 Limit 𝐶) = (𝐵 Limit 𝐷))
Theorem	cmdpropd 50735	If the categories have the same set of objects, morphisms, and compositions, then they have the same colimits. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 Colimit 𝐶) = (𝐵 Colimit 𝐷))
Theorem	rellmd 50736	The set of limits of a diagram is a relation. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ Rel ((𝐶 Limit 𝐷)‘𝐹)
Theorem	relcmd 50737	The set of colimits of a diagram is a relation. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ Rel ((𝐶 Colimit 𝐷)‘𝐹)
Theorem	concl 50738	A natural transformation from a constant functor of an object maps to morphisms whose domain is the object. Therefore, the range of the second component of a cone are morphisms with a common domain. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐾𝑁𝐹))    ⇒   ⊢ (𝜑 → (𝑅‘𝑌) ∈ (𝑋𝐻((1st ‘𝐹)‘𝑌)))
Theorem	coccl 50739	A natural transformation to a constant functor of an object maps to morphisms whose codomain is the object. Therefore, the range of the second component of a co-cone are morphisms with a common codomain. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐾))    ⇒   ⊢ (𝜑 → (𝑅‘𝑌) ∈ (((1st ‘𝐹)‘𝑌)𝐻𝑋))
Theorem	concom 50740	A cone to a diagram commutes with the diagram. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑌𝐽𝑍))    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐾𝑁𝐹))    ⇒   ⊢ (𝜑 → (𝑅‘𝑍) = (((𝑌(2nd ‘𝐹)𝑍)‘𝑀)(⟨𝑋, ((1st ‘𝐹)‘𝑌)⟩ · ((1st ‘𝐹)‘𝑍))(𝑅‘𝑌)))
Theorem	coccom 50741	A co-cone to a diagram commutes with the diagram. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑌𝐽𝑍))    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐾))    ⇒   ⊢ (𝜑 → (𝑅‘𝑌) = ((𝑅‘𝑍)(⟨((1st ‘𝐹)‘𝑌), ((1st ‘𝐹)‘𝑍)⟩ · 𝑋)((𝑌(2nd ‘𝐹)𝑍)‘𝑀)))
Theorem	islmd 50742*	The universal property of limits of a diagram. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝑋((𝐶 Limit 𝐷)‘𝐹)𝑅 ↔ ((𝑋 ∈ 𝐴 ∧ 𝑅 ∈ (((1st ‘𝐿)‘𝑋)𝑁𝐹)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑎 ∈ (((1st ‘𝐿)‘𝑥)𝑁𝐹)∃!𝑚 ∈ (𝑥𝐻𝑋)𝑎 = (𝑗 ∈ 𝐵 ↦ ((𝑅‘𝑗)(⟨𝑥, 𝑋⟩ · ((1st ‘𝐹)‘𝑗))𝑚))))
Theorem	iscmd 50743*	The universal property of colimits of a diagram. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ 𝐿 = (𝐶Δfunc𝐷)    &   ⊢ 𝐴 = (Base‘𝐶)    &   ⊢ 𝑁 = (𝐷 Nat 𝐶)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝑋((𝐶 Colimit 𝐷)‘𝐹)𝑅 ↔ ((𝑋 ∈ 𝐴 ∧ 𝑅 ∈ (𝐹𝑁((1st ‘𝐿)‘𝑋))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑎 ∈ (𝐹𝑁((1st ‘𝐿)‘𝑥))∃!𝑚 ∈ (𝑋𝐻𝑥)𝑎 = (𝑗 ∈ 𝐵 ↦ (𝑚(⟨((1st ‘𝐹)‘𝑗), 𝑋⟩ · 𝑥)(𝑅‘𝑗)))))
Theorem	lmddu 50744	The duality of limits and colimits: limits of a diagram are colimits of an opposite diagram in opposite categories. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝐺 = ( oppFunc ‘𝐹)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝐶 Limit 𝐷)‘𝐹) = ((𝑂 Colimit 𝑃)‘𝐺))
Theorem	cmddu 50745	The duality of limits and colimits: colimits of a diagram are limits of an opposite diagram in opposite categories. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑃 = (oppCat‘𝐷)    &   ⊢ 𝐺 = ( oppFunc ‘𝐹)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝐶 Colimit 𝐷)‘𝐹) = ((𝑂 Limit 𝑃)‘𝐺))
Theorem	initocmd 50746	Initial objects are the object part of colimits of the empty diagram. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (InitO‘𝐶) = dom (∅(𝐶 Colimit ∅)∅)
Theorem	termolmd 50747	Terminal objects are the object part of limits of the empty diagram. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (TermO‘𝐶) = dom (∅(𝐶 Limit ∅)∅)
Theorem	lmdran 50748	To each limit of a diagram there is a corresponding right Kan extention of the diagram along a functor to a terminal category. The morphism parts coincide, while the object parts are one-to-one correspondent (diag1f1o 50611). (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ (𝜑 → 1 ∈ TermCat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 1 ))    &   ⊢ 𝐿 = (𝐶Δfunc 1 )    &   ⊢ (𝜑 → 𝑌 = ((1st ‘𝐿)‘𝑋))    ⇒   ⊢ (𝜑 → (𝑋((𝐶 Limit 𝐷)‘𝐹)𝑀 ↔ 𝑌(𝐺(⟨𝐷, 1 ⟩ Ran 𝐶)𝐹)𝑀))
Theorem	cmdlan 50749	To each colimit of a diagram there is a corresponding left Kan extention of the diagram along a functor to a terminal category. The morphism parts coincide, while the object parts are one-to-one correspondent (diag1f1o 50611). (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ (𝜑 → 1 ∈ TermCat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 1 ))    &   ⊢ 𝐿 = (𝐶Δfunc 1 )    &   ⊢ (𝜑 → 𝑌 = ((1st ‘𝐿)‘𝑋))    ⇒   ⊢ (𝜑 → (𝑋((𝐶 Colimit 𝐷)‘𝐹)𝑀 ↔ 𝑌(𝐺(⟨𝐷, 1 ⟩ Lan 𝐶)𝐹)𝑀))
21.52  Mathbox for Emmett Weisz
21.52.1  Miscellaneous Theorems Some of these theorems are used in the series of lemmas and theorems proving the defining properties of setrecs.
Theorem	nfintd 50750	Bound-variable hypothesis builder for intersection. (Contributed by Emmett Weisz, 16-Jan-2020.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∩ 𝐴)
Theorem	nfiund 50751*	Bound-variable hypothesis builder for indexed union. (Contributed by Emmett Weisz, 6-Dec-2019.) Add disjoint variable condition to avoid ax-13 2402. See nfiundg 50752 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝐴)    &   ⊢ (𝜑 → Ⅎ𝑦𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	nfiundg 50752	Bound-variable hypothesis builder for indexed union. Usage of this theorem is discouraged because it depends on ax-13 2402, see nfiund 50751 for a weaker version that does not require it. (Contributed by Emmett Weisz, 6-Dec-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝐴)    &   ⊢ (𝜑 → Ⅎ𝑦𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunord 50753*	The indexed union of a collection of ordinal numbers 𝐵(𝑥) is ordinal. This proof is based on the proof of ssorduni 7791, but does not use it directly, since ssorduni 7791 does not work when 𝐵 is a proper class. (Contributed by Emmett Weisz, 3-Nov-2019.)
⊢ (∀𝑥 ∈ 𝐴 Ord 𝐵 → Ord ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunordi 50754*	The indexed union of a collection of ordinal numbers 𝐵(𝑥) is ordinal. (Contributed by Emmett Weisz, 3-Nov-2019.)
⊢ Ord 𝐵    ⇒   ⊢ Ord ∪ 𝑥 ∈ 𝐴 𝐵
Theorem	spd 50755	Specialization deduction, using implicit substitution. Based on the proof of spimed 2418. (Contributed by Emmett Weisz, 17-Jan-2020.)
⊢ (𝜒 → Ⅎ𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜒 → (∀𝑥𝜑 → 𝜓))
Theorem	tfis2d 50756*	Transfinite Induction Schema, using implicit substitution. (Contributed by Emmett Weisz, 3-May-2020.)
⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    &   ⊢ (𝜑 → (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜒 → 𝜓)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ On → 𝜓))
21.52.2  Examples and properties of set recursion
Theorem	setrecseq 50757	Equality theorem for set recursion. (Contributed by Emmett Weisz, 17-Feb-2021.)
⊢ (𝐹 = 𝐺 → setrecs(𝐹) = setrecs(𝐺))
Theorem	nfsetrecs 50758	Bound-variable hypothesis builder for setrecs. (Contributed by Emmett Weisz, 21-Oct-2021.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥setrecs(𝐹)
Theorem	setrec2mpt 50759*	Version of setrec2 9970 where 𝐹 is defined using maps-to notation. Deduction form is omitted in the second hypothesis for simplicity. In practice, nothing important is lost since we are only interested in one choice of 𝐴, 𝑆, and 𝑉 at a time. However, we are interested in what happens when 𝐶 varies, so deduction form is used in the third hypothesis. (Contributed by Emmett Weisz, 4-Jun-2024.)
⊢ 𝐵 = setrecs((𝑎 ∈ 𝐴 ↦ 𝑆))    &   ⊢ (𝑎 ∈ 𝐴 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐶 → 𝑆 ⊆ 𝐶))    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	setis 50760*	Version of setrec2 9970 expressed as an induction schema. This theorem is a generalization of tfis3 7867. (Contributed by Emmett Weisz, 27-Feb-2022.)
⊢ 𝐵 = setrecs(𝐹)    &   ⊢ (𝑏 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑎(∀𝑏 ∈ 𝑎 𝜓 → ∀𝑏 ∈ (𝐹‘𝑎)𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝜒))
Theorem	elsetrecslem 50761*	Lemma for elsetrecs 50762. Any element of setrecs(𝐹) is generated by some subset of setrecs(𝐹). This is much weaker than setrec2v 9971. To see why this lemma also requires setrec1 9965, consider what would happen if we replaced 𝐵 with {𝐴}. The antecedent would still hold, but the consequent would fail in general. Consider dispensing with the deduction form. (Contributed by Emmett Weisz, 11-Jul-2021.) (New usage is discouraged.)
⊢ 𝐵 = setrecs(𝐹)    ⇒   ⊢ (𝐴 ∈ 𝐵 → ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ (𝐹‘𝑥)))
Theorem	elsetrecs 50762*	A set 𝐴 is an element of setrecs(𝐹) iff 𝐴 is generated by some subset of setrecs(𝐹). The proof requires both setrec1 9965 and setrec2 9970, but this theorem is not strong enough to uniquely determine setrecs(𝐹). If 𝐹 respects the subset relation, the theorem still holds if both occurrences of ∈ are replaced by ⊆ for a stronger version of the theorem. (Contributed by Emmett Weisz, 12-Jul-2021.)
⊢ 𝐵 = setrecs(𝐹)    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ (𝐹‘𝑥)))
Theorem	setrecsss 50763	The setrecs operator respects the subset relation between two functions 𝐹 and 𝐺. (Contributed by Emmett Weisz, 13-Mar-2022.)
⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐺)    ⇒   ⊢ (𝜑 → setrecs(𝐹) ⊆ setrecs(𝐺))
Theorem	setrecsres 50764	A recursively generated class is unaffected when its input function is restricted to subsets of the class. (Contributed by Emmett Weisz, 14-Mar-2022.)
⊢ 𝐵 = setrecs(𝐹)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ (𝜑 → 𝐵 = setrecs((𝐹 ↾ 𝒫 𝐵)))
Theorem	vsetrec 50765	Construct V using set recursion. The proof indirectly uses trcl 9722, which relies on rec, but theoretically 𝐶 in trcl 9722 could be constructed using setrecs instead. The proof of this theorem uses the dummy variable 𝑎 rather than 𝑥 to avoid a distinct variable requirement between 𝐹 and 𝑥. (Contributed by Emmett Weisz, 23-Jun-2021.)
⊢ 𝐹 = (𝑥 ∈ V ↦ 𝒫 𝑥)    ⇒   ⊢ setrecs(𝐹) = V
Theorem	0setrec 50766	If a function sends the empty set to itself, the function will not recursively generate any sets, regardless of its other values. (Contributed by Emmett Weisz, 23-Jun-2021.)
⊢ (𝜑 → (𝐹‘∅) = ∅)    ⇒   ⊢ (𝜑 → setrecs(𝐹) = ∅)
Theorem	onsetreclem1 50767*	Lemma for onsetrec 50770. (Contributed by Emmett Weisz, 22-Jun-2021.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ V ↦ {∪ 𝑥, suc ∪ 𝑥})    ⇒   ⊢ (𝐹‘𝑎) = {∪ 𝑎, suc ∪ 𝑎}
Theorem	onsetreclem2 50768*	Lemma for onsetrec 50770. (Contributed by Emmett Weisz, 22-Jun-2021.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ V ↦ {∪ 𝑥, suc ∪ 𝑥})    ⇒   ⊢ (𝑎 ⊆ On → (𝐹‘𝑎) ⊆ On)
Theorem	onsetreclem3 50769*	Lemma for onsetrec 50770. (Contributed by Emmett Weisz, 22-Jun-2021.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ V ↦ {∪ 𝑥, suc ∪ 𝑥})    ⇒   ⊢ (𝑎 ∈ On → 𝑎 ∈ (𝐹‘𝑎))
Theorem	onsetrec 50770	Construct On using set recursion. When 𝑥 ∈ On, the function 𝐹 constructs the least ordinal greater than any of the elements of 𝑥, which is ∪ 𝑥 for a limit ordinal and suc ∪ 𝑥 for a successor ordinal. For example, (𝐹‘{1o, 2o}) = {∪ {1o, 2o}, suc ∪ {1o, 2o}} = {2o, 3o} which contains 3o, and (𝐹‘ω) = {∪ ω, suc ∪ ω} = {ω, ω +o 1o}, which contains ω. If we start with the empty set and keep applying 𝐹 transfinitely many times, all ordinal numbers will be generated. Any function 𝐹 fulfilling lemmas onsetreclem2 50768 and onsetreclem3 50769 will recursively generate On; for example, 𝐹 = (𝑥 ∈ V ↦ suc suc ∪ 𝑥}) also works. Whether this function or the function in the theorem is used, taking this theorem as a definition of On is unsatisfying because it relies on the different properties of limit and successor ordinals. A different approach could be to let 𝐹 = (𝑥 ∈ V ↦ {𝑦 ∈ 𝒫 𝑥 ∣ Tr 𝑦}), based on dfon2 36534. The proof of this theorem uses the dummy variable 𝑎 rather than 𝑥 to avoid a distinct variable condition between 𝐹 and 𝑥. (Contributed by Emmett Weisz, 22-Jun-2021.)
⊢ 𝐹 = (𝑥 ∈ V ↦ {∪ 𝑥, suc ∪ 𝑥})    ⇒   ⊢ setrecs(𝐹) = On
21.52.3  Construction of Games and Surreal Numbers Model organization after organization of reals - see TOC
Syntax	cpg 50771	Extend class notation to include the class of partisan game forms.
class Pg
Definition	df-pg 50772	Define the class of partisan games. More precisely, this is the class of partisan game forms, many of which represent equal partisan games. In Metamath, equality between partisan games is represented by a different equivalence relation than class equality. (Contributed by Emmett Weisz, 22-Aug-2021.)
⊢ Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))
Theorem	elpglem1 50773*	Lemma for elpg 50776. (Contributed by Emmett Weisz, 28-Aug-2021.)
⊢ (∃𝑥(𝑥 ⊆ Pg ∧ ((1st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2nd ‘𝐴) ∈ 𝒫 𝑥)) → ((1st ‘𝐴) ⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg))
Theorem	elpglem2 50774*	Lemma for elpg 50776. (Contributed by Emmett Weisz, 28-Aug-2021.)
⊢ (((1st ‘𝐴) ⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg) → ∃𝑥(𝑥 ⊆ Pg ∧ ((1st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2nd ‘𝐴) ∈ 𝒫 𝑥)))
Theorem	elpglem3 50775*	Lemma for elpg 50776. (Contributed by Emmett Weisz, 28-Aug-2021.)
⊢ (∃𝑥(𝑥 ⊆ Pg ∧ 𝐴 ∈ ((𝑦 ∈ V ↦ (𝒫 𝑦 × 𝒫 𝑦))‘𝑥)) ↔ (𝐴 ∈ (V × V) ∧ ∃𝑥(𝑥 ⊆ Pg ∧ ((1st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2nd ‘𝐴) ∈ 𝒫 𝑥))))
Theorem	elpg 50776	Membership in the class of partisan games. In John Horton Conway's On Numbers and Games, this is stated as "If 𝐿 and 𝑅 are any two sets of games, then there is a game {𝐿 ∣ 𝑅}. All games are constructed in this way." The first sentence corresponds to the backward direction of our theorem, and the second to the forward direction. (Contributed by Emmett Weisz, 27-Aug-2021.)
⊢ (𝐴 ∈ Pg ↔ (𝐴 ∈ (V × V) ∧ (1st ‘𝐴) ⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg))
Theorem	pgindlem 50777	Lemma for pgind 50779. (Contributed by Emmett Weisz, 27-May-2024.) (New usage is discouraged.)
⊢ (𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧) → ((1st ‘𝑥) ∪ (2nd ‘𝑥)) ⊆ 𝑧)
Theorem	pgindnf 50778*	Version of pgind 50779 with extraneous not-free requirements. (Contributed by Emmett Weisz, 27-May-2024.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐴 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → ∀𝑥(∀𝑦 ∈ ((1st ‘𝑥) ∪ (2nd ‘𝑥))𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ∈ Pg → 𝜃))
Theorem	pgind 50779*	Induction on partizan games. (Contributed by Emmett Weisz, 27-May-2024.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐴 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → ∀𝑥(∀𝑦 ∈ ((1st ‘𝑥) ∪ (2nd ‘𝑥))𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ∈ Pg → 𝜃))
21.53  Mathbox for David A. Wheeler This is the mathbox of David A. Wheeler, dwheeler at dwheeler dot com . Among other things, I have added a number of formal definitions for widely-used functions, e.g., those defined in ISO 80000-2:2009(E) Quantities and units - Part 2: Mathematical signs and symbols used in the natural sciences and technology and the NIST Digital Library of Mathematical Functions http://dlmf.nist.gov/.
21.53.1  Natural deduction
Theorem	sbidd 50780	An identity theorem for substitution. See sbid 2291. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
⊢ (𝜑 → [𝑥 / 𝑥]𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	sbidd-misc 50781	An identity theorem for substitution. See sbid 2291. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
⊢ ((𝜑 → [𝑥 / 𝑥]𝜓) ↔ (𝜑 → 𝜓))
21.53.2  Greater than, greater than or equal to As a stylistic issue, set.mm prefers 'less than' instead of 'greater than' to reduce the number of conversion steps. Here we formally define the widely-used relations 'greater than' and 'greater than or equal to', so that we have formal definitions of them, as well as a few related theorems.
Syntax	cge-real 50782	Extend wff notation to include the 'greater than or equal to' relation, see df-gte 50784.
class ≥
Syntax	cgt 50783	Extend wff notation to include the 'greater than' relation, see df-gt 50785.
class >
Definition	df-gte 50784	Define the 'greater than or equal' predicate over the reals. Defined in ISO 80000-2:2009(E) operation 2-7.10. It is used as a primitive in the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4. This relation is merely the converse of the 'less than or equal to' relation defined by df-le 11342. We do not write this as (𝑥 ≥ 𝑦 ↔ 𝑦 ≤ 𝑥), and similarly we do not write ` > ` as (𝑥 > 𝑦 ↔ 𝑦 < 𝑥), because these are not definitional axioms as understood by mmj2 (those definitions will be flagged as being "potentially non-conservative"). We could write them this way: ⊢ > = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ 𝑦 < 𝑥)} and ⊢ ≥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ 𝑦 ≤ 𝑥)} but these are very complicated. This definition of ≥, and the similar one for > (df-gt 50785), are a bit strange when you see them for the first time, but these definitions are much simpler for us to process and are clearly conservative definitions. (My thanks to Mario Carneiro for pointing out this simpler approach.) See gte-lte 50786 for a more conventional expression of the relationship between < and >. As a stylistic issue, set.mm prefers 'less than' instead of 'greater than' to reduce the number of conversion steps. Thus, we discourage its use, but include its definition so that there is a formal definition of this symbol. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.)
⊢ ≥ = ◡ ≤
Definition	df-gt 50785	The 'greater than' relation is merely the converse of the 'less than or equal to' relation defined by df-lt 11206. Defined in ISO 80000-2:2009(E) operation 2-7.12. See df-gte 50784 for a discussion on why this approach is used for the definition. See gt-lt 50787 and gt-lth 50789 for more conventional expression of the relationship between < and >. As a stylistic issue, set.mm prefers 'less than or equal' instead of 'greater than or equal' to reduce the number of conversion steps. Thus, we discourage its use, but include its definition so that there is a formal definition of this symbol. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.)
⊢ > = ◡ <
Theorem	gte-lte 50786	Simple relationship between ≤ and ≥. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≥ 𝐵 ↔ 𝐵 ≤ 𝐴))
Theorem	gt-lt 50787	Simple relationship between < and >. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 > 𝐵 ↔ 𝐵 < 𝐴))
Theorem	gte-lteh 50788	Relationship between ≤ and ≥ using hypotheses. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≥ 𝐵 ↔ 𝐵 ≤ 𝐴)
Theorem	gt-lth 50789	Relationship between < and > using hypotheses. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 > 𝐵 ↔ 𝐵 < 𝐴)
Theorem	ex-gt 50790	Simple example of >, in this case, 0 is not greater than 0. This is useful as an example, and helps us gain confidence that we've correctly defined the symbol. (Contributed by David A. Wheeler, 1-Jan-2017.) (New usage is discouraged.)
⊢ ¬ 0 > 0
Theorem	ex-gte 50791	Simple example of ≥, in this case, 0 is greater than or equal to 0. This is useful as an example, and helps us gain confidence that we've correctly defined the symbol. (Contributed by David A. Wheeler, 1-Jan-2017.) (New usage is discouraged.)
⊢ 0 ≥ 0
21.53.3  Hyperbolic trigonometric functions It is a convention of set.mm to not use sinh and so on directly, and instead of use expansions such as (cos‘(i · 𝑥)). However, I believe it's important to give formal definitions for these conventional functions as they are typically used, so here they are. A few related identities are also proved.
Syntax	csinh 50792	Extend class notation to include the hyperbolic sine function, see df-sinh 50795.
class sinh
Syntax	ccosh 50793	Extend class notation to include the hyperbolic cosine function. see df-cosh 50796.
class cosh
Syntax	ctanh 50794	Extend class notation to include the hyperbolic tangent function, see df-tanh 50797.
class tanh
Definition	df-sinh 50795	Define the hyperbolic sine function (sinh). We define it this way for cmpt 5186, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). See sinhval-named 50798 for a simple way to evaluate it. We define this function by dividing by i, which uses fewer operations than many conventional definitions (and thus is more convenient to use in set.mm). See sinh-conventional 50801 for a justification that our definition is the same as the conventional definition of sinh used in other sources. (Contributed by David A. Wheeler, 20-Apr-2015.)
⊢ sinh = (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))
Definition	df-cosh 50796	Define the hyperbolic cosine function (cosh). We define it this way for cmpt 5186, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by David A. Wheeler, 10-May-2015.)
⊢ cosh = (𝑥 ∈ ℂ ↦ (cos‘(i · 𝑥)))
Definition	df-tanh 50797	Define the hyperbolic tangent function (tanh). We define it this way for cmpt 5186, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by David A. Wheeler, 10-May-2015.)
⊢ tanh = (𝑥 ∈ (◡cosh “ (ℂ ∖ {0})) ↦ ((tan‘(i · 𝑥)) / i))
Theorem	sinhval-named 50798	Value of the named sinh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-sinh 50795. See sinhval 16315 for a theorem to convert this further. See sinh-conventional 50801 for a justification that our definition is the same as the conventional definition of sinh used in other sources. (Contributed by David A. Wheeler, 20-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (sinh‘𝐴) = ((sin‘(i · 𝐴)) / i))
Theorem	coshval-named 50799	Value of the named cosh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-cosh 50796. See coshval 16316 for a theorem to convert this further. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ (𝐴 ∈ ℂ → (cosh‘𝐴) = (cos‘(i · 𝐴)))
Theorem	tanhval-named 50800	Value of the named tanh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-tanh 50797. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ (𝐴 ∈ (◡cosh “ (ℂ ∖ {0})) → (tanh‘𝐴) = ((tan‘(i · 𝐴)) / i))