Metamath Proof Explorer

Theorem mrefg2

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

Proof

Step Hyp Ref Expression
1 isnacs.f 
 |-  F = ( mrCls ` C )
2 1 mrcssid 
 |-  ( ( C e. ( Moore ` X ) /\ g C_ X ) -> g C_ ( F ` g ) )
3 simpr 
 |-  ( ( C e. ( Moore ` X ) /\ g C_ ( F ` g ) ) -> g C_ ( F ` g ) )
4 1 mrcssv 
 |-  ( C e. ( Moore ` X ) -> ( F ` g ) C_ X )
5 4 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ g C_ ( F ` g ) ) -> ( F ` g ) C_ X )
6 3 5 sstrd 
 |-  ( ( C e. ( Moore ` X ) /\ g C_ ( F ` g ) ) -> g C_ X )
7 2 6 impbida 
 |-  ( C e. ( Moore ` X ) -> ( g C_ X <-> g C_ ( F ` g ) ) )
8 vex 
 |-  g e. _V
9 8 elpw 
 |-  ( g e. ~P X <-> g C_ X )
10 8 elpw 
 |-  ( g e. ~P ( F ` g ) <-> g C_ ( F ` g ) )
11 7 9 10 3bitr4g 
 |-  ( C e. ( Moore ` X ) -> ( g e. ~P X <-> g e. ~P ( F ` g ) ) )
12 11 anbi1d 
 |-  ( C e. ( Moore ` X ) -> ( ( g e. ~P X /\ g e. Fin ) <-> ( g e. ~P ( F ` g ) /\ g e. Fin ) ) )
13 elin 
 |-  ( g e. ( ~P X i^i Fin ) <-> ( g e. ~P X /\ g e. Fin ) )
14 elin 
 |-  ( g e. ( ~P ( F ` g ) i^i Fin ) <-> ( g e. ~P ( F ` g ) /\ g e. Fin ) )
15 12 13 14 3bitr4g 
 |-  ( C e. ( Moore ` X ) -> ( g e. ( ~P X i^i Fin ) <-> g e. ( ~P ( F ` g ) i^i Fin ) ) )
16 pweq 
 |-  ( S = ( F ` g ) -> ~P S = ~P ( F ` g ) )
17 16 ineq1d 
 |-  ( S = ( F ` g ) -> ( ~P S i^i Fin ) = ( ~P ( F ` g ) i^i Fin ) )
18 17 eleq2d 
 |-  ( S = ( F ` g ) -> ( g e. ( ~P S i^i Fin ) <-> g e. ( ~P ( F ` g ) i^i Fin ) ) )
19 18 bibi2d 
 |-  ( S = ( F ` g ) -> ( ( g e. ( ~P X i^i Fin ) <-> g e. ( ~P S i^i Fin ) ) <-> ( g e. ( ~P X i^i Fin ) <-> g e. ( ~P ( F ` g ) i^i Fin ) ) ) )
20 15 19 syl5ibrcom 
 |-  ( C e. ( Moore ` X ) -> ( S = ( F ` g ) -> ( g e. ( ~P X i^i Fin ) <-> g e. ( ~P S i^i Fin ) ) ) )
21 20 pm5.32rd 
 |-  ( C e. ( Moore ` X ) -> ( ( g e. ( ~P X i^i Fin ) /\ S = ( F ` g ) ) <-> ( g e. ( ~P S i^i Fin ) /\ S = ( F ` g ) ) ) )
22 21 rexbidv2 
 |-  ( 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 ) ) )