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	imasaddfn 17501*	The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))
Theorem	imasaddval 17502*	The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Theorem	imasaddf 17503*	The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵)
Theorem	imasmulfn 17504*	The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))
Theorem	imasmulval 17505*	The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Theorem	imasmulf 17506*	The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵)
Theorem	imasvscafn 17507*	The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))))    ⇒   ⊢ (𝜑 → ∙ Fn (𝐾 × 𝐵))
Theorem	imasvscaval 17508*	The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑋 ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Theorem	imasvscaf 17509*	The image structure's scalar multiplication is closed in the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∙ :(𝐾 × 𝐵)⟶𝐵)
Theorem	imasless 17510	The order relation defined on an image set is a subset of the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ ≤ = (le‘𝑈)    ⇒   ⊢ (𝜑 → ≤ ⊆ (𝐵 × 𝐵))
Theorem	imasleval 17511*	The value of the image structure's ordering when the order is compatible with the mapping function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ ≤ = (le‘𝑈)    &   ⊢ 𝑁 = (le‘𝑅)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑐) ∧ (𝐹‘𝑏) = (𝐹‘𝑑)) → (𝑎𝑁𝑏 ↔ 𝑐𝑁𝑑)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ≤ (𝐹‘𝑌) ↔ 𝑋𝑁𝑌))
Theorem	qusval 17512*	Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
Theorem	quslem 17513*	The function in qusval 17512 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐹:𝑉–onto→(𝑉 / ∼ ))
Theorem	qusin 17514	Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ( ∼ “ 𝑉) ⊆ 𝑉)    ⇒   ⊢ (𝜑 → 𝑈 = (𝑅 /s ( ∼ ∩ (𝑉 × 𝑉))))
Theorem	qusbas 17515	Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (𝑉 / ∼ ) = (Base‘𝑈))
Theorem	quss 17516	The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐾 = (Scalar‘𝑅)    ⇒   ⊢ (𝜑 → 𝐾 = (Scalar‘𝑈))
Theorem	divsfval 17517*	Value of the function in qusval 17512. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = [𝐴] ∼ )
Theorem	ercpbllem 17518*	Lemma for ercpbl 17519. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) = (𝐹‘𝐵) ↔ 𝐴 ∼ 𝐵))
Theorem	ercpbl 17519*	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 17520*	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 17521*	Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusaddflem 17522*	The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	qusaddval 17523*	The addition in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusaddf 17524*	The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	qusmulval 17525*	The multiplication in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	qusmulf 17526*	The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ ))
Theorem	fnpr2o 17527	Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o)
Theorem	fnpr2ob 17528	Biconditional version of fnpr2o 17527. (Contributed by Jim Kingdon, 27-Sep-2023.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} Fn 2o)
Theorem	fvpr0o 17529	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ (𝐴 ∈ 𝑉 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅) = 𝐴)
Theorem	fvpr1o 17530	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
⊢ (𝐵 ∈ 𝑉 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o) = 𝐵)
Theorem	fvprif 17531	The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵))
Theorem	xpsfrnel 17532*	Elementhood in the target space of the function 𝐹 appearing in xpsval 17540. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐺 ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))
Theorem	xpsfeq 17533	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 17534*	Elementhood in the target space of the function 𝐹 appearing in xpsval 17540. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ ({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩} ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))
Theorem	xpscf 17535	Equivalent condition for the pair function to be a proper function on 𝐴. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩}:2o⟶𝐴 ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴))
Theorem	xpsfval 17536*	The value of the function appearing in xpsval 17540. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐹𝑌) = {⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩})
Theorem	xpsff1o 17537*	The function appearing in xpsval 17540 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 17538*	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 17539*	The function appearing in xpsval 17540 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 17540*	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 17541*	The indexed structure product that appears in xpsval 17540 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 17542	The base set of the binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇))
Theorem	xpsaddlem 17543*	Lemma for xpsadd 17544 and xpsmul 17545. (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 17544	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 17545	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 17546	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 17547	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 17548	Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ ≤ = (le‘𝑇)    ⇒   ⊢ (𝜑 → ≤ ⊆ ((𝑋 × 𝑌) × (𝑋 × 𝑌)))
Theorem	xpsle 17549	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 17550	The class of Moore systems.
class Moore
Syntax	cmrc 17551	The class function generating Moore closures.
class mrCls
Syntax	cmri 17552	mrInd is a class function which takes a Moore system to its set of independent sets.
class mrInd
Syntax	cacs 17553	The class of algebraic closure (Moore) systems.
class ACS
Definition	df-mre 17554*	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 22972) and vector spaces (lssmre 20879) 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 17558, mresspw 17560, mre1cl 17562 and mreintcl 17563 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 17568); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 17569. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.)
⊢ Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))})
Definition	df-mrc 17555*	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 22973) and linear span (mrclsp 20902). A Moore closure operation 𝑁 is (1) extensive, i.e., 𝑥 ⊆ (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcssid 17585), (2) isotone, i.e., 𝑥 ⊆ 𝑦 implies that (𝑁‘𝑥) ⊆ (𝑁‘𝑦) for all subsets 𝑥 and 𝑦 of the base set (mrcss 17584), and (3) idempotent, i.e., (𝑁‘(𝑁‘𝑥)) = (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcidm 17587.) 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 17556*	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 17557*	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 9603 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 17558*	Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) ↔ (𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀𝑠 ∈ 𝒫 𝐶(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶)))
Theorem	fnmre 17559	The Moore collection generator is a well-behaved function. Analogue for Moore collections of fntopon 22818 for topologies. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ Moore Fn V
Theorem	mresspw 17560	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 17561	A Moore-closed subset is a subset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → 𝑆 ⊆ 𝑋)
Theorem	mre1cl 17562	In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝐶)
Theorem	mreintcl 17563	A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ 𝐶)
Theorem	mreiincl 17564*	A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶)
Theorem	mrerintcl 17565	The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑆) ∈ 𝐶)
Theorem	mreriincl 17566*	The relative intersection of a family of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → (𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆) ∈ 𝐶)
Theorem	mreincl 17567	Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶)
Theorem	mreuni 17568	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 17569	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 17570*	Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶 ∧ 𝑠 ≠ ∅) → ∩ 𝑠 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋))
Theorem	ismred2 17571*	Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑠) ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋))
Theorem	mremre 17572	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 17573	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 17574*	The domain and codomain of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}):𝒫 𝑋⟶𝐶)
Theorem	fnmrc 17575	Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ mrCls Fn ∪ ran Moore
Theorem	mrcfval 17576*	Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 = (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}))
Theorem	mrcf 17577	The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶)
Theorem	mrcval 17578*	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 17579	The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) ∈ 𝐶)
Theorem	mrcsncl 17580	The Moore closure of a singleton is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝑋) → (𝐹‘{𝑈}) ∈ 𝐶)
Theorem	mrcid 17581	The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝐶) → (𝐹‘𝑈) = 𝑈)
Theorem	mrcssv 17582	The closure of a set is a subset of the base. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹‘𝑈) ⊆ 𝑋)
Theorem	mrcidb 17583	A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) = 𝑈))
Theorem	mrcss 17584	Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘𝑈) ⊆ (𝐹‘𝑉))
Theorem	mrcssid 17585	The closure of a set is a superset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → 𝑈 ⊆ (𝐹‘𝑈))
Theorem	mrcidb2 17586	A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) ⊆ 𝑈))
Theorem	mrcidm 17587	The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘(𝐹‘𝑈)) = (𝐹‘𝑈))
Theorem	mrcsscl 17588	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 17589	Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑈) = (𝐹‘∪ (𝐹 “ 𝑈)))
Theorem	mrcun 17590	Idempotence of closure under a pair union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘(𝑈 ∪ 𝑉)) = (𝐹‘((𝐹‘𝑈) ∪ (𝐹‘𝑉))))
Theorem	mrcssvd 17591	The Moore closure of a set is a subset of the base. Deduction form of mrcssv 17582. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    ⇒   ⊢ (𝜑 → (𝑁‘𝐵) ⊆ 𝑋)
Theorem	mrcssd 17592	Moore closure preserves subset ordering. Deduction form of mrcss 17584. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘𝑈) ⊆ (𝑁‘𝑉))
Theorem	mrcssidd 17593	A set is contained in its Moore closure. Deduction form of mrcssid 17585. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → 𝑈 ⊆ (𝑁‘𝑈))
Theorem	mrcidmd 17594	Moore closure is idempotent. Deduction form of mrcidm 17587. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑁‘𝑈)) = (𝑁‘𝑈))
Theorem	mressmrcd 17595	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 17596	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 17597	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 17606 and mrieqv2d 17607. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})) ↔ (𝑁‘(𝑆 ∖ {𝑌})) = (𝑁‘𝑆)))
7.2.2  Independent sets in a Moore system
Theorem	mrisval 17598*	Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    ⇒   ⊢ (𝐴 ∈ (Moore‘𝑋) → 𝐼 = {𝑠 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))})
Theorem	ismri 17599*	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 17600*	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‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))))