# Metamath Proof Explorer

## Theorem ramub1lem2

Description: Lemma for ramub1 . (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ramub1.m
`|- ( ph -> M e. NN )`
ramub1.r
`|- ( ph -> R e. Fin )`
ramub1.f
`|- ( ph -> F : R --> NN )`
ramub1.g
`|- G = ( x e. R |-> ( M Ramsey ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) ) )`
ramub1.1
`|- ( ph -> G : R --> NN0 )`
ramub1.2
`|- ( ph -> ( ( M - 1 ) Ramsey G ) e. NN0 )`
ramub1.3
`|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
ramub1.4
`|- ( ph -> S e. Fin )`
ramub1.5
`|- ( ph -> ( # ` S ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) )`
ramub1.6
`|- ( ph -> K : ( S C M ) --> R )`
ramub1.x
`|- ( ph -> X e. S )`
ramub1.h
`|- H = ( u e. ( ( S \ { X } ) C ( M - 1 ) ) |-> ( K ` ( u u. { X } ) ) )`
Assertion ramub1lem2
`|- ( ph -> E. c e. R E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) )`

### Proof

Step Hyp Ref Expression
1 ramub1.m
` |-  ( ph -> M e. NN )`
2 ramub1.r
` |-  ( ph -> R e. Fin )`
3 ramub1.f
` |-  ( ph -> F : R --> NN )`
4 ramub1.g
` |-  G = ( x e. R |-> ( M Ramsey ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) ) )`
5 ramub1.1
` |-  ( ph -> G : R --> NN0 )`
6 ramub1.2
` |-  ( ph -> ( ( M - 1 ) Ramsey G ) e. NN0 )`
7 ramub1.3
` |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
8 ramub1.4
` |-  ( ph -> S e. Fin )`
9 ramub1.5
` |-  ( ph -> ( # ` S ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) )`
10 ramub1.6
` |-  ( ph -> K : ( S C M ) --> R )`
11 ramub1.x
` |-  ( ph -> X e. S )`
12 ramub1.h
` |-  H = ( u e. ( ( S \ { X } ) C ( M - 1 ) ) |-> ( K ` ( u u. { X } ) ) )`
13 nnm1nn0
` |-  ( M e. NN -> ( M - 1 ) e. NN0 )`
14 1 13 syl
` |-  ( ph -> ( M - 1 ) e. NN0 )`
15 diffi
` |-  ( S e. Fin -> ( S \ { X } ) e. Fin )`
16 8 15 syl
` |-  ( ph -> ( S \ { X } ) e. Fin )`
17 6 nn0red
` |-  ( ph -> ( ( M - 1 ) Ramsey G ) e. RR )`
18 17 leidd
` |-  ( ph -> ( ( M - 1 ) Ramsey G ) <_ ( ( M - 1 ) Ramsey G ) )`
19 hashcl
` |-  ( ( S \ { X } ) e. Fin -> ( # ` ( S \ { X } ) ) e. NN0 )`
20 16 19 syl
` |-  ( ph -> ( # ` ( S \ { X } ) ) e. NN0 )`
21 20 nn0cnd
` |-  ( ph -> ( # ` ( S \ { X } ) ) e. CC )`
22 6 nn0cnd
` |-  ( ph -> ( ( M - 1 ) Ramsey G ) e. CC )`
23 1cnd
` |-  ( ph -> 1 e. CC )`
24 undif1
` |-  ( ( S \ { X } ) u. { X } ) = ( S u. { X } )`
25 11 snssd
` |-  ( ph -> { X } C_ S )`
26 ssequn2
` |-  ( { X } C_ S <-> ( S u. { X } ) = S )`
27 25 26 sylib
` |-  ( ph -> ( S u. { X } ) = S )`
28 24 27 syl5eq
` |-  ( ph -> ( ( S \ { X } ) u. { X } ) = S )`
29 28 fveq2d
` |-  ( ph -> ( # ` ( ( S \ { X } ) u. { X } ) ) = ( # ` S ) )`
30 neldifsnd
` |-  ( ph -> -. X e. ( S \ { X } ) )`
31 hashunsng
` |-  ( X e. S -> ( ( ( S \ { X } ) e. Fin /\ -. X e. ( S \ { X } ) ) -> ( # ` ( ( S \ { X } ) u. { X } ) ) = ( ( # ` ( S \ { X } ) ) + 1 ) ) )`
32 11 31 syl
` |-  ( ph -> ( ( ( S \ { X } ) e. Fin /\ -. X e. ( S \ { X } ) ) -> ( # ` ( ( S \ { X } ) u. { X } ) ) = ( ( # ` ( S \ { X } ) ) + 1 ) ) )`
33 16 30 32 mp2and
` |-  ( ph -> ( # ` ( ( S \ { X } ) u. { X } ) ) = ( ( # ` ( S \ { X } ) ) + 1 ) )`
34 29 33 9 3eqtr3d
` |-  ( ph -> ( ( # ` ( S \ { X } ) ) + 1 ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) )`
` |-  ( ph -> ( # ` ( S \ { X } ) ) = ( ( M - 1 ) Ramsey G ) )`
36 18 35 breqtrrd
` |-  ( ph -> ( ( M - 1 ) Ramsey G ) <_ ( # ` ( S \ { X } ) ) )`
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> K : ( S C M ) --> R )`
38 fveqeq2
` |-  ( x = ( u u. { X } ) -> ( ( # ` x ) = M <-> ( # ` ( u u. { X } ) ) = M ) )`
39 7 hashbcval
` |-  ( ( ( S \ { X } ) e. Fin /\ ( M - 1 ) e. NN0 ) -> ( ( S \ { X } ) C ( M - 1 ) ) = { x e. ~P ( S \ { X } ) | ( # ` x ) = ( M - 1 ) } )`
40 16 14 39 syl2anc
` |-  ( ph -> ( ( S \ { X } ) C ( M - 1 ) ) = { x e. ~P ( S \ { X } ) | ( # ` x ) = ( M - 1 ) } )`
41 40 eleq2d
` |-  ( ph -> ( u e. ( ( S \ { X } ) C ( M - 1 ) ) <-> u e. { x e. ~P ( S \ { X } ) | ( # ` x ) = ( M - 1 ) } ) )`
42 fveqeq2
` |-  ( x = u -> ( ( # ` x ) = ( M - 1 ) <-> ( # ` u ) = ( M - 1 ) ) )`
43 42 elrab
` |-  ( u e. { x e. ~P ( S \ { X } ) | ( # ` x ) = ( M - 1 ) } <-> ( u e. ~P ( S \ { X } ) /\ ( # ` u ) = ( M - 1 ) ) )`
44 41 43 syl6bb
` |-  ( ph -> ( u e. ( ( S \ { X } ) C ( M - 1 ) ) <-> ( u e. ~P ( S \ { X } ) /\ ( # ` u ) = ( M - 1 ) ) ) )`
45 44 simprbda
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> u e. ~P ( S \ { X } ) )`
46 45 elpwid
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> u C_ ( S \ { X } ) )`
47 46 difss2d
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> u C_ S )`
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> { X } C_ S )`
49 47 48 unssd
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( u u. { X } ) C_ S )`
50 vex
` |-  u e. _V`
51 snex
` |-  { X } e. _V`
52 50 51 unex
` |-  ( u u. { X } ) e. _V`
53 52 elpw
` |-  ( ( u u. { X } ) e. ~P S <-> ( u u. { X } ) C_ S )`
54 49 53 sylibr
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( u u. { X } ) e. ~P S )`
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( S \ { X } ) e. Fin )`
56 55 46 ssfid
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> u e. Fin )`
57 neldifsnd
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> -. X e. ( S \ { X } ) )`
58 46 57 ssneldd
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> -. X e. u )`
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> X e. S )`
60 hashunsng
` |-  ( X e. S -> ( ( u e. Fin /\ -. X e. u ) -> ( # ` ( u u. { X } ) ) = ( ( # ` u ) + 1 ) ) )`
61 59 60 syl
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( ( u e. Fin /\ -. X e. u ) -> ( # ` ( u u. { X } ) ) = ( ( # ` u ) + 1 ) ) )`
62 56 58 61 mp2and
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( # ` ( u u. { X } ) ) = ( ( # ` u ) + 1 ) )`
63 44 simplbda
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( # ` u ) = ( M - 1 ) )`
64 63 oveq1d
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( ( # ` u ) + 1 ) = ( ( M - 1 ) + 1 ) )`
65 1 nncnd
` |-  ( ph -> M e. CC )`
66 ax-1cn
` |-  1 e. CC`
67 npcan
` |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M - 1 ) + 1 ) = M )`
68 65 66 67 sylancl
` |-  ( ph -> ( ( M - 1 ) + 1 ) = M )`
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( ( M - 1 ) + 1 ) = M )`
70 62 64 69 3eqtrd
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( # ` ( u u. { X } ) ) = M )`
71 38 54 70 elrabd
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( u u. { X } ) e. { x e. ~P S | ( # ` x ) = M } )`
72 1 nnnn0d
` |-  ( ph -> M e. NN0 )`
73 7 hashbcval
` |-  ( ( S e. Fin /\ M e. NN0 ) -> ( S C M ) = { x e. ~P S | ( # ` x ) = M } )`
74 8 72 73 syl2anc
` |-  ( ph -> ( S C M ) = { x e. ~P S | ( # ` x ) = M } )`
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( S C M ) = { x e. ~P S | ( # ` x ) = M } )`
76 71 75 eleqtrrd
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( u u. { X } ) e. ( S C M ) )`
77 37 76 ffvelrnd
` |-  ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( K ` ( u u. { X } ) ) e. R )`
78 77 12 fmptd
` |-  ( ph -> H : ( ( S \ { X } ) C ( M - 1 ) ) --> R )`
79 7 14 2 5 6 16 36 78 rami
` |-  ( ph -> E. d e. R E. w e. ~P ( S \ { X } ) ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) )`
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> M e. NN0 )`
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> R e. Fin )`
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> F : R --> NN )`
83 simprll
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> d e. R )`
84 82 83 ffvelrnd
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( F ` d ) e. NN )`
85 nnm1nn0
` |-  ( ( F ` d ) e. NN -> ( ( F ` d ) - 1 ) e. NN0 )`
86 84 85 syl
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( ( F ` d ) - 1 ) e. NN0 )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ y e. R ) -> ( ( F ` d ) - 1 ) e. NN0 )`
88 82 ffvelrnda
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ y e. R ) -> ( F ` y ) e. NN )`
89 88 nnnn0d
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ y e. R ) -> ( F ` y ) e. NN0 )`
90 87 89 ifcld
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ y e. R ) -> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) e. NN0 )`
91 eqid
` |-  ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) = ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) )`
92 90 91 fmptd
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) : R --> NN0 )`
93 equequ2
` |-  ( x = d -> ( y = x <-> y = d ) )`
94 fveq2
` |-  ( x = d -> ( F ` x ) = ( F ` d ) )`
95 94 oveq1d
` |-  ( x = d -> ( ( F ` x ) - 1 ) = ( ( F ` d ) - 1 ) )`
96 93 95 ifbieq1d
` |-  ( x = d -> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) = if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) )`
97 96 mpteq2dv
` |-  ( x = d -> ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) = ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) )`
98 97 oveq2d
` |-  ( x = d -> ( M Ramsey ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) ) = ( M Ramsey ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ) )`
99 ovex
` |-  ( M Ramsey ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ) e. _V`
100 98 4 99 fvmpt
` |-  ( d e. R -> ( G ` d ) = ( M Ramsey ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ) )`
101 83 100 syl
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( G ` d ) = ( M Ramsey ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ) )`
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> G : R --> NN0 )`
103 102 83 ffvelrnd
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( G ` d ) e. NN0 )`
104 101 103 eqeltrrd
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( M Ramsey ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ) e. NN0 )`
105 simprlr
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> w e. ~P ( S \ { X } ) )`
106 simprrl
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( G ` d ) <_ ( # ` w ) )`
107 101 106 eqbrtrrd
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( M Ramsey ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ) <_ ( # ` w ) )`
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> K : ( S C M ) --> R )`
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> S e. Fin )`
110 105 elpwid
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> w C_ ( S \ { X } ) )`
111 110 difss2d
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> w C_ S )`
112 7 hashbcss
` |-  ( ( S e. Fin /\ w C_ S /\ M e. NN0 ) -> ( w C M ) C_ ( S C M ) )`
113 109 111 80 112 syl3anc
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( w C M ) C_ ( S C M ) )`
114 108 113 fssresd
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( K |` ( w C M ) ) : ( w C M ) --> R )`
115 7 80 81 92 104 105 107 114 rami
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> E. c e. R E. v e. ~P w ( ( ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ` c ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) )`
116 equequ1
` |-  ( y = c -> ( y = d <-> c = d ) )`
117 fveq2
` |-  ( y = c -> ( F ` y ) = ( F ` c ) )`
118 116 117 ifbieq2d
` |-  ( y = c -> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) = if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) )`
119 ovex
` |-  ( ( F ` d ) - 1 ) e. _V`
120 fvex
` |-  ( F ` c ) e. _V`
121 119 120 ifex
` |-  if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) e. _V`
122 118 91 121 fvmpt
` |-  ( c e. R -> ( ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ` c ) = if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( c e. R /\ v e. ~P w ) ) -> ( ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ` c ) = if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) )`
124 123 breq1d
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( c e. R /\ v e. ~P w ) ) -> ( ( ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ` c ) <_ ( # ` v ) <-> if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) ) )`
125 124 anbi1d
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( c e. R /\ v e. ~P w ) ) -> ( ( ( ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ` c ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) <-> ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> M e. NN )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> R e. Fin )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> F : R --> NN )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> G : R --> NN0 )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> ( ( M - 1 ) Ramsey G ) e. NN0 )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> S e. Fin )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> ( # ` S ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> K : ( S C M ) --> R )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> X e. S )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> d e. R )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> w C_ ( S \ { X } ) )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> ( G ` d ) <_ ( # ` w ) )`
138 simprrr
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( w C ( M - 1 ) ) C_ ( `' H " { d } ) )`
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> ( w C ( M - 1 ) ) C_ ( `' H " { d } ) )`
140 simprll
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> c e. R )`
141 simprlr
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> v e. ~P w )`
142 141 elpwid
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> v C_ w )`
143 simprrl
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) )`
144 simprrr
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) )`
145 cnvresima
` |-  ( `' ( K |` ( w C M ) ) " { c } ) = ( ( `' K " { c } ) i^i ( w C M ) )`
146 inss1
` |-  ( ( `' K " { c } ) i^i ( w C M ) ) C_ ( `' K " { c } )`
147 145 146 eqsstri
` |-  ( `' ( K |` ( w C M ) ) " { c } ) C_ ( `' K " { c } )`
148 144 147 sstrdi
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> ( v C M ) C_ ( `' K " { c } ) )`
149 126 127 128 4 129 130 7 131 132 133 134 12 135 136 137 139 140 142 143 148 ramub1lem1
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( ( c e. R /\ v e. ~P w ) /\ ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) ) ) -> E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) )`
150 149 expr
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( c e. R /\ v e. ~P w ) ) -> ( ( if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) -> E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) ) )`
151 125 150 sylbid
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ ( c e. R /\ v e. ~P w ) ) -> ( ( ( ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ` c ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) -> E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) ) )`
152 151 anassrs
` |-  ( ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ c e. R ) /\ v e. ~P w ) -> ( ( ( ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ` c ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) -> E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) ) )`
153 152 rexlimdva
` |-  ( ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) /\ c e. R ) -> ( E. v e. ~P w ( ( ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ` c ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) -> E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) ) )`
154 153 reximdva
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( E. c e. R E. v e. ~P w ( ( ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ` c ) <_ ( # ` v ) /\ ( v C M ) C_ ( `' ( K |` ( w C M ) ) " { c } ) ) -> E. c e. R E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) ) )`
155 115 154 mpd
` |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> E. c e. R E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) )`
156 155 expr
` |-  ( ( ph /\ ( d e. R /\ w e. ~P ( S \ { X } ) ) ) -> ( ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) -> E. c e. R E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) ) )`
157 156 rexlimdvva
` |-  ( ph -> ( E. d e. R E. w e. ~P ( S \ { X } ) ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) -> E. c e. R E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) ) )`
158 79 157 mpd
` |-  ( ph -> E. c e. R E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) )`