Metamath Proof Explorer

Theorem isnacs3

Description: A choice-free order equivalent to the Noetherian condition on a closure system. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Assertion isnacs3 
|- ( C e. ( NoeACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) )

Proof

Step Hyp Ref Expression
1 nacsacs 
 |-  ( C e. ( NoeACS ` X ) -> C e. ( ACS ` X ) )
2 1 acsmred 
 |-  ( C e. ( NoeACS ` X ) -> C e. ( Moore ` X ) )
3 simpll 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> C e. ( NoeACS ` X ) )
4 1 ad2antrr 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> C e. ( ACS ` X ) )
5 elpwi 
 |-  ( s e. ~P C -> s C_ C )
6 5 ad2antlr 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> s C_ C )
7 simpr 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> ( toInc ` s ) e. Dirset )
8 acsdrsel 
 |-  ( ( C e. ( ACS ` X ) /\ s C_ C /\ ( toInc ` s ) e. Dirset ) -> U. s e. C )
9 4 6 7 8 syl3anc 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> U. s e. C )
10 eqid 
 |-  ( mrCls ` C ) = ( mrCls ` C )
11 10 nacsfg 
 |-  ( ( C e. ( NoeACS ` X ) /\ U. s e. C ) -> E. g e. ( ~P X i^i Fin ) U. s = ( ( mrCls ` C ) ` g ) )
12 3 9 11 syl2anc 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> E. g e. ( ~P X i^i Fin ) U. s = ( ( mrCls ` C ) ` g ) )
13 10 mrefg2 
 |-  ( C e. ( Moore ` X ) -> ( E. g e. ( ~P X i^i Fin ) U. s = ( ( mrCls ` C ) ` g ) <-> E. g e. ( ~P U. s i^i Fin ) U. s = ( ( mrCls ` C ) ` g ) ) )
14 2 13 syl 
 |-  ( C e. ( NoeACS ` X ) -> ( E. g e. ( ~P X i^i Fin ) U. s = ( ( mrCls ` C ) ` g ) <-> E. g e. ( ~P U. s i^i Fin ) U. s = ( ( mrCls ` C ) ` g ) ) )
15 14 ad2antrr 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> ( E. g e. ( ~P X i^i Fin ) U. s = ( ( mrCls ` C ) ` g ) <-> E. g e. ( ~P U. s i^i Fin ) U. s = ( ( mrCls ` C ) ` g ) ) )
16 12 15 mpbid 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> E. g e. ( ~P U. s i^i Fin ) U. s = ( ( mrCls ` C ) ` g ) )
17 elfpw 
 |-  ( g e. ( ~P U. s i^i Fin ) <-> ( g C_ U. s /\ g e. Fin ) )
18 fissuni 
 |-  ( ( g C_ U. s /\ g e. Fin ) -> E. h e. ( ~P s i^i Fin ) g C_ U. h )
19 17 18 sylbi 
 |-  ( g e. ( ~P U. s i^i Fin ) -> E. h e. ( ~P s i^i Fin ) g C_ U. h )
20 elfpw 
 |-  ( h e. ( ~P s i^i Fin ) <-> ( h C_ s /\ h e. Fin ) )
21 ipodrsfi 
 |-  ( ( ( toInc ` s ) e. Dirset /\ h C_ s /\ h e. Fin ) -> E. i e. s U. h C_ i )
22 21 3expb 
 |-  ( ( ( toInc ` s ) e. Dirset /\ ( h C_ s /\ h e. Fin ) ) -> E. i e. s U. h C_ i )
23 20 22 sylan2b 
 |-  ( ( ( toInc ` s ) e. Dirset /\ h e. ( ~P s i^i Fin ) ) -> E. i e. s U. h C_ i )
24 sstr 
 |-  ( ( g C_ U. h /\ U. h C_ i ) -> g C_ i )
25 24 ancoms 
 |-  ( ( U. h C_ i /\ g C_ U. h ) -> g C_ i )
26 simpr 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) /\ U. s = ( ( mrCls ` C ) ` g ) ) -> U. s = ( ( mrCls ` C ) ` g ) )
27 2 ad2antrr 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) -> C e. ( Moore ` X ) )
28 simprr 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) -> g C_ i )
29 5 ad2antlr 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) -> s C_ C )
30 simprl 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) -> i e. s )
31 29 30 sseldd 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) -> i e. C )
32 10 mrcsscl 
 |-  ( ( C e. ( Moore ` X ) /\ g C_ i /\ i e. C ) -> ( ( mrCls ` C ) ` g ) C_ i )
33 27 28 31 32 syl3anc 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) -> ( ( mrCls ` C ) ` g ) C_ i )
34 33 adantr 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) /\ U. s = ( ( mrCls ` C ) ` g ) ) -> ( ( mrCls ` C ) ` g ) C_ i )
35 26 34 eqsstrd 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) /\ U. s = ( ( mrCls ` C ) ` g ) ) -> U. s C_ i )
36 simplrl 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) /\ U. s = ( ( mrCls ` C ) ` g ) ) -> i e. s )
37 elssuni 
 |-  ( i e. s -> i C_ U. s )
38 36 37 syl 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) /\ U. s = ( ( mrCls ` C ) ` g ) ) -> i C_ U. s )
39 35 38 eqssd 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) /\ U. s = ( ( mrCls ` C ) ` g ) ) -> U. s = i )
40 39 36 eqeltrd 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) /\ U. s = ( ( mrCls ` C ) ` g ) ) -> U. s e. s )
41 40 ex 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( i e. s /\ g C_ i ) ) -> ( U. s = ( ( mrCls ` C ) ` g ) -> U. s e. s ) )
42 41 expr 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ i e. s ) -> ( g C_ i -> ( U. s = ( ( mrCls ` C ) ` g ) -> U. s e. s ) ) )
43 25 42 syl5 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ i e. s ) -> ( ( U. h C_ i /\ g C_ U. h ) -> ( U. s = ( ( mrCls ` C ) ` g ) -> U. s e. s ) ) )
44 43 expd 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ i e. s ) -> ( U. h C_ i -> ( g C_ U. h -> ( U. s = ( ( mrCls ` C ) ` g ) -> U. s e. s ) ) ) )
45 44 rexlimdva 
 |-  ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) -> ( E. i e. s U. h C_ i -> ( g C_ U. h -> ( U. s = ( ( mrCls ` C ) ` g ) -> U. s e. s ) ) ) )
46 23 45 syl5 
 |-  ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) -> ( ( ( toInc ` s ) e. Dirset /\ h e. ( ~P s i^i Fin ) ) -> ( g C_ U. h -> ( U. s = ( ( mrCls ` C ) ` g ) -> U. s e. s ) ) ) )
47 46 expdimp 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> ( h e. ( ~P s i^i Fin ) -> ( g C_ U. h -> ( U. s = ( ( mrCls ` C ) ` g ) -> U. s e. s ) ) ) )
48 47 rexlimdv 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> ( E. h e. ( ~P s i^i Fin ) g C_ U. h -> ( U. s = ( ( mrCls ` C ) ` g ) -> U. s e. s ) ) )
49 19 48 syl5 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> ( g e. ( ~P U. s i^i Fin ) -> ( U. s = ( ( mrCls ` C ) ` g ) -> U. s e. s ) ) )
50 49 rexlimdv 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> ( E. g e. ( ~P U. s i^i Fin ) U. s = ( ( mrCls ` C ) ` g ) -> U. s e. s ) )
51 16 50 mpd 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> U. s e. s )
52 51 ex 
 |-  ( ( C e. ( NoeACS ` X ) /\ s e. ~P C ) -> ( ( toInc ` s ) e. Dirset -> U. s e. s ) )
53 52 ralrimiva 
 |-  ( C e. ( NoeACS ` X ) -> A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) )
54 2 53 jca 
 |-  ( C e. ( NoeACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) )
55 simpl 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) -> C e. ( Moore ` X ) )
56 5 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ s e. ~P C ) -> s C_ C )
57 56 sseld 
 |-  ( ( C e. ( Moore ` X ) /\ s e. ~P C ) -> ( U. s e. s -> U. s e. C ) )
58 57 imim2d 
 |-  ( ( C e. ( Moore ` X ) /\ s e. ~P C ) -> ( ( ( toInc ` s ) e. Dirset -> U. s e. s ) -> ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )
59 58 ralimdva 
 |-  ( C e. ( Moore ` X ) -> ( A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) -> A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )
60 59 imp 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) -> A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) )
61 isacs3 
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )
62 55 60 61 sylanbrc 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) -> C e. ( ACS ` X ) )
63 10 mrcid 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> ( ( mrCls ` C ) ` t ) = t )
64 63 adantlr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> ( ( mrCls ` C ) ` t ) = t )
65 62 adantr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> C e. ( ACS ` X ) )
66 mress 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> t C_ X )
67 66 adantlr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> t C_ X )
68 65 10 67 acsficld 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> ( ( mrCls ` C ) ` t ) = U. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) )
69 64 68 eqtr3d 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> t = U. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) )
70 10 mrcf 
 |-  ( C e. ( Moore ` X ) -> ( mrCls ` C ) : ~P X --> C )
71 70 ffnd 
 |-  ( C e. ( Moore ` X ) -> ( mrCls ` C ) Fn ~P X )
72 71 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> ( mrCls ` C ) Fn ~P X )
73 10 mrcss 
 |-  ( ( C e. ( Moore ` X ) /\ g C_ h /\ h C_ X ) -> ( ( mrCls ` C ) ` g ) C_ ( ( mrCls ` C ) ` h ) )
74 73 3expb 
 |-  ( ( C e. ( Moore ` X ) /\ ( g C_ h /\ h C_ X ) ) -> ( ( mrCls ` C ) ` g ) C_ ( ( mrCls ` C ) ` h ) )
75 74 adantlr 
 |-  ( ( ( C e. ( Moore ` X ) /\ t e. C ) /\ ( g C_ h /\ h C_ X ) ) -> ( ( mrCls ` C ) ` g ) C_ ( ( mrCls ` C ) ` h ) )
76 vex 
 |-  t e. _V
77 fpwipodrs 
 |-  ( t e. _V -> ( toInc ` ( ~P t i^i Fin ) ) e. Dirset )
78 76 77 mp1i 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> ( toInc ` ( ~P t i^i Fin ) ) e. Dirset )
79 inss1 
 |-  ( ~P t i^i Fin ) C_ ~P t
80 66 sspwd 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> ~P t C_ ~P X )
81 79 80 sstrid 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> ( ~P t i^i Fin ) C_ ~P X )
82 fvex 
 |-  ( mrCls ` C ) e. _V
83 imaexg 
 |-  ( ( mrCls ` C ) e. _V -> ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. _V )
84 82 83 ax-mp 
 |-  ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. _V
85 84 a1i 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. _V )
86 72 75 78 81 85 ipodrsima 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> ( toInc ` ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) e. Dirset )
87 86 adantlr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> ( toInc ` ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) e. Dirset )
88 imassrn 
 |-  ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) C_ ran ( mrCls ` C )
89 70 frnd 
 |-  ( C e. ( Moore ` X ) -> ran ( mrCls ` C ) C_ C )
90 88 89 sstrid 
 |-  ( C e. ( Moore ` X ) -> ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) C_ C )
91 90 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) C_ C )
92 84 elpw 
 |-  ( ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. ~P C <-> ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) C_ C )
