Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-nacs Structured version   Visualization version   GIF version

Definition df-nacs 37092
Description: Define a closure system of Noetherian type (not standard terminology) as an algebraic system where all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.)
Assertion
Ref Expression
df-nacs NoeACS = (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠𝑐𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)})
Distinct variable group:   𝑥,𝑐,𝑠,𝑔

Detailed syntax breakdown of Definition df-nacs
StepHypRef Expression
1 cnacs 37091 . 2 class NoeACS
2 vx . . 3 setvar 𝑥
3 cvv 3198 . . 3 class V
4 vs . . . . . . . 8 setvar 𝑠
54cv 1481 . . . . . . 7 class 𝑠
6 vg . . . . . . . . 9 setvar 𝑔
76cv 1481 . . . . . . . 8 class 𝑔
8 vc . . . . . . . . . 10 setvar 𝑐
98cv 1481 . . . . . . . . 9 class 𝑐
10 cmrc 16237 . . . . . . . . 9 class mrCls
119, 10cfv 5886 . . . . . . . 8 class (mrCls‘𝑐)
127, 11cfv 5886 . . . . . . 7 class ((mrCls‘𝑐)‘𝑔)
135, 12wceq 1482 . . . . . 6 wff 𝑠 = ((mrCls‘𝑐)‘𝑔)
142cv 1481 . . . . . . . 8 class 𝑥
1514cpw 4156 . . . . . . 7 class 𝒫 𝑥
16 cfn 7952 . . . . . . 7 class Fin
1715, 16cin 3571 . . . . . 6 class (𝒫 𝑥 ∩ Fin)
1813, 6, 17wrex 2912 . . . . 5 wff 𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)
1918, 4, 9wral 2911 . . . 4 wff 𝑠𝑐𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)
20 cacs 16239 . . . . 5 class ACS
2114, 20cfv 5886 . . . 4 class (ACS‘𝑥)
2219, 8, 21crab 2915 . . 3 class {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠𝑐𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)}
232, 3, 22cmpt 4727 . 2 class (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠𝑐𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)})
241, 23wceq 1482 1 wff NoeACS = (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠𝑐𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)})
Colors of variables: wff setvar class
This definition is referenced by:  isnacs  37093
  Copyright terms: Public domain W3C validator