Metamath Proof Explorer


Theorem isacs2

Description: In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis isacs2.f
|- F = ( mrCls ` C )
Assertion isacs2
|- ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )

Proof

Step Hyp Ref Expression
1 isacs2.f
 |-  F = ( mrCls ` C )
2 isacs
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) ) )
3 ffun
 |-  ( f : ~P X --> ~P X -> Fun f )
4 funiunfv
 |-  ( Fun f -> U_ z e. ( ~P t i^i Fin ) ( f ` z ) = U. ( f " ( ~P t i^i Fin ) ) )
5 3 4 syl
 |-  ( f : ~P X --> ~P X -> U_ z e. ( ~P t i^i Fin ) ( f ` z ) = U. ( f " ( ~P t i^i Fin ) ) )
6 5 sseq1d
 |-  ( f : ~P X --> ~P X -> ( U_ z e. ( ~P t i^i Fin ) ( f ` z ) C_ t <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) )
7 iunss
 |-  ( U_ z e. ( ~P t i^i Fin ) ( f ` z ) C_ t <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t )
8 6 7 bitr3di
 |-  ( f : ~P X --> ~P X -> ( U. ( f " ( ~P t i^i Fin ) ) C_ t <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) )
9 8 bibi2d
 |-  ( f : ~P X --> ~P X -> ( ( t e. C <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) <-> ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) )
10 9 ralbidv
 |-  ( f : ~P X --> ~P X -> ( A. t e. ~P X ( t e. C <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) <-> A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) )
11 10 pm5.32i
 |-  ( ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) <-> ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) )
12 11 exbii
 |-  ( E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) <-> E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) )
13 simpll
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. C ) /\ y e. ( ~P s i^i Fin ) ) -> C e. ( Moore ` X ) )
14 elinel1
 |-  ( y e. ( ~P s i^i Fin ) -> y e. ~P s )
15 14 elpwid
 |-  ( y e. ( ~P s i^i Fin ) -> y C_ s )
16 15 adantl
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. C ) /\ y e. ( ~P s i^i Fin ) ) -> y C_ s )
17 simplr
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. C ) /\ y e. ( ~P s i^i Fin ) ) -> s e. C )
18 1 mrcsscl
 |-  ( ( C e. ( Moore ` X ) /\ y C_ s /\ s e. C ) -> ( F ` y ) C_ s )
19 13 16 17 18 syl3anc
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. C ) /\ y e. ( ~P s i^i Fin ) ) -> ( F ` y ) C_ s )
20 19 ralrimiva
 |-  ( ( C e. ( Moore ` X ) /\ s e. C ) -> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s )
21 20 ad4ant14
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ s e. C ) -> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s )
22 fveq2
 |-  ( z = y -> ( f ` z ) = ( f ` y ) )
23 22 sseq1d
 |-  ( z = y -> ( ( f ` z ) C_ ( F ` y ) <-> ( f ` y ) C_ ( F ` y ) ) )
24 simplll
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> C e. ( Moore ` X ) )
25 15 adantl
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> y C_ s )
26 elpwi
 |-  ( s e. ~P X -> s C_ X )
27 26 ad2antlr
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> s C_ X )
28 25 27 sstrd
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> y C_ X )
29 1 mrccl
 |-  ( ( C e. ( Moore ` X ) /\ y C_ X ) -> ( F ` y ) e. C )
30 24 28 29 syl2anc
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> ( F ` y ) e. C )
31 eleq1
 |-  ( t = ( F ` y ) -> ( t e. C <-> ( F ` y ) e. C ) )
32 pweq
 |-  ( t = ( F ` y ) -> ~P t = ~P ( F ` y ) )
33 32 ineq1d
 |-  ( t = ( F ` y ) -> ( ~P t i^i Fin ) = ( ~P ( F ` y ) i^i Fin ) )
34 sseq2
 |-  ( t = ( F ` y ) -> ( ( f ` z ) C_ t <-> ( f ` z ) C_ ( F ` y ) ) )
35 33 34 raleqbidv
 |-  ( t = ( F ` y ) -> ( A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t <-> A. z e. ( ~P ( F ` y ) i^i Fin ) ( f ` z ) C_ ( F ` y ) ) )
36 31 35 bibi12d
 |-  ( t = ( F ` y ) -> ( ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) <-> ( ( F ` y ) e. C <-> A. z e. ( ~P ( F ` y ) i^i Fin ) ( f ` z ) C_ ( F ` y ) ) ) )
37 simprr
 |-  ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) -> A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) )
38 37 ad2antrr
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) )
39 mresspw
 |-  ( C e. ( Moore ` X ) -> C C_ ~P X )
40 39 ad3antrrr
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> C C_ ~P X )
41 40 30 sseldd
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> ( F ` y ) e. ~P X )
42 36 38 41 rspcdva
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> ( ( F ` y ) e. C <-> A. z e. ( ~P ( F ` y ) i^i Fin ) ( f ` z ) C_ ( F ` y ) ) )
43 30 42 mpbid
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> A. z e. ( ~P ( F ` y ) i^i Fin ) ( f ` z ) C_ ( F ` y ) )
44 24 1 28 mrcssidd
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> y C_ ( F ` y ) )
45 vex
 |-  y e. _V
46 45 elpw
 |-  ( y e. ~P ( F ` y ) <-> y C_ ( F ` y ) )
47 44 46 sylibr
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> y e. ~P ( F ` y ) )
48 elinel2
 |-  ( y e. ( ~P s i^i Fin ) -> y e. Fin )
49 48 adantl
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> y e. Fin )
50 47 49 elind
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> y e. ( ~P ( F ` y ) i^i Fin ) )
51 23 43 50 rspcdva
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> ( f ` y ) C_ ( F ` y ) )
52 sstr2
 |-  ( ( f ` y ) C_ ( F ` y ) -> ( ( F ` y ) C_ s -> ( f ` y ) C_ s ) )
53 51 52 syl
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ y e. ( ~P s i^i Fin ) ) -> ( ( F ` y ) C_ s -> ( f ` y ) C_ s ) )
54 53 ralimdva
 |-  ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) -> ( A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s -> A. y e. ( ~P s i^i Fin ) ( f ` y ) C_ s ) )
55 54 imp
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) -> A. y e. ( ~P s i^i Fin ) ( f ` y ) C_ s )
56 fveq2
 |-  ( y = z -> ( f ` y ) = ( f ` z ) )
57 56 sseq1d
 |-  ( y = z -> ( ( f ` y ) C_ s <-> ( f ` z ) C_ s ) )
58 57 cbvralvw
 |-  ( A. y e. ( ~P s i^i Fin ) ( f ` y ) C_ s <-> A. z e. ( ~P s i^i Fin ) ( f ` z ) C_ s )
59 55 58 sylib
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) -> A. z e. ( ~P s i^i Fin ) ( f ` z ) C_ s )
60 eleq1
 |-  ( t = s -> ( t e. C <-> s e. C ) )
61 pweq
 |-  ( t = s -> ~P t = ~P s )
62 61 ineq1d
 |-  ( t = s -> ( ~P t i^i Fin ) = ( ~P s i^i Fin ) )
63 sseq2
 |-  ( t = s -> ( ( f ` z ) C_ t <-> ( f ` z ) C_ s ) )
64 62 63 raleqbidv
 |-  ( t = s -> ( A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t <-> A. z e. ( ~P s i^i Fin ) ( f ` z ) C_ s ) )
65 60 64 bibi12d
 |-  ( t = s -> ( ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) <-> ( s e. C <-> A. z e. ( ~P s i^i Fin ) ( f ` z ) C_ s ) ) )
66 37 ad2antrr
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) -> A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) )
67 simplr
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) -> s e. ~P X )
68 65 66 67 rspcdva
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) -> ( s e. C <-> A. z e. ( ~P s i^i Fin ) ( f ` z ) C_ s ) )
69 59 68 mpbird
 |-  ( ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) /\ A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) -> s e. C )
