Metamath Proof Explorer

Theorem ramub1lem1

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 } ) ) )
ramub1.d 
|- ( ph -> D e. R )
ramub1.w 
|- ( ph -> W C_ ( S \ { X } ) )
ramub1.7 
|- ( ph -> ( G ` D ) <_ ( # ` W ) )
ramub1.8 
|- ( ph -> ( W C ( M - 1 ) ) C_ ( `' H " { D } ) )
ramub1.e 
|- ( ph -> E e. R )
ramub1.v 
|- ( ph -> V C_ W )
ramub1.9 
|- ( ph -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) <_ ( # ` V ) )
ramub1.s 
|- ( ph -> ( V C M ) C_ ( `' K " { E } ) )
Assertion ramub1lem1 
|- ( ph -> E. z e. ~P S ( ( F ` E ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { E } ) ) )

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 ramub1.d 
 |-  ( ph -> D e. R )
14 ramub1.w 
 |-  ( ph -> W C_ ( S \ { X } ) )
15 ramub1.7 
 |-  ( ph -> ( G ` D ) <_ ( # ` W ) )
16 ramub1.8 
 |-  ( ph -> ( W C ( M - 1 ) ) C_ ( `' H " { D } ) )
17 ramub1.e 
 |-  ( ph -> E e. R )
18 ramub1.v 
 |-  ( ph -> V C_ W )
19 ramub1.9 
 |-  ( ph -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) <_ ( # ` V ) )
20 ramub1.s 
 |-  ( ph -> ( V C M ) C_ ( `' K " { E } ) )
21 18 14 sstrd 
 |-  ( ph -> V C_ ( S \ { X } ) )
22 21 difss2d 
 |-  ( ph -> V C_ S )
23 11 snssd 
 |-  ( ph -> { X } C_ S )
24 22 23 unssd 
 |-  ( ph -> ( V u. { X } ) C_ S )
25 8 24 sselpwd 
 |-  ( ph -> ( V u. { X } ) e. ~P S )
26 25 adantr 
 |-  ( ( ph /\ E = D ) -> ( V u. { X } ) e. ~P S )
27 iftrue 
 |-  ( E = D -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) = ( ( F ` D ) - 1 ) )
28 27 adantl 
 |-  ( ( ph /\ E = D ) -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) = ( ( F ` D ) - 1 ) )
29 19 adantr 
 |-  ( ( ph /\ E = D ) -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) <_ ( # ` V ) )
