MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abianfp Unicode version

Theorem abianfp 6654
Description: "A most fundamental fixed point theorem" of Alexander Abian (1923-1999), apparently proved in 1998. Let  G `  0  =  x,  G `  1  =  F `  x,  G `  2  =  F `  ( F `
 x ),... be the iterates of  F. The theorem reads (using our variable names): "Let  F be a mapping from a set  A into itself. Then  F has a fixed point if and only if: There exists an element  x of  A such that for every ordinal  v,  G `  v is an element of  A, and if  G `  v is not a fixed point of  F then the  G `  u's are all distinct for every ordinal  u  e.  v." See df-rdg 6606 for the  rec operation. The proof's key idea is to assume that  F does not have a fixed point, then use the Axiom of Replacement in the form of f1dmex 5912 to derive that the class of all ordinal numbers exists, contradicting onprc 4707. Our version of this theorem does not require the hypothesis that  F be a mapping. Reference: http://us2.metamath.org:88/abian-themostfixed.html. For an application of this theorem, see http://groups.google.com/group/sci.stat.math/msg/1737ee1133c24aeb for its use in a proof of Tarski's fixed point theorem. (Contributed by NM, 5-Sep-2004.) (Revised by David Abernethy, 19-Jun-2012.)
Hypotheses
Ref Expression
abianfp.1  |-  A  e. 
_V
abianfp.2  |-  G  =  rec ( ( z  e.  _V  |->  ( F `
 z ) ) ,  x )
Assertion
Ref Expression
abianfp  |-  ( E. x  e.  A  ( F `  x )  =  x  <->  E. x  e.  A  A. v  e.  On  ( ( G `
 v )  e.  A  /\  ( -.  ( F `  ( G `  v )
)  =  ( G `
 v )  ->  A. u  e.  v  -.  ( G `  v
)  =  ( G `
 u ) ) ) )
Distinct variable groups:    x, v, A    z, v, F, x   
v, u, G
Allowed substitution hints:    A( z, u)    F( u)    G( x, z)

Proof of Theorem abianfp
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 abianfp.1 . . . . . . . . . . 11  |-  A  e. 
_V
2 abianfp.2 . . . . . . . . . . 11  |-  G  =  rec ( ( z  e.  _V  |->  ( F `
 z ) ) ,  x )
31, 2abianfplem 6653 . . . . . . . . . 10  |-  ( v  e.  On  ->  (
( F `  x
)  =  x  -> 
( G `  v
)  =  x ) )
43imp 419 . . . . . . . . 9  |-  ( ( v  e.  On  /\  ( F `  x )  =  x )  -> 
( G `  v
)  =  x )
54eleq1d 2455 . . . . . . . 8  |-  ( ( v  e.  On  /\  ( F `  x )  =  x )  -> 
( ( G `  v )  e.  A  <->  x  e.  A ) )
65biimprd 215 . . . . . . 7  |-  ( ( v  e.  On  /\  ( F `  x )  =  x )  -> 
( x  e.  A  ->  ( G `  v
)  e.  A ) )
7 fveq2 5670 . . . . . . . . . . . 12  |-  ( ( G `  v )  =  x  ->  ( F `  ( G `  v ) )  =  ( F `  x
) )
8 id 20 . . . . . . . . . . . 12  |-  ( ( G `  v )  =  x  ->  ( G `  v )  =  x )
97, 8eqeq12d 2403 . . . . . . . . . . 11  |-  ( ( G `  v )  =  x  ->  (
( F `  ( G `  v )
)  =  ( G `
 v )  <->  ( F `  x )  =  x ) )
109biimprcd 217 . . . . . . . . . 10  |-  ( ( F `  x )  =  x  ->  (
( G `  v
)  =  x  -> 
( F `  ( G `  v )
)  =  ( G `
 v ) ) )
113, 10sylcom 27 . . . . . . . . 9  |-  ( v  e.  On  ->  (
( F `  x
)  =  x  -> 
( F `  ( G `  v )
)  =  ( G `
 v ) ) )
1211imp 419 . . . . . . . 8  |-  ( ( v  e.  On  /\  ( F `  x )  =  x )  -> 
( F `  ( G `  v )
)  =  ( G `
 v ) )
1312pm2.24d 137 . . . . . . 7  |-  ( ( v  e.  On  /\  ( F `  x )  =  x )  -> 
( -.  ( F `
 ( G `  v ) )  =  ( G `  v
)  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) )
146, 13jctird 529 . . . . . 6  |-  ( ( v  e.  On  /\  ( F `  x )  =  x )  -> 
( x  e.  A  ->  ( ( G `  v )  e.  A  /\  ( -.  ( F `
 ( G `  v ) )  =  ( G `  v
)  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) ) ) )
1514ex 424 . . . . 5  |-  ( v  e.  On  ->  (
( F `  x
)  =  x  -> 
( x  e.  A  ->  ( ( G `  v )  e.  A  /\  ( -.  ( F `
 ( G `  v ) )  =  ( G `  v
)  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) ) ) ) )
1615com13 76 . . . 4  |-  ( x  e.  A  ->  (
( F `  x
)  =  x  -> 
( v  e.  On  ->  ( ( G `  v )  e.  A  /\  ( -.  ( F `
 ( G `  v ) )  =  ( G `  v
)  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) ) ) ) )
1716ralrimdv 2740 . . 3  |-  ( x  e.  A  ->  (
( F `  x
)  =  x  ->  A. v  e.  On  ( ( G `  v )  e.  A  /\  ( -.  ( F `
 ( G `  v ) )  =  ( G `  v
)  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) ) ) )
1817reximia 2756 . 2  |-  ( E. x  e.  A  ( F `  x )  =  x  ->  E. x  e.  A  A. v  e.  On  ( ( G `
 v )  e.  A  /\  ( -.  ( F `  ( G `  v )
)  =  ( G `
 v )  ->  A. u  e.  v  -.  ( G `  v
)  =  ( G `
 u ) ) ) )
19 onprc 4707 . . . . 5  |-  -.  On  e.  _V
20 r19.26 2783 . . . . . 6  |-  ( A. v  e.  On  (
( G `  v
)  e.  A  /\  ( -.  ( F `  ( G `  v
) )  =  ( G `  v )  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) )  <->  ( A. v  e.  On  ( G `  v )  e.  A  /\  A. v  e.  On  ( -.  ( F `  ( G `  v ) )  =  ( G `  v
)  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) ) )
21 fveq2 5670 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( G `  v )  ->  ( F `  y )  =  ( F `  ( G `  v ) ) )
22 id 20 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( G `  v )  ->  y  =  ( G `  v ) )
2321, 22eqeq12d 2403 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( G `  v )  ->  (
( F `  y
)  =  y  <->  ( F `  ( G `  v
) )  =  ( G `  v ) ) )
2423notbid 286 . . . . . . . . . . . . . . 15  |-  ( y  =  ( G `  v )  ->  ( -.  ( F `  y
)  =  y  <->  -.  ( F `  ( G `  v ) )  =  ( G `  v
) ) )
2524rspccv 2994 . . . . . . . . . . . . . 14  |-  ( A. y  e.  A  -.  ( F `  y )  =  y  ->  (
( G `  v
)  e.  A  ->  -.  ( F `  ( G `  v )
)  =  ( G `
 v ) ) )
2625imim1d 71 . . . . . . . . . . . . 13  |-  ( A. y  e.  A  -.  ( F `  y )  =  y  ->  (
( -.  ( F `
 ( G `  v ) )  =  ( G `  v
)  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) )  -> 
( ( G `  v )  e.  A  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) ) )
2726ralimdv 2730 . . . . . . . . . . . 12  |-  ( A. y  e.  A  -.  ( F `  y )  =  y  ->  ( A. v  e.  On  ( -.  ( F `  ( G `  v
) )  =  ( G `  v )  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) )  ->  A. v  e.  On  ( ( G `
 v )  e.  A  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) ) )
28 ralim 2722 . . . . . . . . . . . 12  |-  ( A. v  e.  On  (
( G `  v
)  e.  A  ->  A. u  e.  v  -.  ( G `  v
)  =  ( G `
 u ) )  ->  ( A. v  e.  On  ( G `  v )  e.  A  ->  A. v  e.  On  A. u  e.  v  -.  ( G `  v
)  =  ( G `
 u ) ) )
2927, 28syl6 31 . . . . . . . . . . 11  |-  ( A. y  e.  A  -.  ( F `  y )  =  y  ->  ( A. v  e.  On  ( -.  ( F `  ( G `  v
) )  =  ( G `  v )  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) )  ->  ( A. v  e.  On  ( G `  v )  e.  A  ->  A. v  e.  On  A. u  e.  v  -.  ( G `
 v )  =  ( G `  u
) ) ) )
3029imp 419 . . . . . . . . . 10  |-  ( ( A. y  e.  A  -.  ( F `  y
)  =  y  /\  A. v  e.  On  ( -.  ( F `  ( G `  v )
)  =  ( G `
 v )  ->  A. u  e.  v  -.  ( G `  v
)  =  ( G `
 u ) ) )  ->  ( A. v  e.  On  ( G `  v )  e.  A  ->  A. v  e.  On  A. u  e.  v  -.  ( G `
 v )  =  ( G `  u
) ) )
3130com12 29 . . . . . . . . 9  |-  ( A. v  e.  On  ( G `  v )  e.  A  ->  ( ( A. y  e.  A  -.  ( F `  y
)  =  y  /\  A. v  e.  On  ( -.  ( F `  ( G `  v )
)  =  ( G `
 v )  ->  A. u  e.  v  -.  ( G `  v
)  =  ( G `
 u ) ) )  ->  A. v  e.  On  A. u  e.  v  -.  ( G `
 v )  =  ( G `  u
) ) )
32 rdgfnon 6614 . . . . . . . . . . . . . . 15  |-  rec (
( z  e.  _V  |->  ( F `  z ) ) ,  x )  Fn  On
332fneq1i 5481 . . . . . . . . . . . . . . 15  |-  ( G  Fn  On  <->  rec (
( z  e.  _V  |->  ( F `  z ) ) ,  x )  Fn  On )
3432, 33mpbir 201 . . . . . . . . . . . . . 14  |-  G  Fn  On
35 ffnfv 5835 . . . . . . . . . . . . . . 15  |-  ( G : On --> A  <->  ( G  Fn  On  /\  A. v  e.  On  ( G `  v )  e.  A
) )
3635biimpri 198 . . . . . . . . . . . . . 14  |-  ( ( G  Fn  On  /\  A. v  e.  On  ( G `  v )  e.  A )  ->  G : On --> A )
3734, 36mpan 652 . . . . . . . . . . . . 13  |-  ( A. v  e.  On  ( G `  v )  e.  A  ->  G : On
--> A )
38 ssid 3312 . . . . . . . . . . . . . . 15  |-  On  C_  On
3934tz7.48lem 6636 . . . . . . . . . . . . . . 15  |-  ( ( On  C_  On  /\  A. v  e.  On  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) )  ->  Fun  `' ( G  |`  On ) )
4038, 39mpan 652 . . . . . . . . . . . . . 14  |-  ( A. v  e.  On  A. u  e.  v  -.  ( G `  v )  =  ( G `  u )  ->  Fun  `' ( G  |`  On ) )
41 fnresdm 5496 . . . . . . . . . . . . . . . . 17  |-  ( G  Fn  On  ->  ( G  |`  On )  =  G )
4234, 41ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( G  |`  On )  =  G
4342cnveqi 4989 . . . . . . . . . . . . . . 15  |-  `' ( G  |`  On )  =  `' G
4443funeqi 5416 . . . . . . . . . . . . . 14  |-  ( Fun  `' ( G  |`  On )  <->  Fun  `' G )
4540, 44sylib 189 . . . . . . . . . . . . 13  |-  ( A. v  e.  On  A. u  e.  v  -.  ( G `  v )  =  ( G `  u )  ->  Fun  `' G )
4637, 45anim12i 550 . . . . . . . . . . . 12  |-  ( ( A. v  e.  On  ( G `  v )  e.  A  /\  A. v  e.  On  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) )  -> 
( G : On --> A  /\  Fun  `' G
) )
47 df-f1 5401 . . . . . . . . . . . 12  |-  ( G : On -1-1-> A  <->  ( G : On --> A  /\  Fun  `' G ) )
4846, 47sylibr 204 . . . . . . . . . . 11  |-  ( ( A. v  e.  On  ( G `  v )  e.  A  /\  A. v  e.  On  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) )  ->  G : On -1-1-> A )
49 f1dmex 5912 . . . . . . . . . . 11  |-  ( ( G : On -1-1-> A  /\  A  e.  _V )  ->  On  e.  _V )
5048, 1, 49sylancl 644 . . . . . . . . . 10  |-  ( ( A. v  e.  On  ( G `  v )  e.  A  /\  A. v  e.  On  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) )  ->  On  e.  _V )
5150ex 424 . . . . . . . . 9  |-  ( A. v  e.  On  ( G `  v )  e.  A  ->  ( A. v  e.  On  A. u  e.  v  -.  ( G `  v )  =  ( G `  u )  ->  On  e.  _V ) )
5231, 51syld 42 . . . . . . . 8  |-  ( A. v  e.  On  ( G `  v )  e.  A  ->  ( ( A. y  e.  A  -.  ( F `  y
)  =  y  /\  A. v  e.  On  ( -.  ( F `  ( G `  v )
)  =  ( G `
 v )  ->  A. u  e.  v  -.  ( G `  v
)  =  ( G `
 u ) ) )  ->  On  e.  _V ) )
