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 ) )
35 21 22 23 34 addcan2ad
 |-  ( ph -> ( # ` ( S \ { X } ) ) = ( ( M - 1 ) Ramsey G ) )
36 18 35 breqtrrd
 |-  ( ph -> ( ( M - 1 ) Ramsey G ) <_ ( # ` ( S \ { X } ) ) )
37 10 adantr
 |-  ( ( 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 )
48 25 adantr
 |-  ( ( 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 )
55 16 adantr
 |-  ( ( 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 )
59 11 adantr
 |-  ( ( 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 )
69 68 adantr
 |-  ( ( 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 } )
75 74 adantr
 |-  ( ( 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 } ) ) )
80 72 adantr
 |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> M e. NN0 )
81 2 adantr
 |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> R e. Fin )
82 3 adantr
 |-  ( ( 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 )
87 86 adantr
 |-  ( ( ( 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 ) ) ) ) )
102 5 adantr
 |-  ( ( 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 ) )
108 10 adantr
 |-  ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> K : ( S C M ) --> R )
109 8 adantr
 |-  ( ( 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 ) ) )
123 122 ad2antrl
 |-  ( ( ( 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 } ) ) ) )
126 1 ad2antrr
 |-  ( ( ( 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 )
127 2 ad2antrr
 |-  ( ( ( 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 )
128 3 ad2antrr
 |-  ( ( ( 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 )
129 5 ad2antrr
 |-  ( ( ( 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 )
130 6 ad2antrr
 |-  ( ( ( 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 )
131 8 ad2antrr
 |-  ( ( ( 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 )
132 9 ad2antrr
 |-  ( ( ( 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 ) )
133 10 ad2antrr
 |-  ( ( ( 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 )
134 11 ad2antrr
 |-  ( ( ( 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 )
135 83 adantr
 |-  ( ( ( 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 )
136 110 adantr
 |-  ( ( ( 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 } ) )
137 106 adantr
 |-  ( ( ( 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 } ) )
139 138 adantr
 |-  ( ( ( 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 } ) ) )