Metamath Proof Explorer

Theorem ismrc

Description: A function is a Moore closure operator iff it satisfies mrcssid , mrcss , and mrcidm . (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion ismrc 
|- ( F e. ( mrCls " ( Moore ` B ) ) <-> ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fnmrc 
 |-  mrCls Fn U. ran Moore
2 fnfun 
 |-  ( mrCls Fn U. ran Moore -> Fun mrCls )
3 1 2 ax-mp 
 |-  Fun mrCls
4 fvelima 
 |-  ( ( Fun mrCls /\ F e. ( mrCls " ( Moore ` B ) ) ) -> E. z e. ( Moore ` B ) ( mrCls ` z ) = F )
5 3 4 mpan 
 |-  ( F e. ( mrCls " ( Moore ` B ) ) -> E. z e. ( Moore ` B ) ( mrCls ` z ) = F )
6 elfvex 
 |-  ( z e. ( Moore ` B ) -> B e. _V )
7 eqid 
 |-  ( mrCls ` z ) = ( mrCls ` z )
8 7 mrcf 
 |-  ( z e. ( Moore ` B ) -> ( mrCls ` z ) : ~P B --> z )
9 mresspw 
 |-  ( z e. ( Moore ` B ) -> z C_ ~P B )
10 8 9 fssd 
 |-  ( z e. ( Moore ` B ) -> ( mrCls ` z ) : ~P B --> ~P B )
11 7 mrcssid 
 |-  ( ( z e. ( Moore ` B ) /\ x C_ B ) -> x C_ ( ( mrCls ` z ) ` x ) )
12 11 adantrr 
 |-  ( ( z e. ( Moore ` B ) /\ ( x C_ B /\ y C_ x ) ) -> x C_ ( ( mrCls ` z ) ` x ) )
13 7 mrcss 
 |-  ( ( z e. ( Moore ` B ) /\ y C_ x /\ x C_ B ) -> ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) )
14 13 3expb 
 |-  ( ( z e. ( Moore ` B ) /\ ( y C_ x /\ x C_ B ) ) -> ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) )
15 14 ancom2s 
 |-  ( ( z e. ( Moore ` B ) /\ ( x C_ B /\ y C_ x ) ) -> ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) )
16 7 mrcidm 
 |-  ( ( z e. ( Moore ` B ) /\ x C_ B ) -> ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) )
17 16 adantrr 
 |-  ( ( z e. ( Moore ` B ) /\ ( x C_ B /\ y C_ x ) ) -> ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) )
18 12 15 17 3jca 
 |-  ( ( z e. ( Moore ` B ) /\ ( x C_ B /\ y C_ x ) ) -> ( x C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) ) )
19 18 ex 
 |-  ( z e. ( Moore ` B ) -> ( ( x C_ B /\ y C_ x ) -> ( x C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) ) ) )
20 19 alrimivv 
 |-  ( z e. ( Moore ` B ) -> A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) ) ) )
21 6 10 20 3jca 
 |-  ( z e. ( Moore ` B ) -> ( B e. _V /\ ( mrCls ` z ) : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) ) ) ) )
22 feq1 
 |-  ( ( mrCls ` z ) = F -> ( ( mrCls ` z ) : ~P B --> ~P B <-> F : ~P B --> ~P B ) )
23 fveq1 
 |-  ( ( mrCls ` z ) = F -> ( ( mrCls ` z ) ` x ) = ( F ` x ) )
24 23 sseq2d 
 |-  ( ( mrCls ` z ) = F -> ( x C_ ( ( mrCls ` z ) ` x ) <-> x C_ ( F ` x ) ) )
25 fveq1 
 |-  ( ( mrCls ` z ) = F -> ( ( mrCls ` z ) ` y ) = ( F ` y ) )
26 25 23 sseq12d 
 |-  ( ( mrCls ` z ) = F -> ( ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) <-> ( F ` y ) C_ ( F ` x ) ) )
27 id 
 |-  ( ( mrCls ` z ) = F -> ( mrCls ` z ) = F )
28 27 23 fveq12d 
 |-  ( ( mrCls ` z ) = F -> ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( F ` ( F ` x ) ) )
29 28 23 eqeq12d 
 |-  ( ( mrCls ` z ) = F -> ( ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) <-> ( F ` ( F ` x ) ) = ( F ` x ) ) )