5352exp3acom23 1378 . . . . . . 7  |-  ( A. v  e.  On  ( G `  v )  e.  A  ->  ( A. v  e.  On  ( -.  ( F `  ( G `  v )
)  =  ( G `
 v )  ->  A. u  e.  v  -.  ( G `  v
)  =  ( G `
 u ) )  ->  ( A. y  e.  A  -.  ( F `  y )  =  y  ->  On  e.  _V ) ) )
5453imp 419 . . . . . 6  |-  ( ( A. v  e.  On  ( G `  v )  e.  A  /\  A. v  e.  On  ( -.  ( F `  ( G `  v )
)  =  ( G `
 v )  ->  A. u  e.  v  -.  ( G `  v
)  =  ( G `
 u ) ) )  ->  ( A. y  e.  A  -.  ( F `  y )  =  y  ->  On  e.  _V ) )
5520, 54sylbi 188 . . . . 5  |-  ( A. v  e.  On  (
( G `  v
)  e.  A  /\  ( -.  ( F `  ( G `  v
) )  =  ( G `  v )  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) )  ->  ( A. y  e.  A  -.  ( F `  y
)  =  y  ->  On  e.  _V ) )
5619, 55mtoi 171 . . . 4  |-  ( A. v  e.  On  (
( G `  v
)  e.  A  /\  ( -.  ( F `  ( G `  v
) )  =  ( G `  v )  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) )  ->  -.  A. y  e.  A  -.  ( F `  y )  =  y )
5756rexlimivw 2771 . . 3  |-  ( E. x  e.  A  A. v  e.  On  (
( G `  v
)  e.  A  /\  ( -.  ( F `  ( G `  v
) )  =  ( G `  v )  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) )  ->  -.  A. y  e.  A  -.  ( F `  y )  =  y )
58 fveq2 5670 . . . . . 6  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
59 id 20 . . . . . 6  |-  ( x  =  y  ->  x  =  y )
6058, 59eqeq12d 2403 . . . . 5  |-  ( x  =  y  ->  (
( F `  x
)  =  x  <->  ( F `  y )  =  y ) )
6160cbvrexv 2878 . . . 4  |-  ( E. x  e.  A  ( F `  x )  =  x  <->  E. y  e.  A  ( F `  y )  =  y )
62 dfrex2 2664 . . . 4  |-  ( E. y  e.  A  ( F `  y )  =  y  <->  -.  A. y  e.  A  -.  ( F `  y )  =  y )
6361, 62bitr2i 242 . . 3  |-  ( -. 
A. y  e.  A  -.  ( F `  y
)  =  y  <->  E. x  e.  A  ( F `  x )  =  x )
6457, 63sylib 189 . 2  |-  ( E. x  e.  A  A. v  e.  On  (
( G `  v
)  e.  A  /\  ( -.  ( F `  ( G `  v
) )  =  ( G `  v )  ->  A. u  e.  v  -.  ( G `  v )  =  ( G `  u ) ) )  ->  E. x  e.  A  ( F `  x )  =  x )
6518, 64impbii 181 1  |-  ( E. x  e.  A  ( F `  x )  =  x  <->  E. x  e.  A  A. v  e.  On  ( ( G `
 v )  e.  A  /\  ( -.  ( F `  ( G `  v )
)  =  ( G `
 v )  ->  A. u  e.  v  -.  ( G `  v
)  =  ( G `
 u ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2651   E.wrex 2652   _Vcvv 2901    C_ wss 3265    e. cmpt 4209   Oncon0 4524   `'ccnv 4819    |` cres 4822   Fun wfun 5390    Fn wfn 5391   -->wf 5392   -1-1->wf1 5393   ` cfv 5396   reccrdg 6605
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-rep 4263  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-reu 2658  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-iun 4039  df-br 4156  df-opab 4210  df-mpt 4211  df-tr 4246  df-eprel 4437  df-id 4441  df-po 4446  df-so 4447  df-fr 4484  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530  df-om 4788  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-recs 6571  df-rdg 6606
  Copyright terms: Public domain W3C validator