30 28 29 eqbrtrrd 
 |-  ( ( ph /\ E = D ) -> ( ( F ` D ) - 1 ) <_ ( # ` V ) )
31 3 13 ffvelrnd 
 |-  ( ph -> ( F ` D ) e. NN )
32 31 adantr 
 |-  ( ( ph /\ E = D ) -> ( F ` D ) e. NN )
33 32 nnred 
 |-  ( ( ph /\ E = D ) -> ( F ` D ) e. RR )
34 1red 
 |-  ( ( ph /\ E = D ) -> 1 e. RR )
35 8 22 ssfid 
 |-  ( ph -> V e. Fin )
36 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
37 nn0re 
 |-  ( ( # ` V ) e. NN0 -> ( # ` V ) e. RR )
38 35 36 37 3syl 
 |-  ( ph -> ( # ` V ) e. RR )
39 38 adantr 
 |-  ( ( ph /\ E = D ) -> ( # ` V ) e. RR )
40 33 34 39 lesubaddd 
 |-  ( ( ph /\ E = D ) -> ( ( ( F ` D ) - 1 ) <_ ( # ` V ) <-> ( F ` D ) <_ ( ( # ` V ) + 1 ) ) )
41 30 40 mpbid 
 |-  ( ( ph /\ E = D ) -> ( F ` D ) <_ ( ( # ` V ) + 1 ) )
42 fveq2 
 |-  ( E = D -> ( F ` E ) = ( F ` D ) )
43 snidg 
 |-  ( X e. S -> X e. { X } )
44 11 43 syl 
 |-  ( ph -> X e. { X } )
45 21 sseld 
 |-  ( ph -> ( X e. V -> X e. ( S \ { X } ) ) )
46 eldifn 
 |-  ( X e. ( S \ { X } ) -> -. X e. { X } )
47 45 46 syl6 
 |-  ( ph -> ( X e. V -> -. X e. { X } ) )
48 44 47 mt2d 
 |-  ( ph -> -. X e. V )
49 hashunsng 
 |-  ( X e. S -> ( ( V e. Fin /\ -. X e. V ) -> ( # ` ( V u. { X } ) ) = ( ( # ` V ) + 1 ) ) )
50 11 49 syl 
 |-  ( ph -> ( ( V e. Fin /\ -. X e. V ) -> ( # ` ( V u. { X } ) ) = ( ( # ` V ) + 1 ) ) )
51 35 48 50 mp2and 
 |-  ( ph -> ( # ` ( V u. { X } ) ) = ( ( # ` V ) + 1 ) )
52 42 51 breqan12rd 
 |-  ( ( ph /\ E = D ) -> ( ( F ` E ) <_ ( # ` ( V u. { X } ) ) <-> ( F ` D ) <_ ( ( # ` V ) + 1 ) ) )
53 41 52 mpbird 
 |-  ( ( ph /\ E = D ) -> ( F ` E ) <_ ( # ` ( V u. { X } ) ) )
54 snfi 
 |-  { X } e. Fin
55 unfi 
 |-  ( ( V e. Fin /\ { X } e. Fin ) -> ( V u. { X } ) e. Fin )
56 35 54 55 sylancl 
 |-  ( ph -> ( V u. { X } ) e. Fin )
57 1 nnnn0d 
 |-  ( ph -> M e. NN0 )
58 7 hashbcval 
 |-  ( ( ( V u. { X } ) e. Fin /\ M e. NN0 ) -> ( ( V u. { X } ) C M ) = { x e. ~P ( V u. { X } ) | ( # ` x ) = M } )
59 56 57 58 syl2anc 
 |-  ( ph -> ( ( V u. { X } ) C M ) = { x e. ~P ( V u. { X } ) | ( # ` x ) = M } )
60 59 adantr 
 |-  ( ( ph /\ E = D ) -> ( ( V u. { X } ) C M ) = { x e. ~P ( V u. { X } ) | ( # ` x ) = M } )
61 simpl1l 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ x e. ~P V ) -> ph )
62 7 hashbcval 
 |-  ( ( V e. Fin /\ M e. NN0 ) -> ( V C M ) = { x e. ~P V | ( # ` x ) = M } )
63 35 57 62 syl2anc 
 |-  ( ph -> ( V C M ) = { x e. ~P V | ( # ` x ) = M } )
64 63 20 eqsstrrd 
 |-  ( ph -> { x e. ~P V | ( # ` x ) = M } C_ ( `' K " { E } ) )
65 61 64 syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ x e. ~P V ) -> { x e. ~P V | ( # ` x ) = M } C_ ( `' K " { E } ) )
66 simpr 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ x e. ~P V ) -> x e. ~P V )
67 simpl3 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ x e. ~P V ) -> ( # ` x ) = M )
68 rabid 
 |-  ( x e. { x e. ~P V | ( # ` x ) = M } <-> ( x e. ~P V /\ ( # ` x ) = M ) )
69 66 67 68 sylanbrc 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ x e. ~P V ) -> x e. { x e. ~P V | ( # ` x ) = M } )
70 65 69 sseldd 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ x e. ~P V ) -> x e. ( `' K " { E } ) )
71 simpl2 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x e. ~P ( V u. { X } ) )
72 71 elpwid 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x C_ ( V u. { X } ) )
73 simpl1l 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ph )
74 73 24 syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( V u. { X } ) C_ S )
75 72 74 sstrd 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x C_ S )
76 vex 
 |-  x e. _V
77 76 elpw 
 |-  ( x e. ~P S <-> x C_ S )
78 75 77 sylibr 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x e. ~P S )
79 simpl3 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( # ` x ) = M )
80 rabid 
 |-  ( x e. { x e. ~P S | ( # ` x ) = M } <-> ( x e. ~P S /\ ( # ` x ) = M ) )
81 78 79 80 sylanbrc 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x e. { x e. ~P S | ( # ` x ) = M } )
82 7 hashbcval 
 |-  ( ( S e. Fin /\ M e. NN0 ) -> ( S C M ) = { x e. ~P S | ( # ` x ) = M } )
83 8 57 82 syl2anc 
 |-  ( ph -> ( S C M ) = { x e. ~P S | ( # ` x ) = M } )
84 73 83 syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( S C M ) = { x e. ~P S | ( # ` x ) = M } )
85 81 84 eleqtrrd 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x e. ( S C M ) )
86 14 difss2d 
 |-  ( ph -> W C_ S )
87 8 86 ssfid 
 |-  ( ph -> W e. Fin )
88 nnm1nn0 
 |-  ( M e. NN -> ( M - 1 ) e. NN0 )
89 1 88 syl 
 |-  ( ph -> ( M - 1 ) e. NN0 )
90 7 hashbcval 
 |-  ( ( W e. Fin /\ ( M - 1 ) e. NN0 ) -> ( W C ( M - 1 ) ) = { u e. ~P W | ( # ` u ) = ( M - 1 ) } )
91 87 89 90 syl2anc 
 |-  ( ph -> ( W C ( M - 1 ) ) = { u e. ~P W | ( # ` u ) = ( M - 1 ) } )
92 91 16 eqsstrrd 
 |-  ( ph -> { u e. ~P W | ( # ` u ) = ( M - 1 ) } C_ ( `' H " { D } ) )
93 73 92 syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> { u e. ~P W | ( # ` u ) = ( M - 1 ) } C_ ( `' H " { D } ) )
94 fveqeq2 
 |-  ( u = ( x \ { X } ) -> ( ( # ` u ) = ( M - 1 ) <-> ( # ` ( x \ { X } ) ) = ( M - 1 ) ) )
95 uncom 
 |-  ( V u. { X } ) = ( { X } u. V )
96 72 95 sseqtrdi 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x C_ ( { X } u. V ) )
97 ssundif 
 |-  ( x C_ ( { X } u. V ) <-> ( x \ { X } ) C_ V )
98 96 97 sylib 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( x \ { X } ) C_ V )
99 73 18 syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> V C_ W )
100 98 99 sstrd 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( x \ { X } ) C_ W )
101 76 difexi 
 |-  ( x \ { X } ) e. _V
102 101 elpw 
 |-  ( ( x \ { X } ) e. ~P W <-> ( x \ { X } ) C_ W )
103 100 102 sylibr 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( x \ { X } ) e. ~P W )
104 73 8 syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> S e. Fin )
105 104 75 ssfid 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x e. Fin )
106 diffi 
 |-  ( x e. Fin -> ( x \ { X } ) e. Fin )
107 105 106 syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( x \ { X } ) e. Fin )
108 hashcl 
 |-  ( ( x \ { X } ) e. Fin -> ( # ` ( x \ { X } ) ) e. NN0 )
109 nn0cn 
 |-  ( ( # ` ( x \ { X } ) ) e. NN0 -> ( # ` ( x \ { X } ) ) e. CC )
110 107 108 109 3syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( # ` ( x \ { X } ) ) e. CC )
111 ax-1cn 
 |-  1 e. CC
112 pncan 
 |-  ( ( ( # ` ( x \ { X } ) ) e. CC /\ 1 e. CC ) -> ( ( ( # ` ( x \ { X } ) ) + 1 ) - 1 ) = ( # ` ( x \ { X } ) ) )
113 110 111 112 sylancl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( ( ( # ` ( x \ { X } ) ) + 1 ) - 1 ) = ( # ` ( x \ { X } ) ) )
114 neldifsnd 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> -. X e. ( x \ { X } ) )
115 hashunsng 
 |-  ( X e. S -> ( ( ( x \ { X } ) e. Fin /\ -. X e. ( x \ { X } ) ) -> ( # ` ( ( x \ { X } ) u. { X } ) ) = ( ( # ` ( x \ { X } ) ) + 1 ) ) )
116 73 11 115 3syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( ( ( x \ { X } ) e. Fin /\ -. X e. ( x \ { X } ) ) -> ( # ` ( ( x \ { X } ) u. { X } ) ) = ( ( # ` ( x \ { X } ) ) + 1 ) ) )
117 107 114 116 mp2and 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( # ` ( ( x \ { X } ) u. { X } ) ) = ( ( # ` ( x \ { X } ) ) + 1 ) )
118 undif1 
 |-  ( ( x \ { X } ) u. { X } ) = ( x u. { X } )
119 simpr 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> -. x e. ~P V )
120 71 119 eldifd 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x e. ( ~P ( V u. { X } ) \ ~P V ) )
121 elpwunsn 
 |-  ( x e. ( ~P ( V u. { X } ) \ ~P V ) -> X e. x )
122 120 121 syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> X e. x )
123 122 snssd 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> { X } C_ x )
124 ssequn2 
 |-  ( { X } C_ x <-> ( x u. { X } ) = x )
125 123 124 sylib 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( x u. { X } ) = x )
126 118 125 eqtr2id 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x = ( ( x \ { X } ) u. { X } ) )
127 126 fveq2d 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( # ` x ) = ( # ` ( ( x \ { X } ) u. { X } ) ) )
128 127 79 eqtr3d 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( # ` ( ( x \ { X } ) u. { X } ) ) = M )
129 117 128 eqtr3d 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( ( # ` ( x \ { X } ) ) + 1 ) = M )
130 129 oveq1d 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( ( ( # ` ( x \ { X } ) ) + 1 ) - 1 ) = ( M - 1 ) )
131 113 130 eqtr3d 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( # ` ( x \ { X } ) ) = ( M - 1 ) )
132 94 103 131 elrabd 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( x \ { X } ) e. { u e. ~P W | ( # ` u ) = ( M - 1 ) } )
133 93 132 sseldd 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( x \ { X } ) e. ( `' H " { D } ) )
134 12 mptiniseg 
 |-  ( D e. R -> ( `' H " { D } ) = { u e. ( ( S \ { X } ) C ( M - 1 ) ) | ( K ` ( u u. { X } ) ) = D } )
135 73 13 134 3syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( `' H " { D } ) = { u e. ( ( S \ { X } ) C ( M - 1 ) ) | ( K ` ( u u. { X } ) ) = D } )
136 133 135 eleqtrd 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( x \ { X } ) e. { u e. ( ( S \ { X } ) C ( M - 1 ) ) | ( K ` ( u u. { X } ) ) = D } )
137 uneq1 
 |-  ( u = ( x \ { X } ) -> ( u u. { X } ) = ( ( x \ { X } ) u. { X } ) )
138 137 fveqeq2d 
 |-  ( u = ( x \ { X } ) -> ( ( K ` ( u u. { X } ) ) = D <-> ( K ` ( ( x \ { X } ) u. { X } ) ) = D ) )
139 138 elrab 
 |-  ( ( x \ { X } ) e. { u e. ( ( S \ { X } ) C ( M - 1 ) ) | ( K ` ( u u. { X } ) ) = D } <-> ( ( x \ { X } ) e. ( ( S \ { X } ) C ( M - 1 ) ) /\ ( K ` ( ( x \ { X } ) u. { X } ) ) = D ) )
140 139 simprbi 
 |-  ( ( x \ { X } ) e. { u e. ( ( S \ { X } ) C ( M - 1 ) ) | ( K ` ( u u. { X } ) ) = D } -> ( K ` ( ( x \ { X } ) u. { X } ) ) = D )
141 136 140 syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( K ` ( ( x \ { X } ) u. { X } ) ) = D )
142 126 fveq2d 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( K ` x ) = ( K ` ( ( x \ { X } ) u. { X } ) ) )
143 simpl1r 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> E = D )
144 141 142 143 3eqtr4d 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( K ` x ) = E )
145 10 ffnd 
 |-  ( ph -> K Fn ( S C M ) )
146 fniniseg 
 |-  ( K Fn ( S C M ) -> ( x e. ( `' K " { E } ) <-> ( x e. ( S C M ) /\ ( K ` x ) = E ) ) )
147 73 145 146 3syl 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> ( x e. ( `' K " { E } ) <-> ( x e. ( S C M ) /\ ( K ` x ) = E ) ) )
148 85 144 147 mpbir2and 
 |-  ( ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) /\ -. x e. ~P V ) -> x e. ( `' K " { E } ) )
149 70 148 pm2.61dan 
 |-  ( ( ( ph /\ E = D ) /\ x e. ~P ( V u. { X } ) /\ ( # ` x ) = M ) -> x e. ( `' K " { E } ) )
150 149 rabssdv 
 |-  ( ( ph /\ E = D ) -> { x e. ~P ( V u. { X } ) | ( # ` x ) = M } C_ ( `' K " { E } ) )
151 60 150 eqsstrd 
 |-  ( ( ph /\ E = D ) -> ( ( V u. { X } ) C M ) C_ ( `' K " { E } ) )
152 fveq2 
 |-  ( z = ( V u. { X } ) -> ( # ` z ) = ( # ` ( V u. { X } ) ) )
153 152 breq2d 
 |-  ( z = ( V u. { X } ) -> ( ( F ` E ) <_ ( # ` z ) <-> ( F ` E ) <_ ( # ` ( V u. { X } ) ) ) )
154 oveq1 
 |-  ( z = ( V u. { X } ) -> ( z C M ) = ( ( V u. { X } ) C M ) )
155 154 sseq1d 
 |-  ( z = ( V u. { X } ) -> ( ( z C M ) C_ ( `' K " { E } ) <-> ( ( V u. { X } ) C M ) C_ ( `' K " { E } ) ) )
156 153 155 anbi12d 
 |-  ( z = ( V u. { X } ) -> ( ( ( F ` E ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { E } ) ) <-> ( ( F ` E ) <_ ( # ` ( V u. { X } ) ) /\ ( ( V u. { X } ) C M ) C_ ( `' K " { E } ) ) ) )
157 156 rspcev 
 |-  ( ( ( V u. { X } ) e. ~P S /\ ( ( F ` E ) <_ ( # ` ( V u. { X } ) ) /\ ( ( V u. { X } ) C M ) C_ ( `' K " { E } ) ) ) -> E. z e. ~P S ( ( F ` E ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { E } ) ) )
158 26 53 151 157 syl12anc 
 |-  ( ( ph /\ E = D ) -> E. z e. ~P S ( ( F ` E ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { E } ) ) )
159 8 22 sselpwd 
 |-  ( ph -> V e. ~P S )
160 159 adantr 
 |-  ( ( ph /\ E =/= D ) -> V e. ~P S )
161 ifnefalse 
 |-  ( E =/= D -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) = ( F ` E ) )
162 161 adantl 
 |-  ( ( ph /\ E =/= D ) -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) = ( F ` E ) )
163 19 adantr 
 |-  ( ( ph /\ E =/= D ) -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) <_ ( # ` V ) )
164 162 163 eqbrtrrd 
 |-  ( ( ph /\ E =/= D ) -> ( F ` E ) <_ ( # ` V ) )
165 20 adantr 
 |-  ( ( ph /\ E =/= D ) -> ( V C M ) C_ ( `' K " { E } ) )
166 fveq2 
 |-  ( z = V -> ( # ` z ) = ( # ` V ) )
167 166 breq2d 
 |-  ( z = V -> ( ( F ` E ) <_ ( # ` z ) <-> ( F ` E ) <_ ( # ` V ) ) )
168 oveq1 
 |-  ( z = V -> ( z C M ) = ( V C M ) )
169 168 sseq1d 
 |-  ( z = V -> ( ( z C M ) C_ ( `' K " { E } ) <-> ( V C M ) C_ ( `' K " { E } ) ) )
170 167 169 anbi12d 
 |-  ( z = V -> ( ( ( F ` E ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { E } ) ) <-> ( ( F ` E ) <_ ( # ` V ) /\ ( V C M ) C_ ( `' K " { E } ) ) ) )
171 170 rspcev 
 |-  ( ( V e. ~P S /\ ( ( F ` E ) <_ ( # ` V ) /\ ( V C M ) C_ ( `' K " { E } ) ) ) -> E. z e. ~P S ( ( F ` E ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { E } ) ) )
172 160 164 165 171 syl12anc 
 |-  ( ( ph /\ E =/= D ) -> E. z e. ~P S ( ( F ` E ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { E } ) ) )
173 158 172 pm2.61dane 
 |-  ( ph -> E. z e. ~P S ( ( F ` E ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { E } ) ) )