# 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 )`
` |-  ( ( ( ( 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* )`
` |-  ( ( ( ( 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* )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) ) ) )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) ) )`
` |-  ( ( ( ( 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 , < ) )`