Theorem ramub1lem2 15731

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

Hypotheses

Ref	Expression
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

Ref	Expression
ramub1lem2	|- ( ph -> E. c e. R E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) )

Distinct variable groups:   x, u, c, y, z, F   a, b, c, i, u, x, y, z, M   G, a, c, i, u, x, y, z   R, c, u, x, y, z   ph, c, u, x, y, z   S, a, c, i, u, x, y, z   C, c, u, x, y, z   H, c, u, x, y, z   K, c, u, x, y, z   X, a, c, i, u, x, y, z

Allowed substitution hints:   ph( i, a, b)   C( i, a, b)   R( i, a, b)   S( b)   F( i, a, b)   G( b)   H( i, a, b)   K( i, a, b)   X( b)

Proof of Theorem ramub1lem2

Dummy variables d v w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ramub1.3	. . 3 |- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
2		ramub1.m	. . . 4 |- ( ph -> M e. NN )
3		nnm1nn0 11334	. . . 4 |- ( M e. NN -> ( M - 1 ) e. NN0 )
4	2, 3	syl 17	. . 3 |- ( ph -> ( M - 1 ) e. NN0 )
5		ramub1.r	. . 3 |- ( ph -> R e. Fin )
6		ramub1.1	. . 3 |- ( ph -> G : R --> NN0 )
7		ramub1.2	. . 3 |- ( ph -> ( ( M - 1 ) Ramsey G ) e. NN0 )
8		ramub1.4	. . . 4 |- ( ph -> S e. Fin )
9		diffi 8192	. . . 4 |- ( S e. Fin -> ( S \ { X } ) e. Fin )
10	8, 9	syl 17	. . 3 |- ( ph -> ( S \ { X } ) e. Fin )
11	7	nn0red 11352	. . . . 5 |- ( ph -> ( ( M - 1 ) Ramsey G ) e. RR )
12	11	leidd 10594	. . . 4 |- ( ph -> ( ( M - 1 ) Ramsey G ) <_ ( ( M - 1 ) Ramsey G ) )
13		hashcl 13147	. . . . . . 7 |- ( ( S \ { X } ) e. Fin -> ( # ` ( S \ { X } ) ) e. NN0 )
14	10, 13	syl 17	. . . . . 6 |- ( ph -> ( # ` ( S \ { X } ) ) e. NN0 )
15	14	nn0cnd 11353	. . . . 5 |- ( ph -> ( # ` ( S \ { X } ) ) e. CC )
16	7	nn0cnd 11353	. . . . 5 |- ( ph -> ( ( M - 1 ) Ramsey G ) e. CC )
17		1cnd 10056	. . . . 5 |- ( ph -> 1 e. CC )
18		undif1 4043	. . . . . . . 8 |- ( ( S \ { X } ) u. { X } ) = ( S u. { X } )
19		ramub1.x	. . . . . . . . . 10 |- ( ph -> X e. S )
20	19	snssd 4340	. . . . . . . . 9 |- ( ph -> { X } C_ S )
21		ssequn2 3786	. . . . . . . . 9 |- ( { X } C_ S <-> ( S u. { X } ) = S )
22	20, 21	sylib 208	. . . . . . . 8 |- ( ph -> ( S u. { X } ) = S )
23	18, 22	syl5eq 2668	. . . . . . 7 |- ( ph -> ( ( S \ { X } ) u. { X } ) = S )
24	23	fveq2d 6195	. . . . . 6 |- ( ph -> ( # ` ( ( S \ { X } ) u. { X } ) ) = ( # ` S ) )
25		neldifsnd 4322	. . . . . . 7 |- ( ph -> -. X e. ( S \ { X } ) )
26		hashunsng 13181	. . . . . . . 8 |- ( X e. S -> ( ( ( S \ { X } ) e. Fin /\ -. X e. ( S \ { X } ) ) -> ( # ` ( ( S \ { X } ) u. { X } ) ) = ( ( # ` ( S \ { X } ) ) + 1 ) ) )
27	19, 26	syl 17	. . . . . . 7 |- ( ph -> ( ( ( S \ { X } ) e. Fin /\ -. X e. ( S \ { X } ) ) -> ( # ` ( ( S \ { X } ) u. { X } ) ) = ( ( # ` ( S \ { X } ) ) + 1 ) ) )
28	10, 25, 27	mp2and 715	. . . . . 6 |- ( ph -> ( # ` ( ( S \ { X } ) u. { X } ) ) = ( ( # ` ( S \ { X } ) ) + 1 ) )
29		ramub1.5	. . . . . 6 |- ( ph -> ( # ` S ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) )
30	24, 28, 29	3eqtr3d 2664	. . . . 5 |- ( ph -> ( ( # ` ( S \ { X } ) ) + 1 ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) )
31	15, 16, 17, 30	addcan2ad 10242	. . . 4 |- ( ph -> ( # ` ( S \ { X } ) ) = ( ( M - 1 ) Ramsey G ) )
32	12, 31	breqtrrd 4681	. . 3 |- ( ph -> ( ( M - 1 ) Ramsey G ) <_ ( # ` ( S \ { X } ) ) )
33		ramub1.6	. . . . . 6 |- ( ph -> K : ( S C M ) --> R )
34	33	adantr 481	. . . . 5 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> K : ( S C M ) --> R )
35	1	hashbcval 15706	. . . . . . . . . . . . . . 15 |- ( ( ( S \ { X } ) e. Fin /\ ( M - 1 ) e. NN0 ) -> ( ( S \ { X } ) C ( M - 1 ) ) = { x e. ~P ( S \ { X } ) | ( # ` x ) = ( M - 1 ) } )
36	10, 4, 35	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ph -> ( ( S \ { X } ) C ( M - 1 ) ) = { x e. ~P ( S \ { X } ) | ( # ` x ) = ( M - 1 ) } )
37	36	eleq2d 2687	. . . . . . . . . . . . 13 |- ( ph -> ( u e. ( ( S \ { X } ) C ( M - 1 ) ) <-> u e. { x e. ~P ( S \ { X } ) | ( # ` x ) = ( M - 1 ) } ) )
38		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( x = u -> ( # ` x ) = ( # ` u ) )
39	38	eqeq1d 2624	. . . . . . . . . . . . . 14 |- ( x = u -> ( ( # ` x ) = ( M - 1 ) <-> ( # ` u ) = ( M - 1 ) ) )
40	39	elrab 3363	. . . . . . . . . . . . 13 |- ( u e. { x e. ~P ( S \ { X } ) | ( # ` x ) = ( M - 1 ) } <-> ( u e. ~P ( S \ { X } ) /\ ( # ` u ) = ( M - 1 ) ) )
41	37, 40	syl6bb 276	. . . . . . . . . . . 12 |- ( ph -> ( u e. ( ( S \ { X } ) C ( M - 1 ) ) <-> ( u e. ~P ( S \ { X } ) /\ ( # ` u ) = ( M - 1 ) ) ) )
42	41	simprbda 653	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> u e. ~P ( S \ { X } ) )
43	42	elpwid 4170	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> u C_ ( S \ { X } ) )
44	43	difss2d 3740	. . . . . . . . 9 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> u C_ S )
45	20	adantr 481	. . . . . . . . 9 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> { X } C_ S )
46	44, 45	unssd 3789	. . . . . . . 8 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( u u. { X } ) C_ S )
47		vex 3203	. . . . . . . . . 10 |- u e. _V
48		snex 4908	. . . . . . . . . 10 |- { X } e. _V
49	47, 48	unex 6956	. . . . . . . . 9 |- ( u u. { X } ) e. _V
50	49	elpw 4164	. . . . . . . 8 |- ( ( u u. { X } ) e. ~P S <-> ( u u. { X } ) C_ S )
51	46, 50	sylibr 224	. . . . . . 7 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( u u. { X } ) e. ~P S )
52	10	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( S \ { X } ) e. Fin )
53		ssfi 8180	. . . . . . . . . 10 |- ( ( ( S \ { X } ) e. Fin /\ u C_ ( S \ { X } ) ) -> u e. Fin )
54	52, 43, 53	syl2anc 693	. . . . . . . . 9 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> u e. Fin )
55		neldifsnd 4322	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> -. X e. ( S \ { X } ) )
56	43, 55	ssneldd 3606	. . . . . . . . 9 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> -. X e. u )
57	19	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> X e. S )
58		hashunsng 13181	. . . . . . . . . 10 |- ( X e. S -> ( ( u e. Fin /\ -. X e. u ) -> ( # ` ( u u. { X } ) ) = ( ( # ` u ) + 1 ) ) )
59	57, 58	syl 17	. . . . . . . . 9 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( ( u e. Fin /\ -. X e. u ) -> ( # ` ( u u. { X } ) ) = ( ( # ` u ) + 1 ) ) )
60	54, 56, 59	mp2and 715	. . . . . . . 8 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( # ` ( u u. { X } ) ) = ( ( # ` u ) + 1 ) )
61	41	simplbda 654	. . . . . . . . 9 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( # ` u ) = ( M - 1 ) )
62	61	oveq1d 6665	. . . . . . . 8 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( ( # ` u ) + 1 ) = ( ( M - 1 ) + 1 ) )
63	2	nncnd 11036	. . . . . . . . . 10 |- ( ph -> M e. CC )
64		ax-1cn 9994	. . . . . . . . . 10 |- 1 e. CC
65		npcan 10290	. . . . . . . . . 10 |- ( ( M e. CC /\ 1 e. CC ) -> ( ( M - 1 ) + 1 ) = M )
66	63, 64, 65	sylancl 694	. . . . . . . . 9 |- ( ph -> ( ( M - 1 ) + 1 ) = M )
67	66	adantr 481	. . . . . . . 8 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( ( M - 1 ) + 1 ) = M )
68	60, 62, 67	3eqtrd 2660	. . . . . . 7 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( # ` ( u u. { X } ) ) = M )
69		fveq2 6191	. . . . . . . . 9 |- ( x = ( u u. { X } ) -> ( # ` x ) = ( # ` ( u u. { X } ) ) )
70	69	eqeq1d 2624	. . . . . . . 8 |- ( x = ( u u. { X } ) -> ( ( # ` x ) = M <-> ( # ` ( u u. { X } ) ) = M ) )
71	70	elrab 3363	. . . . . . 7 |- ( ( u u. { X } ) e. { x e. ~P S | ( # ` x ) = M } <-> ( ( u u. { X } ) e. ~P S /\ ( # ` ( u u. { X } ) ) = M ) )
72	51, 68, 71	sylanbrc 698	. . . . . 6 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( u u. { X } ) e. { x e. ~P S | ( # ` x ) = M } )
73	2	nnnn0d 11351	. . . . . . . 8 |- ( ph -> M e. NN0 )
74	1	hashbcval 15706	. . . . . . . 8 |- ( ( S e. Fin /\ M e. NN0 ) -> ( S C M ) = { x e. ~P S | ( # ` x ) = M } )
75	8, 73, 74	syl2anc 693	. . . . . . 7 |- ( ph -> ( S C M ) = { x e. ~P S | ( # ` x ) = M } )
76	75	adantr 481	. . . . . 6 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( S C M ) = { x e. ~P S | ( # ` x ) = M } )
77	72, 76	eleqtrrd 2704	. . . . 5 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( u u. { X } ) e. ( S C M ) )
78	34, 77	ffvelrnd 6360	. . . 4 |- ( ( ph /\ u e. ( ( S \ { X } ) C ( M - 1 ) ) ) -> ( K ` ( u u. { X } ) ) e. R )
79		ramub1.h	. . . 4 |- H = ( u e. ( ( S \ { X } ) C ( M - 1 ) ) |-> ( K ` ( u u. { X } ) ) )
80	78, 79	fmptd 6385	. . 3 |- ( ph -> H : ( ( S \ { X } ) C ( M - 1 ) ) --> R )
81	1, 4, 5, 6, 7, 10, 32, 80	rami 15719	. 2 |- ( ph -> E. d e. R E. w e. ~P ( S \ { X } ) ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) )
82	73	adantr 481	. . . . . 6 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> M e. NN0 )
83	5	adantr 481	. . . . . 6 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> R e. Fin )
84		ramub1.f	. . . . . . . . . . . 12 |- ( ph -> F : R --> NN )
85	84	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> F : R --> NN )
86		simprll 802	. . . . . . . . . . 11 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> d e. R )
87	85, 86	ffvelrnd 6360	. . . . . . . . . 10 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( F ` d ) e. NN )
88		nnm1nn0 11334	. . . . . . . . . 10 |- ( ( F ` d ) e. NN -> ( ( F ` d ) - 1 ) e. NN0 )
89	87, 88	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( ( F ` d ) - 1 ) e. NN0 )
90	89	adantr 481	. . . . . . . 8 |- ( ( ( 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 )
91	85	ffvelrnda 6359	. . . . . . . . 9 |- ( ( ( 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 )
92	91	nnnn0d 11351	. . . . . . . 8 |- ( ( ( 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 )
93	90, 92	ifcld 4131	. . . . . . 7 |- ( ( ( 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 )
94		eqid 2622	. . . . . . 7 |- ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) = ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) )
95	93, 94	fmptd 6385	. . . . . 6 |- ( ( 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 )
96		equequ2 1953	. . . . . . . . . . . 12 |- ( x = d -> ( y = x <-> y = d ) )
97		fveq2 6191	. . . . . . . . . . . . 13 |- ( x = d -> ( F ` x ) = ( F ` d ) )
98	97	oveq1d 6665	. . . . . . . . . . . 12 |- ( x = d -> ( ( F ` x ) - 1 ) = ( ( F ` d ) - 1 ) )
99	96, 98	ifbieq1d 4109	. . . . . . . . . . 11 |- ( x = d -> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) = if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) )
100	99	mpteq2dv 4745	. . . . . . . . . 10 |- ( x = d -> ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) = ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) )
101	100	oveq2d 6666	. . . . . . . . 9 |- ( 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 ) ) ) ) )
102		ramub1.g	. . . . . . . . 9 |- G = ( x e. R |-> ( M Ramsey ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) ) )
103		ovex 6678	. . . . . . . . 9 |- ( M Ramsey ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ) e. _V
104	101, 102, 103	fvmpt 6282	. . . . . . . 8 |- ( d e. R -> ( G ` d ) = ( M Ramsey ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ) )
105	86, 104	syl 17	. . . . . . 7 |- ( ( 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 ) ) ) ) )
106	6	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> G : R --> NN0 )
107	106, 86	ffvelrnd 6360	. . . . . . 7 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( G ` d ) e. NN0 )
108	105, 107	eqeltrrd 2702	. . . . . 6 |- ( ( 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 )
109		simprlr 803	. . . . . 6 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> w e. ~P ( S \ { X } ) )
110		simprrl 804	. . . . . . 7 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> ( G ` d ) <_ ( # ` w ) )
111	105, 110	eqbrtrrd 4677	. . . . . 6 |- ( ( 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 ) )
112	33	adantr 481	. . . . . . 7 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> K : ( S C M ) --> R )
113	8	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> S e. Fin )
114	109	elpwid 4170	. . . . . . . . 9 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> w C_ ( S \ { X } ) )
115	114	difss2d 3740	. . . . . . . 8 |- ( ( ph /\ ( ( d e. R /\ w e. ~P ( S \ { X } ) ) /\ ( ( G ` d ) <_ ( # ` w ) /\ ( w C ( M - 1 ) ) C_ ( `' H " { d } ) ) ) ) -> w C_ S )
116	1	hashbcss 15708	. . . . . . . 8 |- ( ( S e. Fin /\ w C_ S /\ M e. NN0 ) -> ( w C M ) C_ ( S C M ) )
117	113, 115, 82, 116	syl3anc 1326	. . . . . . 7 |- ( ( 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 ) )
118	112, 117	fssresd 6071	. . . . . 6 |- ( ( 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 )
119	1, 82, 83, 95, 108, 109, 111, 118	rami 15719	. . . . 5 |- ( ( 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 } ) ) )
120		equequ1 1952	. . . . . . . . . . . . . 14 |- ( y = c -> ( y = d <-> c = d ) )
121		fveq2 6191	. . . . . . . . . . . . . 14 |- ( y = c -> ( F ` y ) = ( F ` c ) )
122	120, 121	ifbieq2d 4111	. . . . . . . . . . . . 13 |- ( y = c -> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) = if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) )
123		ovex 6678	. . . . . . . . . . . . . 14 |- ( ( F ` d ) - 1 ) e. _V
124		fvex 6201	. . . . . . . . . . . . . 14 |- ( F ` c ) e. _V
125	123, 124	ifex 4156	. . . . . . . . . . . . 13 |- if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) e. _V
126	122, 94, 125	fvmpt 6282	. . . . . . . . . . . 12 |- ( c e. R -> ( ( y e. R |-> if ( y = d , ( ( F ` d ) - 1 ) , ( F ` y ) ) ) ` c ) = if ( c = d , ( ( F ` d ) - 1 ) , ( F ` c ) ) )
127	126	ad2antrl 764	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
128	127	breq1d 4663	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
129	128	anbi1d 741	. . . . . . . . 9 |- ( ( ( 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 } ) ) ) )
130	2	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( 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 )
131	5	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( 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 )
132	84	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( 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 )
133	6	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( 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 )
134	7	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( 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 )
135	8	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( 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 )
136	29	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( 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 ) )
137	33	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( 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 )
138	19	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( 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 )
139	86	adantr 481	. . . . . . . . . . 11 |- ( ( ( 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 )
140	114	adantr 481	. . . . . . . . . . 11 |- ( ( ( 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 } ) )
141	110	adantr 481	. . . . . . . . . . 11 |- ( ( ( 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 ) )
142		simprrr 805	. . . . . . . . . . . 12 |- ( ( 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 } ) )
143	142	adantr 481	. . . . . . . . . . 11 |- ( ( ( 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 } ) )
144		simprll 802	. . . . . . . . . . 11 |- ( ( ( 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 )
145		simprlr 803	. . . . . . . . . . . 12 |- ( ( ( 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 )
146	145	elpwid 4170	. . . . . . . . . . 11 |- ( ( ( 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 )
147		simprrl 804	. . . . . . . . . . 11 |- ( ( ( 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 ) )
148		simprrr 805	. . . . . . . . . . . 12 |- ( ( ( 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 } ) )
149		cnvresima 5623	. . . . . . . . . . . . 13 |- ( `' ( K |` ( w C M ) ) " { c } ) = ( ( `' K " { c } ) i^i ( w C M ) )
150		inss1 3833	. . . . . . . . . . . . 13 |- ( ( `' K " { c } ) i^i ( w C M ) ) C_ ( `' K " { c } )
151	149, 150	eqsstri 3635	. . . . . . . . . . . 12 |- ( `' ( K |` ( w C M ) ) " { c } ) C_ ( `' K " { c } )
152	148, 151	syl6ss 3615	. . . . . . . . . . 11 |- ( ( ( 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 } ) )
153	130, 131, 132, 102, 133, 134, 1, 135, 136, 137, 138, 79, 139, 140, 141, 143, 144, 146, 147, 152	ramub1lem1 15730	. . . . . . . . . 10 |- ( ( ( 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 } ) ) )
154	153	expr 643	. . . . . . . . 9 |- ( ( ( 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 } ) ) ) )
155	129, 154	sylbid 230	. . . . . . . 8 |- ( ( ( 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 } ) ) ) )
156	155	anassrs 680	. . . . . . 7 |- ( ( ( ( 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 } ) ) ) )
157	156	rexlimdva 3031	. . . . . 6 |- ( ( ( 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 } ) ) ) )
158	157	reximdva 3017	. . . . 5 |- ( ( 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 } ) ) ) )
159	119, 158	mpd 15	. . . 4 |- ( ( 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 } ) ) )
160	159	expr 643	. . 3 |- ( ( 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 } ) ) ) )
161	160	rexlimdvva 3038	. 2 |- ( 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 } ) ) ) )
162	81, 161	mpd 15	1 |- ( ph -> E. c e. R E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   ifcif 4086   ~Pcpw 4158   {csn 4177   class class class wbr 4653   |-> cmpt 4729   `'ccnv 5113   |` cres 5116   "cima 5117   -->wf 5884   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   Fincfn 7955   CCcc 9934   1c1 9937   + caddc 9939   <_ cle 10075   - cmin 10266   NNcn 11020   NN0cn0 11292   #chash 13117   Ramsey cram 15703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-hash 13118  df-ram 15705

This theorem is referenced by:  ramub1  15732