Metamath Proof Explorer

Theorem isacs1i

Description: A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion isacs1i 
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } e. ( ACS ` X ) )

Proof

Step Hyp Ref Expression
1 ssrab2 
 |-  { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } C_ ~P X
2 1 a1i 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } C_ ~P X )
3 pweq 
 |-  ( s = ( X i^i |^| t ) -> ~P s = ~P ( X i^i |^| t ) )
4 3 ineq1d 
 |-  ( s = ( X i^i |^| t ) -> ( ~P s i^i Fin ) = ( ~P ( X i^i |^| t ) i^i Fin ) )
5 4 imaeq2d 
 |-  ( s = ( X i^i |^| t ) -> ( F " ( ~P s i^i Fin ) ) = ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) )
6 5 unieqd 
 |-  ( s = ( X i^i |^| t ) -> U. ( F " ( ~P s i^i Fin ) ) = U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) )
7 id 
 |-  ( s = ( X i^i |^| t ) -> s = ( X i^i |^| t ) )
8 6 7 sseq12d 
 |-  ( s = ( X i^i |^| t ) -> ( U. ( F " ( ~P s i^i Fin ) ) C_ s <-> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ( X i^i |^| t ) ) )
9 inss1 
 |-  ( X i^i |^| t ) C_ X
10 elpw2g 
 |-  ( X e. V -> ( ( X i^i |^| t ) e. ~P X <-> ( X i^i |^| t ) C_ X ) )
11 9 10 mpbiri 
 |-  ( X e. V -> ( X i^i |^| t ) e. ~P X )
12 11 ad2antrr 
 |-  ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> ( X i^i |^| t ) e. ~P X )
13 imassrn 
 |-  ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ran F
14 frn 
 |-  ( F : ~P X --> ~P X -> ran F C_ ~P X )
15 14 adantl 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> ran F C_ ~P X )
16 13 15 sstrid 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ~P X )
17 16 unissd 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ U. ~P X )
18 unipw 
 |-  U. ~P X = X
19 17 18 sseqtrdi 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ X )
20 19 adantr 
 |-  ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ X )
21 inss2 
 |-  ( X i^i |^| t ) C_ |^| t
22 intss1 
 |-  ( a e. t -> |^| t C_ a )
23 21 22 sstrid 
 |-  ( a e. t -> ( X i^i |^| t ) C_ a )
24 23 adantl 
 |-  ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> ( X i^i |^| t ) C_ a )
25 24 sspwd 
 |-  ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> ~P ( X i^i |^| t ) C_ ~P a )
26 25 ssrind 
 |-  ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> ( ~P ( X i^i |^| t ) i^i Fin ) C_ ( ~P a i^i Fin ) )
27 imass2 
 |-  ( ( ~P ( X i^i |^| t ) i^i Fin ) C_ ( ~P a i^i Fin ) -> ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ( F " ( ~P a i^i Fin ) ) )
28 26 27 syl 
 |-  ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ( F " ( ~P a i^i Fin ) ) )
29 28 unissd 
 |-  ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ U. ( F " ( ~P a i^i Fin ) ) )
30 ssel2 
 |-  ( ( t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } /\ a e. t ) -> a e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } )
31 pweq 
 |-  ( s = a -> ~P s = ~P a )
32 31 ineq1d 
 |-  ( s = a -> ( ~P s i^i Fin ) = ( ~P a i^i Fin ) )
33 32 imaeq2d 
 |-  ( s = a -> ( F " ( ~P s i^i Fin ) ) = ( F " ( ~P a i^i Fin ) ) )
34 33 unieqd 
 |-  ( s = a -> U. ( F " ( ~P s i^i Fin ) ) = U. ( F " ( ~P a i^i Fin ) ) )
35 id 
 |-  ( s = a -> s = a )
36 34 35 sseq12d 
 |-  ( s = a -> ( U. ( F " ( ~P s i^i Fin ) ) C_ s <-> U. ( F " ( ~P a i^i Fin ) ) C_ a ) )
37 36 elrab 
 |-  ( a e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> ( a e. ~P X /\ U. ( F " ( ~P a i^i Fin ) ) C_ a ) )
38 37 simprbi 
 |-  ( a e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } -> U. ( F " ( ~P a i^i Fin ) ) C_ a )
39 30 38 syl 
 |-  ( ( t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } /\ a e. t ) -> U. ( F " ( ~P a i^i Fin ) ) C_ a )
40 39 adantll 
 |-  ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> U. ( F " ( ~P a i^i Fin ) ) C_ a )
41 29 40 sstrd 
 |-  ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ a )
42 41 ralrimiva 
 |-  ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> A. a e. t U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ a )
43 ssint 
 |-  ( U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ |^| t <-> A. a e. t U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ a )
44 42 43 sylibr 
 |-  ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ |^| t )
45 20 44 ssind 
 |-  ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ( X i^i |^| t ) )
46 8 12 45 elrabd 
 |-  ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> ( X i^i |^| t ) e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } )
47 2 46 ismred2 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } e. ( Moore ` X ) )
48 fssxp 
 |-  ( F : ~P X --> ~P X -> F C_ ( ~P X X. ~P X ) )
