P. 511 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 51001-51100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lanfval 51001*	Value of the function generating the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ Lan 𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (𝐶 Func 𝐸) ↦ ((⟨𝐷, 𝐸⟩ −∘F 𝑓)(𝑅 UP 𝑆)𝑥)))
Theorem	ranfval 51002*	Value of the function generating the set of right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ 𝑂 = (oppCat‘𝑅)    &   ⊢ 𝑃 = (oppCat‘𝑆)    ⇒   ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ Ran 𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (𝐶 Func 𝐸) ↦ (( oppFunc ‘(⟨𝐷, 𝐸⟩ −∘F 𝑓))(𝑂 UP 𝑃)𝑥)))
Theorem	lanpropd 51003	If the categories have the same set of objects, morphisms, and compositions, then they have the same left Kan extensions. (Contributed by Zhi Wang, 21-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → (Homf ‘𝐸) = (Homf ‘𝐹))    &   ⊢ (𝜑 → (compf‘𝐸) = (compf‘𝐹))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐶⟩ Lan 𝐸) = (⟨𝐵, 𝐷⟩ Lan 𝐹))
Theorem	ranpropd 51004	If the categories have the same set of objects, morphisms, and compositions, then they have the same right Kan extensions. (Contributed by Zhi Wang, 21-Nov-2025.)
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))    &   ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → (Homf ‘𝐸) = (Homf ‘𝐹))    &   ⊢ (𝜑 → (compf‘𝐸) = (compf‘𝐹))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐶⟩ Ran 𝐸) = (⟨𝐵, 𝐷⟩ Ran 𝐹))
Theorem	reldmlan2 51005	The domain of (𝑃 Lan 𝐸) is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel dom (𝑃 Lan 𝐸)
Theorem	reldmran2 51006	The domain of (𝑃 Ran 𝐸) is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel dom (𝑃 Ran 𝐸)
Theorem	lanval 51007	Value of the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = 𝐾)    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) = (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	ranval 51008	Value of the set of right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐽, 𝐾⟩)    &   ⊢ 𝑂 = (oppCat‘𝑅)    &   ⊢ 𝑃 = (oppCat‘𝑆)    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) = (⟨𝐽, tpos 𝐾⟩(𝑂 UP 𝑃)𝑋))
Theorem	lanrcl 51009	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (𝐶 Func 𝐸)))
Theorem	ranrcl 51010	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (𝐶 Func 𝐸)))
Theorem	rellan 51011	The set of left Kan extensions is a relation. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ Rel (𝐹(𝑃 Lan 𝐸)𝑋)
Theorem	relran 51012	The set of right Kan extensions is a relation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ Rel (𝐹(𝑃 Ran 𝐸)𝑋)
Theorem	islan 51013	A left Kan extension is a universal pair. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐿 ∈ (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) → 𝐿 ∈ (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	islan2 51014	A left Kan extension is a universal pair. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴 → 𝐿(𝐾(𝑅 UP 𝑆)𝑋)𝐴)
Theorem	lanval2 51015	The set of left Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by isup2 50515 and upciclem1 50487. (Contributed by Zhi Wang, 3-Nov-2025.)
⊢ 𝑅 = (𝐷 FuncCat 𝐸)    &   ⊢ 𝑆 = (𝐶 FuncCat 𝐸)    &   ⊢ 𝐾 = (⟨𝐷, 𝐸⟩ −∘F 𝐹)    ⇒   ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) = (𝐾(𝑅 UP 𝑆)𝑋))
Theorem	isran 51016	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 51017	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 51018	The set of right Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by oppcup2 50529 and oppcup3lem 50527. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ 𝑂 = (oppCat‘(𝐷 FuncCat 𝐸))    &   ⊢ 𝑃 = (oppCat‘(𝐶 FuncCat 𝐸))    &   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨𝐽, 𝐾⟩)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))    ⇒   ⊢ (𝜑 → (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) = (⟨𝐽, tpos 𝐾⟩(𝑂 UP 𝑃)𝑋))
Theorem	ranval3 51019	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 51020	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
Theorem	lanrcl3 51021	Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))
Theorem	lanrcl4 51022	The first component of a left Kan extension is a functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))
Theorem	lanrcl5 51023	The second component of a left Kan extension is a natural transformation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋)𝐴)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝑁(𝐿 ∘func 𝐹)))
Theorem	ranrcl2 51024	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
Theorem	ranrcl3 51025	Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐶 Func 𝐸))
Theorem	ranrcl4lem 51026	Lemma for ranrcl4 51027 and ranrcl5 51028. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → (⟨𝐷, 𝐸⟩ −∘F 𝐹) = ⟨(1st ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹)), (2nd ‘(⟨𝐷, 𝐸⟩ −∘F 𝐹))⟩)
Theorem	ranrcl4 51027	The first component of a right Kan extension is a functor. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐷 Func 𝐸))
Theorem	ranrcl5 51028	The second component of a right Kan extension is a natural transformation. (Contributed by Zhi Wang, 4-Nov-2025.)
⊢ (𝜑 → 𝐿(𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋)𝐴)    &   ⊢ 𝑁 = (𝐶 Nat 𝐸)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ((𝐿 ∘func 𝐹)𝑁𝑋))
Theorem	lanup 51029*	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 51030*	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.53.17.2  Limits and colimits
Syntax	clmd 51031	Class function defining the limit of a diagram.
class Limit
Syntax	ccmd 51032	Class function defining the colimit of a diagram.
class Colimit
Definition	df-lmd 51033*	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 51049). The naturality guarantees that the combination of the diagram with the cone must commute (concom 51051). 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 51053). Definition 11.3(2) of [Adamek] p. 194. Terminal objects (termolmd 51058), products, equalizers, pullbacks, and inverse limits can be considered as limits of some diagram; limits can be further generalized as right Kan extensions (lmdran 51059). "lmd" is short for "limit of a diagram". See df-cmd 51034 for the dual concept (lmddu 51055, cmddu 51056). (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Limit = (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ (( oppFunc ‘(𝑐Δfunc𝑑))((oppCat‘𝑐) UP (oppCat‘(𝑑 FuncCat 𝑐)))𝑓)))
Definition	df-cmd 51034*	A co-cone (or cocone) to a diagram (see df-lmd 51033 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 51050). The naturality guarantees that the combination of the diagram with the co-cone must commute (coccom 51052). 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 51054). Definition 11.27(2) of [Adamek] p. 202. Initial objects (initocmd 51057), coproducts, coequalizers, pushouts, and direct limits can be considered as colimits of some diagram; colimits can be further generalized as left Kan extensions (cmdlan 51060). "cmd" is short for "colimit of a diagram". See df-lmd 51033 for the dual concept (lmddu 51055, cmddu 51056). (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Colimit = (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((𝑐Δfunc𝑑)(𝑐 UP (𝑑 FuncCat 𝑐))𝑓)))
Theorem	reldmlmd 51035	The domain of Limit is a relation. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Rel dom Limit
Theorem	reldmcmd 51036	The domain of Colimit is a relation. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ Rel dom Colimit
Theorem	lmdfval 51037*	Function value of Limit. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ (𝐶 Limit 𝐷) = (𝑓 ∈ (𝐷 Func 𝐶) ↦ (( oppFunc ‘(𝐶Δfunc𝐷))((oppCat‘𝐶) UP (oppCat‘(𝐷 FuncCat 𝐶)))𝑓))
Theorem	cmdfval 51038*	Function value of Colimit. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ (𝐶 Colimit 𝐷) = (𝑓 ∈ (𝐷 Func 𝐶) ↦ ((𝐶Δfunc𝐷)(𝐶 UP (𝐷 FuncCat 𝐶))𝑓))
Theorem	lmdrcl 51039	Reverse closure for a limit of a diagram. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝑋 ∈ ((𝐶 Limit 𝐷)‘𝐹) → 𝐹 ∈ (𝐷 Func 𝐶))
Theorem	cmdrcl 51040	Reverse closure for a colimit of a diagram. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝑋 ∈ ((𝐶 Colimit 𝐷)‘𝐹) → 𝐹 ∈ (𝐷 Func 𝐶))
Theorem	reldmlmd2 51041	The domain of (𝐶 Limit 𝐷) is a relation. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ Rel dom (𝐶 Limit 𝐷)
Theorem	reldmcmd2 51042	The domain of (𝐶 Colimit 𝐷) is a relation. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ Rel dom (𝐶 Colimit 𝐷)
Theorem	lmdfval2 51043	The set of limits of a diagram. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ ((𝐶 Limit 𝐷)‘𝐹) = (( oppFunc ‘(𝐶Δfunc𝐷))((oppCat‘𝐶) UP (oppCat‘(𝐷 FuncCat 𝐶)))𝐹)
Theorem	cmdfval2 51044	The set of colimits of a diagram. (Contributed by Zhi Wang, 12-Nov-2025.)
⊢ ((𝐶 Colimit 𝐷)‘𝐹) = ((𝐶Δfunc𝐷)(𝐶 UP (𝐷 FuncCat 𝐶))𝐹)
Theorem	lmdpropd 51045	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 51046	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 51047	The set of limits of a diagram is a relation. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ Rel ((𝐶 Limit 𝐷)‘𝐹)
Theorem	relcmd 51048	The set of colimits of a diagram is a relation. (Contributed by Zhi Wang, 13-Nov-2025.)
⊢ Rel ((𝐶 Colimit 𝐷)‘𝐹)
Theorem	concl 51049	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 51050	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 51051	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 51052	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 51053*	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 51054*	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 51055	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 51056	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 51057	Initial objects are the object part of colimits of the empty diagram. (Contributed by Zhi Wang, 17-Nov-2025.)
⊢ (InitO‘𝐶) = dom (∅(𝐶 Colimit ∅)∅)
Theorem	termolmd 51058	Terminal objects are the object part of limits of the empty diagram. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (TermO‘𝐶) = dom (∅(𝐶 Limit ∅)∅)
Theorem	lmdran 51059	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 50874). (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ (𝜑 → 1 ∈ TermCat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 1 ))    &   ⊢ 𝐿 = (𝐶Δfunc 1 )    &   ⊢ (𝜑 → 𝑌 = ((1st ‘𝐿)‘𝑋))    ⇒   ⊢ (𝜑 → (𝑋((𝐶 Limit 𝐷)‘𝐹)𝑀 ↔ 𝑌(𝐺(⟨𝐷, 1 ⟩ Ran 𝐶)𝐹)𝑀))
Theorem	cmdlan 51060	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 50874). (Contributed by Zhi Wang, 26-Nov-2025.)
⊢ (𝜑 → 1 ∈ TermCat)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 1 ))    &   ⊢ 𝐿 = (𝐶Δfunc 1 )    &   ⊢ (𝜑 → 𝑌 = ((1st ‘𝐿)‘𝑋))    ⇒   ⊢ (𝜑 → (𝑋((𝐶 Colimit 𝐷)‘𝐹)𝑀 ↔ 𝑌(𝐺(⟨𝐷, 1 ⟩ Lan 𝐶)𝐹)𝑀))
21.54  Mathbox for Emmett Weisz
21.54.1  Miscellaneous Theorems Some of these theorems are used in the series of lemmas and theorems proving the defining properties of setrecs.
Theorem	nfintd 51061	Bound-variable hypothesis builder for intersection. (Contributed by Emmett Weisz, 16-Jan-2020.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∩ 𝐴)
Theorem	nfiund 51062*	Bound-variable hypothesis builder for indexed union. (Contributed by Emmett Weisz, 6-Dec-2019.) Add disjoint variable condition to avoid ax-13 2404. See nfiundg 51063 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝐴)    &   ⊢ (𝜑 → Ⅎ𝑦𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	nfiundg 51063	Bound-variable hypothesis builder for indexed union. Usage of this theorem is discouraged because it depends on ax-13 2404, see nfiund 51062 for a weaker version that does not require it. (Contributed by Emmett Weisz, 6-Dec-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝐴)    &   ⊢ (𝜑 → Ⅎ𝑦𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunord 51064*	The indexed union of a collection of ordinal numbers 𝐵(𝑥) is ordinal. This proof is based on the proof of ssorduni 7817, but does not use it directly, since ssorduni 7817 does not work when 𝐵 is a proper class. (Contributed by Emmett Weisz, 3-Nov-2019.)
⊢ (∀𝑥 ∈ 𝐴 Ord 𝐵 → Ord ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunordi 51065*	The indexed union of a collection of ordinal numbers 𝐵(𝑥) is ordinal. (Contributed by Emmett Weisz, 3-Nov-2019.)
⊢ Ord 𝐵    ⇒   ⊢ Ord ∪ 𝑥 ∈ 𝐴 𝐵
Theorem	spd 51066	Specialization deduction, using implicit substitution. Based on the proof of spimed 2420. (Contributed by Emmett Weisz, 17-Jan-2020.)
⊢ (𝜒 → Ⅎ𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜒 → (∀𝑥𝜑 → 𝜓))
Theorem	tfis2d 51067*	Transfinite Induction Schema, using implicit substitution. (Contributed by Emmett Weisz, 3-May-2020.)
⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    &   ⊢ (𝜑 → (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜒 → 𝜓)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ On → 𝜓))
21.54.2  Examples and properties of set recursion
Theorem	setrecseq 51068	Equality theorem for set recursion. (Contributed by Emmett Weisz, 17-Feb-2021.)
⊢ (𝐹 = 𝐺 → setrecs(𝐹) = setrecs(𝐺))
Theorem	nfsetrecs 51069	Bound-variable hypothesis builder for setrecs. (Contributed by Emmett Weisz, 21-Oct-2021.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥setrecs(𝐹)
Theorem	setrec2mpt 51070*	Version of setrec2 10004 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 51071*	Version of setrec2 10004 expressed as an induction schema. This theorem is a generalization of tfis3 7893. (Contributed by Emmett Weisz, 27-Feb-2022.)
⊢ 𝐵 = setrecs(𝐹)    &   ⊢ (𝑏 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑎(∀𝑏 ∈ 𝑎 𝜓 → ∀𝑏 ∈ (𝐹‘𝑎)𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝜒))
Theorem	elsetrecslem 51072*	Lemma for elsetrecs 51073. Any element of setrecs(𝐹) is generated by some subset of setrecs(𝐹). This is much weaker than setrec2v 10005. To see why this lemma also requires setrec1 9999, 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 51073*	A set 𝐴 is an element of setrecs(𝐹) iff 𝐴 is generated by some subset of setrecs(𝐹). The proof requires both setrec1 9999 and setrec2 10004, 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 51074	The setrecs operator respects the subset relation between two functions 𝐹 and 𝐺. (Contributed by Emmett Weisz, 13-Mar-2022.)
⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐺)    ⇒   ⊢ (𝜑 → setrecs(𝐹) ⊆ setrecs(𝐺))
Theorem	setrecsres 51075	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 51076	Construct V using set recursion. The proof indirectly uses trcl 9756, which relies on rec, but theoretically 𝐶 in trcl 9756 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 51077	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 51078*	Lemma for onsetrec 51081. (Contributed by Emmett Weisz, 22-Jun-2021.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ V ↦ {∪ 𝑥, suc ∪ 𝑥})    ⇒   ⊢ (𝐹‘𝑎) = {∪ 𝑎, suc ∪ 𝑎}
Theorem	onsetreclem2 51079*	Lemma for onsetrec 51081. (Contributed by Emmett Weisz, 22-Jun-2021.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ V ↦ {∪ 𝑥, suc ∪ 𝑥})    ⇒   ⊢ (𝑎 ⊆ On → (𝐹‘𝑎) ⊆ On)
Theorem	onsetreclem3 51080*	Lemma for onsetrec 51081. (Contributed by Emmett Weisz, 22-Jun-2021.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ V ↦ {∪ 𝑥, suc ∪ 𝑥})    ⇒   ⊢ (𝑎 ∈ On → 𝑎 ∈ (𝐹‘𝑎))
Theorem	onsetrec 51081	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 51079 and onsetreclem3 51080 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 36732. 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.54.3  Construction of Games and Surreal Numbers Model organization after organization of reals - see TOC
Syntax	cpg 51082	Extend class notation to include the class of partisan game forms.
class Pg
Definition	df-pg 51083	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 51084*	Lemma for elpg 51087. (Contributed by Emmett Weisz, 28-Aug-2021.)
⊢ (∃𝑥(𝑥 ⊆ Pg ∧ ((1st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2nd ‘𝐴) ∈ 𝒫 𝑥)) → ((1st ‘𝐴) ⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg))
Theorem	elpglem2 51085*	Lemma for elpg 51087. (Contributed by Emmett Weisz, 28-Aug-2021.)
⊢ (((1st ‘𝐴) ⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg) → ∃𝑥(𝑥 ⊆ Pg ∧ ((1st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2nd ‘𝐴) ∈ 𝒫 𝑥)))
Theorem	elpglem3 51086*	Lemma for elpg 51087. (Contributed by Emmett Weisz, 28-Aug-2021.)
⊢ (∃𝑥(𝑥 ⊆ Pg ∧ 𝐴 ∈ ((𝑦 ∈ V ↦ (𝒫 𝑦 × 𝒫 𝑦))‘𝑥)) ↔ (𝐴 ∈ (V × V) ∧ ∃𝑥(𝑥 ⊆ Pg ∧ ((1st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2nd ‘𝐴) ∈ 𝒫 𝑥))))
Theorem	elpg 51087	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 51088	Lemma for pgind 51090. (Contributed by Emmett Weisz, 27-May-2024.) (New usage is discouraged.)
⊢ (𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧) → ((1st ‘𝑥) ∪ (2nd ‘𝑥)) ⊆ 𝑧)
Theorem	pgindnf 51089*	Version of pgind 51090 with extraneous not-free requirements. (Contributed by Emmett Weisz, 27-May-2024.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐴 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → ∀𝑥(∀𝑦 ∈ ((1st ‘𝑥) ∪ (2nd ‘𝑥))𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ∈ Pg → 𝜃))
Theorem	pgind 51090*	Induction on partizan games. (Contributed by Emmett Weisz, 27-May-2024.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐴 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → ∀𝑥(∀𝑦 ∈ ((1st ‘𝑥) ∪ (2nd ‘𝑥))𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ∈ Pg → 𝜃))
21.55  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.55.1  Natural deduction
Theorem	sbidd 51091	An identity theorem for substitution. See sbid 2294. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
⊢ (𝜑 → [𝑥 / 𝑥]𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	sbidd-misc 51092	An identity theorem for substitution. See sbid 2294. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
⊢ ((𝜑 → [𝑥 / 𝑥]𝜓) ↔ (𝜑 → 𝜓))
21.55.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 51093	Extend wff notation to include the 'greater than or equal to' relation, see df-gte 51095.
class ≥
Syntax	cgt 51094	Extend wff notation to include the 'greater than' relation, see df-gt 51096.
class >
Definition	df-gte 51095	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 11376. 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 51096), 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 51097 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 51096	The 'greater than' relation is merely the converse of the 'less than or equal to' relation defined by df-lt 11240. Defined in ISO 80000-2:2009(E) operation 2-7.12. See df-gte 51095 for a discussion on why this approach is used for the definition. See gt-lt 51098 and gt-lth 51100 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 51097	Simple relationship between ≤ and ≥. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≥ 𝐵 ↔ 𝐵 ≤ 𝐴))
Theorem	gt-lt 51098	Simple relationship between < and >. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 > 𝐵 ↔ 𝐵 < 𝐴))
Theorem	gte-lteh 51099	Relationship between ≤ and ≥ using hypotheses. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≥ 𝐵 ↔ 𝐵 ≤ 𝐴)
Theorem	gt-lth 51100	Relationship between < and > using hypotheses. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 > 𝐵 ↔ 𝐵 < 𝐴)