Metamath Proof Explorer


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 ) ) ⊆ 𝑠 ) ) } )