49 pwexg 
 |-  ( X e. V -> ~P X e. _V )
50 49 49 xpexd 
 |-  ( X e. V -> ( ~P X X. ~P X ) e. _V )
51 ssexg 
 |-  ( ( F C_ ( ~P X X. ~P X ) /\ ( ~P X X. ~P X ) e. _V ) -> F e. _V )
52 48 50 51 syl2anr 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> F e. _V )
53 simpr 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> F : ~P X --> ~P X )
54 pweq 
 |-  ( s = t -> ~P s = ~P t )
55 54 ineq1d 
 |-  ( s = t -> ( ~P s i^i Fin ) = ( ~P t i^i Fin ) )
56 55 imaeq2d 
 |-  ( s = t -> ( F " ( ~P s i^i Fin ) ) = ( F " ( ~P t i^i Fin ) ) )
57 56 unieqd 
 |-  ( s = t -> U. ( F " ( ~P s i^i Fin ) ) = U. ( F " ( ~P t i^i Fin ) ) )
58 id 
 |-  ( s = t -> s = t )
59 57 58 sseq12d 
 |-  ( s = t -> ( U. ( F " ( ~P s i^i Fin ) ) C_ s <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) )
60 59 elrab3 
 |-  ( t e. ~P X -> ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) )
61 60 rgen 
 |-  A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t )
62 53 61 jctir 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> ( F : ~P X --> ~P X /\ A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) )
63 feq1 
 |-  ( f = F -> ( f : ~P X --> ~P X <-> F : ~P X --> ~P X ) )
64 imaeq1 
 |-  ( f = F -> ( f " ( ~P t i^i Fin ) ) = ( F " ( ~P t i^i Fin ) ) )
65 64 unieqd 
 |-  ( f = F -> U. ( f " ( ~P t i^i Fin ) ) = U. ( F " ( ~P t i^i Fin ) ) )
66 65 sseq1d 
 |-  ( f = F -> ( U. ( f " ( ~P t i^i Fin ) ) C_ t <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) )
67 66 bibi2d 
 |-  ( f = F -> ( ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) <-> ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) )
68 67 ralbidv 
 |-  ( f = F -> ( A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) <-> A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) )
69 63 68 anbi12d 
 |-  ( f = F -> ( ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) <-> ( F : ~P X --> ~P X /\ A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) ) )
70 52 62 69 spcedv 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) )
71 isacs 
 |-  ( { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } e. ( ACS ` X ) <-> ( { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } e. ( Moore ` X ) /\ E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) ) )
72 47 70 71 sylanbrc 
 |-  ( ( X e. V /\ F : ~P X --> ~P X ) -> { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } e. ( ACS ` X ) )