Definition df-mrc

Description: Define theMoore 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 ) and linear span ( mrclsp ).

A Moore closure operation N is (1) extensive, i.e., x C_ ( Nx ) for all subsets x of the base set ( mrcssid ), (2) isotone, i.e., x C_ y implies that ( Nx ) C_ ( Ny ) for all subsets x and y of the base set ( mrcss ), and (3) idempotent, i.e., ( N( Nx ) ) = ( Nx ) for all subsets x of the base set ( mrcidm .) 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 N 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)

	Ref	Expression
Assertion	df-mrc	⊢ mrCls = ( 𝑐 ∈ ∪ ran Moore ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmrc	⊢ mrCls
1		vc	⊢ 𝑐
2		cmre	⊢ Moore
3	2	crn	⊢ ran Moore
4	3	cuni	⊢ ∪ ran Moore
5		vx	⊢ 𝑥
6	1	cv	⊢ 𝑐
7	6	cuni	⊢ ∪ 𝑐
8	7	cpw	⊢ 𝒫 ∪ 𝑐
9		vs	⊢ 𝑠
10	5	cv	⊢ 𝑥
11	9	cv	⊢ 𝑠
12	10 11	wss	⊢ 𝑥 ⊆ 𝑠
13	12 9 6	crab	⊢ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 }
14	13	cint	⊢ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 }
15	5 8 14	cmpt	⊢ ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } )
16	1 4 15	cmpt	⊢ ( 𝑐 ∈ ∪ ran Moore ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) )
17	0 16	wceq	⊢ mrCls = ( 𝑐 ∈ ∪ ran Moore ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) )