Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem57 Structured version   Visualization version   GIF version

Theorem stoweidlem57 44384
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.)
Hypotheses
Ref Expression
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
Ref Expression
stoweidlem57 (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝐷 (π‘₯β€˜π‘‘) < 𝐸 ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ 𝐸) < (π‘₯β€˜π‘‘)))
Distinct variable groups:   𝑒,π‘Ž,𝑓,𝑑   π‘ž,π‘Ž,π‘Ÿ,𝑓,𝑑,𝐴   𝐴,𝑒,𝑓,𝑑   𝐷,π‘Ž,𝑒,𝑓   𝑇,π‘Ž,𝑒,𝑓,𝑑   π‘ˆ,π‘Ž,𝑒,𝑓   πœ‘,π‘Ž,𝑒,𝑓   𝑒,𝑔,β„Ž,𝑓,𝑑,𝐴   𝑀,𝑒,β„Ž,𝑑,𝐴   𝑒,𝐸,𝑓,𝑔,β„Ž,𝑑   𝑔,π‘Ÿ,β„Ž,𝐴   π‘₯,𝑓,𝑔,β„Ž,𝑑,𝐴   𝐡,𝑓,𝑔,π‘Ÿ   𝑓,𝑉,𝑔,π‘Ÿ   𝑓,π‘Œ,𝑔,π‘Ÿ   𝑔,π‘ž,𝐷   𝐷,β„Ž,π‘Ÿ   𝑔,𝐽,β„Ž,𝑑   𝑇,𝑔,β„Ž,π‘Ÿ   π‘ˆ,𝑔,β„Ž,π‘Ÿ   πœ‘,𝑔,β„Ž,π‘Ÿ   𝑀,π‘Ÿ,𝐸   𝐴,π‘ž   𝐷,π‘ž   𝑇,π‘ž   π‘ˆ,π‘ž   πœ‘,π‘ž   𝑀,𝐷   𝑀,𝐡   𝑑,𝐾   πœ‘,𝑀   𝑀,𝐽   𝑀,𝑇   𝑀,π‘ˆ   𝑀,π‘Œ   π‘₯,𝐡   π‘₯,𝐷   π‘₯,𝐸   π‘₯,𝑇
Allowed substitution hints:   πœ‘(π‘₯,𝑑)   𝐡(𝑑,𝑒,β„Ž,π‘ž,π‘Ž)   𝐢(π‘₯,𝑀,𝑑,𝑒,𝑓,𝑔,β„Ž,π‘Ÿ,π‘ž,π‘Ž)   𝐷(𝑑)   π‘ˆ(π‘₯,𝑑)   𝐸(π‘ž,π‘Ž)   𝐽(π‘₯,𝑒,𝑓,π‘Ÿ,π‘ž,π‘Ž)   𝐾(π‘₯,𝑀,𝑒,𝑓,𝑔,β„Ž,π‘Ÿ,π‘ž,π‘Ž)   𝑉(π‘₯,𝑀,𝑑,𝑒,β„Ž,π‘ž,π‘Ž)   π‘Œ(π‘₯,𝑑,𝑒,β„Ž,π‘ž,π‘Ž)

Proof of Theorem stoweidlem57
Dummy variables 𝑠 π‘š 𝑖 𝑣 𝑦 𝑒 π‘˜ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem57.2 . . . . . . . . . 10 β„²π‘‘π‘ˆ
2 stoweidlem57.3 . . . . . . . . . . 11 β„²π‘‘πœ‘
3 stoweidlem57.1 . . . . . . . . . . . 12 Ⅎ𝑑𝐷
43nfcri 2891 . . . . . . . . . . 11 Ⅎ𝑑 𝑠 ∈ 𝐷
52, 4nfan 1903 . . . . . . . . . 10 Ⅎ𝑑(πœ‘ ∧ 𝑠 ∈ 𝐷)
6 stoweidlem57.6 . . . . . . . . . 10 𝐾 = (topGenβ€˜ran (,))
7 stoweidlem57.10 . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 ∈ Comp)
87adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝐽 ∈ Comp)
9 stoweidlem57.7 . . . . . . . . . 10 𝑇 = βˆͺ 𝐽
10 stoweidlem57.8 . . . . . . . . . 10 𝐢 = (𝐽 Cn 𝐾)
11 stoweidlem57.11 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 βŠ† 𝐢)
1211adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝐴 βŠ† 𝐢)
13 stoweidlem57.12 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
14133adant1r 1178 . . . . . . . . . 10 (((πœ‘ ∧ 𝑠 ∈ 𝐷) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
15 stoweidlem57.13 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
16153adant1r 1178 . . . . . . . . . 10 (((πœ‘ ∧ 𝑠 ∈ 𝐷) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
17 stoweidlem57.14 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ π‘Ž) ∈ 𝐴)
1817adantlr 714 . . . . . . . . . 10 (((πœ‘ ∧ 𝑠 ∈ 𝐷) ∧ π‘Ž ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ π‘Ž) ∈ 𝐴)
19 stoweidlem57.15 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘Ÿ ∈ 𝑇 ∧ 𝑑 ∈ 𝑇 ∧ π‘Ÿ β‰  𝑑)) β†’ βˆƒπ‘ž ∈ 𝐴 (π‘žβ€˜π‘Ÿ) β‰  (π‘žβ€˜π‘‘))
2019adantlr 714 . . . . . . . . . 10 (((πœ‘ ∧ 𝑠 ∈ 𝐷) ∧ (π‘Ÿ ∈ 𝑇 ∧ 𝑑 ∈ 𝑇 ∧ π‘Ÿ β‰  𝑑)) β†’ βˆƒπ‘ž ∈ 𝐴 (π‘žβ€˜π‘Ÿ) β‰  (π‘žβ€˜π‘‘))
21 stoweidlem57.9 . . . . . . . . . . . 12 π‘ˆ = (𝑇 βˆ– 𝐡)
22 stoweidlem57.16 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐡 ∈ (Clsdβ€˜π½))
23 cmptop 22762 . . . . . . . . . . . . . . 15 (𝐽 ∈ Comp β†’ 𝐽 ∈ Top)
249iscld 22394 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top β†’ (𝐡 ∈ (Clsdβ€˜π½) ↔ (𝐡 βŠ† 𝑇 ∧ (𝑇 βˆ– 𝐡) ∈ 𝐽)))
257, 23, 243syl 18 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐡 ∈ (Clsdβ€˜π½) ↔ (𝐡 βŠ† 𝑇 ∧ (𝑇 βˆ– 𝐡) ∈ 𝐽)))
2622, 25mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐡 βŠ† 𝑇 ∧ (𝑇 βˆ– 𝐡) ∈ 𝐽))
2726simprd 497 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑇 βˆ– 𝐡) ∈ 𝐽)
2821, 27eqeltrid 2838 . . . . . . . . . . 11 (πœ‘ β†’ π‘ˆ ∈ 𝐽)
2928adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ π‘ˆ ∈ 𝐽)
30 stoweidlem57.17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 ∈ (Clsdβ€˜π½))
319cldss 22396 . . . . . . . . . . . . . 14 (𝐷 ∈ (Clsdβ€˜π½) β†’ 𝐷 βŠ† 𝑇)
3230, 31syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 βŠ† 𝑇)
3332sselda 3945 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝑠 ∈ 𝑇)
34 stoweidlem57.18 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐡 ∩ 𝐷) = βˆ…)
35 disjr 4410 . . . . . . . . . . . . . 14 ((𝐡 ∩ 𝐷) = βˆ… ↔ βˆ€π‘  ∈ 𝐷 Β¬ 𝑠 ∈ 𝐡)
3634, 35sylib 217 . . . . . . . . . . . . 13 (πœ‘ β†’ βˆ€π‘  ∈ 𝐷 Β¬ 𝑠 ∈ 𝐡)
3736r19.21bi 3233 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ Β¬ 𝑠 ∈ 𝐡)
3833, 37eldifd 3922 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝑠 ∈ (𝑇 βˆ– 𝐡))
3938, 21eleqtrrdi 2845 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝑠 ∈ π‘ˆ)
401, 5, 6, 8, 9, 10, 12, 14, 16, 18, 20, 29, 39stoweidlem56 44383 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ βˆƒπ‘€ ∈ 𝐽 ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))))
41 simpl 484 . . . . . . . . . . 11 ((𝑀 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘)))) β†’ 𝑀 ∈ 𝐽)
42 simprll 778 . . . . . . . . . . 11 ((𝑀 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘)))) β†’ 𝑠 ∈ 𝑀)
43 simprr 772 . . . . . . . . . . . 12 ((𝑀 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘)))) β†’ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘)))
44 stoweidlem57.5 . . . . . . . . . . . . 13 𝑉 = {𝑀 ∈ 𝐽 ∣ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))}
4544reqabi 3428 . . . . . . . . . . . 12 (𝑀 ∈ 𝑉 ↔ (𝑀 ∈ 𝐽 ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))))
4641, 43, 45sylanbrc 584 . . . . . . . . . . 11 ((𝑀 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘)))) β†’ 𝑀 ∈ 𝑉)
4741, 42, 46jca32 517 . . . . . . . . . 10 ((𝑀 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘)))) β†’ (𝑀 ∈ 𝐽 ∧ (𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉)))
4847reximi2 3079 . . . . . . . . 9 (βˆƒπ‘€ ∈ 𝐽 ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))) β†’ βˆƒπ‘€ ∈ 𝐽 (𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉))
49 rexex 3076 . . . . . . . . 9 (βˆƒπ‘€ ∈ 𝐽 (𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉) β†’ βˆƒπ‘€(𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉))
5040, 48, 493syl 18 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ βˆƒπ‘€(𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉))
51 nfcv 2904 . . . . . . . . 9 Ⅎ𝑀𝑠
52 nfrab1 3425 . . . . . . . . . 10 Ⅎ𝑀{𝑀 ∈ 𝐽 ∣ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))}
5344, 52nfcxfr 2902 . . . . . . . . 9 Ⅎ𝑀𝑉
5451, 53elunif 43309 . . . . . . . 8 (𝑠 ∈ βˆͺ 𝑉 ↔ βˆƒπ‘€(𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉))
5550, 54sylibr 233 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝑠 ∈ βˆͺ 𝑉)
5655ex 414 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ 𝐷 β†’ 𝑠 ∈ βˆͺ 𝑉))
5756ssrdv 3951 . . . . 5 (πœ‘ β†’ 𝐷 βŠ† βˆͺ 𝑉)
58 cmpcld 22769 . . . . . . . 8 ((𝐽 ∈ Comp ∧ 𝐷 ∈ (Clsdβ€˜π½)) β†’ (𝐽 β†Ύt 𝐷) ∈ Comp)
597, 30, 58syl2anc 585 . . . . . . 7 (πœ‘ β†’ (𝐽 β†Ύt 𝐷) ∈ Comp)
607, 23syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐽 ∈ Top)
619cmpsub 22767 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐷 βŠ† 𝑇) β†’ ((𝐽 β†Ύt 𝐷) ∈ Comp ↔ βˆ€π‘˜ ∈ 𝒫 𝐽(𝐷 βŠ† βˆͺ π‘˜ β†’ βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒)))
6260, 32, 61syl2anc 585 . . . . . . 7 (πœ‘ β†’ ((𝐽 β†Ύt 𝐷) ∈ Comp ↔ βˆ€π‘˜ ∈ 𝒫 𝐽(𝐷 βŠ† βˆͺ π‘˜ β†’ βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒)))
6359, 62mpbid 231 . . . . . 6 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝒫 𝐽(𝐷 βŠ† βˆͺ π‘˜ β†’ βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒))
64 ssrab2 4038 . . . . . . . 8 {𝑀 ∈ 𝐽 ∣ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))} βŠ† 𝐽
6544, 64eqsstri 3979 . . . . . . 7 𝑉 βŠ† 𝐽
6644, 7rabexd 5291 . . . . . . . 8 (πœ‘ β†’ 𝑉 ∈ V)
67 elpwg 4564 . . . . . . . 8 (𝑉 ∈ V β†’ (𝑉 ∈ 𝒫 𝐽 ↔ 𝑉 βŠ† 𝐽))
6866, 67syl 17 . . . . . . 7 (πœ‘ β†’ (𝑉 ∈ 𝒫 𝐽 ↔ 𝑉 βŠ† 𝐽))
6965, 68mpbiri 258 . . . . . 6 (πœ‘ β†’ 𝑉 ∈ 𝒫 𝐽)
70 unieq 4877 . . . . . . . . 9 (π‘˜ = 𝑉 β†’ βˆͺ π‘˜ = βˆͺ 𝑉)
7170sseq2d 3977 . . . . . . . 8 (π‘˜ = 𝑉 β†’ (𝐷 βŠ† βˆͺ π‘˜ ↔ 𝐷 βŠ† βˆͺ 𝑉))
72 pweq 4575 . . . . . . . . . 10 (π‘˜ = 𝑉 β†’ 𝒫 π‘˜ = 𝒫 𝑉)
7372ineq1d 4172 . . . . . . . . 9 (π‘˜ = 𝑉 β†’ (𝒫 π‘˜ ∩ Fin) = (𝒫 𝑉 ∩ Fin))
7473rexeqdv 3313 . . . . . . . 8 (π‘˜ = 𝑉 β†’ (βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒 ↔ βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒))
7571, 74imbi12d 345 . . . . . . 7 (π‘˜ = 𝑉 β†’ ((𝐷 βŠ† βˆͺ π‘˜ β†’ βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒) ↔ (𝐷 βŠ† βˆͺ 𝑉 β†’ βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒)))
7675rspccva 3579 . . . . . 6 ((βˆ€π‘˜ ∈ 𝒫 𝐽(𝐷 βŠ† βˆͺ π‘˜ β†’ βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒) ∧ 𝑉 ∈ 𝒫 𝐽) β†’ (𝐷 βŠ† βˆͺ 𝑉 β†’ βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒))
7763, 69, 76syl2anc 585 . . . . 5 (πœ‘ β†’ (𝐷 βŠ† βˆͺ 𝑉 β†’ βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒))
7857, 77mpd 15 . . . 4 (πœ‘ β†’ βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒)
79 elinel1 4156 . . . . . . . . 9 (𝑒 ∈ (𝒫 𝑉 ∩ Fin) β†’ 𝑒 ∈ 𝒫 𝑉)
80 elpwi 4568 . . . . . . . . . . 11 (𝑒 ∈ 𝒫 𝑉 β†’ 𝑒 βŠ† 𝑉)
8180ssdifssd 4103 . . . . . . . . . 10 (𝑒 ∈ 𝒫 𝑉 β†’ (𝑒 βˆ– {βˆ…}) βŠ† 𝑉)
82 vex 3448 . . . . . . . . . . . 12 𝑒 ∈ V
83 difexg 5285 . . . . . . . . . . . 12 (𝑒 ∈ V β†’ (𝑒 βˆ– {βˆ…}) ∈ V)
8482, 83ax-mp 5 . . . . . . . . . . 11 (𝑒 βˆ– {βˆ…}) ∈ V
8584elpw 4565 . . . . . . . . . 10 ((𝑒 βˆ– {βˆ…}) ∈ 𝒫 𝑉 ↔ (𝑒 βˆ– {βˆ…}) βŠ† 𝑉)
8681, 85sylibr 233 . . . . . . . . 9 (𝑒 ∈ 𝒫 𝑉 β†’ (𝑒 βˆ– {βˆ…}) ∈ 𝒫 𝑉)
8779, 86syl 17 . . . . . . . 8 (𝑒 ∈ (𝒫 𝑉 ∩ Fin) β†’ (𝑒 βˆ– {βˆ…}) ∈ 𝒫 𝑉)
88 elinel2 4157 . . . . . . . . 9 (𝑒 ∈ (𝒫 𝑉 ∩ Fin) β†’ 𝑒 ∈ Fin)
89 diffi 9126 . . . . . . . . 9 (𝑒 ∈ Fin β†’ (𝑒 βˆ– {βˆ…}) ∈ Fin)
9088, 89syl 17 . . . . . . . 8 (𝑒 ∈ (𝒫 𝑉 ∩ Fin) β†’ (𝑒 βˆ– {βˆ…}) ∈ Fin)
9187, 90elind 4155 . . . . . . 7 (𝑒 ∈ (𝒫 𝑉 ∩ Fin) β†’ (𝑒 βˆ– {βˆ…}) ∈ (𝒫 𝑉 ∩ Fin))
92913ad2ant2 1135 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 βŠ† βˆͺ 𝑒) β†’ (𝑒 βˆ– {βˆ…}) ∈ (𝒫 𝑉 ∩ Fin))
93 unidif0 5316 . . . . . . . . 9 βˆͺ (𝑒 βˆ– {βˆ…}) = βˆͺ 𝑒
9493sseq2i 3974 . . . . . . . 8 (𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…}) ↔ 𝐷 βŠ† βˆͺ 𝑒)
9594biimpri 227 . . . . . . 7 (𝐷 βŠ† βˆͺ 𝑒 β†’ 𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…}))
96953ad2ant3 1136 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 βŠ† βˆͺ 𝑒) β†’ 𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…}))
97 eldifsni 4751 . . . . . . . 8 (𝑀 ∈ (𝑒 βˆ– {βˆ…}) β†’ 𝑀 β‰  βˆ…)
9897rgen 3063 . . . . . . 7 βˆ€π‘€ ∈ (𝑒 βˆ– {βˆ…})𝑀 β‰  βˆ…
9998a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 βŠ† βˆͺ 𝑒) β†’ βˆ€π‘€ ∈ (𝑒 βˆ– {βˆ…})𝑀 β‰  βˆ…)
100 unieq 4877 . . . . . . . . 9 (π‘Ÿ = (𝑒 βˆ– {βˆ…}) β†’ βˆͺ π‘Ÿ = βˆͺ (𝑒 βˆ– {βˆ…}))
101100sseq2d 3977 . . . . . . . 8 (π‘Ÿ = (𝑒 βˆ– {βˆ…}) β†’ (𝐷 βŠ† βˆͺ π‘Ÿ ↔ 𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…})))
102 raleq 3308 . . . . . . . 8 (π‘Ÿ = (𝑒 βˆ– {βˆ…}) β†’ (βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ… ↔ βˆ€π‘€ ∈ (𝑒 βˆ– {βˆ…})𝑀 β‰  βˆ…))
103101, 102anbi12d 632 . . . . . . 7 (π‘Ÿ = (𝑒 βˆ– {βˆ…}) β†’ ((𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…) ↔ (𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…}) ∧ βˆ€π‘€ ∈ (𝑒 βˆ– {βˆ…})𝑀 β‰  βˆ…)))
104103rspcev 3580 . . . . . 6 (((𝑒 βˆ– {βˆ…}) ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…}) ∧ βˆ€π‘€ ∈ (𝑒 βˆ– {βˆ…})𝑀 β‰  βˆ…)) β†’ βˆƒπ‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
10592, 96, 99, 104syl12anc 836 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 βŠ† βˆͺ 𝑒) β†’ βˆƒπ‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
106105rexlimdv3a 3153 . . . 4 (πœ‘ β†’ (βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒 β†’ βˆƒπ‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)))
10778, 106mpd 15 . . 3 (πœ‘ β†’ βˆƒπ‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
108 nfv 1918 . . . . . 6 β„²β„Žπœ‘
109 nfcv 2904 . . . . . . . . . . . 12 β„²β„Žβ„+
110 nfre1 3267 . . . . . . . . . . . 12 β„²β„Žβˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))
111109, 110nfralw 3293 . . . . . . . . . . 11 β„²β„Žβˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))
112 nfcv 2904 . . . . . . . . . . 11 β„²β„Žπ½
113111, 112nfrabw 3439 . . . . . . . . . 10 β„²β„Ž{𝑀 ∈ 𝐽 ∣ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))}
11444, 113nfcxfr 2902 . . . . . . . . 9 β„²β„Žπ‘‰
115114nfpw 4580 . . . . . . . 8 β„²β„Žπ’« 𝑉
116 nfcv 2904 . . . . . . . 8 β„²β„ŽFin
117115, 116nfin 4177 . . . . . . 7 β„²β„Ž(𝒫 𝑉 ∩ Fin)
118117nfcri 2891 . . . . . 6 β„²β„Ž π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)
119 nfv 1918 . . . . . 6 β„²β„Ž(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)
120108, 118, 119nf3an 1905 . . . . 5 β„²β„Ž(πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
121 nfcv 2904 . . . . . . . . . . . 12 Ⅎ𝑑ℝ+
122 nfcv 2904 . . . . . . . . . . . . 13 Ⅎ𝑑𝐴
123 nfra1 3266 . . . . . . . . . . . . . 14 β„²π‘‘βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)
124 nfra1 3266 . . . . . . . . . . . . . 14 β„²π‘‘βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒
125 nfra1 3266 . . . . . . . . . . . . . 14 β„²π‘‘βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘)
126123, 124, 125nf3an 1905 . . . . . . . . . . . . 13 Ⅎ𝑑(βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))
127122, 126nfrexw 3295 . . . . . . . . . . . 12 β„²π‘‘βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))
128121, 127nfralw 3293 . . . . . . . . . . 11 β„²π‘‘βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))
129 nfcv 2904 . . . . . . . . . . 11 Ⅎ𝑑𝐽
130128, 129nfrabw 3439 . . . . . . . . . 10 Ⅎ𝑑{𝑀 ∈ 𝐽 ∣ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))}
13144, 130nfcxfr 2902 . . . . . . . . 9 Ⅎ𝑑𝑉
132131nfpw 4580 . . . . . . . 8 Ⅎ𝑑𝒫 𝑉
133 nfcv 2904 . . . . . . . 8 Ⅎ𝑑Fin
134132, 133nfin 4177 . . . . . . 7 Ⅎ𝑑(𝒫 𝑉 ∩ Fin)
135134nfcri 2891 . . . . . 6 Ⅎ𝑑 π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)
136 nfcv 2904 . . . . . . . 8 Ⅎ𝑑βˆͺ π‘Ÿ
1373, 136nfss 3937 . . . . . . 7 Ⅎ𝑑 𝐷 βŠ† βˆͺ π‘Ÿ
138 nfv 1918 . . . . . . 7 β„²π‘‘βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…
139137, 138nfan 1903 . . . . . 6 Ⅎ𝑑(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)
1402, 135, 139nf3an 1905 . . . . 5 Ⅎ𝑑(πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
141 nfv 1918 . . . . . 6 β„²π‘€πœ‘
14253nfpw 4580 . . . . . . . 8 Ⅎ𝑀𝒫 𝑉
143 nfcv 2904 . . . . . . . 8 Ⅎ𝑀Fin
144142, 143nfin 4177 . . . . . . 7 Ⅎ𝑀(𝒫 𝑉 ∩ Fin)
145144nfcri 2891 . . . . . 6 Ⅎ𝑀 π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)
146 nfv 1918 . . . . . . 7 Ⅎ𝑀 𝐷 βŠ† βˆͺ π‘Ÿ
147 nfra1 3266 . . . . . . 7 β„²π‘€βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…
148146, 147nfan 1903 . . . . . 6 Ⅎ𝑀(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)
149141, 145, 148nf3an 1905 . . . . 5 Ⅎ𝑀(πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
150 stoweidlem57.4 . . . . 5 π‘Œ = {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}
151 simp2 1138 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin))
152 simp3l 1202 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝐷 βŠ† βˆͺ π‘Ÿ)
153 stoweidlem57.19 . . . . . 6 (πœ‘ β†’ 𝐷 β‰  βˆ…)
1541533ad2ant1 1134 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝐷 β‰  βˆ…)
155 stoweidlem57.20 . . . . . 6 (πœ‘ β†’ 𝐸 ∈ ℝ+)
1561553ad2ant1 1134 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝐸 ∈ ℝ+)
15726simpld 496 . . . . . 6 (πœ‘ β†’ 𝐡 βŠ† 𝑇)
1581573ad2ant1 1134 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝐡 βŠ† 𝑇)
159663ad2ant1 1134 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝑉 ∈ V)
160 retop 24141 . . . . . . . . 9 (topGenβ€˜ran (,)) ∈ Top
1616, 160eqeltri 2830 . . . . . . . 8 𝐾 ∈ Top
162 cnfex 43321 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) β†’ (𝐽 Cn 𝐾) ∈ V)
16360, 161, 162sylancl 587 . . . . . . 7 (πœ‘ β†’ (𝐽 Cn 𝐾) ∈ V)
16411, 10sseqtrdi 3995 . . . . . . 7 (πœ‘ β†’ 𝐴 βŠ† (𝐽 Cn 𝐾))
165163, 164ssexd 5282 . . . . . 6 (πœ‘ β†’ 𝐴 ∈ V)
1661653ad2ant1 1134 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝐴 ∈ V)
167120, 140, 149, 21, 150, 44, 151, 152, 154, 156, 158, 159, 166stoweidlem39 44366 . . . 4 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ βˆƒπ‘š ∈ β„• βˆƒπ‘£(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
168167rexlimdv3a 3153 . . 3 (πœ‘ β†’ (βˆƒπ‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…) β†’ βˆƒπ‘š ∈ β„• βˆƒπ‘£(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))))
169107, 168mpd 15 . 2 (πœ‘ β†’ βˆƒπ‘š ∈ β„• βˆƒπ‘£(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
170 nfv 1918 . . . . . . 7 Ⅎ𝑖(πœ‘ ∧ π‘š ∈ β„•)
171 nfv 1918 . . . . . . . 8 Ⅎ𝑖 𝑣:(1...π‘š)βŸΆπ‘‰
172 nfv 1918 . . . . . . . 8 Ⅎ𝑖 𝐷 βŠ† βˆͺ ran 𝑣
173 nfv 1918 . . . . . . . . . 10 Ⅎ𝑖 𝑦:(1...π‘š)βŸΆπ‘Œ
174 nfra1 3266 . . . . . . . . . 10 β„²π‘–βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))
175173, 174nfan 1903 . . . . . . . . 9 Ⅎ𝑖(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
176175nfex 2318 . . . . . . . 8 β„²π‘–βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
177171, 172, 176nf3an 1905 . . . . . . 7 Ⅎ𝑖(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
178170, 177nfan 1903 . . . . . 6 Ⅎ𝑖((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
179 nfv 1918 . . . . . . . 8 Ⅎ𝑑 π‘š ∈ β„•
1802, 179nfan 1903 . . . . . . 7 Ⅎ𝑑(πœ‘ ∧ π‘š ∈ β„•)
181 nfcv 2904 . . . . . . . . 9 Ⅎ𝑑𝑣
182 nfcv 2904 . . . . . . . . 9 Ⅎ𝑑(1...π‘š)
183181, 182, 131nff 6665 . . . . . . . 8 Ⅎ𝑑 𝑣:(1...π‘š)βŸΆπ‘‰
184 nfcv 2904 . . . . . . . . 9 Ⅎ𝑑βˆͺ ran 𝑣
1853, 184nfss 3937 . . . . . . . 8 Ⅎ𝑑 𝐷 βŠ† βˆͺ ran 𝑣
186 nfcv 2904 . . . . . . . . . . 11 Ⅎ𝑑𝑦
187123, 122nfrabw 3439 . . . . . . . . . . . 12 Ⅎ𝑑{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}
188150, 187nfcxfr 2902 . . . . . . . . . . 11 β„²π‘‘π‘Œ
189186, 182, 188nff 6665 . . . . . . . . . 10 Ⅎ𝑑 𝑦:(1...π‘š)βŸΆπ‘Œ
190 nfra1 3266 . . . . . . . . . . . 12 β„²π‘‘βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š)
191 nfra1 3266 . . . . . . . . . . . 12 β„²π‘‘βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)
192190, 191nfan 1903 . . . . . . . . . . 11 Ⅎ𝑑(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))
193182, 192nfralw 3293 . . . . . . . . . 10 β„²π‘‘βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))
194189, 193nfan 1903 . . . . . . . . 9 Ⅎ𝑑(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
195194nfex 2318 . . . . . . . 8 β„²π‘‘βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
196183, 185, 195nf3an 1905 . . . . . . 7 Ⅎ𝑑(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
197180, 196nfan 1903 . . . . . 6 Ⅎ𝑑((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
198 nfv 1918 . . . . . . 7 Ⅎ𝑦(πœ‘ ∧ π‘š ∈ β„•)
199 nfv 1918 . . . . . . . 8 Ⅎ𝑦 𝑣:(1...π‘š)βŸΆπ‘‰
200 nfv 1918 . . . . . . . 8 Ⅎ𝑦 𝐷 βŠ† βˆͺ ran 𝑣
201 nfe1 2148 . . . . . . . 8 β„²π‘¦βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
202199, 200, 201nf3an 1905 . . . . . . 7 Ⅎ𝑦(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
203198, 202nfan 1903 . . . . . 6 Ⅎ𝑦((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
204 nfv 1918 . . . . . . 7 Ⅎ𝑀(πœ‘ ∧ π‘š ∈ β„•)
205 nfcv 2904 . . . . . . . . 9 Ⅎ𝑀𝑣
206 nfcv 2904 . . . . . . . . 9 Ⅎ𝑀(1...π‘š)
207205, 206, 53nff 6665 . . . . . . . 8 Ⅎ𝑀 𝑣:(1...π‘š)βŸΆπ‘‰
208 nfv 1918 . . . . . . . 8 Ⅎ𝑀 𝐷 βŠ† βˆͺ ran 𝑣
209 nfv 1918 . . . . . . . 8 β„²π‘€βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
210207, 208, 209nf3an 1905 . . . . . . 7 Ⅎ𝑀(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
211204, 210nfan 1903 . . . . . 6 Ⅎ𝑀((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
212 eqid 2733 . . . . . 6 {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} = {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}
213 eqid 2733 . . . . . 6 (𝑓 ∈ {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}, 𝑔 ∈ {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ↦ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘)))) = (𝑓 ∈ {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}, 𝑔 ∈ {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ↦ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))))
214 eqid 2733 . . . . . 6 (𝑑 ∈ 𝑇 ↦ (𝑖 ∈ (1...π‘š) ↦ ((π‘¦β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝑖 ∈ (1...π‘š) ↦ ((π‘¦β€˜π‘–)β€˜π‘‘)))
215 eqid 2733 . . . . . 6 (𝑑 ∈ 𝑇 ↦ (seq1( Β· , ((𝑑 ∈ 𝑇 ↦ (𝑖 ∈ (1...π‘š) ↦ ((π‘¦β€˜π‘–)β€˜π‘‘)))β€˜π‘‘))β€˜π‘š)) = (𝑑 ∈ 𝑇 ↦ (seq1( Β· , ((𝑑 ∈ 𝑇 ↦ (𝑖 ∈ (1...π‘š) ↦ ((π‘¦β€˜π‘–)β€˜π‘‘)))β€˜π‘‘))β€˜π‘š))
216 simp1ll 1237 . . . . . . 7 ((((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ πœ‘)
217216, 15syld3an1 1411 . . . . . 6 ((((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
21811sselda 3945 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓 ∈ 𝐢)
2196, 9, 10, 218fcnre 43318 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
220219ad4ant14 751 . . . . . 6 ((((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
221 simplr 768 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ π‘š ∈ β„•)
222 simpr1 1195 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝑣:(1...π‘š)βŸΆπ‘‰)
2239cldss 22396 . . . . . . . 8 (𝐡 ∈ (Clsdβ€˜π½) β†’ 𝐡 βŠ† 𝑇)
22422, 223syl 17 . . . . . . 7 (πœ‘ β†’ 𝐡 βŠ† 𝑇)
225224ad2antrr 725 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝐡 βŠ† 𝑇)
226 simpr2 1196 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝐷 βŠ† βˆͺ ran 𝑣)
22732ad2antrr 725 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝐷 βŠ† 𝑇)
228 feq3 6652 . . . . . . . . . . . 12 (π‘Œ = {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} β†’ (𝑦:(1...π‘š)βŸΆπ‘Œ ↔ 𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}))
229150, 228ax-mp 5 . . . . . . . . . . 11 (𝑦:(1...π‘š)βŸΆπ‘Œ ↔ 𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)})
230229biimpi 215 . . . . . . . . . 10 (𝑦:(1...π‘š)βŸΆπ‘Œ β†’ 𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)})
231230anim1i 616 . . . . . . . . 9 ((𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))) β†’ (𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
232231eximi 1838 . . . . . . . 8 (βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))) β†’ βˆƒπ‘¦(𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
2332323ad2ant3 1136 . . . . . . 7 ((𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))) β†’ βˆƒπ‘¦(𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
234233adantl 483 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ βˆƒπ‘¦(𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
2357uniexd 7680 . . . . . . . 8 (πœ‘ β†’ βˆͺ 𝐽 ∈ V)
2369, 235eqeltrid 2838 . . . . . . 7 (πœ‘ β†’ 𝑇 ∈ V)
237236ad2antrr 725 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝑇 ∈ V)
238155ad2antrr 725 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝐸 ∈ ℝ+)
239 stoweidlem57.21 . . . . . . 7 (πœ‘ β†’ 𝐸 < (1 / 3))
240239ad2antrr 725 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝐸 < (1 / 3))
241178, 197, 203, 211, 9, 212, 213, 214, 215, 44, 217, 220, 221, 222, 225, 226, 227, 234, 237, 238, 240stoweidlem54 44381 . . . . 5 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝐷 (π‘₯β€˜π‘‘) < 𝐸 ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ 𝐸) < (π‘₯β€˜π‘‘)))
242241ex 414 . . . 4 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))) β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝐷 (π‘₯β€˜π‘‘) < 𝐸 ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ 𝐸) < (π‘₯β€˜π‘‘))))
243242exlimdv 1937 . . 3 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (βˆƒπ‘£(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))) β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝐷 (π‘₯β€˜π‘‘) < 𝐸 ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ 𝐸) < (π‘₯β€˜π‘‘))))
244243rexlimdva 3149 . 2 (πœ‘ β†’ (βˆƒπ‘š ∈ β„• βˆƒπ‘£(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))) β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝐷 (π‘₯β€˜π‘‘) < 𝐸 ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ 𝐸) < (π‘₯β€˜π‘‘))))
245169, 244mpd 15 1 (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝐷 (π‘₯β€˜π‘‘) < 𝐸 ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ 𝐸) < (π‘₯β€˜π‘‘)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782  β„²wnf 1786   ∈ wcel 2107  β„²wnfc 2884   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406  Vcvv 3444   βˆ– cdif 3908   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  π’« cpw 4561  {csn 4587  βˆͺ cuni 4866   class class class wbr 5106   ↦ cmpt 5189  ran crn 5635  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358   ∈ cmpo 7360  Fincfn 8886  β„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061   < clt 11194   ≀ cle 11195   βˆ’ cmin 11390   / cdiv 11817  β„•cn 12158  3c3 12214  β„+crp 12920  (,)cioo 13270  ...cfz 13430  seqcseq 13912   β†Ύt crest 17307  topGenctg 17324  Topctop 22258  Clsdccld 22383   Cn ccn 22591  Compccmp 22753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-seq 13913  df-exp 13974  df-hash 14237  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-clim 15376  df-rlim 15377  df-sum 15577  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-mulg 18878  df-cntz 19102  df-cmn 19569  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-cn 22594  df-cnp 22595  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-xms 23689  df-ms 23690  df-tms 23691
This theorem is referenced by:  stoweidlem58  44385
  Copyright terms: Public domain W3C validator