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