Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ismrcd1 Unicode version

Theorem ismrcd1 26172
Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 13513), isotone (satisfies mrcss 13512), and idempotent (satisfies mrcidm 13515) 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 26173 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Hypotheses
Ref Expression
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
Ref Expression
ismrcd1  |-  ( ph  ->  dom  (  F  i^i  _I  )  e.  (Moore `  B ) )
Distinct variable groups:    ph, x, y   
x, B, y    x, F, y    x, V, y

Proof of Theorem ismrcd1
StepHypRef Expression
1 inss1 3390 . . . 4  |-  ( F  i^i  _I  )  C_  F
2 dmss 4877 . . . 4  |-  ( ( F  i^i  _I  )  C_  F  ->  dom  (  F  i^i  _I  )  C_  dom  F )
31, 2ax-mp 10 . . 3  |-  dom  (  F  i^i  _I  )  C_  dom  F
4 ismrcd.f . . . 4  |-  ( ph  ->  F : ~P B --> ~P B )
5 fdm 5358 . . . 4  |-  ( F : ~P B --> ~P B  ->  dom  F  =  ~P B )
64, 5syl 17 . . 3  |-  ( ph  ->  dom  F  =  ~P B )
73, 6syl5sseq 3227 . 2  |-  ( ph  ->  dom  (  F  i^i  _I  )  C_  ~P B
)
8 ssid 3198 . . . . . . 7  |-  B  C_  B
9 ismrcd.b . . . . . . . 8  |-  ( ph  ->  B  e.  V )
10 elpwg 3633 . . . . . . . 8  |-  ( B  e.  V  ->  ( B  e.  ~P B  <->  B 
C_  B ) )
119, 10syl 17 . . . . . . 7  |-  ( ph  ->  ( B  e.  ~P B 
<->  B  C_  B )
)
128, 11mpbiri 226 . . . . . 6  |-  ( ph  ->  B  e.  ~P B
)
13 ffvelrn 5624 . . . . . 6  |-  ( ( F : ~P B --> ~P B  /\  B  e. 
~P B )  -> 
( F `  B
)  e.  ~P B
)
144, 12, 13syl2anc 645 . . . . 5  |-  ( ph  ->  ( F `  B
)  e.  ~P B
)
15 fvex 5499 . . . . . 6  |-  ( F `
 B )  e. 
_V
1615elpw 3632 . . . . 5  |-  ( ( F `  B )  e.  ~P B  <->  ( F `  B )  C_  B
)
1714, 16sylib 190 . . . 4  |-  ( ph  ->  ( F `  B
)  C_  B )
18 vex 2792 . . . . . . . 8  |-  x  e. 
_V
1918elpw 3632 . . . . . . 7  |-  ( x  e.  ~P B  <->  x  C_  B
)
20 ismrcd.e . . . . . . 7  |-  ( (
ph  /\  x  C_  B
)  ->  x  C_  ( F `  x )
)
2119, 20sylan2b 463 . . . . . 6  |-  ( (
ph  /\  x  e.  ~P B )  ->  x  C_  ( F `  x
) )
2221ralrimiva 2627 . . . . 5  |-  ( ph  ->  A. x  e.  ~P  B x  C_  ( F `
 x ) )
23 id 21 . . . . . . 7  |-  ( x  =  B  ->  x  =  B )
24 fveq2 5485 . . . . . . 7  |-  ( x  =  B  ->  ( F `  x )  =  ( F `  B ) )
2523, 24sseq12d 3208 . . . . . 6  |-  ( x  =  B  ->  (
x  C_  ( F `  x )  <->  B  C_  ( F `  B )
) )
2625rspcva 2883 . . . . 5  |-  ( ( B  e.  ~P B  /\  A. x  e.  ~P  B x  C_  ( F `
 x ) )  ->  B  C_  ( F `  B )
)
2712, 22, 26syl2anc 645 . . . 4  |-  ( ph  ->  B  C_  ( F `  B ) )
2817, 27eqssd 3197 . . 3  |-  ( ph  ->  ( F `  B
)  =  B )
29 ffn 5354 . . . . 5  |-  ( F : ~P B --> ~P B  ->  F  Fn  ~P B
)
304, 29syl 17 . . . 4  |-  ( ph  ->  F  Fn  ~P B
)
31 fnelfp 26154 . . . 4  |-  ( ( F  Fn  ~P B  /\  B  e.  ~P B )  ->  ( B  e.  dom  (  F  i^i  _I  )  <->  ( F `  B )  =  B ) )
3230, 12, 31syl2anc 645 . . 3  |-  ( ph  ->  ( B  e.  dom  (  F  i^i  _I  )  <->  ( F `  B )  =  B ) )
3328, 32mpbird 225 . 2  |-  ( ph  ->  B  e.  dom  (  F  i^i  _I  ) )
34 simp2 961 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  z  C_  dom  (  F  i^i  _I  ) )
3573ad2ant1 981 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  dom  (  F  i^i  _I  )  C_  ~P B )
3634, 35sstrd 3190 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  z  C_  ~P B )
37 simp3 962 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  z  =/=  (/) )
38 intssuni2 3888 . . . . . . . . . . . 12  |-  ( ( z  C_  ~P B  /\  z  =/=  (/) )  ->  |^| z  C_  U. ~P B )
3936, 37, 38syl2anc 645 . . . . . . . . . . 11  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  |^| z  C_ 
U. ~P B )
40 unipw 4223 . . . . . . . . . . 11  |-  U. ~P B  =  B
4139, 40syl6sseq 3225 . . . . . . . . . 10  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  |^| z  C_  B )
42 intex 4170 . . . . . . . . . . . 12  |-  ( z  =/=  (/)  <->  |^| z  e.  _V )
43 elpwg 3633 . . . . . . . . . . . 12  |-  ( |^| z  e.  _V  ->  (
|^| z  e.  ~P B 
<-> 
|^| z  C_  B
) )
4442, 43sylbi 189 . . . . . . . . . . 11  |-  ( z  =/=  (/)  ->  ( |^| z  e.  ~P B  <->  |^| z  C_  B )
)
45443ad2ant3 983 . . . . . . . . . 10  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  ( |^| z  e.  ~P B  <->  |^| z  C_  B )
)
4641, 45mpbird 225 . . . . . . . . 9  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  |^| z  e.  ~P B )
4746adantr 453 . . . . . . . 8  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  |^| z  e.  ~P B )
48 ismrcd.m . . . . . . . . . . . 12  |-  ( (
ph  /\  x  C_  B  /\  y  C_  x )  ->  ( F `  y )  C_  ( F `  x )
)
49483expib 1159 . . . . . . . . . . 11  |-  ( ph  ->  ( ( x  C_  B  /\  y  C_  x
)  ->  ( F `  y )  C_  ( F `  x )
) )
5049alrimiv 1622 . . . . . . . . . 10  |-  ( ph  ->  A. y ( ( x  C_  B  /\  y  C_  x )  -> 
( F `  y
)  C_  ( F `  x ) ) )
51503ad2ant1 981 . . . . . . . . 9  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  A. y
( ( x  C_  B  /\  y  C_  x
)  ->  ( F `  y )  C_  ( F `  x )
) )
5251adantr 453 . . . . . . . 8  |-  ( ( ( 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 )
) )
5336sselda 3181 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  x  e.  ~P B )
5453, 19sylib 190 . . . . . . . . 9  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  x  C_  B )
55 intss1 3878 . . . . . . . . . 10  |-  ( x  e.  z  ->  |^| z  C_  x )
5655adantl 454 . . . . . . . . 9  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  |^| z  C_  x )
5754, 56jca 520 . . . . . . . 8  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  (
x  C_  B  /\  |^| z  C_  x )
)
58 sseq1 3200 . . . . . . . . . . 11  |-  ( y  =  |^| z  -> 
( y  C_  x  <->  |^| z  C_  x )
)
5958anbi2d 687 . . . . . . . . . 10  |-  ( y  =  |^| z  -> 
( ( x  C_  B  /\  y  C_  x
)  <->  ( x  C_  B  /\  |^| z  C_  x
) ) )
60 fveq2 5485 . . . . . . . . . . 11  |-  ( y  =  |^| z  -> 
( F `  y
)  =  ( F `
 |^| z ) )
