P. 174 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17301-17400   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cmrc 17301	The class function generating Moore closures.
class mrCls
Syntax	cmri 17302	mrInd is a class function which takes a Moore system to its set of independent sets.
class mrInd
Syntax	cacs 17303	The class of algebraic closure (Moore) systems.
class ACS
Definition	df-mre 17304*	Define a Moore collection, which is a family of subsets of a base set which preserve arbitrary intersection. Elements of a Moore collection are termed closed; Moore collections generalize the notion of closedness from topologies (cldmre 22238) and vector spaces (lssmre 20237) to the most general setting in which such concepts make sense. Definition of Moore collection of sets in [Schechter] p. 78. A Moore collection may also be called a closure system (Section 0.6 in [Gratzer] p. 23.) The name Moore collection is after Eliakim Hastings Moore, who discussed these systems in Part I of [Moore] p. 53 to 76. See ismre 17308, mresspw 17310, mre1cl 17312 and mreintcl 17313 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 17318); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 17319. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.)
⊢ Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})
Definition	df-mrc 17305*	Define the Moore closure of a generating set, which is the smallest closed set containing all generating elements. Definition of Moore closure in [Schechter] p. 79. This generalizes topological closure (mrccls 22239) and linear span (mrclsp 20260). A Moore closure operation 𝑁 is (1) extensive, i.e., 𝑥 ⊆ (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcssid 17335), (2) isotone, i.e., 𝑥 ⊆ 𝑦 implies that (𝑁‘𝑥) ⊆ (𝑁‘𝑦) for all subsets 𝑥 and 𝑦 of the base set (mrcss 17334), and (3) idempotent, i.e., (𝑁‘(𝑁‘𝑥)) = (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcidm 17337.) Operators satisfying these three properties are in bijective correspondence with Moore collections, so these properties may be used to give an alternate characterization of a Moore collection by providing a closure operation 𝑁 on the set of subsets of a given base set which satisfies (1), (2), and (3); the closed sets can be recovered as those sets which equal their closures (Section 4.5 in [Schechter] p. 82.) (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by David Moews, 1-May-2017.)
⊢ mrCls = (𝑐 ∈ ∪ ran Moore ↦ (𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}))
Definition	df-mri 17306*	In a Moore system, a set is independent if no element of the set is in the closure of the set with the element removed (Section 0.6 in [Gratzer] p. 27; Definition 4.1.1 in [FaureFrolicher] p. 83.) mrInd is a class function which takes a Moore system to its set of independent sets. (Contributed by David Moews, 1-May-2017.)
⊢ mrInd = (𝑐 ∈ ∪ ran Moore ↦ {𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))})
Definition	df-acs 17307*	An important subclass of Moore systems are those which can be interpreted as closure under some collection of operators of finite arity (the collection itself is not required to be finite). These are termed algebraic closure systems; similar to definition (A) of an algebraic closure system in [Schechter] p. 84, but to avoid the complexity of an arbitrary mixed collection of functions of various arities (especially if the axiom of infinity omex 9410 is to be avoided), we consider a single function defined on finite sets instead. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
Theorem	ismre 17308*	Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) ↔ (𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀𝑠 ∈ 𝒫 𝐶(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶)))
Theorem	fnmre 17309	The Moore collection generator is a well-behaved function. Analogue for Moore collections of fntopon 22082 for topologies. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ Moore Fn V
Theorem	mresspw 17310	A Moore collection is a subset of the power of the base set; each closed subset of the system is actually a subset of the base. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋)
Theorem	mress 17311	A Moore-closed subset is a subset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → 𝑆 ⊆ 𝑋)
Theorem	mre1cl 17312	In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝐶)
Theorem	mreintcl 17313	A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ 𝐶)
Theorem	mreiincl 17314*	A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶)
Theorem	mrerintcl 17315	The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑆) ∈ 𝐶)
Theorem	mreriincl 17316*	The relative intersection of a family of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → (𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆) ∈ 𝐶)
Theorem	mreincl 17317	Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶)
Theorem	mreuni 17318	Since the entire base set of a Moore collection is the greatest element of it, the base set can be recovered from a Moore collection by set union. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) → ∪ 𝐶 = 𝑋)
Theorem	mreunirn 17319	Two ways to express the notion of being a Moore collection on an unspecified base. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ ∪ ran Moore ↔ 𝐶 ∈ (Moore‘∪ 𝐶))
Theorem	ismred 17320*	Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶 ∧ 𝑠 ≠ ∅) → ∩ 𝑠 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋))
Theorem	ismred2 17321*	Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑠) ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋))
Theorem	mremre 17322	The Moore collections of subsets of a space, viewed as a kind of subset of the power set, form a Moore collection in their own right on the power set. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝑋 ∈ 𝑉 → (Moore‘𝑋) ∈ (Moore‘𝒫 𝑋))
Theorem	submre 17323	The subcollection of a closed set system below a given closed set is itself a closed set system. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) → (𝐶 ∩ 𝒫 𝐴) ∈ (Moore‘𝐴))
7.2.1  Moore closures
Theorem	mrcflem 17324*	The domain and range of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}):𝒫 𝑋⟶𝐶)
Theorem	fnmrc 17325	Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ mrCls Fn ∪ ran Moore
Theorem	mrcfval 17326*	Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 = (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}))
Theorem	mrcf 17327	The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶)
Theorem	mrcval 17328*	Evaluation of the Moore closure of a set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Fan Zheng, 6-Jun-2016.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) = ∩ {𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠})
Theorem	mrccl 17329	The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) ∈ 𝐶)
Theorem	mrcsncl 17330	The Moore closure of a singleton is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝑋) → (𝐹‘{𝑈}) ∈ 𝐶)
Theorem	mrcid 17331	The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝐶) → (𝐹‘𝑈) = 𝑈)
Theorem	mrcssv 17332	The closure of a set is a subset of the base. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹‘𝑈) ⊆ 𝑋)
Theorem	mrcidb 17333	A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) = 𝑈))
Theorem	mrcss 17334	Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘𝑈) ⊆ (𝐹‘𝑉))
Theorem	mrcssid 17335	The closure of a set is a superset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → 𝑈 ⊆ (𝐹‘𝑈))
Theorem	mrcidb2 17336	A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) ⊆ 𝑈))
Theorem	mrcidm 17337	The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘(𝐹‘𝑈)) = (𝐹‘𝑈))
Theorem	mrcsscl 17338	The closure is the minimal closed set; any closed set which contains the generators is a superset of the closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ∈ 𝐶) → (𝐹‘𝑈) ⊆ 𝑉)
Theorem	mrcuni 17339	Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑈) = (𝐹‘∪ (𝐹 “ 𝑈)))
Theorem	mrcun 17340	Idempotence of closure under a pair union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘(𝑈 ∪ 𝑉)) = (𝐹‘((𝐹‘𝑈) ∪ (𝐹‘𝑉))))
Theorem	mrcssvd 17341	The Moore closure of a set is a subset of the base. Deduction form of mrcssv 17332. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    ⇒   ⊢ (𝜑 → (𝑁‘𝐵) ⊆ 𝑋)
Theorem	mrcssd 17342	Moore closure preserves subset ordering. Deduction form of mrcss 17334. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘𝑈) ⊆ (𝑁‘𝑉))
Theorem	mrcssidd 17343	A set is contained in its Moore closure. Deduction form of mrcssid 17335. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → 𝑈 ⊆ (𝑁‘𝑈))
Theorem	mrcidmd 17344	Moore closure is idempotent. Deduction form of mrcidm 17337. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑁‘𝑈)) = (𝑁‘𝑈))
Theorem	mressmrcd 17345	In a Moore system, if a set is between another set and its closure, the two sets have the same closure. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇))    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))
Theorem	submrc 17346	In a closure system which is cut off above some level, closures below that level act as normal. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    &   ⊢ 𝐺 = (mrCls‘(𝐶 ∩ 𝒫 𝐷))    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐷 ∈ 𝐶 ∧ 𝑈 ⊆ 𝐷) → (𝐺‘𝑈) = (𝐹‘𝑈))
Theorem	mrieqvlemd 17347	In a Moore system, if 𝑌 is a member of 𝑆, (𝑆 ∖ {𝑌}) and 𝑆 have the same closure if and only if 𝑌 is in the closure of (𝑆 ∖ {𝑌}). Used in the proof of mrieqvd 17356 and mrieqv2d 17357. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})) ↔ (𝑁‘(𝑆 ∖ {𝑌})) = (𝑁‘𝑆)))
7.2.2  Independent sets in a Moore system
Theorem	mrisval 17348*	Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    ⇒   ⊢ (𝐴 ∈ (Moore‘𝑋) → 𝐼 = {𝑠 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))})
Theorem	ismri 17349*	Criterion for a set to be an independent set of a Moore system. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    ⇒   ⊢ (𝐴 ∈ (Moore‘𝑋) → (𝑆 ∈ 𝐼 ↔ (𝑆 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))))
Theorem	ismri2 17350*	Criterion for a subset of the base set in a Moore system to be independent. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    ⇒   ⊢ ((𝐴 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))))
Theorem	ismri2d 17351*	Criterion for a subset of the base set in a Moore system to be independent. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))))
Theorem	ismri2dd 17352*	Definition of independence of a subset of the base set in a Moore system. One-way deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))    ⇒   ⊢ (𝜑 → 𝑆 ∈ 𝐼)
Theorem	mriss 17353	An independent set of a Moore system is a subset of the base set. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐼 = (mrInd‘𝐴)    ⇒   ⊢ ((𝐴 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐼) → 𝑆 ⊆ 𝑋)
Theorem	mrissd 17354	An independent set of a Moore system is a subset of the base set. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)
Theorem	ismri2dad 17355	Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})))
Theorem	mrieqvd 17356*	In a Moore system, a set is independent if and only if, for all elements of the set, the closure of the set with the element removed is unequal to the closure of the original set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁‘𝑆)))
Theorem	mrieqv2d 17357*	In a Moore system, a set is independent if and only if all its proper subsets have closure properly contained in the closure of the set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆))))
Theorem	mrissmrcd 17358	In a Moore system, if an independent set is between a set and its closure, the two sets are equal (since the two sets must have equal closures by mressmrcd 17345, and so are equal by mrieqv2d 17357.) (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇))    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝑆 = 𝑇)
Theorem	mrissmrid 17359	In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝑇 ∈ 𝐼)
Theorem	mreexd 17360*	In a Moore system, the closure operator is said to have the exchange property if, for all elements 𝑦 and 𝑧 of the base set and subsets 𝑆 of the base set such that 𝑧 is in the closure of (𝑆 ∪ {𝑦}) but not in the closure of 𝑆, 𝑦 is in the closure of (𝑆 ∪ {𝑧}) (Definition 3.1.9 in [FaureFrolicher] p. 57 to 58.) This theorem allows us to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))    &   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆))    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍})))
Theorem	mreexmrid 17361*	In a Moore system whose closure operator has the exchange property, if a set is independent and an element is not in its closure, then adding the element to the set gives another independent set. Lemma 4.1.5 in [FaureFrolicher] p. 84. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘𝑆))    ⇒   ⊢ (𝜑 → (𝑆 ∪ {𝑌}) ∈ 𝐼)
Theorem	mreexexlemd 17362*	This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 17366. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → (𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾))    &   ⊢ (𝜑 → ∀𝑡∀𝑢 ∈ 𝒫 (𝑋 ∖ 𝑡)∀𝑣 ∈ 𝒫 (𝑋 ∖ 𝑡)(((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼)))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexexlem2d 17363*	Used in mreexexlem4d 17365 to prove the induction step in mreexexd 17366. See the proof of Proposition 4.2.1 in [FaureFrolicher] p. 86 to 87. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝐺 (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼))
Theorem	mreexexlem3d 17364*	Base case of the induction in mreexexd 17366. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → (𝐹 = ∅ ∨ 𝐺 = ∅))    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ 𝒫 𝐺(𝐹 ≈ 𝑖 ∧ (𝑖 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexexlem4d 17365*	Induction step of the induction in mreexexd 17366. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → 𝐿 ∈ ω)    &   ⊢ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐿 ∨ 𝑔 ≈ 𝐿) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼)))    &   ⊢ (𝜑 → (𝐹 ≈ suc 𝐿 ∨ 𝐺 ≈ suc 𝐿))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexexd 17366*	Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if 𝐹 and 𝐺 are disjoint from 𝐻, (𝐹 ∪ 𝐻) is independent, 𝐹 is contained in the closure of (𝐺 ∪ 𝐻), and either 𝐹 or 𝐺 is finite, then there is a subset 𝑞 of 𝐺 equinumerous to 𝐹 such that (𝑞 ∪ 𝐻) is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either (𝐴 ∖ 𝐵) or (𝐵 ∖ 𝐴) is finite. The theorem is proven by induction using mreexexlem3d 17364 for the base case and mreexexlem4d 17365 for the induction step. (Contributed by David Moews, 1-May-2017.) Remove dependencies on ax-rep 5210 and ax-ac2 10228. (Revised by Brendan Leahy, 2-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin))    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹 ≈ 𝑞 ∧ (𝑞 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexdomd 17367*	In a Moore system whose closure operator has the exchange property, if 𝑆 is independent and contained in the closure of 𝑇, and either 𝑆 or 𝑇 is finite, then 𝑇 dominates 𝑆. This is an immediate consequence of mreexexd 17366. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇))    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑆 ∈ Fin ∨ 𝑇 ∈ Fin))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝑆 ≼ 𝑇)
Theorem	mreexfidimd 17368*	In a Moore system whose closure operator has the exchange property, if two independent sets have equal closure and one is finite, then they are equinumerous. Proven by using mreexdomd 17367 twice. This implies a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
7.2.3  Algebraic closure systems
Theorem	isacs 17369*	A set is an algebraic closure system iff it is specified by some function of the finite subsets, such that a set is closed iff it does not expand under the operation. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))))
Theorem	acsmre 17370	Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋))
Theorem	isacs2 17371*	In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑠)))
Theorem	acsfiel 17372*	A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (ACS‘𝑋) → (𝑆 ∈ 𝐶 ↔ (𝑆 ⊆ 𝑋 ∧ ∀𝑦 ∈ (𝒫 𝑆 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑆)))
Theorem	acsfiel2 17373*	A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑆 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑆))
Theorem	acsmred 17374	An algebraic closure system is also a Moore system. Deduction form of acsmre 17370. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))
Theorem	isacs1i 17375*	A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (ACS‘𝑋))
Theorem	mreacs 17376	Algebraicity is a composable property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))
Theorem	acsfn 17377*	Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋) ∧ (𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇 ⊆ 𝑎 → 𝐾 ∈ 𝑎)} ∈ (ACS‘𝑋))
Theorem	acsfn0 17378*	Algebraicity of a point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ 𝐾 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	acsfn1 17379*	Algebraicity of a one-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	acsfn1c 17380*	Algebraicity of a one-argument closure condition with additional constant. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝐾 ∀𝑐 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝐾 ∀𝑐 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	acsfn2 17381*	Algebraicity of a two-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
PART 8  BASIC CATEGORY THEORY
8.1  Categories
8.1.1  Categories
Syntax	ccat 17382	Extend class notation with the class of categories.
class Cat
Syntax	ccid 17383	Extend class notation with the identity arrow of a category.
class Id
Syntax	chomf 17384	Extend class notation to include functionalized Hom-set extractor.
class Homf
Syntax	ccomf 17385	Extend class notation to include functionalized composition operation.
class compf
Definition	df-cat 17386*	A category is an abstraction of a structure (a group, a topology, an order...) Category theory consists in finding new formulation of the concepts associated with those structures (product, substructure...) using morphisms instead of the belonging relation. That trick has the interesting property that heterogeneous structures like topologies or groups for instance become comparable. Definition in [Lang] p. 53, without the axiom CAT 1, i.e., pairwise disjointness of hom-sets (cat1 17821). See setc2obas 17818 and setc2ohom 17819 for a counterexample. In contrast to definition 3.1 of [Adamek] p. 21, where "A category is a quadruple A = (O, hom, id, o)", a category is defined as an extensible structure consisting of three slots: the objects "O" ((Base‘𝑐)), the morphisms "hom" ((Hom ‘𝑐)) and the composition law "o" ((comp‘𝑐)). The identities "id" are defined by their properties related to morphisms and their composition, see condition 3.1(b) in [Adamek] p. 21 and df-cid 17387. (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)
⊢ Cat = {𝑐 ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))))}
Definition	df-cid 17387*	Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ Id = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))
Definition	df-homf 17388*	Define the functionalized Hom-set operator, which is exactly like Hom but is guaranteed to be a function on the base. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Homf = (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦)))
Definition	df-comf 17389*	Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ compf = (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))))
Theorem	iscat 17390*	The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))))))
Theorem	iscatd 17391*	Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈ (𝑥𝐻𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(⟨𝑥, 𝑥⟩ · 𝑦) 1 ) = 𝑓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    &   ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	catidex 17392*	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋⟩ · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋⟩ · 𝑦)𝑔) = 𝑓))
Theorem	catideu 17393*	Each object in a category has a unique identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋⟩ · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋⟩ · 𝑦)𝑔) = 𝑓))
Theorem	cidfval 17394*	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝜑 → 1 = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓))))
Theorem	cidval 17395*	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = (℩𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋⟩ · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋⟩ · 𝑦)𝑔) = 𝑓)))
Theorem	cidffn 17396	The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ Id Fn Cat
Theorem	cidfn 17397	The identity arrow operator is a function from objects to arrows. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → 1 Fn 𝐵)
Theorem	catidd 17398*	Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈ (𝑥𝐻𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(⟨𝑥, 𝑥⟩ · 𝑦) 1 ) = 𝑓)    ⇒   ⊢ (𝜑 → (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ 1 ))
Theorem	iscatd2 17399*	Version of iscatd 17391 with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1 ∈ (𝑦𝐻𝑦))    &   ⊢ ((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    &   ⊢ ((𝜑 ∧ 𝜓) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))    ⇒   ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 )))
Theorem	catidcl 17400	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐻𝑋))