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 ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ) )