Metamath Proof Explorer

Theorem ismrcd1

Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid ), isotone (satisfies mrcss ), and idempotent (satisfies mrcidm ) has a collection of fixed points which is a Moore collection, and itself is the closure operator for that collection. This can be taken as an alternate definition for the closure operators. This is the first half, ismrcd2 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses ismrcd.b 
|- ( ph -> B e. V )
ismrcd.f 
|- ( ph -> F : ~P B --> ~P B )
ismrcd.e 
|- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )
ismrcd.m 
|- ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )
ismrcd.i 
|- ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )
Assertion ismrcd1 
|- ( ph -> dom ( F i^i _I ) e. ( Moore ` B ) )

Proof

Step Hyp Ref Expression
1 ismrcd.b 
 |-  ( ph -> B e. V )
2 ismrcd.f 
 |-  ( ph -> F : ~P B --> ~P B )
3 ismrcd.e 
 |-  ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )
4 ismrcd.m 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )
5 ismrcd.i 
 |-  ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )
6 inss1 
 |-  ( F i^i _I ) C_ F
7 dmss 
 |-  ( ( F i^i _I ) C_ F -> dom ( F i^i _I ) C_ dom F )
8 6 7 ax-mp 
 |-  dom ( F i^i _I ) C_ dom F
9 8 2 fssdm 
 |-  ( ph -> dom ( F i^i _I ) C_ ~P B )
10 ssid 
 |-  B C_ B
11 elpwg 
 |-  ( B e. V -> ( B e. ~P B <-> B C_ B ) )
12 1 11 syl 
 |-  ( ph -> ( B e. ~P B <-> B C_ B ) )
13 10 12 mpbiri 
 |-  ( ph -> B e. ~P B )
14 2 13 ffvelrnd 
 |-  ( ph -> ( F ` B ) e. ~P B )
15 14 elpwid 
 |-  ( ph -> ( F ` B ) C_ B )
16 velpw 
 |-  ( x e. ~P B <-> x C_ B )
17 16 3 sylan2b 
 |-  ( ( ph /\ x e. ~P B ) -> x C_ ( F ` x ) )
18 17 ralrimiva 
 |-  ( ph -> A. x e. ~P B x C_ ( F ` x ) )
19 id 
 |-  ( x = B -> x = B )
20 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
21 19 20 sseq12d 
 |-  ( x = B -> ( x C_ ( F ` x ) <-> B C_ ( F ` B ) ) )
22 21 rspcva 
 |-  ( ( B e. ~P B /\ A. x e. ~P B x C_ ( F ` x ) ) -> B C_ ( F ` B ) )
23 13 18 22 syl2anc 
 |-  ( ph -> B C_ ( F ` B ) )
24 15 23 eqssd 
 |-  ( ph -> ( F ` B ) = B )
25 2 ffnd 
 |-  ( ph -> F Fn ~P B )
26 fnelfp 
 |-  ( ( F Fn ~P B /\ B e. ~P B ) -> ( B e. dom ( F i^i _I ) <-> ( F ` B ) = B ) )
