Definition df-acs

Description: 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 termedalgebraic 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 is to be avoided), we consider a single function defined on finite sets instead. (Contributed by Stefan O'Rear, 2-Apr-2015)

	Ref	Expression
Assertion	df-acs	⊢ ACS = ( 𝑥 ∈ V ↦ { 𝑐 ∈ ( Moore ‘ 𝑥 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ∧ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cacs	⊢ ACS
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vc	⊢ 𝑐
4		cmre	⊢ Moore
5	1	cv	⊢ 𝑥
6	5 4	cfv	⊢ ( Moore ‘ 𝑥 )
7		vf	⊢ 𝑓
8	7	cv	⊢ 𝑓
9	5	cpw	⊢ 𝒫 𝑥
10	9 9 8	wf	⊢ 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥
11		vs	⊢ 𝑠
12	11	cv	⊢ 𝑠
13	3	cv	⊢ 𝑐
14	12 13	wcel	⊢ 𝑠 ∈ 𝑐
15	12	cpw	⊢ 𝒫 𝑠
16		cfn	⊢ Fin
17	15 16	cin	⊢ ( 𝒫 𝑠 ∩ Fin )
18	8 17	cima	⊢ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) )
19	18	cuni	⊢ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) )
20	19 12	wss	⊢ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠
21	14 20	wb	⊢ ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 )
22	21 11 9	wral	⊢ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 )
23	10 22	wa	⊢ ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ∧ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) )
24	23 7	wex	⊢ ∃ 𝑓 ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ∧ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) )
25	24 3 6	crab	⊢ { 𝑐 ∈ ( Moore ‘ 𝑥 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ∧ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) }
26	1 2 25	cmpt	⊢ ( 𝑥 ∈ V ↦ { 𝑐 ∈ ( Moore ‘ 𝑥 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ∧ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) } )
27	0 26	wceq	⊢ ACS = ( 𝑥 ∈ V ↦ { 𝑐 ∈ ( Moore ‘ 𝑥 ) ∣ ∃ 𝑓 ( 𝑓 : 𝒫 𝑥 ⟶ 𝒫 𝑥 ∧ ∀ 𝑠 ∈ 𝒫 𝑥 ( 𝑠 ∈ 𝑐 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) } )