6160sseq1d 3206 . . . . . . . . . 10  |-  ( y  =  |^| z  -> 
( ( F `  y )  C_  ( F `  x )  <->  ( F `  |^| z
)  C_  ( F `  x ) ) )
6259, 61imbi12d 313 . . . . . . . . 9  |-  ( y  =  |^| z  -> 
( ( ( x 
C_  B  /\  y  C_  x )  ->  ( F `  y )  C_  ( F `  x
) )  <->  ( (
x  C_  B  /\  |^| z  C_  x )  ->  ( F `  |^| z )  C_  ( F `  x )
) ) )
6362spcgv 2869 . . . . . . . 8  |-  ( |^| 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 )
) ) )
6447, 52, 57, 63syl3c 59 . . . . . . 7  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  ( F `  |^| z ) 
C_  ( F `  x ) )
6534sselda 3181 . . . . . . . 8  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  x  e.  dom  (  F  i^i  _I  ) )
66303ad2ant1 981 . . . . . . . . . 10  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  F  Fn  ~P B )
6766adantr 453 . . . . . . . . 9  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  F  Fn  ~P B )
68 fnelfp 26154 . . . . . . . . 9  |-  ( ( F  Fn  ~P B  /\  x  e.  ~P B )  ->  (
x  e.  dom  (  F  i^i  _I  )  <->  ( F `  x )  =  x ) )
6967, 53, 68syl2anc 645 . . . . . . . 8  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  (
x  e.  dom  (  F  i^i  _I  )  <->  ( F `  x )  =  x ) )
7065, 69mpbid 203 . . . . . . 7  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  ( F `  x )  =  x )
7164, 70sseqtrd 3215 . . . . . 6  |-  ( ( ( ph  /\  z  C_ 
dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  /\  x  e.  z )  ->  ( F `  |^| z ) 
C_  x )
7271ralrimiva 2627 . . . . 5  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  A. x  e.  z  ( F `  |^| z )  C_  x )
73 ssint 3879 . . . . 5  |-  ( ( F `  |^| z
)  C_  |^| z  <->  A. x  e.  z  ( F `  |^| z )  C_  x )
7472, 73sylibr 205 . . . 4  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  ( F `
 |^| z )  C_  |^| z )
75223ad2ant1 981 . . . . 5  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  A. x  e.  ~P  B x  C_  ( F `  x ) )
76 id 21 . . . . . . 7  |-  ( x  =  |^| z  ->  x  =  |^| z )
77 fveq2 5485 . . . . . . 7  |-  ( x  =  |^| z  -> 
( F `  x
)  =  ( F `
 |^| z ) )
7876, 77sseq12d 3208 . . . . . 6  |-  ( x  =  |^| z  -> 
( x  C_  ( F `  x )  <->  |^| z  C_  ( F `  |^| z ) ) )
7978rspcva 2883 . . . . 5  |-  ( (
|^| z  e.  ~P B  /\  A. x  e. 
~P  B x  C_  ( F `  x ) )  ->  |^| z  C_  ( F `  |^| z
) )
8046, 75, 79syl2anc 645 . . . 4  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  |^| z  C_  ( F `  |^| z ) )
8174, 80eqssd 3197 . . 3  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  ( F `
 |^| z )  = 
|^| z )
82 fnelfp 26154 . . . 4  |-  ( ( F  Fn  ~P B  /\  |^| z  e.  ~P B )  ->  ( |^| z  e.  dom  (  F  i^i  _I  )  <->  ( F `  |^| z
)  =  |^| z
) )
8366, 46, 82syl2anc 645 . . 3  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  ( |^| z  e.  dom  (  F  i^i  _I  )  <->  ( F `  |^| z )  = 
|^| z ) )
8481, 83mpbird 225 . 2  |-  ( (
ph  /\  z  C_  dom  (  F  i^i  _I  )  /\  z  =/=  (/) )  ->  |^| z  e.  dom  (  F  i^i  _I  ) )
857, 33, 84ismred 13498 1  |-  ( ph  ->  dom  (  F  i^i  _I  )  e.  (Moore `  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    /\ w3a 939   A.wal 1532    = wceq 1628    e. wcel 1688    =/= wne 2447   A.wral 2544   _Vcvv 2789    i^i cin 3152    C_ wss 3153   (/)c0 3456   ~Pcpw 3626   U.cuni 3828   |^|cint 3863    _I cid 4303   dom cdm 4688    Fn wfn 5216   -->wf 5217   ` cfv 5221  Moorecmre 13478
This theorem is referenced by:  ismrcd2  26173  istopclsd  26174  ismrc  26175
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-13 1690  ax-14 1692  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-int 3864  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-fv 5229  df-mre 13482
  Copyright terms: Public domain W3C validator