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 ffvelrn
 |-  ( ( 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 ffvelrnd
 |-  ( ( ( ( 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 syl5bb
 |-  ( 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 ffvelrnda
 |-  ( ( ( ( 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 syl5bi
 |-  ( ( ( ( ( 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 , < ) )