Metamath Proof Explorer

Theorem mrefg3

Description: Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypothesis isnacs.f 
|- F = ( mrCls ` C )
Assertion mrefg3 
|- ( ( C e. ( Moore ` X ) /\ S e. C ) -> ( E. g e. ( ~P X i^i Fin ) S = ( F ` g ) <-> E. g e. ( ~P S i^i Fin ) S C_ ( F ` g ) ) )

Proof

Step Hyp Ref Expression
1 isnacs.f 
 |-  F = ( mrCls ` C )
2 1 mrefg2 
 |-  ( C e. ( Moore ` X ) -> ( E. g e. ( ~P X i^i Fin ) S = ( F ` g ) <-> E. g e. ( ~P S i^i Fin ) S = ( F ` g ) ) )
3 2 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ S e. C ) -> ( E. g e. ( ~P X i^i Fin ) S = ( F ` g ) <-> E. g e. ( ~P S i^i Fin ) S = ( F ` g ) ) )
4 eqss 
 |-  ( S = ( F ` g ) <-> ( S C_ ( F ` g ) /\ ( F ` g ) C_ S ) )
5 simpll 
 |-  ( ( ( C e. ( Moore ` X ) /\ S e. C ) /\ g e. ( ~P S i^i Fin ) ) -> C e. ( Moore ` X ) )
6 inss1 
 |-  ( ~P S i^i Fin ) C_ ~P S
7 6 sseli 
 |-  ( g e. ( ~P S i^i Fin ) -> g e. ~P S )
8 7 elpwid 
 |-  ( g e. ( ~P S i^i Fin ) -> g C_ S )
9 8 adantl 
 |-  ( ( ( C e. ( Moore ` X ) /\ S e. C ) /\ g e. ( ~P S i^i Fin ) ) -> g C_ S )
10 simplr 
 |-  ( ( ( C e. ( Moore ` X ) /\ S e. C ) /\ g e. ( ~P S i^i Fin ) ) -> S e. C )
11 1 mrcsscl 
 |-  ( ( C e. ( Moore ` X ) /\ g C_ S /\ S e. C ) -> ( F ` g ) C_ S )
12 5 9 10 11 syl3anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ S e. C ) /\ g e. ( ~P S i^i Fin ) ) -> ( F ` g ) C_ S )
13 12 biantrud 
 |-  ( ( ( C e. ( Moore ` X ) /\ S e. C ) /\ g e. ( ~P S i^i Fin ) ) -> ( S C_ ( F ` g ) <-> ( S C_ ( F ` g ) /\ ( F ` g ) C_ S ) ) )
14 4 13 bitr4id 
 |-  ( ( ( C e. ( Moore ` X ) /\ S e. C ) /\ g e. ( ~P S i^i Fin ) ) -> ( S = ( F ` g ) <-> S C_ ( F ` g ) ) )
15 14 rexbidva 
 |-  ( ( C e. ( Moore ` X ) /\ S e. C ) -> ( E. g e. ( ~P S i^i Fin ) S = ( F ` g ) <-> E. g e. ( ~P S i^i Fin ) S C_ ( F ` g ) ) )
16 3 15 bitrd 
 |-  ( ( C e. ( Moore ` X ) /\ S e. C ) -> ( E. g e. ( ~P X i^i Fin ) S = ( F ` g ) <-> E. g e. ( ~P S i^i Fin ) S C_ ( F ` g ) ) )