30 24 26 29 3anbi123d 
 |-  ( ( mrCls ` z ) = F -> ( ( x C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) ) <-> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) )
31 30 imbi2d 
 |-  ( ( mrCls ` z ) = F -> ( ( ( x C_ B /\ y C_ x ) -> ( x C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) ) ) <-> ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) )
32 31 2albidv 
 |-  ( ( mrCls ` z ) = F -> ( A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) ) ) <-> A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) )
33 22 32 3anbi23d 
 |-  ( ( mrCls ` z ) = F -> ( ( B e. _V /\ ( mrCls ` z ) : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` y ) C_ ( ( mrCls ` z ) ` x ) /\ ( ( mrCls ` z ) ` ( ( mrCls ` z ) ` x ) ) = ( ( mrCls ` z ) ` x ) ) ) ) <-> ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) ) )
34 21 33 syl5ibcom 
 |-  ( z e. ( Moore ` B ) -> ( ( mrCls ` z ) = F -> ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) ) )
35 34 rexlimiv 
 |-  ( E. z e. ( Moore ` B ) ( mrCls ` z ) = F -> ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) )
36 5 35 syl 
 |-  ( F e. ( mrCls " ( Moore ` B ) ) -> ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) )
37 simp1 
 |-  ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) -> B e. _V )
38 simp2 
 |-  ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) -> F : ~P B --> ~P B )
39 ssid 
 |-  z C_ z
40 3simpb 
 |-  ( ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) -> ( x C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) )
41 40 imim2i 
 |-  ( ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) -> ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) )
42 41 2alimi 
 |-  ( A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) -> A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) )
43 sseq1 
 |-  ( x = z -> ( x C_ B <-> z C_ B ) )
44 43 adantr 
 |-  ( ( x = z /\ y = z ) -> ( x C_ B <-> z C_ B ) )
45 sseq12 
 |-  ( ( y = z /\ x = z ) -> ( y C_ x <-> z C_ z ) )
46 45 ancoms 
 |-  ( ( x = z /\ y = z ) -> ( y C_ x <-> z C_ z ) )
47 44 46 anbi12d 
 |-  ( ( x = z /\ y = z ) -> ( ( x C_ B /\ y C_ x ) <-> ( z C_ B /\ z C_ z ) ) )
48 id 
 |-  ( x = z -> x = z )
49 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
50 48 49 sseq12d 
 |-  ( x = z -> ( x C_ ( F ` x ) <-> z C_ ( F ` z ) ) )
51 50 adantr 
 |-  ( ( x = z /\ y = z ) -> ( x C_ ( F ` x ) <-> z C_ ( F ` z ) ) )
52 2fveq3 
 |-  ( x = z -> ( F ` ( F ` x ) ) = ( F ` ( F ` z ) ) )
53 52 49 eqeq12d 
 |-  ( x = z -> ( ( F ` ( F ` x ) ) = ( F ` x ) <-> ( F ` ( F ` z ) ) = ( F ` z ) ) )
54 53 adantr 
 |-  ( ( x = z /\ y = z ) -> ( ( F ` ( F ` x ) ) = ( F ` x ) <-> ( F ` ( F ` z ) ) = ( F ` z ) ) )
55 51 54 anbi12d 
 |-  ( ( x = z /\ y = z ) -> ( ( x C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) <-> ( z C_ ( F ` z ) /\ ( F ` ( F ` z ) ) = ( F ` z ) ) ) )
56 47 55 imbi12d 
 |-  ( ( x = z /\ y = z ) -> ( ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) <-> ( ( z C_ B /\ z C_ z ) -> ( z C_ ( F ` z ) /\ ( F ` ( F ` z ) ) = ( F ` z ) ) ) ) )
57 56 spc2gv 
 |-  ( ( z e. _V /\ z e. _V ) -> ( A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) -> ( ( z C_ B /\ z C_ z ) -> ( z C_ ( F ` z ) /\ ( F ` ( F ` z ) ) = ( F ` z ) ) ) ) )
58 57 el2v 
 |-  ( A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) -> ( ( z C_ B /\ z C_ z ) -> ( z C_ ( F ` z ) /\ ( F ` ( F ` z ) ) = ( F ` z ) ) ) )
59 42 58 syl 
 |-  ( A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) -> ( ( z C_ B /\ z C_ z ) -> ( z C_ ( F ` z ) /\ ( F ` ( F ` z ) ) = ( F ` z ) ) ) )
60 59 3ad2ant3 
 |-  ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) -> ( ( z C_ B /\ z C_ z ) -> ( z C_ ( F ` z ) /\ ( F ` ( F ` z ) ) = ( F ` z ) ) ) )
