Metamath Proof Explorer

Theorem 0ram

Description: The Ramsey number when M = 0 . (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion 0ram 
|- ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ( 0 Ramsey F ) = sup ( ran F , RR , < ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
2 0nn0 
 |-  0 e. NN0
3 2 a1i 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> 0 e. NN0 )
4 simpl1 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> R e. V )
5 simpl3 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> F : R --> NN0 )
6 5 frnd 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ran F C_ NN0 )
7 nn0ssz 
 |-  NN0 C_ ZZ
8 6 7 sstrdi 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ran F C_ ZZ )
9 5 fdmd 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> dom F = R )
10 simpl2 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> R =/= (/) )
11 9 10 eqnetrd 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> dom F =/= (/) )
12 dm0rn0 
 |-  ( dom F = (/) <-> ran F = (/) )
13 12 necon3bii 
 |-  ( dom F =/= (/) <-> ran F =/= (/) )
14 11 13 sylib 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ran F =/= (/) )
15 simpr 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> E. x e. ZZ A. y e. ran F y <_ x )
16 suprzcl2 
 |-  ( ( ran F C_ ZZ /\ ran F =/= (/) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> sup ( ran F , RR , < ) e. ran F )
17 8 14 15 16 syl3anc 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> sup ( ran F , RR , < ) e. ran F )
18 6 17 sseldd 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> sup ( ran F , RR , < ) e. NN0 )
19 1 hashbc0 
 |-  ( s e. _V -> ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) = { (/) } )
20 19 elv 
 |-  ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) = { (/) }
21 20 feq2i 
 |-  ( f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) --> R <-> f : { (/) } --> R )
22 21 biimpi 
 |-  ( f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) --> R -> f : { (/) } --> R )
23 simprr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> f : { (/) } --> R )
24 0ex 
 |-  (/) e. _V
25 24 snid 
 |-  (/) e. { (/) }
26 ffvelcdm 
 |-  ( ( f : { (/) } --> R /\ (/) e. { (/) } ) -> ( f ` (/) ) e. R )
27 23 25 26 sylancl 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ( f ` (/) ) e. R )
28 vex 
 |-  s e. _V
29 28 pwid 
 |-  s e. ~P s
30 29 a1i 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> s e. ~P s )
31 5 adantr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> F : R --> NN0 )
32 31 27 ffvelcdmd 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ( F ` ( f ` (/) ) ) e. NN0 )
33 32 nn0red 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ( F ` ( f ` (/) ) ) e. RR )
34 33 rexrd 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ( F ` ( f ` (/) ) ) e. RR* )
35 18 nn0red 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> sup ( ran F , RR , < ) e. RR )
36 35 rexrd 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> sup ( ran F , RR , < ) e. RR* )
37 36 adantr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> sup ( ran F , RR , < ) e. RR* )
38 hashxrcl 
 |-  ( s e. _V -> ( # ` s ) e. RR* )
39 28 38 mp1i 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ( # ` s ) e. RR* )
40 8 adantr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ran F C_ ZZ )
41 15 adantr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> E. x e. ZZ A. y e. ran F y <_ x )
42 31 ffnd 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> F Fn R )
43 fnfvelrn 
 |-  ( ( F Fn R /\ ( f ` (/) ) e. R ) -> ( F ` ( f ` (/) ) ) e. ran F )
44 42 27 43 syl2anc 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ( F ` ( f ` (/) ) ) e. ran F )
45 suprzub 
 |-  ( ( ran F C_ ZZ /\ E. x e. ZZ A. y e. ran F y <_ x /\ ( F ` ( f ` (/) ) ) e. ran F ) -> ( F ` ( f ` (/) ) ) <_ sup ( ran F , RR , < ) )
46 40 41 44 45 syl3anc 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ( F ` ( f ` (/) ) ) <_ sup ( ran F , RR , < ) )
47 simprl 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> sup ( ran F , RR , < ) <_ ( # ` s ) )
48 34 37 39 46 47 xrletrd 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ( F ` ( f ` (/) ) ) <_ ( # ` s ) )
49 25 a1i 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> (/) e. { (/) } )
50 fvex 
 |-  ( f ` (/) ) e. _V
51 50 snid 
 |-  ( f ` (/) ) e. { ( f ` (/) ) }
52 51 a1i 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ( f ` (/) ) e. { ( f ` (/) ) } )
53 ffn 
 |-  ( f : { (/) } --> R -> f Fn { (/) } )
54 elpreima 
 |-  ( f Fn { (/) } -> ( (/) e. ( `' f " { ( f ` (/) ) } ) <-> ( (/) e. { (/) } /\ ( f ` (/) ) e. { ( f ` (/) ) } ) ) )
55 23 53 54 3syl 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> ( (/) e. ( `' f " { ( f ` (/) ) } ) <-> ( (/) e. { (/) } /\ ( f ` (/) ) e. { ( f ` (/) ) } ) ) )
56 49 52 55 mpbir2and 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> (/) e. ( `' f " { ( f ` (/) ) } ) )
57 fveq2 
 |-  ( c = ( f ` (/) ) -> ( F ` c ) = ( F ` ( f ` (/) ) ) )
58 57 breq1d 
 |-  ( c = ( f ` (/) ) -> ( ( F ` c ) <_ ( # ` z ) <-> ( F ` ( f ` (/) ) ) <_ ( # ` z ) ) )
59 1 hashbc0 
 |-  ( z e. _V -> ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) = { (/) } )
60 59 elv 
 |-  ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) = { (/) }
61 60 sseq1i 
 |-  ( ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) C_ ( `' f " { c } ) <-> { (/) } C_ ( `' f " { c } ) )
62 24 snss 
 |-  ( (/) e. ( `' f " { c } ) <-> { (/) } C_ ( `' f " { c } ) )
63 61 62 bitr4i 
 |-  ( ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) C_ ( `' f " { c } ) <-> (/) e. ( `' f " { c } ) )
64 sneq 
 |-  ( c = ( f ` (/) ) -> { c } = { ( f ` (/) ) } )
65 64 imaeq2d 
 |-  ( c = ( f ` (/) ) -> ( `' f " { c } ) = ( `' f " { ( f ` (/) ) } ) )
66 65 eleq2d 
 |-  ( c = ( f ` (/) ) -> ( (/) e. ( `' f " { c } ) <-> (/) e. ( `' f " { ( f ` (/) ) } ) ) )
67 63 66 bitrid 
 |-  ( c = ( f ` (/) ) -> ( ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) C_ ( `' f " { c } ) <-> (/) e. ( `' f " { ( f ` (/) ) } ) ) )
68 58 67 anbi12d 
 |-  ( c = ( f ` (/) ) -> ( ( ( F ` c ) <_ ( # ` z ) /\ ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) C_ ( `' f " { c } ) ) <-> ( ( F ` ( f ` (/) ) ) <_ ( # ` z ) /\ (/) e. ( `' f " { ( f ` (/) ) } ) ) ) )
69 fveq2 
 |-  ( z = s -> ( # ` z ) = ( # ` s ) )
70 69 breq2d 
 |-  ( z = s -> ( ( F ` ( f ` (/) ) ) <_ ( # ` z ) <-> ( F ` ( f ` (/) ) ) <_ ( # ` s ) ) )
71 70 anbi1d 
 |-  ( z = s -> ( ( ( F ` ( f ` (/) ) ) <_ ( # ` z ) /\ (/) e. ( `' f " { ( f ` (/) ) } ) ) <-> ( ( F ` ( f ` (/) ) ) <_ ( # ` s ) /\ (/) e. ( `' f " { ( f ` (/) ) } ) ) ) )
72 68 71 rspc2ev 
 |-  ( ( ( f ` (/) ) e. R /\ s e. ~P s /\ ( ( F ` ( f ` (/) ) ) <_ ( # ` s ) /\ (/) e. ( `' f " { ( f ` (/) ) } ) ) ) -> E. c e. R E. z e. ~P s ( ( F ` c ) <_ ( # ` z ) /\ ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) C_ ( `' f " { c } ) ) )
73 27 30 48 56 72 syl112anc 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : { (/) } --> R ) ) -> E. c e. R E. z e. ~P s ( ( F ` c ) <_ ( # ` z ) /\ ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) C_ ( `' f " { c } ) ) )
74 22 73 sylanr2 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) <_ ( # ` s ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) --> R ) ) -> E. c e. R E. z e. ~P s ( ( F ` c ) <_ ( # ` z ) /\ ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) C_ ( `' f " { c } ) ) )
75 1 3 4 5 18 74 ramub 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ( 0 Ramsey F ) <_ sup ( ran F , RR , < ) )
76 ffn 
 |-  ( F : R --> NN0 -> F Fn R )
77 fvelrnb 
 |-  ( F Fn R -> ( sup ( ran F , RR , < ) e. ran F <-> E. c e. R ( F ` c ) = sup ( ran F , RR , < ) ) )
78 5 76 77 3syl 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ( sup ( ran F , RR , < ) e. ran F <-> E. c e. R ( F ` c ) = sup ( ran F , RR , < ) ) )
79 17 78 mpbid 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> E. c e. R ( F ` c ) = sup ( ran F , RR , < ) )
80 2 a1i 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> 0 e. NN0 )
81 simpll1 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> R e. V )
82 simpll3 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> F : R --> NN0 )
83 nnm1nn0 
 |-  ( ( F ` c ) e. NN -> ( ( F ` c ) - 1 ) e. NN0 )
84 83 ad2antll 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> ( ( F ` c ) - 1 ) e. NN0 )
85 vex 
 |-  c e. _V
86 24 85 f1osn 
 |-  { <. (/) , c >. } : { (/) } -1-1-onto-> { c }
87 f1of 
 |-  ( { <. (/) , c >. } : { (/) } -1-1-onto-> { c } -> { <. (/) , c >. } : { (/) } --> { c } )
88 86 87 ax-mp 
 |-  { <. (/) , c >. } : { (/) } --> { c }
89 simprl 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> c e. R )
90 89 snssd 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> { c } C_ R )
91 fss 
 |-  ( ( { <. (/) , c >. } : { (/) } --> { c } /\ { c } C_ R ) -> { <. (/) , c >. } : { (/) } --> R )
92 88 90 91 sylancr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> { <. (/) , c >. } : { (/) } --> R )
93 ovex 
 |-  ( 1 ... ( ( F ` c ) - 1 ) ) e. _V
94 1 hashbc0 
 |-  ( ( 1 ... ( ( F ` c ) - 1 ) ) e. _V -> ( ( 1 ... ( ( F ` c ) - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) = { (/) } )
95 93 94 ax-mp 
 |-  ( ( 1 ... ( ( F ` c ) - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) = { (/) }
96 95 feq2i 
 |-  ( { <. (/) , c >. } : ( ( 1 ... ( ( F ` c ) - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) --> R <-> { <. (/) , c >. } : { (/) } --> R )
97 92 96 sylibr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> { <. (/) , c >. } : ( ( 1 ... ( ( F ` c ) - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) --> R )
98 60 sseq1i 
 |-  ( ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) C_ ( `' { <. (/) , c >. } " { d } ) <-> { (/) } C_ ( `' { <. (/) , c >. } " { d } ) )
99 24 snss 
 |-  ( (/) e. ( `' { <. (/) , c >. } " { d } ) <-> { (/) } C_ ( `' { <. (/) , c >. } " { d } ) )
100 98 99 bitr4i 
 |-  ( ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) C_ ( `' { <. (/) , c >. } " { d } ) <-> (/) e. ( `' { <. (/) , c >. } " { d } ) )
101 fzfid 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( 1 ... ( ( F ` c ) - 1 ) ) e. Fin )
102 simprr 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> z C_ ( 1 ... ( ( F ` c ) - 1 ) ) )
103 ssdomg 
 |-  ( ( 1 ... ( ( F ` c ) - 1 ) ) e. Fin -> ( z C_ ( 1 ... ( ( F ` c ) - 1 ) ) -> z ~<_ ( 1 ... ( ( F ` c ) - 1 ) ) ) )
104 101 102 103 sylc 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> z ~<_ ( 1 ... ( ( F ` c ) - 1 ) ) )
105 101 102 ssfid 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> z e. Fin )
106 hashdom 
 |-  ( ( z e. Fin /\ ( 1 ... ( ( F ` c ) - 1 ) ) e. Fin ) -> ( ( # ` z ) <_ ( # ` ( 1 ... ( ( F ` c ) - 1 ) ) ) <-> z ~<_ ( 1 ... ( ( F ` c ) - 1 ) ) ) )
107 105 101 106 syl2anc 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( ( # ` z ) <_ ( # ` ( 1 ... ( ( F ` c ) - 1 ) ) ) <-> z ~<_ ( 1 ... ( ( F ` c ) - 1 ) ) ) )
108 104 107 mpbird 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( # ` z ) <_ ( # ` ( 1 ... ( ( F ` c ) - 1 ) ) ) )
109 84 adantr 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( ( F ` c ) - 1 ) e. NN0 )
110 hashfz1 
 |-  ( ( ( F ` c ) - 1 ) e. NN0 -> ( # ` ( 1 ... ( ( F ` c ) - 1 ) ) ) = ( ( F ` c ) - 1 ) )
111 109 110 syl 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( # ` ( 1 ... ( ( F ` c ) - 1 ) ) ) = ( ( F ` c ) - 1 ) )
112 108 111 breqtrd 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( # ` z ) <_ ( ( F ` c ) - 1 ) )
113 hashcl 
 |-  ( z e. Fin -> ( # ` z ) e. NN0 )
114 105 113 syl 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( # ` z ) e. NN0 )
115 5 ffvelcdmda 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ c e. R ) -> ( F ` c ) e. NN0 )
116 115 adantrr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> ( F ` c ) e. NN0 )
117 116 adantr 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( F ` c ) e. NN0 )
118 nn0ltlem1 
 |-  ( ( ( # ` z ) e. NN0 /\ ( F ` c ) e. NN0 ) -> ( ( # ` z ) < ( F ` c ) <-> ( # ` z ) <_ ( ( F ` c ) - 1 ) ) )
119 114 117 118 syl2anc 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( ( # ` z ) < ( F ` c ) <-> ( # ` z ) <_ ( ( F ` c ) - 1 ) ) )
120 112 119 mpbird 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( # ` z ) < ( F ` c ) )
121 24 85 fvsn 
 |-  ( { <. (/) , c >. } ` (/) ) = c
122 f1ofn 
 |-  ( { <. (/) , c >. } : { (/) } -1-1-onto-> { c } -> { <. (/) , c >. } Fn { (/) } )
123 elpreima 
 |-  ( { <. (/) , c >. } Fn { (/) } -> ( (/) e. ( `' { <. (/) , c >. } " { d } ) <-> ( (/) e. { (/) } /\ ( { <. (/) , c >. } ` (/) ) e. { d } ) ) )
124 86 122 123 mp2b 
 |-  ( (/) e. ( `' { <. (/) , c >. } " { d } ) <-> ( (/) e. { (/) } /\ ( { <. (/) , c >. } ` (/) ) e. { d } ) )
125 124 simprbi 
 |-  ( (/) e. ( `' { <. (/) , c >. } " { d } ) -> ( { <. (/) , c >. } ` (/) ) e. { d } )
126 121 125 eqeltrrid 
 |-  ( (/) e. ( `' { <. (/) , c >. } " { d } ) -> c e. { d } )
127 elsni 
 |-  ( c e. { d } -> c = d )
128 126 127 syl 
 |-  ( (/) e. ( `' { <. (/) , c >. } " { d } ) -> c = d )
129 128 fveq2d 
 |-  ( (/) e. ( `' { <. (/) , c >. } " { d } ) -> ( F ` c ) = ( F ` d ) )
130 129 breq2d 
 |-  ( (/) e. ( `' { <. (/) , c >. } " { d } ) -> ( ( # ` z ) < ( F ` c ) <-> ( # ` z ) < ( F ` d ) ) )
131 120 130 syl5ibcom 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( (/) e. ( `' { <. (/) , c >. } " { d } ) -> ( # ` z ) < ( F ` d ) ) )
132 100 131 biimtrid 
 |-  ( ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) /\ ( d e. R /\ z C_ ( 1 ... ( ( F ` c ) - 1 ) ) ) ) -> ( ( z ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) 0 ) C_ ( `' { <. (/) , c >. } " { d } ) -> ( # ` z ) < ( F ` d ) ) )
133 1 80 81 82 84 97 132 ramlb 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> ( ( F ` c ) - 1 ) < ( 0 Ramsey F ) )
134 ramubcl 
 |-  ( ( ( 0 e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( sup ( ran F , RR , < ) e. NN0 /\ ( 0 Ramsey F ) <_ sup ( ran F , RR , < ) ) ) -> ( 0 Ramsey F ) e. NN0 )
135 3 4 5 18 75 134 syl32anc 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ( 0 Ramsey F ) e. NN0 )
136 135 adantr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> ( 0 Ramsey F ) e. NN0 )
137 nn0lem1lt 
 |-  ( ( ( F ` c ) e. NN0 /\ ( 0 Ramsey F ) e. NN0 ) -> ( ( F ` c ) <_ ( 0 Ramsey F ) <-> ( ( F ` c ) - 1 ) < ( 0 Ramsey F ) ) )
138 116 136 137 syl2anc 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> ( ( F ` c ) <_ ( 0 Ramsey F ) <-> ( ( F ` c ) - 1 ) < ( 0 Ramsey F ) ) )
139 133 138 mpbird 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ ( c e. R /\ ( F ` c ) e. NN ) ) -> ( F ` c ) <_ ( 0 Ramsey F ) )
140 139 expr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ c e. R ) -> ( ( F ` c ) e. NN -> ( F ` c ) <_ ( 0 Ramsey F ) ) )
141 135 adantr 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ c e. R ) -> ( 0 Ramsey F ) e. NN0 )
142 141 nn0ge0d 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ c e. R ) -> 0 <_ ( 0 Ramsey F ) )
143 breq1 
 |-  ( ( F ` c ) = 0 -> ( ( F ` c ) <_ ( 0 Ramsey F ) <-> 0 <_ ( 0 Ramsey F ) ) )
144 142 143 syl5ibrcom 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ c e. R ) -> ( ( F ` c ) = 0 -> ( F ` c ) <_ ( 0 Ramsey F ) ) )
145 elnn0 
 |-  ( ( F ` c ) e. NN0 <-> ( ( F ` c ) e. NN \/ ( F ` c ) = 0 ) )
146 115 145 sylib 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ c e. R ) -> ( ( F ` c ) e. NN \/ ( F ` c ) = 0 ) )
147 140 144 146 mpjaod 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ c e. R ) -> ( F ` c ) <_ ( 0 Ramsey F ) )
148 breq1 
 |-  ( ( F ` c ) = sup ( ran F , RR , < ) -> ( ( F ` c ) <_ ( 0 Ramsey F ) <-> sup ( ran F , RR , < ) <_ ( 0 Ramsey F ) ) )
149 147 148 syl5ibcom 
 |-  ( ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) /\ c e. R ) -> ( ( F ` c ) = sup ( ran F , RR , < ) -> sup ( ran F , RR , < ) <_ ( 0 Ramsey F ) ) )
150 149 rexlimdva 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ( E. c e. R ( F ` c ) = sup ( ran F , RR , < ) -> sup ( ran F , RR , < ) <_ ( 0 Ramsey F ) ) )
151 79 150 mpd 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> sup ( ran F , RR , < ) <_ ( 0 Ramsey F ) )
152 135 nn0red 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ( 0 Ramsey F ) e. RR )
153 152 35 letri3d 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ( ( 0 Ramsey F ) = sup ( ran F , RR , < ) <-> ( ( 0 Ramsey F ) <_ sup ( ran F , RR , < ) /\ sup ( ran F , RR , < ) <_ ( 0 Ramsey F ) ) ) )
154 75 151 153 mpbir2and 
 |-  ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ( 0 Ramsey F ) = sup ( ran F , RR , < ) )