Theorem stoweidlem52

Description: There exists a neighborhood V as in Lemma 1 of BrosowskiDeutsh p. 90. Here Z is used to represent t_0 in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem52.1	⊢ Ⅎ 𝑡 𝑈
	stoweidlem52.2	⊢ Ⅎ 𝑡 𝜑
	stoweidlem52.3	⊢ Ⅎ 𝑡 𝑃
	stoweidlem52.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
	stoweidlem52.5	⊢ 𝑉 = { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
	stoweidlem52.7	⊢ 𝑇 = ∪ 𝐽
	stoweidlem52.8	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
	stoweidlem52.9	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
	stoweidlem52.10	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem52.11	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem52.12	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
	stoweidlem52.13	⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
	stoweidlem52.14	⊢ ( 𝜑 → 𝐷 < 1 )
	stoweidlem52.15	⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
	stoweidlem52.16	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
	stoweidlem52.17	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
	stoweidlem52.18	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
	stoweidlem52.19	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑍 ) = 0 )
	stoweidlem52.20	⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
Assertion	stoweidlem52	⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem52.1	⊢ Ⅎ 𝑡 𝑈
2		stoweidlem52.2	⊢ Ⅎ 𝑡 𝜑
3		stoweidlem52.3	⊢ Ⅎ 𝑡 𝑃
4		stoweidlem52.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
5		stoweidlem52.5	⊢ 𝑉 = { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
6		stoweidlem52.7	⊢ 𝑇 = ∪ 𝐽
7		stoweidlem52.8	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
8		stoweidlem52.9	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
9		stoweidlem52.10	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10		stoweidlem52.11	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
11		stoweidlem52.12	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
12		stoweidlem52.13	⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
13		stoweidlem52.14	⊢ ( 𝜑 → 𝐷 < 1 )
14		stoweidlem52.15	⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
15		stoweidlem52.16	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
16		stoweidlem52.17	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
17		stoweidlem52.18	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
18		stoweidlem52.19	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑍 ) = 0 )
19		stoweidlem52.20	⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
20		nfcv	⊢ Ⅎ 𝑡 ( 𝐷 / 2 )
21	12	rpred	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
22	21	rehalfcld	⊢ ( 𝜑 → ( 𝐷 / 2 ) ∈ ℝ )
23	22	rexrd	⊢ ( 𝜑 → ( 𝐷 / 2 ) ∈ ℝ* )
24	8 7	sseqtrdi	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
25	24 16	sseldd	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐽 Cn 𝐾 ) )
26	20 3 2 4 6 5 23 25	rfcnpre2	⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
27		elssuni	⊢ ( 𝑈 ∈ 𝐽 → 𝑈 ⊆ ∪ 𝐽 )
28	14 27	syl	⊢ ( 𝜑 → 𝑈 ⊆ ∪ 𝐽 )
29	28 6	sseqtrrdi	⊢ ( 𝜑 → 𝑈 ⊆ 𝑇 )
30	29 15	sseldd	⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
31		2re	⊢ 2 ∈ ℝ
32	31	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
33	12	rpgt0d	⊢ ( 𝜑 → 0 < 𝐷 )
34		2pos	⊢ 0 < 2
35	34	a1i	⊢ ( 𝜑 → 0 < 2 )
36	21 32 33 35	divgt0d	⊢ ( 𝜑 → 0 < ( 𝐷 / 2 ) )
37	18 36	eqbrtrd	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑍 ) < ( 𝐷 / 2 ) )
38		nfcv	⊢ Ⅎ 𝑡 𝑍
39		nfcv	⊢ Ⅎ 𝑡 𝑇
40	3 38	nffv	⊢ Ⅎ 𝑡 ( 𝑃 ‘ 𝑍 )
41		nfcv	⊢ Ⅎ 𝑡 <
42	40 41 20	nfbr	⊢ Ⅎ 𝑡 ( 𝑃 ‘ 𝑍 ) < ( 𝐷 / 2 )
43		fveq2	⊢ ( 𝑡 = 𝑍 → ( 𝑃 ‘ 𝑡 ) = ( 𝑃 ‘ 𝑍 ) )
44	43	breq1d	⊢ ( 𝑡 = 𝑍 → ( ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) ↔ ( 𝑃 ‘ 𝑍 ) < ( 𝐷 / 2 ) ) )
45	38 39 42 44	elrabf	⊢ ( 𝑍 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) } ↔ ( 𝑍 ∈ 𝑇 ∧ ( 𝑃 ‘ 𝑍 ) < ( 𝐷 / 2 ) ) )
46	30 37 45	sylanbrc	⊢ ( 𝜑 → 𝑍 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) } )
47	46 5	eleqtrrdi	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
48		nfrab1	⊢ Ⅎ 𝑡 { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
49	5 48	nfcxfr	⊢ Ⅎ 𝑡 𝑉
50	8 16	sseldd	⊢ ( 𝜑 → 𝑃 ∈ 𝐶 )
51	4 6 7 50	fcnre	⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
52	51	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝑃 : 𝑇 ⟶ ℝ )
53	5	reqabi	⊢ ( 𝑡 ∈ 𝑉 ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) ) )
54	53	bilani	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑡 ∈ 𝑇 ∧ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) ) )
55	54	simpld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝑡 ∈ 𝑇 )
56	52 55	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
57	22	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐷 / 2 ) ∈ ℝ )
58	21	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝐷 ∈ ℝ )
59	54	simprd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) )
60		halfpos	⊢ ( 𝐷 ∈ ℝ → ( 0 < 𝐷 ↔ ( 𝐷 / 2 ) < 𝐷 ) )
61	21 60	syl	⊢ ( 𝜑 → ( 0 < 𝐷 ↔ ( 𝐷 / 2 ) < 𝐷 ) )
62	33 61	mpbid	⊢ ( 𝜑 → ( 𝐷 / 2 ) < 𝐷 )
63	62	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐷 / 2 ) < 𝐷 )
64	56 57 58 59 63	lttrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) < 𝐷 )
65	64	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → ( 𝑃 ‘ 𝑡 ) < 𝐷 )
66	21	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → 𝐷 ∈ ℝ )
67	56	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
68	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
69	55	anim1i	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → ( 𝑡 ∈ 𝑇 ∧ ¬ 𝑡 ∈ 𝑈 ) )
70		eldif	⊢ ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ↔ ( 𝑡 ∈ 𝑇 ∧ ¬ 𝑡 ∈ 𝑈 ) )
71	69 70	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) )
72		rsp	⊢ ( ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) → ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) → 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) ) )
73	68 71 72	sylc	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
74	66 67 73	lensymd	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → ¬ ( 𝑃 ‘ 𝑡 ) < 𝐷 )
75	65 74	condan	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝑡 ∈ 𝑈 )
76	75	ex	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑉 → 𝑡 ∈ 𝑈 ) )
77	2 49 1 76	ssrd	⊢ ( 𝜑 → 𝑉 ⊆ 𝑈 )
78		nfv	⊢ Ⅎ 𝑡 𝑒 ∈ ℝ+
79	2 78	nfan	⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑒 ∈ ℝ+ )
80		nfv	⊢ Ⅎ 𝑡 𝑦 ∈ 𝐴
81	79 80	nfan	⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 )
82		nfra1	⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 )
83		nfra1	⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 )
84		nfra1	⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒
85	82 83 84	nf3an	⊢ Ⅎ 𝑡 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 )
86	81 85	nfan	⊢ Ⅎ 𝑡 ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) )
87		eqid	⊢ ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( 𝑦 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
88		eqid	⊢ ( 𝑡 ∈ 𝑇 ↦ 1 ) = ( 𝑡 ∈ 𝑇 ↦ 1 )
89		ssrab2	⊢ { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) } ⊆ 𝑇
90	5 89	eqsstri	⊢ 𝑉 ⊆ 𝑇
91		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → 𝑦 ∈ 𝐴 )
92		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → 𝜑 )
93	8	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐶 )
94	4 6 7 93	fcnre	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 : 𝑇 ⟶ ℝ )
95	92 91 94	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → 𝑦 : 𝑇 ⟶ ℝ )
96	8	sselda	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ 𝐶 )
97	4 6 7 96	fcnre	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
98	92 97	sylan	⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
99	92 9	syl3an1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
100	92 10	syl3an1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
101	92 11	sylan	⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
102		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → 𝑒 ∈ ℝ+ )
103		simpr1	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) )
104		simpr2	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) )
105		simpr3	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 )
106	86 87 88 90 91 95 98 99 100 101 102 103 104 105	stoweidlem41	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) )
107	12	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝐷 ∈ ℝ+ )
108	13	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝐷 < 1 )
109	16	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑃 ∈ 𝐴 )
110	51	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑃 : 𝑇 ⟶ ℝ )
111	17	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
112	19	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
113	97	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
114	9	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
115	10	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
116	11	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
117		simpr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑒 ∈ ℝ+ )
118	3 79 5 107 108 109 110 111 112 113 114 115 116 117	stoweidlem49	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) )
119	106 118	r19.29a	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) )
120	119	ralrimiva	⊢ ( 𝜑 → ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) )
121	47 77 120	jca31	⊢ ( 𝜑 → ( ( 𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
122		eleq2	⊢ ( 𝑣 = 𝑉 → ( 𝑍 ∈ 𝑣 ↔ 𝑍 ∈ 𝑉 ) )
123		sseq1	⊢ ( 𝑣 = 𝑉 → ( 𝑣 ⊆ 𝑈 ↔ 𝑉 ⊆ 𝑈 ) )
124	122 123	anbi12d	⊢ ( 𝑣 = 𝑉 → ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ↔ ( 𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈 ) ) )
125		nfcv	⊢ Ⅎ 𝑡 𝑣
126	125 49	raleqf	⊢ ( 𝑣 = 𝑉 → ( ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ↔ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ) )
127	126	3anbi2d	⊢ ( 𝑣 = 𝑉 → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
128	127	rexbidv	⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
129	128	ralbidv	⊢ ( 𝑣 = 𝑉 → ( ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
130	124 129	anbi12d	⊢ ( 𝑣 = 𝑉 → ( ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) ↔ ( ( 𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) ) )
131	130	rspcev	⊢ ( ( 𝑉 ∈ 𝐽 ∧ ( ( 𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) ) → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
132	26 121 131	syl2anc	⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )