Metamath Proof Explorer


Theorem isnacs2

Description: Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 isnacs.f 𝐹 = ( mrCls ‘ 𝐶 )
2 1 isnacs ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ) )
3 eqcom ( 𝑠 = ( 𝐹𝑔 ) ↔ ( 𝐹𝑔 ) = 𝑠 )
4 3 rexbii ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐹𝑔 ) = 𝑠 )
5 acsmre ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
6 1 mrcf ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋𝐶 )
7 ffn ( 𝐹 : 𝒫 𝑋𝐶𝐹 Fn 𝒫 𝑋 )
8 5 6 7 3syl ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝐹 Fn 𝒫 𝑋 )
9 inss1 ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋
10 fvelimab ( ( 𝐹 Fn 𝒫 𝑋 ∧ ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋 ) → ( 𝑠 ∈ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐹𝑔 ) = 𝑠 ) )
11 8 9 10 sylancl ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑠 ∈ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐹𝑔 ) = 𝑠 ) )
12 4 11 bitr4id ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ↔ 𝑠 ∈ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) )
13 12 ralbidv ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ↔ ∀ 𝑠𝐶 𝑠 ∈ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) )
14 dfss3 ( 𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ↔ ∀ 𝑠𝐶 𝑠 ∈ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) )
15 13 14 bitr4di ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ↔ 𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) )
16 imassrn ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ⊆ ran 𝐹
17 frn ( 𝐹 : 𝒫 𝑋𝐶 → ran 𝐹𝐶 )
18 5 6 17 3syl ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ran 𝐹𝐶 )
19 16 18 sstrid ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ⊆ 𝐶 )
20 19 biantrurd ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ↔ ( ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ⊆ 𝐶𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) ) )
21 eqss ( ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ↔ ( ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ⊆ 𝐶𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) )
22 20 21 bitr4di ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ↔ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ) )
23 15 22 bitrd ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ↔ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ) )
24 23 pm5.32i ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠𝐶𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹𝑔 ) ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ) )
25 2 24 bitri ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ) )