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 )`
` |-  ( ( ph /\ E = D ) -> ( V u. { X } ) e. ~P S )`
27 iftrue
` |-  ( E = D -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) = ( ( F ` D ) - 1 ) )`
` |-  ( ( ph /\ E = D ) -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) = ( ( F ` D ) - 1 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ E = D ) -> ( # ` V ) e. RR )`
` |-  ( ( 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 } )`
` |-  ( ( 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 syl5req
` |-  ( ( ( ( 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 )`
` |-  ( ( ph /\ E =/= D ) -> V e. ~P S )`
161 ifnefalse
` |-  ( E =/= D -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) = ( F ` E ) )`
` |-  ( ( ph /\ E =/= D ) -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) = ( F ` E ) )`
` |-  ( ( ph /\ E =/= D ) -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) <_ ( # ` V ) )`
164 162 163 eqbrtrrd
` |-  ( ( ph /\ E =/= D ) -> ( F ` E ) <_ ( # ` V ) )`
` |-  ( ( 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 } ) ) )`