93 91 92 sylibr 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. ~P C )
94 93 adantlr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. ~P C )
95 simplr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) )
96 fveq2 
 |-  ( s = ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) -> ( toInc ` s ) = ( toInc ` ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) )
97 96 eleq1d 
 |-  ( s = ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) -> ( ( toInc ` s ) e. Dirset <-> ( toInc ` ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) e. Dirset ) )
98 unieq 
 |-  ( s = ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) -> U. s = U. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) )
99 id 
 |-  ( s = ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) -> s = ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) )
100 98 99 eleq12d 
 |-  ( s = ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) -> ( U. s e. s <-> U. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) )
101 97 100 imbi12d 
 |-  ( s = ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) -> ( ( ( toInc ` s ) e. Dirset -> U. s e. s ) <-> ( ( toInc ` ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) e. Dirset -> U. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) ) )
102 101 rspcva 
 |-  ( ( ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. ~P C /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) -> ( ( toInc ` ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) e. Dirset -> U. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) )
103 94 95 102 syl2anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> ( ( toInc ` ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) e. Dirset -> U. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) ) )
104 87 103 mpd 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> U. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) e. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) )
105 69 104 eqeltrd 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> t e. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) )
106 fvelimab 
 |-  ( ( ( mrCls ` C ) Fn ~P X /\ ( ~P t i^i Fin ) C_ ~P X ) -> ( t e. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) <-> E. g e. ( ~P t i^i Fin ) ( ( mrCls ` C ) ` g ) = t ) )
107 72 81 106 syl2anc 
 |-  ( ( C e. ( Moore ` X ) /\ t e. C ) -> ( t e. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) <-> E. g e. ( ~P t i^i Fin ) ( ( mrCls ` C ) ` g ) = t ) )
108 107 adantlr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> ( t e. ( ( mrCls ` C ) " ( ~P t i^i Fin ) ) <-> E. g e. ( ~P t i^i Fin ) ( ( mrCls ` C ) ` g ) = t ) )
109 105 108 mpbid 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> E. g e. ( ~P t i^i Fin ) ( ( mrCls ` C ) ` g ) = t )
110 eqcom 
 |-  ( t = ( ( mrCls ` C ) ` g ) <-> ( ( mrCls ` C ) ` g ) = t )
111 110 rexbii 
 |-  ( E. g e. ( ~P t i^i Fin ) t = ( ( mrCls ` C ) ` g ) <-> E. g e. ( ~P t i^i Fin ) ( ( mrCls ` C ) ` g ) = t )
112 109 111 sylibr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> E. g e. ( ~P t i^i Fin ) t = ( ( mrCls ` C ) ` g ) )
113 10 mrefg2 
 |-  ( C e. ( Moore ` X ) -> ( E. g e. ( ~P X i^i Fin ) t = ( ( mrCls ` C ) ` g ) <-> E. g e. ( ~P t i^i Fin ) t = ( ( mrCls ` C ) ` g ) ) )
114 113 ad2antrr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> ( E. g e. ( ~P X i^i Fin ) t = ( ( mrCls ` C ) ` g ) <-> E. g e. ( ~P t i^i Fin ) t = ( ( mrCls ` C ) ` g ) ) )
115 112 114 mpbird 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) /\ t e. C ) -> E. g e. ( ~P X i^i Fin ) t = ( ( mrCls ` C ) ` g ) )
116 115 ralrimiva 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) -> A. t e. C E. g e. ( ~P X i^i Fin ) t = ( ( mrCls ` C ) ` g ) )
117 10 isnacs 
 |-  ( C e. ( NoeACS ` X ) <-> ( C e. ( ACS ` X ) /\ A. t e. C E. g e. ( ~P X i^i Fin ) t = ( ( mrCls ` C ) ` g ) ) )
118 62 116 117 sylanbrc 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) -> C e. ( NoeACS ` X ) )
119 54 118 impbii 
 |-  ( C e. ( NoeACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. s ) ) )