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 ) ) = 𝐶 ) )