Metamath Proof Explorer

Theorem stoweidlem28

Description: There exists a δ as in Lemma 1 BrosowskiDeutsh p. 90: 0 < delta < 1 and p >= delta on T \ U . Here d is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem28.1 
|- F/_ t U
stoweidlem28.2 
|- F/ t ph
stoweidlem28.3 
|- K = ( topGen ` ran (,) )
stoweidlem28.4 
|- T = U. J
stoweidlem28.5 
|- ( ph -> J e. Comp )
stoweidlem28.6 
|- ( ph -> P e. ( J Cn K ) )
stoweidlem28.7 
|- ( ph -> A. t e. ( T \ U ) 0 < ( P ` t ) )
stoweidlem28.8 
|- ( ph -> U e. J )
Assertion stoweidlem28 
|- ( ph -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem28.1 
 |-  F/_ t U
2 stoweidlem28.2 
 |-  F/ t ph
3 stoweidlem28.3 
 |-  K = ( topGen ` ran (,) )
4 stoweidlem28.4 
 |-  T = U. J
5 stoweidlem28.5 
 |-  ( ph -> J e. Comp )
6 stoweidlem28.6 
 |-  ( ph -> P e. ( J Cn K ) )
7 stoweidlem28.7 
 |-  ( ph -> A. t e. ( T \ U ) 0 < ( P ` t ) )
8 stoweidlem28.8 
 |-  ( ph -> U e. J )
9 halfre 
 |-  ( 1 / 2 ) e. RR
10 halfgt0 
 |-  0 < ( 1 / 2 )
11 9 10 elrpii 
 |-  ( 1 / 2 ) e. RR+
12 11 a1i 
 |-  ( ( ph /\ ( T \ U ) = (/) ) -> ( 1 / 2 ) e. RR+ )
13 halflt1 
 |-  ( 1 / 2 ) < 1
14 13 a1i 
 |-  ( ( ph /\ ( T \ U ) = (/) ) -> ( 1 / 2 ) < 1 )
15 nfcv 
 |-  F/_ t T
16 15 1 nfdif 
 |-  F/_ t ( T \ U )
17 16 nfeq1 
 |-  F/ t ( T \ U ) = (/)
18 17 rzalf 
 |-  ( ( T \ U ) = (/) -> A. t e. ( T \ U ) ( 1 / 2 ) <_ ( P ` t ) )
19 18 adantl 
 |-  ( ( ph /\ ( T \ U ) = (/) ) -> A. t e. ( T \ U ) ( 1 / 2 ) <_ ( P ` t ) )
20 ovex 
 |-  ( 1 / 2 ) e. _V
21 eleq1 
 |-  ( d = ( 1 / 2 ) -> ( d e. RR+ <-> ( 1 / 2 ) e. RR+ ) )
22 breq1 
 |-  ( d = ( 1 / 2 ) -> ( d < 1 <-> ( 1 / 2 ) < 1 ) )
23 breq1 
 |-  ( d = ( 1 / 2 ) -> ( d <_ ( P ` t ) <-> ( 1 / 2 ) <_ ( P ` t ) ) )
24 23 ralbidv 
 |-  ( d = ( 1 / 2 ) -> ( A. t e. ( T \ U ) d <_ ( P ` t ) <-> A. t e. ( T \ U ) ( 1 / 2 ) <_ ( P ` t ) ) )
25 21 22 24 3anbi123d 
 |-  ( d = ( 1 / 2 ) -> ( ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) <-> ( ( 1 / 2 ) e. RR+ /\ ( 1 / 2 ) < 1 /\ A. t e. ( T \ U ) ( 1 / 2 ) <_ ( P ` t ) ) ) )
26 20 25 spcev 
 |-  ( ( ( 1 / 2 ) e. RR+ /\ ( 1 / 2 ) < 1 /\ A. t e. ( T \ U ) ( 1 / 2 ) <_ ( P ` t ) ) -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) )
27 12 14 19 26 syl3anc 
 |-  ( ( ph /\ ( T \ U ) = (/) ) -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) )
28 simplll 
 |-  ( ( ( ( ph /\ -. ( T \ U ) = (/) ) /\ x e. ( T \ U ) ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) -> ph )
29 simplr 
 |-  ( ( ( ( ph /\ -. ( T \ U ) = (/) ) /\ x e. ( T \ U ) ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) -> x e. ( T \ U ) )
30 simpr 
 |-  ( ( ( ( ph /\ -. ( T \ U ) = (/) ) /\ x e. ( T \ U ) ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) -> A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) )
31 eqid 
 |-  ( J Cn K ) = ( J Cn K )
32 3 4 31 6 fcnre 
 |-  ( ph -> P : T --> RR )
33 32 adantr 
 |-  ( ( ph /\ x e. ( T \ U ) ) -> P : T --> RR )
34 eldifi 
 |-  ( x e. ( T \ U ) -> x e. T )
35 34 adantl 
 |-  ( ( ph /\ x e. ( T \ U ) ) -> x e. T )
36 33 35 ffvelrnd 
 |-  ( ( ph /\ x e. ( T \ U ) ) -> ( P ` x ) e. RR )
37 nfcv 
 |-  F/_ x ( T \ U )
38 nfv 
 |-  F/ x 0 < ( P ` t )
39 nfv 
 |-  F/ t 0 < ( P ` x )
40 fveq2 
 |-  ( t = x -> ( P ` t ) = ( P ` x ) )
41 40 breq2d 
 |-  ( t = x -> ( 0 < ( P ` t ) <-> 0 < ( P ` x ) ) )
42 16 37 38 39 41 cbvralfw 
 |-  ( A. t e. ( T \ U ) 0 < ( P ` t ) <-> A. x e. ( T \ U ) 0 < ( P ` x ) )
43 42 biimpi 
 |-  ( A. t e. ( T \ U ) 0 < ( P ` t ) -> A. x e. ( T \ U ) 0 < ( P ` x ) )
44 43 r19.21bi 
 |-  ( ( A. t e. ( T \ U ) 0 < ( P ` t ) /\ x e. ( T \ U ) ) -> 0 < ( P ` x ) )
45 7 44 sylan 
 |-  ( ( ph /\ x e. ( T \ U ) ) -> 0 < ( P ` x ) )
46 36 45 elrpd 
 |-  ( ( ph /\ x e. ( T \ U ) ) -> ( P ` x ) e. RR+ )
47 46 3adant3 
 |-  ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) -> ( P ` x ) e. RR+ )
48 16 nfcri 
 |-  F/ t x e. ( T \ U )
49 nfra1 
 |-  F/ t A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t )
50 2 48 49 nf3an 
 |-  F/ t ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) )
51 rspa 
 |-  ( ( A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) /\ t e. ( T \ U ) ) -> ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) )
52 51 3ad2antl3 
 |-  ( ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) /\ t e. ( T \ U ) ) -> ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) )
53 simpl2 
 |-  ( ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) /\ t e. ( T \ U ) ) -> x e. ( T \ U ) )
54 fvres 
 |-  ( x e. ( T \ U ) -> ( ( P |` ( T \ U ) ) ` x ) = ( P ` x ) )
55 53 54 syl 
 |-  ( ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) /\ t e. ( T \ U ) ) -> ( ( P |` ( T \ U ) ) ` x ) = ( P ` x ) )
56 fvres 
 |-  ( t e. ( T \ U ) -> ( ( P |` ( T \ U ) ) ` t ) = ( P ` t ) )
57 56 adantl 
 |-  ( ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) /\ t e. ( T \ U ) ) -> ( ( P |` ( T \ U ) ) ` t ) = ( P ` t ) )
58 52 55 57 3brtr3d 
 |-  ( ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) /\ t e. ( T \ U ) ) -> ( P ` x ) <_ ( P ` t ) )
59 58 ex 
 |-  ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) -> ( t e. ( T \ U ) -> ( P ` x ) <_ ( P ` t ) ) )
60 50 59 ralrimi 
 |-  ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) -> A. t e. ( T \ U ) ( P ` x ) <_ ( P ` t ) )
61 eleq1 
 |-  ( c = ( P ` x ) -> ( c e. RR+ <-> ( P ` x ) e. RR+ ) )
62 breq1 
 |-  ( c = ( P ` x ) -> ( c <_ ( P ` t ) <-> ( P ` x ) <_ ( P ` t ) ) )
63 62 ralbidv 
 |-  ( c = ( P ` x ) -> ( A. t e. ( T \ U ) c <_ ( P ` t ) <-> A. t e. ( T \ U ) ( P ` x ) <_ ( P ` t ) ) )
64 61 63 anbi12d 
 |-  ( c = ( P ` x ) -> ( ( c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) <-> ( ( P ` x ) e. RR+ /\ A. t e. ( T \ U ) ( P ` x ) <_ ( P ` t ) ) ) )
65 64 spcegv 
 |-  ( ( P ` x ) e. RR+ -> ( ( ( P ` x ) e. RR+ /\ A. t e. ( T \ U ) ( P ` x ) <_ ( P ` t ) ) -> E. c ( c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) ) )
66 47 65 syl 
 |-  ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) -> ( ( ( P ` x ) e. RR+ /\ A. t e. ( T \ U ) ( P ` x ) <_ ( P ` t ) ) -> E. c ( c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) ) )
67 47 60 66 mp2and 
 |-  ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) -> E. c ( c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) )
68 simpl1 
 |-  ( ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) /\ ( c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) ) -> ph )
69 simprl 
 |-  ( ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) /\ ( c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) ) -> c e. RR+ )
70 simprr 
 |-  ( ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) /\ ( c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) ) -> A. t e. ( T \ U ) c <_ ( P ` t ) )
71 nfv 
 |-  F/ t c e. RR+
72 nfra1 
 |-  F/ t A. t e. ( T \ U ) c <_ ( P ` t )
73 2 71 72 nf3an 
 |-  F/ t ( ph /\ c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) )
74 eqid 
 |-  if ( c <_ ( 1 / 2 ) , c , ( 1 / 2 ) ) = if ( c <_ ( 1 / 2 ) , c , ( 1 / 2 ) )
75 32 3ad2ant1 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) -> P : T --> RR )
76 difssd 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) -> ( T \ U ) C_ T )
77 simp2 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) -> c e. RR+ )
78 simp3 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) -> A. t e. ( T \ U ) c <_ ( P ` t ) )
79 73 74 75 76 77 78 stoweidlem5 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) )
80 68 69 70 79 syl3anc 
 |-  ( ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) /\ ( c e. RR+ /\ A. t e. ( T \ U ) c <_ ( P ` t ) ) ) -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) )
81 67 80 exlimddv 
 |-  ( ( ph /\ x e. ( T \ U ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) )
82 28 29 30 81 syl3anc 
 |-  ( ( ( ( ph /\ -. ( T \ U ) = (/) ) /\ x e. ( T \ U ) ) /\ A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) )
83 eqid 
 |-  U. ( J |`t ( T \ U ) ) = U. ( J |`t ( T \ U ) )
84 cmptop 
 |-  ( J e. Comp -> J e. Top )
85 5 84 syl 
 |-  ( ph -> J e. Top )
86 elssuni 
 |-  ( U e. J -> U C_ U. J )
87 8 86 syl 
 |-  ( ph -> U C_ U. J )
88 87 4 sseqtrrdi 
 |-  ( ph -> U C_ T )
89 4 isopn2 
 |-  ( ( J e. Top /\ U C_ T ) -> ( U e. J <-> ( T \ U ) e. ( Clsd ` J ) ) )
90 85 88 89 syl2anc 
 |-  ( ph -> ( U e. J <-> ( T \ U ) e. ( Clsd ` J ) ) )
91 8 90 mpbid 
 |-  ( ph -> ( T \ U ) e. ( Clsd ` J ) )
92 cmpcld 
 |-  ( ( J e. Comp /\ ( T \ U ) e. ( Clsd ` J ) ) -> ( J |`t ( T \ U ) ) e. Comp )
93 5 91 92 syl2anc 
 |-  ( ph -> ( J |`t ( T \ U ) ) e. Comp )
94 93 adantr 
 |-  ( ( ph /\ -. ( T \ U ) = (/) ) -> ( J |`t ( T \ U ) ) e. Comp )
95 6 adantr 
 |-  ( ( ph /\ -. ( T \ U ) = (/) ) -> P e. ( J Cn K ) )
96 difssd 
 |-  ( ( ph /\ -. ( T \ U ) = (/) ) -> ( T \ U ) C_ T )
97 4 cnrest 
 |-  ( ( P e. ( J Cn K ) /\ ( T \ U ) C_ T ) -> ( P |` ( T \ U ) ) e. ( ( J |`t ( T \ U ) ) Cn K ) )
98 95 96 97 syl2anc 
 |-  ( ( ph /\ -. ( T \ U ) = (/) ) -> ( P |` ( T \ U ) ) e. ( ( J |`t ( T \ U ) ) Cn K ) )
99 difssd 
 |-  ( ph -> ( T \ U ) C_ T )
100 4 restuni 
 |-  ( ( J e. Top /\ ( T \ U ) C_ T ) -> ( T \ U ) = U. ( J |`t ( T \ U ) ) )
101 85 99 100 syl2anc 
 |-  ( ph -> ( T \ U ) = U. ( J |`t ( T \ U ) ) )
102 101 neeq1d 
 |-  ( ph -> ( ( T \ U ) =/= (/) <-> U. ( J |`t ( T \ U ) ) =/= (/) ) )
103 df-ne 
 |-  ( ( T \ U ) =/= (/) <-> -. ( T \ U ) = (/) )
104 102 103 bitr3di 
 |-  ( ph -> ( U. ( J |`t ( T \ U ) ) =/= (/) <-> -. ( T \ U ) = (/) ) )
105 104 biimpar 
 |-  ( ( ph /\ -. ( T \ U ) = (/) ) -> U. ( J |`t ( T \ U ) ) =/= (/) )
106 83 3 94 98 105 evth2 
 |-  ( ( ph /\ -. ( T \ U ) = (/) ) -> E. x e. U. ( J |`t ( T \ U ) ) A. s e. U. ( J |`t ( T \ U ) ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` s ) )
107 nfcv 
 |-  F/_ s U. ( J |`t ( T \ U ) )
108 nfcv 
 |-  F/_ t J
109 nfcv 
 |-  F/_ t |`t
110 108 109 16 nfov 
 |-  F/_ t ( J |`t ( T \ U ) )
111 110 nfuni 
 |-  F/_ t U. ( J |`t ( T \ U ) )
112 nfcv 
 |-  F/_ t P
113 112 16 nfres 
 |-  F/_ t ( P |` ( T \ U ) )
114 nfcv 
 |-  F/_ t x
115 113 114 nffv 
 |-  F/_ t ( ( P |` ( T \ U ) ) ` x )
116 nfcv 
 |-  F/_ t <_
117 nfcv 
 |-  F/_ t s
118 113 117 nffv 
 |-  F/_ t ( ( P |` ( T \ U ) ) ` s )
119 115 116 118 nfbr 
 |-  F/ t ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` s )
120 nfv 
 |-  F/ s ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t )
121 fveq2 
 |-  ( s = t -> ( ( P |` ( T \ U ) ) ` s ) = ( ( P |` ( T \ U ) ) ` t ) )
122 121 breq2d 
 |-  ( s = t -> ( ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` s ) <-> ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) )
123 107 111 119 120 122 cbvralfw 
 |-  ( A. s e. U. ( J |`t ( T \ U ) ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` s ) <-> A. t e. U. ( J |`t ( T \ U ) ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) )
124 123 rexbii 
 |-  ( E. x e. U. ( J |`t ( T \ U ) ) A. s e. U. ( J |`t ( T \ U ) ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` s ) <-> E. x e. U. ( J |`t ( T \ U ) ) A. t e. U. ( J |`t ( T \ U ) ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) )
125 106 124 sylib 
 |-  ( ( ph /\ -. ( T \ U ) = (/) ) -> E. x e. U. ( J |`t ( T \ U ) ) A. t e. U. ( J |`t ( T \ U ) ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) )
126 16 111 raleqf 
 |-  ( ( T \ U ) = U. ( J |`t ( T \ U ) ) -> ( A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) <-> A. t e. U. ( J |`t ( T \ U ) ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) )
127 126 rexeqbi1dv 
 |-  ( ( T \ U ) = U. ( J |`t ( T \ U ) ) -> ( E. x e. ( T \ U ) A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) <-> E. x e. U. ( J |`t ( T \ U ) ) A. t e. U. ( J |`t ( T \ U ) ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) )
128 101 127 syl 
 |-  ( ph -> ( E. x e. ( T \ U ) A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) <-> E. x e. U. ( J |`t ( T \ U ) ) A. t e. U. ( J |`t ( T \ U ) ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) )
129 128 adantr 
 |-  ( ( ph /\ -. ( T \ U ) = (/) ) -> ( E. x e. ( T \ U ) A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) <-> E. x e. U. ( J |`t ( T \ U ) ) A. t e. U. ( J |`t ( T \ U ) ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) ) )
130 125 129 mpbird 
 |-  ( ( ph /\ -. ( T \ U ) = (/) ) -> E. x e. ( T \ U ) A. t e. ( T \ U ) ( ( P |` ( T \ U ) ) ` x ) <_ ( ( P |` ( T \ U ) ) ` t ) )
131 82 130 r19.29a 
 |-  ( ( ph /\ -. ( T \ U ) = (/) ) -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) )
132 27 131 pm2.61dan 
 |-  ( ph -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) )