70 21 69 impbida
 |-  ( ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) /\ s e. ~P X ) -> ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) )
71 70 ralrimiva
 |-  ( ( C e. ( Moore ` X ) /\ ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) -> A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) )
72 71 ex
 |-  ( C e. ( Moore ` X ) -> ( ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) -> A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )
73 72 exlimdv
 |-  ( C e. ( Moore ` X ) -> ( E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) -> A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )
74 1 mrcf
 |-  ( C e. ( Moore ` X ) -> F : ~P X --> C )
75 74 39 fssd
 |-  ( C e. ( Moore ` X ) -> F : ~P X --> ~P X )
76 1 fvexi
 |-  F e. _V
77 feq1
 |-  ( f = F -> ( f : ~P X --> ~P X <-> F : ~P X --> ~P X ) )
78 fveq1
 |-  ( f = F -> ( f ` z ) = ( F ` z ) )
79 78 sseq1d
 |-  ( f = F -> ( ( f ` z ) C_ t <-> ( F ` z ) C_ t ) )
80 79 ralbidv
 |-  ( f = F -> ( A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t <-> A. z e. ( ~P t i^i Fin ) ( F ` z ) C_ t ) )
81 fveq2
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
82 81 sseq1d
 |-  ( z = y -> ( ( F ` z ) C_ t <-> ( F ` y ) C_ t ) )
83 82 cbvralvw
 |-  ( A. z e. ( ~P t i^i Fin ) ( F ` z ) C_ t <-> A. y e. ( ~P t i^i Fin ) ( F ` y ) C_ t )
84 80 83 bitrdi
 |-  ( f = F -> ( A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t <-> A. y e. ( ~P t i^i Fin ) ( F ` y ) C_ t ) )
85 84 bibi2d
 |-  ( f = F -> ( ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) <-> ( t e. C <-> A. y e. ( ~P t i^i Fin ) ( F ` y ) C_ t ) ) )
86 85 ralbidv
 |-  ( f = F -> ( A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) <-> A. t e. ~P X ( t e. C <-> A. y e. ( ~P t i^i Fin ) ( F ` y ) C_ t ) ) )
87 sseq2
 |-  ( t = s -> ( ( F ` y ) C_ t <-> ( F ` y ) C_ s ) )
88 62 87 raleqbidv
 |-  ( t = s -> ( A. y e. ( ~P t i^i Fin ) ( F ` y ) C_ t <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) )
89 60 88 bibi12d
 |-  ( t = s -> ( ( t e. C <-> A. y e. ( ~P t i^i Fin ) ( F ` y ) C_ t ) <-> ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )
90 89 cbvralvw
 |-  ( A. t e. ~P X ( t e. C <-> A. y e. ( ~P t i^i Fin ) ( F ` y ) C_ t ) <-> A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) )
91 86 90 bitrdi
 |-  ( f = F -> ( A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) <-> A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )
92 77 91 anbi12d
 |-  ( f = F -> ( ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) <-> ( F : ~P X --> ~P X /\ A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) ) )
93 76 92 spcev
 |-  ( ( F : ~P X --> ~P X /\ A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) -> E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) )
94 75 93 sylan
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) -> E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) )
95 94 ex
 |-  ( C e. ( Moore ` X ) -> ( A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) -> E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) ) )
96 73 95 impbid
 |-  ( C e. ( Moore ` X ) -> ( E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> A. z e. ( ~P t i^i Fin ) ( f ` z ) C_ t ) ) <-> A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )
97 12 96 syl5bb
 |-  ( C e. ( Moore ` X ) -> ( E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) <-> A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )
98 97 pm5.32i
 |-  ( ( C e. ( Moore ` X ) /\ E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. C <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )
99 2 98 bitri
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )