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	ercpbllem 17501*	Lemma for ercpbl 17502. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) = (𝐹‘𝐵) ↔ 𝐴 ∼ 𝐵))
Theorem	ercpbl 17502*	Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 + 𝑏) ∈ 𝑉)    &   ⊢ (𝜑 → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷)))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷))))
Theorem	erlecpbl 17503*	Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴𝑁𝐵 ↔ 𝐶𝑁𝐷)))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐴𝑁𝐵 ↔ 𝐶𝑁𝐷)))
Theorem	qusaddvallem 17504*	Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusaddflem 17505*	The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	qusaddval 17506*	The addition in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusaddf 17507*	The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	qusmulval 17508*	The multiplication in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusmulf 17509*	The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	fnpr2o 17510	Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o)
Theorem	fnpr2ob 17511	Biconditional version of fnpr2o 17510. (Contributed by Jim Kingdon, 27-Sep-2023.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o)
Theorem	fvpr0o 17512	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ (𝐴 ∈ 𝑉 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅) = 𝐴)
Theorem	fvpr1o 17513	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ (𝐵 ∈ 𝑉 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o) = 𝐵)
Theorem	fvprif 17514	The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵))
Theorem	xpsfrnel 17515*	Elementhood in the target space of the function 𝐹 appearing in xpsval 17523. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐺 ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))
Theorem	xpsfeq 17516	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 17517*	Elementhood in the target space of the function 𝐹 appearing in xpsval 17523. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ ({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩} ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))
Theorem	xpscf 17518	Equivalent condition for the pair function to be a proper function on 𝐴. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩}:2o⟶𝐴 ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴))
Theorem	xpsfval 17519*	The value of the function appearing in xpsval 17523. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐹𝑌) = {⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩})
Theorem	xpsff1o 17520*	The function appearing in xpsval 17523 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 17521*	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 17522*	The function appearing in xpsval 17523 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 17523*	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 17524*	The indexed structure product that appears in xpsval 17523 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 17525	The base set of the binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇))
Theorem	xpsaddlem 17526*	Lemma for xpsadd 17527 and xpsmul 17528. (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 17527	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 17528	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 17529	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 17530	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 17531	Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ ≤ = (le‘𝑇)    ⇒   ⊢ (𝜑 → ≤ ⊆ ((𝑋 × 𝑌) × (𝑋 × 𝑌)))
Theorem	xpsle 17532	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 17533	The class of Moore systems.
class Moore
Syntax	cmrc 17534	The class function generating Moore closures.
class mrCls
Syntax	cmri 17535	mrInd is a class function which takes a Moore system to its set of independent sets.
class mrInd
Syntax	cacs 17536	The class of algebraic closure (Moore) systems.
class ACS
Definition	df-mre 17537*	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 23052) and vector spaces (lssmre 20950) 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 17541, mresspw 17543, mre1cl 17545 and mreintcl 17546 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 17551); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 17552. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.)
⊢ Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})
Definition	df-mrc 17538*	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 23053) and linear span (mrclsp 20973). A Moore closure operation 𝑁 is (1) extensive, i.e., 𝑥 ⊆ (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcssid 17572), (2) isotone, i.e., 𝑥 ⊆ 𝑦 implies that (𝑁‘𝑥) ⊆ (𝑁‘𝑦) for all subsets 𝑥 and 𝑦 of the base set (mrcss 17571), and (3) idempotent, i.e., (𝑁‘(𝑁‘𝑥)) = (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcidm 17574.) 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 17539*	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 17540*	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 9553 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 17541*	Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) ↔ (𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀𝑠 ∈ 𝒫 𝐶(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶)))
Theorem	fnmre 17542	The Moore collection generator is a well-behaved function. Analogue for Moore collections of fntopon 22898 for topologies. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ Moore Fn V
Theorem	mresspw 17543	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 17544	A Moore-closed subset is a subset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → 𝑆 ⊆ 𝑋)
Theorem	mre1cl 17545	In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝐶)
Theorem	mreintcl 17546	A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ 𝐶)
Theorem	mreiincl 17547*	A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶)
Theorem	mrerintcl 17548	The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑆) ∈ 𝐶)
Theorem	mreriincl 17549*	The relative intersection of a family of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → (𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆) ∈ 𝐶)
Theorem	mreincl 17550	Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶)
Theorem	mreuni 17551	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 17552	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 17553*	Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶 ∧ 𝑠 ≠ ∅) → ∩ 𝑠 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋))
Theorem	ismred2 17554*	Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑠) ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋))
Theorem	mremre 17555	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 17556	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‘𝐴))
Theorem	xrsle 17557	The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ≤ = (le‘ℝ*𝑠)
Theorem	xrge0le 17558	The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.)
⊢ ≤ = (le‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrsbas 17559	The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ* = (Base‘ℝ*𝑠)
Theorem	xrge0base 17560	The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞)))
7.2.1  Moore closures
Theorem	mrcflem 17561*	The domain and codomain of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}):𝒫 𝑋⟶𝐶)
Theorem	fnmrc 17562	Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ mrCls Fn ∪ ran Moore
Theorem	mrcfval 17563*	Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 = (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}))
Theorem	mrcf 17564	The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶)
Theorem	mrcval 17565*	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 17566	The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) ∈ 𝐶)
Theorem	mrcsncl 17567	The Moore closure of a singleton is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝑋) → (𝐹‘{𝑈}) ∈ 𝐶)
Theorem	mrcid 17568	The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝐶) → (𝐹‘𝑈) = 𝑈)
Theorem	mrcssv 17569	The closure of a set is a subset of the base. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹‘𝑈) ⊆ 𝑋)
Theorem	mrcidb 17570	A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) = 𝑈))
Theorem	mrcss 17571	Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘𝑈) ⊆ (𝐹‘𝑉))
Theorem	mrcssid 17572	The closure of a set is a superset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → 𝑈 ⊆ (𝐹‘𝑈))
Theorem	mrcidb2 17573	A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) ⊆ 𝑈))
Theorem	mrcidm 17574	The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘(𝐹‘𝑈)) = (𝐹‘𝑈))
Theorem	mrcsscl 17575	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 17576	Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑈) = (𝐹‘∪ (𝐹 “ 𝑈)))
Theorem	mrcun 17577	Idempotence of closure under a pair union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘(𝑈 ∪ 𝑉)) = (𝐹‘((𝐹‘𝑈) ∪ (𝐹‘𝑉))))
Theorem	mrcssvd 17578	The Moore closure of a set is a subset of the base. Deduction form of mrcssv 17569. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    ⇒   ⊢ (𝜑 → (𝑁‘𝐵) ⊆ 𝑋)
Theorem	mrcssd 17579	Moore closure preserves subset ordering. Deduction form of mrcss 17571. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘𝑈) ⊆ (𝑁‘𝑉))
Theorem	mrcssidd 17580	A set is contained in its Moore closure. Deduction form of mrcssid 17572. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → 𝑈 ⊆ (𝑁‘𝑈))
Theorem	mrcidmd 17581	Moore closure is idempotent. Deduction form of mrcidm 17574. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑁‘𝑈)) = (𝑁‘𝑈))
Theorem	mressmrcd 17582	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 17583	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 17584	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 17593 and mrieqv2d 17594. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})) ↔ (𝑁‘(𝑆 ∖ {𝑌})) = (𝑁‘𝑆)))
7.2.2  Independent sets in a Moore system
Theorem	mrisval 17585*	Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    ⇒   ⊢ (𝐴 ∈ (Moore‘𝑋) → 𝐼 = {𝑠 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))})
Theorem	ismri 17586*	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 17587*	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 17588*	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 17589*	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 17590	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 17591	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 17592	Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})))
Theorem	mrieqvd 17593*	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 17594*	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 17595	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 17582, and so are equal by mrieqv2d 17594.) (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇))    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝑆 = 𝑇)
Theorem	mrissmrid 17596	In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝑇 ∈ 𝐼)
Theorem	mreexd 17597*	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 17598*	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 17599*	This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 17603. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → (𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾))    &   ⊢ (𝜑 → ∀𝑡∀𝑢 ∈ 𝒫 (𝑋 ∖ 𝑡)∀𝑣 ∈ 𝒫 (𝑋 ∖ 𝑡)(((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼)))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexexlem2d 17600*	Used in mreexexlem4d 17602 to prove the induction step in mreexexd 17603. See the proof of Proposition 4.2.1 in [FaureFrolicher] p. 86 to 87. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝐺 (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼))