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