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 
|- F = ( mrCls ` C )
Assertion isnacs2 
|- ( C e. ( NoeACS ` X ) <-> ( C e. ( ACS ` X ) /\ ( F " ( ~P X i^i Fin ) ) = C ) )

Proof

Step Hyp Ref Expression
1 isnacs.f 
 |-  F = ( mrCls ` C )
2 1 isnacs 
 |-  ( C e. ( NoeACS ` X ) <-> ( C e. ( ACS ` X ) /\ A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) )
3 eqcom 
 |-  ( s = ( F ` g ) <-> ( F ` g ) = s )
4 3 rexbii 
 |-  ( E. g e. ( ~P X i^i Fin ) s = ( F ` g ) <-> E. g e. ( ~P X i^i Fin ) ( F ` g ) = s )
5 acsmre 
 |-  ( C e. ( ACS ` X ) -> C e. ( Moore ` X ) )
6 1 mrcf 
 |-  ( C e. ( Moore ` X ) -> F : ~P X --> C )
7 ffn 
 |-  ( F : ~P X --> C -> F Fn ~P X )
8 5 6 7 3syl 
 |-  ( C e. ( ACS ` X ) -> F Fn ~P X )
9 inss1 
 |-  ( ~P X i^i Fin ) C_ ~P X
10 fvelimab 
 |-  ( ( F Fn ~P X /\ ( ~P X i^i Fin ) C_ ~P X ) -> ( s e. ( F " ( ~P X i^i Fin ) ) <-> E. g e. ( ~P X i^i Fin ) ( F ` g ) = s ) )
11 8 9 10 sylancl 
 |-  ( C e. ( ACS ` X ) -> ( s e. ( F " ( ~P X i^i Fin ) ) <-> E. g e. ( ~P X i^i Fin ) ( F ` g ) = s ) )
12 4 11 bitr4id 
 |-  ( C e. ( ACS ` X ) -> ( E. g e. ( ~P X i^i Fin ) s = ( F ` g ) <-> s e. ( F " ( ~P X i^i Fin ) ) ) )
13 12 ralbidv 
 |-  ( C e. ( ACS ` X ) -> ( A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) <-> A. s e. C s e. ( F " ( ~P X i^i Fin ) ) ) )
14 dfss3 
 |-  ( C C_ ( F " ( ~P X i^i Fin ) ) <-> A. s e. C s e. ( F " ( ~P X i^i Fin ) ) )
15 13 14 bitr4di 
 |-  ( C e. ( ACS ` X ) -> ( A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) <-> C C_ ( F " ( ~P X i^i Fin ) ) ) )
16 imassrn 
 |-  ( F " ( ~P X i^i Fin ) ) C_ ran F
17 frn 
 |-  ( F : ~P X --> C -> ran F C_ C )
18 5 6 17 3syl 
 |-  ( C e. ( ACS ` X ) -> ran F C_ C )
19 16 18 sstrid 
 |-  ( C e. ( ACS ` X ) -> ( F " ( ~P X i^i Fin ) ) C_ C )
20 19 biantrurd 
 |-  ( C e. ( ACS ` X ) -> ( C C_ ( F " ( ~P X i^i Fin ) ) <-> ( ( F " ( ~P X i^i Fin ) ) C_ C /\ C C_ ( F " ( ~P X i^i Fin ) ) ) ) )
21 eqss 
 |-  ( ( F " ( ~P X i^i Fin ) ) = C <-> ( ( F " ( ~P X i^i Fin ) ) C_ C /\ C C_ ( F " ( ~P X i^i Fin ) ) ) )
22 20 21 bitr4di 
 |-  ( C e. ( ACS ` X ) -> ( C C_ ( F " ( ~P X i^i Fin ) ) <-> ( F " ( ~P X i^i Fin ) ) = C ) )
23 15 22 bitrd 
 |-  ( C e. ( ACS ` X ) -> ( A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) <-> ( F " ( ~P X i^i Fin ) ) = C ) )
24 23 pm5.32i 
 |-  ( ( C e. ( ACS ` X ) /\ A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) <-> ( C e. ( ACS ` X ) /\ ( F " ( ~P X i^i Fin ) ) = C ) )
25 2 24 bitri 
 |-  ( C e. ( NoeACS ` X ) <-> ( C e. ( ACS ` X ) /\ ( F " ( ~P X i^i Fin ) ) = C ) )