Metamath Proof Explorer

Theorem isacs

Description: A set is an algebraic closure system iff it is specified by some function of the finite subsets, such that a set is closed iff it does not expand under the operation. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion isacs 
|- ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. C <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) ) )

Proof

Step Hyp Ref Expression
1 elfvex 
 |-  ( C e. ( ACS ` X ) -> X e. _V )
2 elfvex 
 |-  ( C e. ( Moore ` X ) -> X e. _V )
3 2 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. C <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) ) -> X e. _V )
4 fveq2 
 |-  ( x = X -> ( Moore ` x ) = ( Moore ` X ) )
5 pweq 
 |-  ( x = X -> ~P x = ~P X )
6 5 5 feq23d 
 |-  ( x = X -> ( f : ~P x --> ~P x <-> f : ~P X --> ~P X ) )
7 5 raleqdv 
 |-  ( x = X -> ( A. s e. ~P x ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) <-> A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) )
8 6 7 anbi12d 
 |-  ( x = X -> ( ( f : ~P x --> ~P x /\ A. s e. ~P x ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) <-> ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) ) )
9 8 exbidv 
 |-  ( x = X -> ( E. f ( f : ~P x --> ~P x /\ A. s e. ~P x ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) <-> E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) ) )
10 4 9 rabeqbidv 
 |-  ( x = X -> { c e. ( Moore ` x ) | E. f ( f : ~P x --> ~P x /\ A. s e. ~P x ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) } = { c e. ( Moore ` X ) | E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) } )
11 df-acs 
 |-  ACS = ( x e. _V |-> { c e. ( Moore ` x ) | E. f ( f : ~P x --> ~P x /\ A. s e. ~P x ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) } )
12 fvex 
 |-  ( Moore ` X ) e. _V
13 12 rabex 
 |-  { c e. ( Moore ` X ) | E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) } e. _V
14 10 11 13 fvmpt 
 |-  ( X e. _V -> ( ACS ` X ) = { c e. ( Moore ` X ) | E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) } )
15 14 eleq2d 
 |-  ( X e. _V -> ( C e. ( ACS ` X ) <-> C e. { c e. ( Moore ` X ) | E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) } ) )
16 eleq2 
 |-  ( c = C -> ( s e. c <-> s e. C ) )
17 16 bibi1d 
 |-  ( c = C -> ( ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) <-> ( s e. C <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) )
18 17 ralbidv 
 |-  ( c = C -> ( A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) <-> A. s e. ~P X ( s e. C <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) )
19 18 anbi2d 
 |-  ( c = C -> ( ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) <-> ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. C <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) ) )
20 19 exbidv 
 |-  ( c = C -> ( E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) <-> E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. C <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) ) )
21 20 elrab 
 |-  ( C e. { c e. ( Moore ` X ) | E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. c <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) } <-> ( C e. ( Moore ` X ) /\ E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. C <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) ) )
22 15 21 bitrdi 
 |-  ( X e. _V -> ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. C <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) ) ) )
23 1 3 22 pm5.21nii 
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ E. f ( f : ~P X --> ~P X /\ A. s e. ~P X ( s e. C <-> U. ( f " ( ~P s i^i Fin ) ) C_ s ) ) ) )