P. 176 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17501-17600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	qusaddval 17501*	The addition in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusaddf 17502*	The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	qusmulval 17503*	The multiplication in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusmulf 17504*	The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	fnpr2o 17505	Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o)
Theorem	fnpr2ob 17506	Biconditional version of fnpr2o 17505. (Contributed by Jim Kingdon, 27-Sep-2023.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o)
Theorem	fvpr0o 17507	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ (𝐴 ∈ 𝑉 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅) = 𝐴)
Theorem	fvpr1o 17508	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ (𝐵 ∈ 𝑉 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o) = 𝐵)
Theorem	fvprif 17509	The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵))
Theorem	xpsfrnel 17510*	Elementhood in the target space of the function 𝐹 appearing in xpsval 17518. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐺 ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))
Theorem	xpsfeq 17511	A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (𝐺 Fn 2o → {⟨∅, (𝐺‘∅)⟩, ⟨1o, (𝐺‘1o)⟩} = 𝐺)
Theorem	xpsfrnel2 17512*	Elementhood in the target space of the function 𝐹 appearing in xpsval 17518. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ ({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩} ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))
Theorem	xpscf 17513	Equivalent condition for the pair function to be a proper function on 𝐴. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩}:2o⟶𝐴 ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴))
Theorem	xpsfval 17514*	The value of the function appearing in xpsval 17518. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐹𝑌) = {⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩})
Theorem	xpsff1o 17515*	The function appearing in xpsval 17518 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {∅, 1o}. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    ⇒   ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)
Theorem	xpsfrn 17516*	A short expression for the indexed cartesian product on two indices. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    ⇒   ⊢ ran 𝐹 = X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)
Theorem	xpsff1o2 17517*	The function appearing in xpsval 17518 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {∅, 1o}. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    ⇒   ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→ran 𝐹
Theorem	xpsval 17518*	Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝑈 = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})    ⇒   ⊢ (𝜑 → 𝑇 = (◡𝐹 “s 𝑈))
Theorem	xpsrnbas 17519*	The indexed structure product that appears in xpsval 17518 has the same base as the target of the function 𝐹. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝑈 = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})    ⇒   ⊢ (𝜑 → ran 𝐹 = (Base‘𝑈))
Theorem	xpsbas 17520	The base set of the binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇))
Theorem	xpsaddlem 17521*	Lemma for xpsadd 17522 and xpsmul 17523. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋)    &   ⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌)    &   ⊢ · = (𝐸‘𝑅)    &   ⊢ × = (𝐸‘𝑆)    &   ⊢ ∙ = (𝐸‘𝑇)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    &   ⊢ 𝑈 = ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})    &   ⊢ ((𝜑 ∧ {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ∈ ran 𝐹 ∧ {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩} ∈ ran 𝐹) → ((◡𝐹‘{⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}) ∙ (◡𝐹‘{⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})) = (◡𝐹‘({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} (𝐸‘𝑈){⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})))    &   ⊢ (({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o ∧ {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ∈ (Base‘𝑈) ∧ {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩} ∈ (Base‘𝑈)) → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} (𝐸‘𝑈){⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}) = (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(𝐸‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))))    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩ ∙ ⟨𝐶, 𝐷⟩) = ⟨(𝐴 · 𝐶), (𝐵 × 𝐷)⟩)
Theorem	xpsadd 17522	Value of the addition operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋)    &   ⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌)    &   ⊢ · = (+g‘𝑅)    &   ⊢ × = (+g‘𝑆)    &   ⊢ ∙ = (+g‘𝑇)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩ ∙ ⟨𝐶, 𝐷⟩) = ⟨(𝐴 · 𝐶), (𝐵 × 𝐷)⟩)
Theorem	xpsmul 17523	Value of the multiplication operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋)    &   ⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑆)    &   ⊢ ∙ = (.r‘𝑇)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩ ∙ ⟨𝐶, 𝐷⟩) = ⟨(𝐴 · 𝐶), (𝐵 × 𝐷)⟩)
Theorem	xpssca 17524	Value of the scalar field of a binary structure product. For concreteness, we choose the scalar field to match the left argument, but in most cases where this slot is meaningful both factors will have the same scalar field, so that it doesn't matter which factor is chosen. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐺 = (Scalar‘𝑇))
Theorem	xpsvsca 17525	Value of the scalar multiplication function in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ × = ( ·𝑠 ‘𝑆)    &   ⊢ ∙ = ( ·𝑠 ‘𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑌)    &   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑋)    &   ⊢ (𝜑 → (𝐴 × 𝐶) ∈ 𝑌)    ⇒   ⊢ (𝜑 → (𝐴 ∙ ⟨𝐵, 𝐶⟩) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩)
Theorem	xpsless 17526	Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ ≤ = (le‘𝑇)    ⇒   ⊢ (𝜑 → ≤ ⊆ ((𝑋 × 𝑌) × (𝑋 × 𝑌)))
Theorem	xpsle 17527	Value of the ordering in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ ≤ = (le‘𝑇)    &   ⊢ 𝑀 = (le‘𝑅)    &   ⊢ 𝑁 = (le‘𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩ ≤ ⟨𝐶, 𝐷⟩ ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷)))
7.2  Moore spaces
Syntax	cmre 17528	The class of Moore systems.
class Moore
Syntax	cmrc 17529	The class function generating Moore closures.
class mrCls
Syntax	cmri 17530	mrInd is a class function which takes a Moore system to its set of independent sets.
class mrInd
Syntax	cacs 17531	The class of algebraic closure (Moore) systems.
class ACS
Definition	df-mre 17532*	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 22589) and vector spaces (lssmre 20582) 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 17536, mresspw 17538, mre1cl 17540 and mreintcl 17541 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 17546); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 17547. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.)
⊢ Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})
Definition	df-mrc 17533*	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 22590) and linear span (mrclsp 20605). A Moore closure operation 𝑁 is (1) extensive, i.e., 𝑥 ⊆ (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcssid 17563), (2) isotone, i.e., 𝑥 ⊆ 𝑦 implies that (𝑁‘𝑥) ⊆ (𝑁‘𝑦) for all subsets 𝑥 and 𝑦 of the base set (mrcss 17562), and (3) idempotent, i.e., (𝑁‘(𝑁‘𝑥)) = (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcidm 17565.) 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 17534*	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 17535*	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 9640 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 17536*	Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) ↔ (𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀𝑠 ∈ 𝒫 𝐶(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶)))
Theorem	fnmre 17537	The Moore collection generator is a well-behaved function. Analogue for Moore collections of fntopon 22433 for topologies. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ Moore Fn V
Theorem	mresspw 17538	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 17539	A Moore-closed subset is a subset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → 𝑆 ⊆ 𝑋)
Theorem	mre1cl 17540	In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝐶)
Theorem	mreintcl 17541	A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ 𝐶)
Theorem	mreiincl 17542*	A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶)
Theorem	mrerintcl 17543	The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑆) ∈ 𝐶)
Theorem	mreriincl 17544*	The relative intersection of a family of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → (𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆) ∈ 𝐶)
Theorem	mreincl 17545	Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶)
Theorem	mreuni 17546	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 17547	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 17548*	Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶 ∧ 𝑠 ≠ ∅) → ∩ 𝑠 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋))
Theorem	ismred2 17549*	Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑠) ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋))
Theorem	mremre 17550	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 17551	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 17552*	The domain and codomain of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}):𝒫 𝑋⟶𝐶)
Theorem	fnmrc 17553	Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ mrCls Fn ∪ ran Moore
Theorem	mrcfval 17554*	Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 = (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}))
Theorem	mrcf 17555	The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶)
Theorem	mrcval 17556*	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 17557	The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) ∈ 𝐶)
Theorem	mrcsncl 17558	The Moore closure of a singleton is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝑋) → (𝐹‘{𝑈}) ∈ 𝐶)
Theorem	mrcid 17559	The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝐶) → (𝐹‘𝑈) = 𝑈)
Theorem	mrcssv 17560	The closure of a set is a subset of the base. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹‘𝑈) ⊆ 𝑋)
Theorem	mrcidb 17561	A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) = 𝑈))
Theorem	mrcss 17562	Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘𝑈) ⊆ (𝐹‘𝑉))
Theorem	mrcssid 17563	The closure of a set is a superset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → 𝑈 ⊆ (𝐹‘𝑈))
Theorem	mrcidb2 17564	A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) ⊆ 𝑈))
Theorem	mrcidm 17565	The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘(𝐹‘𝑈)) = (𝐹‘𝑈))
Theorem	mrcsscl 17566	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 17567	Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑈) = (𝐹‘∪ (𝐹 “ 𝑈)))
Theorem	mrcun 17568	Idempotence of closure under a pair union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘(𝑈 ∪ 𝑉)) = (𝐹‘((𝐹‘𝑈) ∪ (𝐹‘𝑉))))
Theorem	mrcssvd 17569	The Moore closure of a set is a subset of the base. Deduction form of mrcssv 17560. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    ⇒   ⊢ (𝜑 → (𝑁‘𝐵) ⊆ 𝑋)
Theorem	mrcssd 17570	Moore closure preserves subset ordering. Deduction form of mrcss 17562. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘𝑈) ⊆ (𝑁‘𝑉))
Theorem	mrcssidd 17571	A set is contained in its Moore closure. Deduction form of mrcssid 17563. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → 𝑈 ⊆ (𝑁‘𝑈))
Theorem	mrcidmd 17572	Moore closure is idempotent. Deduction form of mrcidm 17565. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑁‘𝑈)) = (𝑁‘𝑈))
Theorem	mressmrcd 17573	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 17574	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 17575	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 17584 and mrieqv2d 17585. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})) ↔ (𝑁‘(𝑆 ∖ {𝑌})) = (𝑁‘𝑆)))
7.2.2  Independent sets in a Moore system
Theorem	mrisval 17576*	Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    ⇒   ⊢ (𝐴 ∈ (Moore‘𝑋) → 𝐼 = {𝑠 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))})
Theorem	ismri 17577*	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 17578*	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 17579*	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 17580*	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 17581	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 17582	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 17583	Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})))
Theorem	mrieqvd 17584*	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 17585*	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 17586	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 17573, and so are equal by mrieqv2d 17585.) (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇))    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝑆 = 𝑇)
Theorem	mrissmrid 17587	In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝑇 ∈ 𝐼)
Theorem	mreexd 17588*	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 to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))    &   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆))    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍})))
Theorem	mreexmrid 17589*	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 17590*	This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 17594. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → (𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾))    &   ⊢ (𝜑 → ∀𝑡∀𝑢 ∈ 𝒫 (𝑋 ∖ 𝑡)∀𝑣 ∈ 𝒫 (𝑋 ∖ 𝑡)(((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼)))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexexlem2d 17591*	Used in mreexexlem4d 17593 to prove the induction step in mreexexd 17594. 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 17592*	Base case of the induction in mreexexd 17594. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → (𝐹 = ∅ ∨ 𝐺 = ∅))    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ 𝒫 𝐺(𝐹 ≈ 𝑖 ∧ (𝑖 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexexlem4d 17593*	Induction step of the induction in mreexexd 17594. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → 𝐿 ∈ ω)    &   ⊢ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐿 ∨ 𝑔 ≈ 𝐿) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼)))    &   ⊢ (𝜑 → (𝐹 ≈ suc 𝐿 ∨ 𝐺 ≈ suc 𝐿))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexexd 17594*	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 17592 for the base case and mreexexlem4d 17593 for the induction step. (Contributed by David Moews, 1-May-2017.) Remove dependencies on ax-rep 5285 and ax-ac2 10460. (Revised by Brendan Leahy, 2-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin))    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹 ≈ 𝑞 ∧ (𝑞 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexdomd 17595*	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 17594. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇))    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑆 ∈ Fin ∨ 𝑇 ∈ Fin))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝑆 ≼ 𝑇)
Theorem	mreexfidimd 17596*	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 17595 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 17597*	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 17598	Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋))
Theorem	isacs2 17599*	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 17600*	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)(𝐹‘𝑦) ⊆ 𝑆)))