27 25 13 26 syl2anc 
 |-  ( ph -> ( B e. dom ( F i^i _I ) <-> ( F ` B ) = B ) )
28 24 27 mpbird 
 |-  ( ph -> B e. dom ( F i^i _I ) )
29 simp2 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> z C_ dom ( F i^i _I ) )
30 9 3ad2ant1 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> dom ( F i^i _I ) C_ ~P B )
31 29 30 sstrd 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> z C_ ~P B )
32 simp3 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> z =/= (/) )
33 intssuni2 
 |-  ( ( z C_ ~P B /\ z =/= (/) ) -> |^| z C_ U. ~P B )
34 31 32 33 syl2anc 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> |^| z C_ U. ~P B )
35 unipw 
 |-  U. ~P B = B
36 34 35 sseqtrdi 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> |^| z C_ B )
37 intex 
 |-  ( z =/= (/) <-> |^| z e. _V )
38 elpwg 
 |-  ( |^| z e. _V -> ( |^| z e. ~P B <-> |^| z C_ B ) )
39 37 38 sylbi 
 |-  ( z =/= (/) -> ( |^| z e. ~P B <-> |^| z C_ B ) )
40 39 3ad2ant3 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> ( |^| z e. ~P B <-> |^| z C_ B ) )
41 36 40 mpbird 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> |^| z e. ~P B )
42 41 adantr 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> |^| z e. ~P B )
43 4 3expib 
 |-  ( ph -> ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
44 43 alrimiv 
 |-  ( ph -> A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
45 44 3ad2ant1 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
46 45 adantr 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
47 31 sselda 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> x e. ~P B )
48 47 elpwid 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> x C_ B )
49 intss1 
 |-  ( x e. z -> |^| z C_ x )
50 49 adantl 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> |^| z C_ x )
51 48 50 jca 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> ( x C_ B /\ |^| z C_ x ) )
52 sseq1 
 |-  ( y = |^| z -> ( y C_ x <-> |^| z C_ x ) )
53 52 anbi2d 
 |-  ( y = |^| z -> ( ( x C_ B /\ y C_ x ) <-> ( x C_ B /\ |^| z C_ x ) ) )
54 fveq2 
 |-  ( y = |^| z -> ( F ` y ) = ( F ` |^| z ) )
55 54 sseq1d 
 |-  ( y = |^| z -> ( ( F ` y ) C_ ( F ` x ) <-> ( F ` |^| z ) C_ ( F ` x ) ) )
56 53 55 imbi12d 
 |-  ( y = |^| z -> ( ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) <-> ( ( x C_ B /\ |^| z C_ x ) -> ( F ` |^| z ) C_ ( F ` x ) ) ) )
57 56 spcgv 
 |-  ( |^| z e. ~P B -> ( A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) -> ( ( x C_ B /\ |^| z C_ x ) -> ( F ` |^| z ) C_ ( F ` x ) ) ) )
58 42 46 51 57 syl3c 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> ( F ` |^| z ) C_ ( F ` x ) )
59 29 sselda 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> x e. dom ( F i^i _I ) )
60 25 3ad2ant1 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> F Fn ~P B )
61 60 adantr 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> F Fn ~P B )
62 fnelfp 
 |-  ( ( F Fn ~P B /\ x e. ~P B ) -> ( x e. dom ( F i^i _I ) <-> ( F ` x ) = x ) )
63 61 47 62 syl2anc 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> ( x e. dom ( F i^i _I ) <-> ( F ` x ) = x ) )
64 59 63 mpbid 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> ( F ` x ) = x )
65 58 64 sseqtrd 
 |-  ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> ( F ` |^| z ) C_ x )
66 65 ralrimiva 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> A. x e. z ( F ` |^| z ) C_ x )
67 ssint 
 |-  ( ( F ` |^| z ) C_ |^| z <-> A. x e. z ( F ` |^| z ) C_ x )
68 66 67 sylibr 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> ( F ` |^| z ) C_ |^| z )
69 18 3ad2ant1 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> A. x e. ~P B x C_ ( F ` x ) )
70 id 
 |-  ( x = |^| z -> x = |^| z )
71 fveq2 
 |-  ( x = |^| z -> ( F ` x ) = ( F ` |^| z ) )
72 70 71 sseq12d 
 |-  ( x = |^| z -> ( x C_ ( F ` x ) <-> |^| z C_ ( F ` |^| z ) ) )
73 72 rspcva 
 |-  ( ( |^| z e. ~P B /\ A. x e. ~P B x C_ ( F ` x ) ) -> |^| z C_ ( F ` |^| z ) )
74 41 69 73 syl2anc 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> |^| z C_ ( F ` |^| z ) )
75 68 74 eqssd 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> ( F ` |^| z ) = |^| z )
76 fnelfp 
 |-  ( ( F Fn ~P B /\ |^| z e. ~P B ) -> ( |^| z e. dom ( F i^i _I ) <-> ( F ` |^| z ) = |^| z ) )
77 60 41 76 syl2anc 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> ( |^| z e. dom ( F i^i _I ) <-> ( F ` |^| z ) = |^| z ) )
78 75 77 mpbird 
 |-  ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> |^| z e. dom ( F i^i _I ) )
79 9 28 78 ismred 
 |-  ( ph -> dom ( F i^i _I ) e. ( Moore ` B ) )