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 , < ) ) |