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