61 39 60 mpan2i 
 |-  ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) -> ( z C_ B -> ( z C_ ( F ` z ) /\ ( F ` ( F ` z ) ) = ( F ` z ) ) ) )
62 61 imp 
 |-  ( ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) /\ z C_ B ) -> ( z C_ ( F ` z ) /\ ( F ` ( F ` z ) ) = ( F ` z ) ) )
63 62 simpld 
 |-  ( ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) /\ z C_ B ) -> z C_ ( F ` z ) )
64 simp2 
 |-  ( ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) -> ( F ` y ) C_ ( F ` x ) )
65 64 imim2i 
 |-  ( ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) -> ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
66 65 2alimi 
 |-  ( A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) -> A. x A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
67 66 3ad2ant3 
 |-  ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) -> A. x A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
68 43 adantr 
 |-  ( ( x = z /\ y = w ) -> ( x C_ B <-> z C_ B ) )
69 sseq12 
 |-  ( ( y = w /\ x = z ) -> ( y C_ x <-> w C_ z ) )
70 69 ancoms 
 |-  ( ( x = z /\ y = w ) -> ( y C_ x <-> w C_ z ) )
71 68 70 anbi12d 
 |-  ( ( x = z /\ y = w ) -> ( ( x C_ B /\ y C_ x ) <-> ( z C_ B /\ w C_ z ) ) )
72 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
73 sseq12 
 |-  ( ( ( F ` y ) = ( F ` w ) /\ ( F ` x ) = ( F ` z ) ) -> ( ( F ` y ) C_ ( F ` x ) <-> ( F ` w ) C_ ( F ` z ) ) )
74 72 49 73 syl2anr 
 |-  ( ( x = z /\ y = w ) -> ( ( F ` y ) C_ ( F ` x ) <-> ( F ` w ) C_ ( F ` z ) ) )
75 71 74 imbi12d 
 |-  ( ( x = z /\ y = w ) -> ( ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) <-> ( ( z C_ B /\ w C_ z ) -> ( F ` w ) C_ ( F ` z ) ) ) )
76 75 spc2gv 
 |-  ( ( z e. _V /\ w e. _V ) -> ( A. x A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) -> ( ( z C_ B /\ w C_ z ) -> ( F ` w ) C_ ( F ` z ) ) ) )
77 76 el2v 
 |-  ( A. x A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) -> ( ( z C_ B /\ w C_ z ) -> ( F ` w ) C_ ( F ` z ) ) )
78 67 77 syl 
 |-  ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) -> ( ( z C_ B /\ w C_ z ) -> ( F ` w ) C_ ( F ` z ) ) )
79 78 3impib 
 |-  ( ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) /\ z C_ B /\ w C_ z ) -> ( F ` w ) C_ ( F ` z ) )
80 62 simprd 
 |-  ( ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) /\ z C_ B ) -> ( F ` ( F ` z ) ) = ( F ` z ) )
81 37 38 63 79 80 ismrcd2 
 |-  ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) -> F = ( mrCls ` dom ( F i^i _I ) ) )
82 37 38 63 79 80 ismrcd1 
 |-  ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) -> dom ( F i^i _I ) e. ( Moore ` B ) )
83 fvssunirn 
 |-  ( Moore ` B ) C_ U. ran Moore
84 1 fndmi 
 |-  dom mrCls = U. ran Moore
85 83 84 sseqtrri 
 |-  ( Moore ` B ) C_ dom mrCls
86 funfvima2 
 |-  ( ( Fun mrCls /\ ( Moore ` B ) C_ dom mrCls ) -> ( dom ( F i^i _I ) e. ( Moore ` B ) -> ( mrCls ` dom ( F i^i _I ) ) e. ( mrCls " ( Moore ` B ) ) ) )
87 3 85 86 mp2an 
 |-  ( dom ( F i^i _I ) e. ( Moore ` B ) -> ( mrCls ` dom ( F i^i _I ) ) e. ( mrCls " ( Moore ` B ) ) )
88 82 87 syl 
 |-  ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) -> ( mrCls ` dom ( F i^i _I ) ) e. ( mrCls " ( Moore ` B ) ) )
89 81 88 eqeltrd 
 |-  ( ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) -> F e. ( mrCls " ( Moore ` B ) ) )
90 36 89 impbii 
 |-  ( F e. ( mrCls " ( Moore ` B ) ) <-> ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) )