Metamath Proof Explorer

Theorem stoweidlem56

Description: This theorem proves Lemma 1 in BrosowskiDeutsh p. 90. Here Z is used to represent t_0 in the paper, v is used to represent V in the paper, and e is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem56.1 ⊢ Ⅎ 𝑡 𝑈
stoweidlem56.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem56.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
stoweidlem56.4 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
stoweidlem56.5 ⊢ 𝑇 = ∪ 𝐽
stoweidlem56.6 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
stoweidlem56.7 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
stoweidlem56.8 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem56.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem56.10 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑦 ) ∈ 𝐴 )
stoweidlem56.11 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
stoweidlem56.12 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
stoweidlem56.13 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
Assertion stoweidlem56 ( 𝜑 → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem56.1 ⊢ Ⅎ 𝑡 𝑈
2 stoweidlem56.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem56.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
4 stoweidlem56.4 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
5 stoweidlem56.5 ⊢ 𝑇 = ∪ 𝐽
6 stoweidlem56.6 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
7 stoweidlem56.7 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
8 stoweidlem56.8 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
9 stoweidlem56.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10 stoweidlem56.10 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑦 ) ∈ 𝐴 )
11 stoweidlem56.11 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
12 stoweidlem56.12 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
13 stoweidlem56.13 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
14 eqid ⊢ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
15 eqid ⊢ { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } = { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 stoweidlem55 ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )
17 df-rex ⊢ ( ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ↔ ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) )
18 16 17 sylib ⊢ ( 𝜑 → ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) )
19 simpl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) → 𝜑 )
20 simprl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) → 𝑝 ∈ 𝐴 )
21 simprr3 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) )
22 nfv ⊢ Ⅎ 𝑡 𝑝 ∈ 𝐴
23 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 )
24 2 22 23 nf3an ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) )
25 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) → 𝐽 ∈ Comp )
26 7 sselda ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐶 )
27 26 6 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ( 𝐽 Cn 𝐾 ) )
28 27 3adant3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) → 𝑝 ∈ ( 𝐽 Cn 𝐾 ) )
29 simp3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) )
30 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) → 𝑈 ∈ 𝐽 )
31 1 24 3 5 25 28 29 30 stoweidlem28 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) → ∃ 𝑑 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) )
32 19 20 21 31 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) → ∃ 𝑑 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) )
33 simpr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) → 𝑑 ∈ ℝ+ )
34 simpr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) → 𝑑 < 1 )
35 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) → 𝑝 ∈ 𝐴 )
36 simprr1 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) )
38 simprr2 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) → ( 𝑝 ‘ 𝑍 ) = 0 )
39 38 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) → ( 𝑝 ‘ 𝑍 ) = 0 )
40 simpr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) )
41 37 39 40 3jca ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) )
42 35 41 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) → ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) )
43 33 34 42 3jca ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) → ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) )
44 43 ex ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) → ( ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) → ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) )
45 44 eximdv ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) → ( ∃ 𝑑 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) → ∃ 𝑑 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) )
46 32 45 mpd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) → ∃ 𝑑 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) )
47 46 ex ⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) → ∃ 𝑑 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) )
48 47 eximdv ⊢ ( 𝜑 → ( ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) → ∃ 𝑝 ∃ 𝑑 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) )
49 18 48 mpd ⊢ ( 𝜑 → ∃ 𝑝 ∃ 𝑑 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) )
50 nfv ⊢ Ⅎ 𝑡 𝑑 ∈ ℝ+
51 nfv ⊢ Ⅎ 𝑡 𝑑 < 1
52 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 )
53 nfv ⊢ Ⅎ 𝑡 ( 𝑝 ‘ 𝑍 ) = 0
54 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 )
55 52 53 54 nf3an ⊢ Ⅎ 𝑡 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) )
56 22 55 nfan ⊢ Ⅎ 𝑡 ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) )
57 50 51 56 nf3an ⊢ Ⅎ 𝑡 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) )
58 2 57 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) )
59 nfcv ⊢ Ⅎ 𝑡 𝑝
60 eqid ⊢ { 𝑡 ∈ 𝑇 ∣ ( 𝑝 ‘ 𝑡 ) < ( 𝑑 / 2 ) } = { 𝑡 ∈ 𝑇 ∣ ( 𝑝 ‘ 𝑡 ) < ( 𝑑 / 2 ) }
61 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) → 𝐴 ⊆ 𝐶 )
62 8 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
63 9 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
64 10 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) ∧ 𝑦 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑦 ) ∈ 𝐴 )
65 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) → 𝑑 ∈ ℝ+ )
66 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) → 𝑑 < 1 )
67 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) → 𝑈 ∈ 𝐽 )
68 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) → 𝑍 ∈ 𝑈 )
69 simpr3l ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) → 𝑝 ∈ 𝐴 )
70 simp3r1 ⊢ ( ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) )
71 70 adantl ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) )
72 simp3r2 ⊢ ( ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) → ( 𝑝 ‘ 𝑍 ) = 0 )
73 72 adantl ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) → ( 𝑝 ‘ 𝑍 ) = 0 )
74 simp3r3 ⊢ ( ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) )
75 74 adantl ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) )
76 1 58 59 3 60 5 6 61 62 63 64 65 66 67 68 69 71 73 75 stoweidlem52 ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) ) → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
77 76 ex ⊢ ( 𝜑 → ( ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) ) )
78 77 exlimdvv ⊢ ( 𝜑 → ( ∃ 𝑝 ∃ 𝑑 ( 𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝑑 ≤ ( 𝑝 ‘ 𝑡 ) ) ) ) → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) ) )
79 49 78 mpd ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )