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 bitrdi 
 |-  ( 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 } ) ) )