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 39687
 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 39686 . 2 class NoeACS
2 vx . . 3 setvar 𝑥
3 cvv 3441 . . 3 class V
4 vs . . . . . . . 8 setvar 𝑠
54cv 1537 . . . . . . 7 class 𝑠
6 vg . . . . . . . . 9 setvar 𝑔
76cv 1537 . . . . . . . 8 class 𝑔
8 vc . . . . . . . . . 10 setvar 𝑐
98cv 1537 . . . . . . . . 9 class 𝑐
10 cmrc 16849 . . . . . . . . 9 class mrCls
119, 10cfv 6325 . . . . . . . 8 class (mrCls‘𝑐)
127, 11cfv 6325 . . . . . . 7 class ((mrCls‘𝑐)‘𝑔)
135, 12wceq 1538 . . . . . 6 wff 𝑠 = ((mrCls‘𝑐)‘𝑔)
142cv 1537 . . . . . . . 8 class 𝑥
1514cpw 4497 . . . . . . 7 class 𝒫 𝑥
16 cfn 8495 . . . . . . 7 class Fin
1715, 16cin 3880 . . . . . 6 class (𝒫 𝑥 ∩ Fin)
1813, 6, 17wrex 3107 . . . . 5 wff 𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)
1918, 4, 9wral 3106 . . . 4 wff 𝑠𝑐𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)
20 cacs 16851 . . . . 5 class ACS
2114, 20cfv 6325 . . . 4 class (ACS‘𝑥)
2219, 8, 21crab 3110 . . 3 class {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠𝑐𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)}
232, 3, 22cmpt 5111 . 2 class (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠𝑐𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)})
241, 23wceq 1538 1 wff NoeACS = (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠𝑐𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)})
 Colors of variables: wff setvar class This definition is referenced by:  isnacs  39688
 Copyright terms: Public domain W3C validator