Metamath Proof Explorer


Theorem isnacs

Description: Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypothesis isnacs.f 𝐹 = ( mrCls ‘ 𝐶 )
Assertion isnacs ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ) )

Proof

Step Hyp Ref Expression
1 isnacs.f 𝐹 = ( mrCls ‘ 𝐶 )
2 elfvex ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) → 𝑋 ∈ V )
3 elfvex ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝑋 ∈ V )
4 3 adantr ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ) → 𝑋 ∈ V )
5 fveq2 ( 𝑥 = 𝑋 → ( ACS ‘ 𝑥 ) = ( ACS ‘ 𝑋 ) )
6 pweq ( 𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋 )
7 6 ineq1d ( 𝑥 = 𝑋 → ( 𝒫 𝑥 ∩ Fin ) = ( 𝒫 𝑋 ∩ Fin ) )
8 7 rexeqdv ( 𝑥 = 𝑋 → ( ∃ 𝑔 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) ) )
9 8 ralbidv ( 𝑥 = 𝑋 → ( ∀ 𝑠𝑐𝑔 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) ↔ ∀ 𝑠𝑐𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) ) )
10 5 9 rabeqbidv ( 𝑥 = 𝑋 → { 𝑐 ∈ ( ACS ‘ 𝑥 ) ∣ ∀ 𝑠𝑐𝑔 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) } = { 𝑐 ∈ ( ACS ‘ 𝑋 ) ∣ ∀ 𝑠𝑐𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) } )
11 df-nacs NoeACS = ( 𝑥 ∈ V ↦ { 𝑐 ∈ ( ACS ‘ 𝑥 ) ∣ ∀ 𝑠𝑐𝑔 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) } )
12 fvex ( ACS ‘ 𝑋 ) ∈ V
13 12 rabex { 𝑐 ∈ ( ACS ‘ 𝑋 ) ∣ ∀ 𝑠𝑐𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) } ∈ V
14 10 11 13 fvmpt ( 𝑋 ∈ V → ( NoeACS ‘ 𝑋 ) = { 𝑐 ∈ ( ACS ‘ 𝑋 ) ∣ ∀ 𝑠𝑐𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) } )
15 14 eleq2d ( 𝑋 ∈ V → ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ 𝐶 ∈ { 𝑐 ∈ ( ACS ‘ 𝑋 ) ∣ ∀ 𝑠𝑐𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) } ) )
16 fveq2 ( 𝑐 = 𝐶 → ( mrCls ‘ 𝑐 ) = ( mrCls ‘ 𝐶 ) )
17 16 1 eqtr4di ( 𝑐 = 𝐶 → ( mrCls ‘ 𝑐 ) = 𝐹 )
18 17 fveq1d ( 𝑐 = 𝐶 → ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) = ( 𝐹𝑔 ) )
19 18 eqeq2d ( 𝑐 = 𝐶 → ( 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) ↔ 𝑠 = ( 𝐹𝑔 ) ) )
20 19 rexbidv ( 𝑐 = 𝐶 → ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ) )
21 20 raleqbi1dv ( 𝑐 = 𝐶 → ( ∀ 𝑠𝑐𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) ↔ ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ) )
22 21 elrab ( 𝐶 ∈ { 𝑐 ∈ ( ACS ‘ 𝑋 ) ∣ ∀ 𝑠𝑐𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( ( mrCls ‘ 𝑐 ) ‘ 𝑔 ) } ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ) )
23 15 22 bitrdi ( 𝑋 ∈ V → ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ) ) )
24 2 4 23 pm5.21nii ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ) )