Metamath Proof Explorer

Theorem stoweidlem57

Description: There exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91. In this theorem, it is proven the non-trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem57.1 ⊢ Ⅎ 𝑡 𝐷
stoweidlem57.2 ⊢ Ⅎ 𝑡 𝑈
stoweidlem57.3 ⊢ Ⅎ 𝑡 𝜑
stoweidlem57.4 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
stoweidlem57.5 ⊢ 𝑉 = { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
stoweidlem57.6 ⊢ 𝐾 = ( topGen ‘ ran (,) )
stoweidlem57.7 ⊢ 𝑇 = ∪ 𝐽
stoweidlem57.8 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
stoweidlem57.9 ⊢ 𝑈 = ( 𝑇 ∖ 𝐵 )
stoweidlem57.10 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
stoweidlem57.11 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
stoweidlem57.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem57.13 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem57.14 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
stoweidlem57.15 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
stoweidlem57.16 ⊢ ( 𝜑 → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
stoweidlem57.17 ⊢ ( 𝜑 → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
stoweidlem57.18 ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐷 ) = ∅ )
stoweidlem57.19 ⊢ ( 𝜑 → 𝐷 ≠ ∅ )
stoweidlem57.20 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem57.21 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
Assertion stoweidlem57 ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem57.1 ⊢ Ⅎ 𝑡 𝐷
2 stoweidlem57.2 ⊢ Ⅎ 𝑡 𝑈
3 stoweidlem57.3 ⊢ Ⅎ 𝑡 𝜑
4 stoweidlem57.4 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
5 stoweidlem57.5 ⊢ 𝑉 = { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
6 stoweidlem57.6 ⊢ 𝐾 = ( topGen ‘ ran (,) )
7 stoweidlem57.7 ⊢ 𝑇 = ∪ 𝐽
8 stoweidlem57.8 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
9 stoweidlem57.9 ⊢ 𝑈 = ( 𝑇 ∖ 𝐵 )
10 stoweidlem57.10 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
11 stoweidlem57.11 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
12 stoweidlem57.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
13 stoweidlem57.13 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
14 stoweidlem57.14 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
15 stoweidlem57.15 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
16 stoweidlem57.16 ⊢ ( 𝜑 → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
17 stoweidlem57.17 ⊢ ( 𝜑 → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
18 stoweidlem57.18 ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐷 ) = ∅ )
19 stoweidlem57.19 ⊢ ( 𝜑 → 𝐷 ≠ ∅ )
20 stoweidlem57.20 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
21 stoweidlem57.21 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
22 1 nfcri ⊢ Ⅎ 𝑡 𝑠 ∈ 𝐷
23 3 22 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑠 ∈ 𝐷 )
24 10 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → 𝐽 ∈ Comp )
25 11 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → 𝐴 ⊆ 𝐶 )
26 12 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
27 13 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
28 14 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
29 15 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
30 cmptop ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
31 7 iscld ⊢ ( 𝐽 ∈ Top → ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝐵 ⊆ 𝑇 ∧ ( 𝑇 ∖ 𝐵 ) ∈ 𝐽 ) ) )
32 10 30 31 3syl ⊢ ( 𝜑 → ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝐵 ⊆ 𝑇 ∧ ( 𝑇 ∖ 𝐵 ) ∈ 𝐽 ) ) )
33 16 32 mpbid ⊢ ( 𝜑 → ( 𝐵 ⊆ 𝑇 ∧ ( 𝑇 ∖ 𝐵 ) ∈ 𝐽 ) )
34 33 simprd ⊢ ( 𝜑 → ( 𝑇 ∖ 𝐵 ) ∈ 𝐽 )
35 9 34 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → 𝑈 ∈ 𝐽 )
37 7 cldss ⊢ ( 𝐷 ∈ ( Clsd ‘ 𝐽 ) → 𝐷 ⊆ 𝑇 )
38 17 37 syl ⊢ ( 𝜑 → 𝐷 ⊆ 𝑇 )
39 38 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → 𝑠 ∈ 𝑇 )
40 disjr ⊢ ( ( 𝐵 ∩ 𝐷 ) = ∅ ↔ ∀ 𝑠 ∈ 𝐷 ¬ 𝑠 ∈ 𝐵 )
41 18 40 sylib ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝐷 ¬ 𝑠 ∈ 𝐵 )
42 41 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → ¬ 𝑠 ∈ 𝐵 )
43 39 42 eldifd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → 𝑠 ∈ ( 𝑇 ∖ 𝐵 ) )
44 43 9 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → 𝑠 ∈ 𝑈 )
45 2 23 6 24 7 8 25 26 27 28 29 36 44 stoweidlem56 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → ∃ 𝑤 ∈ 𝐽 ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) )
46 simpl ⊢ ( ( 𝑤 ∈ 𝐽 ∧ ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) ) → 𝑤 ∈ 𝐽 )
47 simprll ⊢ ( ( 𝑤 ∈ 𝐽 ∧ ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) ) → 𝑠 ∈ 𝑤 )
48 simprr ⊢ ( ( 𝑤 ∈ 𝐽 ∧ ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) ) → ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) )
49 5 rabeq2i ⊢ ( 𝑤 ∈ 𝑉 ↔ ( 𝑤 ∈ 𝐽 ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) )
50 46 48 49 sylanbrc ⊢ ( ( 𝑤 ∈ 𝐽 ∧ ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) ) → 𝑤 ∈ 𝑉 )
51 46 47 50 jca32 ⊢ ( ( 𝑤 ∈ 𝐽 ∧ ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) ) → ( 𝑤 ∈ 𝐽 ∧ ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉 ) ) )
52 51 reximi2 ⊢ ( ∃ 𝑤 ∈ 𝐽 ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) → ∃ 𝑤 ∈ 𝐽 ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉 ) )
53 rexex ⊢ ( ∃ 𝑤 ∈ 𝐽 ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉 ) → ∃ 𝑤 ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉 ) )
54 45 52 53 3syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → ∃ 𝑤 ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉 ) )
55 nfcv ⊢ Ⅎ 𝑤 𝑠
56 nfrab1 ⊢ Ⅎ 𝑤 { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
57 5 56 nfcxfr ⊢ Ⅎ 𝑤 𝑉
58 55 57 elunif ⊢ ( 𝑠 ∈ ∪ 𝑉 ↔ ∃ 𝑤 ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉 ) )
59 54 58 sylibr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → 𝑠 ∈ ∪ 𝑉 )
60 59 ex ⊢ ( 𝜑 → ( 𝑠 ∈ 𝐷 → 𝑠 ∈ ∪ 𝑉 ) )
61 60 ssrdv ⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑉 )
62 cmpcld ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ↾t 𝐷 ) ∈ Comp )
63 10 17 62 syl2anc ⊢ ( 𝜑 → ( 𝐽 ↾t 𝐷 ) ∈ Comp )
64 10 30 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
65 7 cmpsub ⊢ ( ( 𝐽 ∈ Top ∧ 𝐷 ⊆ 𝑇 ) → ( ( 𝐽 ↾t 𝐷 ) ∈ Comp ↔ ∀ 𝑘 ∈ 𝒫 𝐽 ( 𝐷 ⊆ ∪ 𝑘 → ∃ 𝑢 ∈ ( 𝒫 𝑘 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 ) ) )
66 64 38 65 syl2anc ⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝐷 ) ∈ Comp ↔ ∀ 𝑘 ∈ 𝒫 𝐽 ( 𝐷 ⊆ ∪ 𝑘 → ∃ 𝑢 ∈ ( 𝒫 𝑘 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 ) ) )
67 63 66 mpbid ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝒫 𝐽 ( 𝐷 ⊆ ∪ 𝑘 → ∃ 𝑢 ∈ ( 𝒫 𝑘 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 ) )
68 ssrab2 ⊢ { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) } ⊆ 𝐽
69 5 68 eqsstri ⊢ 𝑉 ⊆ 𝐽
70 5 10 rabexd ⊢ ( 𝜑 → 𝑉 ∈ V )
71 elpwg ⊢ ( 𝑉 ∈ V → ( 𝑉 ∈ 𝒫 𝐽 ↔ 𝑉 ⊆ 𝐽 ) )
72 70 71 syl ⊢ ( 𝜑 → ( 𝑉 ∈ 𝒫 𝐽 ↔ 𝑉 ⊆ 𝐽 ) )
73 69 72 mpbiri ⊢ ( 𝜑 → 𝑉 ∈ 𝒫 𝐽 )
74 unieq ⊢ ( 𝑘 = 𝑉 → ∪ 𝑘 = ∪ 𝑉 )
75 74 sseq2d ⊢ ( 𝑘 = 𝑉 → ( 𝐷 ⊆ ∪ 𝑘 ↔ 𝐷 ⊆ ∪ 𝑉 ) )
76 pweq ⊢ ( 𝑘 = 𝑉 → 𝒫 𝑘 = 𝒫 𝑉 )
77 76 ineq1d ⊢ ( 𝑘 = 𝑉 → ( 𝒫 𝑘 ∩ Fin ) = ( 𝒫 𝑉 ∩ Fin ) )
78 77 rexeqdv ⊢ ( 𝑘 = 𝑉 → ( ∃ 𝑢 ∈ ( 𝒫 𝑘 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 ↔ ∃ 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 ) )
79 75 78 imbi12d ⊢ ( 𝑘 = 𝑉 → ( ( 𝐷 ⊆ ∪ 𝑘 → ∃ 𝑢 ∈ ( 𝒫 𝑘 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 ) ↔ ( 𝐷 ⊆ ∪ 𝑉 → ∃ 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 ) ) )
80 79 rspccva ⊢ ( ( ∀ 𝑘 ∈ 𝒫 𝐽 ( 𝐷 ⊆ ∪ 𝑘 → ∃ 𝑢 ∈ ( 𝒫 𝑘 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 ) ∧ 𝑉 ∈ 𝒫 𝐽 ) → ( 𝐷 ⊆ ∪ 𝑉 → ∃ 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 ) )
81 67 73 80 syl2anc ⊢ ( 𝜑 → ( 𝐷 ⊆ ∪ 𝑉 → ∃ 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 ) )
82 61 81 mpd ⊢ ( 𝜑 → ∃ 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 )
83 elinel1 ⊢ ( 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) → 𝑢 ∈ 𝒫 𝑉 )
84 elpwi ⊢ ( 𝑢 ∈ 𝒫 𝑉 → 𝑢 ⊆ 𝑉 )
85 84 ssdifssd ⊢ ( 𝑢 ∈ 𝒫 𝑉 → ( 𝑢 ∖ { ∅ } ) ⊆ 𝑉 )
86 vex ⊢ 𝑢 ∈ V
87 difexg ⊢ ( 𝑢 ∈ V → ( 𝑢 ∖ { ∅ } ) ∈ V )
88 86 87 ax-mp ⊢ ( 𝑢 ∖ { ∅ } ) ∈ V
89 88 elpw ⊢ ( ( 𝑢 ∖ { ∅ } ) ∈ 𝒫 𝑉 ↔ ( 𝑢 ∖ { ∅ } ) ⊆ 𝑉 )
90 85 89 sylibr ⊢ ( 𝑢 ∈ 𝒫 𝑉 → ( 𝑢 ∖ { ∅ } ) ∈ 𝒫 𝑉 )
91 83 90 syl ⊢ ( 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) → ( 𝑢 ∖ { ∅ } ) ∈ 𝒫 𝑉 )
92 elinel2 ⊢ ( 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) → 𝑢 ∈ Fin )
93 diffi ⊢ ( 𝑢 ∈ Fin → ( 𝑢 ∖ { ∅ } ) ∈ Fin )
94 92 93 syl ⊢ ( 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) → ( 𝑢 ∖ { ∅ } ) ∈ Fin )
95 91 94 elind ⊢ ( 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) → ( 𝑢 ∖ { ∅ } ) ∈ ( 𝒫 𝑉 ∩ Fin ) )
96 95 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ 𝐷 ⊆ ∪ 𝑢 ) → ( 𝑢 ∖ { ∅ } ) ∈ ( 𝒫 𝑉 ∩ Fin ) )
97 unidif0 ⊢ ∪ ( 𝑢 ∖ { ∅ } ) = ∪ 𝑢
98 97 sseq2i ⊢ ( 𝐷 ⊆ ∪ ( 𝑢 ∖ { ∅ } ) ↔ 𝐷 ⊆ ∪ 𝑢 )
99 98 biimpri ⊢ ( 𝐷 ⊆ ∪ 𝑢 → 𝐷 ⊆ ∪ ( 𝑢 ∖ { ∅ } ) )
100 99 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ 𝐷 ⊆ ∪ 𝑢 ) → 𝐷 ⊆ ∪ ( 𝑢 ∖ { ∅ } ) )
101 eldifsni ⊢ ( 𝑤 ∈ ( 𝑢 ∖ { ∅ } ) → 𝑤 ≠ ∅ )
102 101 rgen ⊢ ∀ 𝑤 ∈ ( 𝑢 ∖ { ∅ } ) 𝑤 ≠ ∅
103 102 a1i ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ 𝐷 ⊆ ∪ 𝑢 ) → ∀ 𝑤 ∈ ( 𝑢 ∖ { ∅ } ) 𝑤 ≠ ∅ )
104 unieq ⊢ ( 𝑟 = ( 𝑢 ∖ { ∅ } ) → ∪ 𝑟 = ∪ ( 𝑢 ∖ { ∅ } ) )
105 104 sseq2d ⊢ ( 𝑟 = ( 𝑢 ∖ { ∅ } ) → ( 𝐷 ⊆ ∪ 𝑟 ↔ 𝐷 ⊆ ∪ ( 𝑢 ∖ { ∅ } ) ) )
106 raleq ⊢ ( 𝑟 = ( 𝑢 ∖ { ∅ } ) → ( ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ↔ ∀ 𝑤 ∈ ( 𝑢 ∖ { ∅ } ) 𝑤 ≠ ∅ ) )
107 105 106 anbi12d ⊢ ( 𝑟 = ( 𝑢 ∖ { ∅ } ) → ( ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) ↔ ( 𝐷 ⊆ ∪ ( 𝑢 ∖ { ∅ } ) ∧ ∀ 𝑤 ∈ ( 𝑢 ∖ { ∅ } ) 𝑤 ≠ ∅ ) ) )
108 107 rspcev ⊢ ( ( ( 𝑢 ∖ { ∅ } ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ ( 𝑢 ∖ { ∅ } ) ∧ ∀ 𝑤 ∈ ( 𝑢 ∖ { ∅ } ) 𝑤 ≠ ∅ ) ) → ∃ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) )
109 96 100 103 108 syl12anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ 𝐷 ⊆ ∪ 𝑢 ) → ∃ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) )
110 109 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( 𝒫 𝑉 ∩ Fin ) 𝐷 ⊆ ∪ 𝑢 → ∃ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) ) )
111 82 110 mpd ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) )
112 nfv ⊢ Ⅎ ℎ 𝜑
113 nfcv ⊢ Ⅎ ℎ ℝ+
114 nfre1 ⊢ Ⅎ ℎ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) )
115 113 114 nfralw ⊢ Ⅎ ℎ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) )
116 nfcv ⊢ Ⅎ ℎ 𝐽
117 115 116 nfrabw ⊢ Ⅎ ℎ { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
118 5 117 nfcxfr ⊢ Ⅎ ℎ 𝑉
119 118 nfpw ⊢ Ⅎ ℎ 𝒫 𝑉
120 nfcv ⊢ Ⅎ ℎ Fin
121 119 120 nfin ⊢ Ⅎ ℎ ( 𝒫 𝑉 ∩ Fin )
122 121 nfcri ⊢ Ⅎ ℎ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin )
123 nfv ⊢ Ⅎ ℎ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ )
124 112 122 123 nf3an ⊢ Ⅎ ℎ ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) )
125 nfcv ⊢ Ⅎ 𝑡 ℝ+
126 nfcv ⊢ Ⅎ 𝑡 𝐴
127 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 )
128 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒
129 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 )
130 127 128 129 nf3an ⊢ Ⅎ 𝑡 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) )
131 126 130 nfrex ⊢ Ⅎ 𝑡 ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) )
132 125 131 nfralw ⊢ Ⅎ 𝑡 ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) )
133 nfcv ⊢ Ⅎ 𝑡 𝐽
134 132 133 nfrabw ⊢ Ⅎ 𝑡 { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
135 5 134 nfcxfr ⊢ Ⅎ 𝑡 𝑉
136 135 nfpw ⊢ Ⅎ 𝑡 𝒫 𝑉
137 nfcv ⊢ Ⅎ 𝑡 Fin
138 136 137 nfin ⊢ Ⅎ 𝑡 ( 𝒫 𝑉 ∩ Fin )
139 138 nfcri ⊢ Ⅎ 𝑡 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin )
140 nfcv ⊢ Ⅎ 𝑡 ∪ 𝑟
141 1 140 nfss ⊢ Ⅎ 𝑡 𝐷 ⊆ ∪ 𝑟
142 nfv ⊢ Ⅎ 𝑡 ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅
143 141 142 nfan ⊢ Ⅎ 𝑡 ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ )
144 3 139 143 nf3an ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) )
145 nfv ⊢ Ⅎ 𝑤 𝜑
146 57 nfpw ⊢ Ⅎ 𝑤 𝒫 𝑉
147 nfcv ⊢ Ⅎ 𝑤 Fin
148 146 147 nfin ⊢ Ⅎ 𝑤 ( 𝒫 𝑉 ∩ Fin )
149 148 nfcri ⊢ Ⅎ 𝑤 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin )
150 nfv ⊢ Ⅎ 𝑤 𝐷 ⊆ ∪ 𝑟
151 nfra1 ⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅
152 150 151 nfan ⊢ Ⅎ 𝑤 ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ )
153 145 149 152 nf3an ⊢ Ⅎ 𝑤 ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) )
154 simp2 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) ) → 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) )
155 simp3l ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) ) → 𝐷 ⊆ ∪ 𝑟 )
156 19 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) ) → 𝐷 ≠ ∅ )
157 20 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) ) → 𝐸 ∈ ℝ+ )
158 33 simpld ⊢ ( 𝜑 → 𝐵 ⊆ 𝑇 )
159 158 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) ) → 𝐵 ⊆ 𝑇 )
160 70 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) ) → 𝑉 ∈ V )
161 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
162 6 161 eqeltri ⊢ 𝐾 ∈ Top
163 cnfex ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 Cn 𝐾 ) ∈ V )
164 64 162 163 sylancl ⊢ ( 𝜑 → ( 𝐽 Cn 𝐾 ) ∈ V )
165 11 8 sseqtrdi ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
166 164 165 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
167 166 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) ) → 𝐴 ∈ V )
168 124 144 153 9 4 5 154 155 156 157 159 160 167 stoweidlem39 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) ) → ∃ 𝑚 ∈ ℕ ∃ 𝑣 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
169 168 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( 𝒫 𝑉 ∩ Fin ) ( 𝐷 ⊆ ∪ 𝑟 ∧ ∀ 𝑤 ∈ 𝑟 𝑤 ≠ ∅ ) → ∃ 𝑚 ∈ ℕ ∃ 𝑣 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) )
170 111 169 mpd ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ∃ 𝑣 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
171 nfv ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑚 ∈ ℕ )
172 nfv ⊢ Ⅎ 𝑖 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉
173 nfv ⊢ Ⅎ 𝑖 𝐷 ⊆ ∪ ran 𝑣
174 nfv ⊢ Ⅎ 𝑖 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌
175 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) )
176 174 175 nfan ⊢ Ⅎ 𝑖 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
177 176 nfex ⊢ Ⅎ 𝑖 ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
178 172 173 177 nf3an ⊢ Ⅎ 𝑖 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
179 171 178 nfan ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
180 nfv ⊢ Ⅎ 𝑡 𝑚 ∈ ℕ
181 3 180 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑚 ∈ ℕ )
182 nfcv ⊢ Ⅎ 𝑡 𝑣
183 nfcv ⊢ Ⅎ 𝑡 ( 1 ... 𝑚 )
184 182 183 135 nff ⊢ Ⅎ 𝑡 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉
185 nfcv ⊢ Ⅎ 𝑡 ∪ ran 𝑣
186 1 185 nfss ⊢ Ⅎ 𝑡 𝐷 ⊆ ∪ ran 𝑣
187 nfcv ⊢ Ⅎ 𝑡 𝑦
188 127 126 nfrabw ⊢ Ⅎ 𝑡 { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
189 4 188 nfcxfr ⊢ Ⅎ 𝑡 𝑌
190 187 183 189 nff ⊢ Ⅎ 𝑡 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌
191 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 )
192 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 )
193 191 192 nfan ⊢ Ⅎ 𝑡 ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) )
194 183 193 nfralw ⊢ Ⅎ 𝑡 ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) )
195 190 194 nfan ⊢ Ⅎ 𝑡 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
196 195 nfex ⊢ Ⅎ 𝑡 ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
197 184 186 196 nf3an ⊢ Ⅎ 𝑡 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
198 181 197 nfan ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
199 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑚 ∈ ℕ )
200 nfv ⊢ Ⅎ 𝑦 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉
201 nfv ⊢ Ⅎ 𝑦 𝐷 ⊆ ∪ ran 𝑣
202 nfe1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
203 200 201 202 nf3an ⊢ Ⅎ 𝑦 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
204 199 203 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
205 nfv ⊢ Ⅎ 𝑤 ( 𝜑 ∧ 𝑚 ∈ ℕ )
206 nfcv ⊢ Ⅎ 𝑤 𝑣
207 nfcv ⊢ Ⅎ 𝑤 ( 1 ... 𝑚 )
208 206 207 57 nff ⊢ Ⅎ 𝑤 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉
209 nfv ⊢ Ⅎ 𝑤 𝐷 ⊆ ∪ ran 𝑣
210 nfv ⊢ Ⅎ 𝑤 ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
211 208 209 210 nf3an ⊢ Ⅎ 𝑤 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
212 205 211 nfan ⊢ Ⅎ 𝑤 ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
213 eqid ⊢ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
214 eqid ⊢ ( 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } , 𝑔 ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } , 𝑔 ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
215 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
216 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( seq 1 ( · , ( ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ‘ 𝑚 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( seq 1 ( · , ( ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ‘ 𝑚 ) )
217 simp1ll ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → 𝜑 )
218 217 13 syld3an1 ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
219 11 sselda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ 𝐶 )
220 6 7 8 219 fcnre ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
221 220 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
222 simplr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) → 𝑚 ∈ ℕ )
223 simpr1 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) → 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 )
224 7 cldss ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐵 ⊆ 𝑇 )
225 16 224 syl ⊢ ( 𝜑 → 𝐵 ⊆ 𝑇 )
226 225 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) → 𝐵 ⊆ 𝑇 )
227 simpr2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) → 𝐷 ⊆ ∪ ran 𝑣 )
228 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) → 𝐷 ⊆ 𝑇 )
229 feq3 ⊢ ( 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } → ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ↔ 𝑦 : ( 1 ... 𝑚 ) ⟶ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ) )
230 4 229 ax-mp ⊢ ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ↔ 𝑦 : ( 1 ... 𝑚 ) ⟶ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } )
231 230 biimpi ⊢ ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 → 𝑦 : ( 1 ... 𝑚 ) ⟶ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } )
232 231 anim1i ⊢ ( ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ( 𝑦 : ( 1 ... 𝑚 ) ⟶ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
233 232 eximi ⊢ ( ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
234 233 3ad2ant3 ⊢ ( ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
235 234 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) → ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
236 10 uniexd ⊢ ( 𝜑 → ∪ 𝐽 ∈ V )
237 7 236 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ V )
238 237 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) → 𝑇 ∈ V )
239 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) → 𝐸 ∈ ℝ+ )
240 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) → 𝐸 < ( 1 / 3 ) )
241 179 198 204 212 7 213 214 215 216 5 218 221 222 223 226 227 228 235 238 239 240 stoweidlem54 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )
242 241 ex ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
243 242 exlimdv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑣 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
244 243 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑣 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑉 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
245 170 244 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )