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 ⊢ Ⅎ 𝑡 𝑈
stoweidlem28.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem28.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
stoweidlem28.4 ⊢ 𝑇 = ∪ 𝐽
stoweidlem28.5 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
stoweidlem28.6 ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐽 Cn 𝐾 ) )
stoweidlem28.7 ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑃 ‘ 𝑡 ) )
stoweidlem28.8 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
Assertion stoweidlem28 ( 𝜑 → ∃ 𝑑 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑃 ‘ 𝑡 ) ) )

Proof

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