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 45368
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 2885 . . . . . . . . . . 11 Ⅎ𝑑 𝑠 ∈ 𝐷
52, 4nfan 1895 . . . . . . . . . 10 Ⅎ𝑑(πœ‘ ∧ 𝑠 ∈ 𝐷)
6 stoweidlem57.6 . . . . . . . . . 10 𝐾 = (topGenβ€˜ran (,))
7 stoweidlem57.10 . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 ∈ Comp)
87adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝐽 ∈ Comp)
9 stoweidlem57.7 . . . . . . . . . 10 𝑇 = βˆͺ 𝐽
10 stoweidlem57.8 . . . . . . . . . 10 𝐢 = (𝐽 Cn 𝐾)
11 stoweidlem57.11 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 βŠ† 𝐢)
1211adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝐴 βŠ† 𝐢)
13 stoweidlem57.12 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
14133adant1r 1175 . . . . . . . . . 10 (((πœ‘ ∧ 𝑠 ∈ 𝐷) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
15 stoweidlem57.13 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
16153adant1r 1175 . . . . . . . . . 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 23286 . . . . . . . . . . . . . . 15 (𝐽 ∈ Comp β†’ 𝐽 ∈ Top)
249iscld 22918 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top β†’ (𝐡 ∈ (Clsdβ€˜π½) ↔ (𝐡 βŠ† 𝑇 ∧ (𝑇 βˆ– 𝐡) ∈ 𝐽)))
257, 23, 243syl 18 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐡 ∈ (Clsdβ€˜π½) ↔ (𝐡 βŠ† 𝑇 ∧ (𝑇 βˆ– 𝐡) ∈ 𝐽)))
2622, 25mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐡 βŠ† 𝑇 ∧ (𝑇 βˆ– 𝐡) ∈ 𝐽))
2726simprd 495 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑇 βˆ– 𝐡) ∈ 𝐽)
2821, 27eqeltrid 2832 . . . . . . . . . . 11 (πœ‘ β†’ π‘ˆ ∈ 𝐽)
2928adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ π‘ˆ ∈ 𝐽)
30 stoweidlem57.17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 ∈ (Clsdβ€˜π½))
319cldss 22920 . . . . . . . . . . . . . 14 (𝐷 ∈ (Clsdβ€˜π½) β†’ 𝐷 βŠ† 𝑇)
3230, 31syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 βŠ† 𝑇)
3332sselda 3978 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝑠 ∈ 𝑇)
34 stoweidlem57.18 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐡 ∩ 𝐷) = βˆ…)
35 disjr 4445 . . . . . . . . . . . . . 14 ((𝐡 ∩ 𝐷) = βˆ… ↔ βˆ€π‘  ∈ 𝐷 Β¬ 𝑠 ∈ 𝐡)
3634, 35sylib 217 . . . . . . . . . . . . 13 (πœ‘ β†’ βˆ€π‘  ∈ 𝐷 Β¬ 𝑠 ∈ 𝐡)
3736r19.21bi 3243 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ Β¬ 𝑠 ∈ 𝐡)
3833, 37eldifd 3955 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝑠 ∈ (𝑇 βˆ– 𝐡))
3938, 21eleqtrrdi 2839 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝑠 ∈ π‘ˆ)
401, 5, 6, 8, 9, 10, 12, 14, 16, 18, 20, 29, 39stoweidlem56 45367 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ βˆƒπ‘€ ∈ 𝐽 ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))))
41 simpl 482 . . . . . . . . . . 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 3449 . . . . . . . . . . . 12 (𝑀 ∈ 𝑉 ↔ (𝑀 ∈ 𝐽 ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))))
4641, 43, 45sylanbrc 582 . . . . . . . . . . 11 ((𝑀 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘)))) β†’ 𝑀 ∈ 𝑉)
4741, 42, 46jca32 515 . . . . . . . . . 10 ((𝑀 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘)))) β†’ (𝑀 ∈ 𝐽 ∧ (𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉)))
4847reximi2 3074 . . . . . . . . 9 (βˆƒπ‘€ ∈ 𝐽 ((𝑠 ∈ 𝑀 ∧ 𝑀 βŠ† π‘ˆ) ∧ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))) β†’ βˆƒπ‘€ ∈ 𝐽 (𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉))
49 rexex 3071 . . . . . . . . 9 (βˆƒπ‘€ ∈ 𝐽 (𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉) β†’ βˆƒπ‘€(𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉))
5040, 48, 493syl 18 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ βˆƒπ‘€(𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉))
51 nfcv 2898 . . . . . . . . 9 Ⅎ𝑀𝑠
52 nfrab1 3446 . . . . . . . . . 10 Ⅎ𝑀{𝑀 ∈ 𝐽 ∣ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))}
5344, 52nfcxfr 2896 . . . . . . . . 9 Ⅎ𝑀𝑉
5451, 53elunif 44301 . . . . . . . 8 (𝑠 ∈ βˆͺ 𝑉 ↔ βˆƒπ‘€(𝑠 ∈ 𝑀 ∧ 𝑀 ∈ 𝑉))
5550, 54sylibr 233 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ 𝐷) β†’ 𝑠 ∈ βˆͺ 𝑉)
5655ex 412 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ 𝐷 β†’ 𝑠 ∈ βˆͺ 𝑉))
5756ssrdv 3984 . . . . 5 (πœ‘ β†’ 𝐷 βŠ† βˆͺ 𝑉)
58 cmpcld 23293 . . . . . . . 8 ((𝐽 ∈ Comp ∧ 𝐷 ∈ (Clsdβ€˜π½)) β†’ (𝐽 β†Ύt 𝐷) ∈ Comp)
597, 30, 58syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐽 β†Ύt 𝐷) ∈ Comp)
607, 23syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐽 ∈ Top)
619cmpsub 23291 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐷 βŠ† 𝑇) β†’ ((𝐽 β†Ύt 𝐷) ∈ Comp ↔ βˆ€π‘˜ ∈ 𝒫 𝐽(𝐷 βŠ† βˆͺ π‘˜ β†’ βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒)))
6260, 32, 61syl2anc 583 . . . . . . 7 (πœ‘ β†’ ((𝐽 β†Ύt 𝐷) ∈ Comp ↔ βˆ€π‘˜ ∈ 𝒫 𝐽(𝐷 βŠ† βˆͺ π‘˜ β†’ βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒)))
6359, 62mpbid 231 . . . . . 6 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝒫 𝐽(𝐷 βŠ† βˆͺ π‘˜ β†’ βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒))
64 ssrab2 4073 . . . . . . . 8 {𝑀 ∈ 𝐽 ∣ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))} βŠ† 𝐽
6544, 64eqsstri 4012 . . . . . . 7 𝑉 βŠ† 𝐽
6644, 7rabexd 5329 . . . . . . . 8 (πœ‘ β†’ 𝑉 ∈ V)
67 elpwg 4601 . . . . . . . 8 (𝑉 ∈ V β†’ (𝑉 ∈ 𝒫 𝐽 ↔ 𝑉 βŠ† 𝐽))
6866, 67syl 17 . . . . . . 7 (πœ‘ β†’ (𝑉 ∈ 𝒫 𝐽 ↔ 𝑉 βŠ† 𝐽))
6965, 68mpbiri 258 . . . . . 6 (πœ‘ β†’ 𝑉 ∈ 𝒫 𝐽)
70 unieq 4914 . . . . . . . . 9 (π‘˜ = 𝑉 β†’ βˆͺ π‘˜ = βˆͺ 𝑉)
7170sseq2d 4010 . . . . . . . 8 (π‘˜ = 𝑉 β†’ (𝐷 βŠ† βˆͺ π‘˜ ↔ 𝐷 βŠ† βˆͺ 𝑉))
72 pweq 4612 . . . . . . . . . 10 (π‘˜ = 𝑉 β†’ 𝒫 π‘˜ = 𝒫 𝑉)
7372ineq1d 4207 . . . . . . . . 9 (π‘˜ = 𝑉 β†’ (𝒫 π‘˜ ∩ Fin) = (𝒫 𝑉 ∩ Fin))
7473rexeqdv 3321 . . . . . . . 8 (π‘˜ = 𝑉 β†’ (βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒 ↔ βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒))
7571, 74imbi12d 344 . . . . . . 7 (π‘˜ = 𝑉 β†’ ((𝐷 βŠ† βˆͺ π‘˜ β†’ βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒) ↔ (𝐷 βŠ† βˆͺ 𝑉 β†’ βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒)))
7675rspccva 3606 . . . . . 6 ((βˆ€π‘˜ ∈ 𝒫 𝐽(𝐷 βŠ† βˆͺ π‘˜ β†’ βˆƒπ‘’ ∈ (𝒫 π‘˜ ∩ Fin)𝐷 βŠ† βˆͺ 𝑒) ∧ 𝑉 ∈ 𝒫 𝐽) β†’ (𝐷 βŠ† βˆͺ 𝑉 β†’ βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒))
7763, 69, 76syl2anc 583 . . . . 5 (πœ‘ β†’ (𝐷 βŠ† βˆͺ 𝑉 β†’ βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒))
7857, 77mpd 15 . . . 4 (πœ‘ β†’ βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒)
79 elinel1 4191 . . . . . . . . 9 (𝑒 ∈ (𝒫 𝑉 ∩ Fin) β†’ 𝑒 ∈ 𝒫 𝑉)
80 elpwi 4605 . . . . . . . . . . 11 (𝑒 ∈ 𝒫 𝑉 β†’ 𝑒 βŠ† 𝑉)
8180ssdifssd 4138 . . . . . . . . . 10 (𝑒 ∈ 𝒫 𝑉 β†’ (𝑒 βˆ– {βˆ…}) βŠ† 𝑉)
82 vex 3473 . . . . . . . . . . . 12 𝑒 ∈ V
83 difexg 5323 . . . . . . . . . . . 12 (𝑒 ∈ V β†’ (𝑒 βˆ– {βˆ…}) ∈ V)
8482, 83ax-mp 5 . . . . . . . . . . 11 (𝑒 βˆ– {βˆ…}) ∈ V
8584elpw 4602 . . . . . . . . . 10 ((𝑒 βˆ– {βˆ…}) ∈ 𝒫 𝑉 ↔ (𝑒 βˆ– {βˆ…}) βŠ† 𝑉)
8681, 85sylibr 233 . . . . . . . . 9 (𝑒 ∈ 𝒫 𝑉 β†’ (𝑒 βˆ– {βˆ…}) ∈ 𝒫 𝑉)
8779, 86syl 17 . . . . . . . 8 (𝑒 ∈ (𝒫 𝑉 ∩ Fin) β†’ (𝑒 βˆ– {βˆ…}) ∈ 𝒫 𝑉)
88 elinel2 4192 . . . . . . . . 9 (𝑒 ∈ (𝒫 𝑉 ∩ Fin) β†’ 𝑒 ∈ Fin)
89 diffi 9195 . . . . . . . . 9 (𝑒 ∈ Fin β†’ (𝑒 βˆ– {βˆ…}) ∈ Fin)
9088, 89syl 17 . . . . . . . 8 (𝑒 ∈ (𝒫 𝑉 ∩ Fin) β†’ (𝑒 βˆ– {βˆ…}) ∈ Fin)
9187, 90elind 4190 . . . . . . 7 (𝑒 ∈ (𝒫 𝑉 ∩ Fin) β†’ (𝑒 βˆ– {βˆ…}) ∈ (𝒫 𝑉 ∩ Fin))
92913ad2ant2 1132 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 βŠ† βˆͺ 𝑒) β†’ (𝑒 βˆ– {βˆ…}) ∈ (𝒫 𝑉 ∩ Fin))
93 unidif0 5354 . . . . . . . . 9 βˆͺ (𝑒 βˆ– {βˆ…}) = βˆͺ 𝑒
9493sseq2i 4007 . . . . . . . 8 (𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…}) ↔ 𝐷 βŠ† βˆͺ 𝑒)
9594biimpri 227 . . . . . . 7 (𝐷 βŠ† βˆͺ 𝑒 β†’ 𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…}))
96953ad2ant3 1133 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 βŠ† βˆͺ 𝑒) β†’ 𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…}))
97 eldifsni 4789 . . . . . . . 8 (𝑀 ∈ (𝑒 βˆ– {βˆ…}) β†’ 𝑀 β‰  βˆ…)
9897rgen 3058 . . . . . . 7 βˆ€π‘€ ∈ (𝑒 βˆ– {βˆ…})𝑀 β‰  βˆ…
9998a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 βŠ† βˆͺ 𝑒) β†’ βˆ€π‘€ ∈ (𝑒 βˆ– {βˆ…})𝑀 β‰  βˆ…)
100 unieq 4914 . . . . . . . . 9 (π‘Ÿ = (𝑒 βˆ– {βˆ…}) β†’ βˆͺ π‘Ÿ = βˆͺ (𝑒 βˆ– {βˆ…}))
101100sseq2d 4010 . . . . . . . 8 (π‘Ÿ = (𝑒 βˆ– {βˆ…}) β†’ (𝐷 βŠ† βˆͺ π‘Ÿ ↔ 𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…})))
102 raleq 3317 . . . . . . . 8 (π‘Ÿ = (𝑒 βˆ– {βˆ…}) β†’ (βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ… ↔ βˆ€π‘€ ∈ (𝑒 βˆ– {βˆ…})𝑀 β‰  βˆ…))
103101, 102anbi12d 630 . . . . . . 7 (π‘Ÿ = (𝑒 βˆ– {βˆ…}) β†’ ((𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…) ↔ (𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…}) ∧ βˆ€π‘€ ∈ (𝑒 βˆ– {βˆ…})𝑀 β‰  βˆ…)))
104103rspcev 3607 . . . . . 6 (((𝑒 βˆ– {βˆ…}) ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ (𝑒 βˆ– {βˆ…}) ∧ βˆ€π‘€ ∈ (𝑒 βˆ– {βˆ…})𝑀 β‰  βˆ…)) β†’ βˆƒπ‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
10592, 96, 99, 104syl12anc 836 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 βŠ† βˆͺ 𝑒) β†’ βˆƒπ‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
106105rexlimdv3a 3154 . . . 4 (πœ‘ β†’ (βˆƒπ‘’ ∈ (𝒫 𝑉 ∩ Fin)𝐷 βŠ† βˆͺ 𝑒 β†’ βˆƒπ‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)))
10778, 106mpd 15 . . 3 (πœ‘ β†’ βˆƒπ‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
108 nfv 1910 . . . . . 6 β„²β„Žπœ‘
109 nfcv 2898 . . . . . . . . . . . 12 β„²β„Žβ„+
110 nfre1 3277 . . . . . . . . . . . 12 β„²β„Žβˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))
111109, 110nfralw 3303 . . . . . . . . . . 11 β„²β„Žβˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))
112 nfcv 2898 . . . . . . . . . . 11 β„²β„Žπ½
113111, 112nfrabw 3463 . . . . . . . . . 10 β„²β„Ž{𝑀 ∈ 𝐽 ∣ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))}
11444, 113nfcxfr 2896 . . . . . . . . 9 β„²β„Žπ‘‰
115114nfpw 4617 . . . . . . . 8 β„²β„Žπ’« 𝑉
116 nfcv 2898 . . . . . . . 8 β„²β„ŽFin
117115, 116nfin 4212 . . . . . . 7 β„²β„Ž(𝒫 𝑉 ∩ Fin)
118117nfcri 2885 . . . . . 6 β„²β„Ž π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)
119 nfv 1910 . . . . . 6 β„²β„Ž(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)
120108, 118, 119nf3an 1897 . . . . 5 β„²β„Ž(πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
121 nfcv 2898 . . . . . . . . . . . 12 Ⅎ𝑑ℝ+
122 nfcv 2898 . . . . . . . . . . . . 13 Ⅎ𝑑𝐴
123 nfra1 3276 . . . . . . . . . . . . . 14 β„²π‘‘βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)
124 nfra1 3276 . . . . . . . . . . . . . 14 β„²π‘‘βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒
125 nfra1 3276 . . . . . . . . . . . . . 14 β„²π‘‘βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘)
126123, 124, 125nf3an 1897 . . . . . . . . . . . . 13 Ⅎ𝑑(βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))
127122, 126nfrexw 3305 . . . . . . . . . . . 12 β„²π‘‘βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))
128121, 127nfralw 3303 . . . . . . . . . . 11 β„²π‘‘βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))
129 nfcv 2898 . . . . . . . . . . 11 Ⅎ𝑑𝐽
130128, 129nfrabw 3463 . . . . . . . . . 10 Ⅎ𝑑{𝑀 ∈ 𝐽 ∣ βˆ€π‘’ ∈ ℝ+ βˆƒβ„Ž ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝑀 (β„Žβ€˜π‘‘) < 𝑒 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)(1 βˆ’ 𝑒) < (β„Žβ€˜π‘‘))}
13144, 130nfcxfr 2896 . . . . . . . . 9 Ⅎ𝑑𝑉
132131nfpw 4617 . . . . . . . 8 Ⅎ𝑑𝒫 𝑉
133 nfcv 2898 . . . . . . . 8 Ⅎ𝑑Fin
134132, 133nfin 4212 . . . . . . 7 Ⅎ𝑑(𝒫 𝑉 ∩ Fin)
135134nfcri 2885 . . . . . 6 Ⅎ𝑑 π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)
136 nfcv 2898 . . . . . . . 8 Ⅎ𝑑βˆͺ π‘Ÿ
1373, 136nfss 3970 . . . . . . 7 Ⅎ𝑑 𝐷 βŠ† βˆͺ π‘Ÿ
138 nfv 1910 . . . . . . 7 β„²π‘‘βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…
139137, 138nfan 1895 . . . . . 6 Ⅎ𝑑(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)
1402, 135, 139nf3an 1897 . . . . 5 Ⅎ𝑑(πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
141 nfv 1910 . . . . . 6 β„²π‘€πœ‘
14253nfpw 4617 . . . . . . . 8 Ⅎ𝑀𝒫 𝑉
143 nfcv 2898 . . . . . . . 8 Ⅎ𝑀Fin
144142, 143nfin 4212 . . . . . . 7 Ⅎ𝑀(𝒫 𝑉 ∩ Fin)
145144nfcri 2885 . . . . . 6 Ⅎ𝑀 π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)
146 nfv 1910 . . . . . . 7 Ⅎ𝑀 𝐷 βŠ† βˆͺ π‘Ÿ
147 nfra1 3276 . . . . . . 7 β„²π‘€βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…
148146, 147nfan 1895 . . . . . 6 Ⅎ𝑀(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)
149141, 145, 148nf3an 1897 . . . . 5 Ⅎ𝑀(πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…))
150 stoweidlem57.4 . . . . 5 π‘Œ = {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}
151 simp2 1135 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin))
152 simp3l 1199 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝐷 βŠ† βˆͺ π‘Ÿ)
153 stoweidlem57.19 . . . . . 6 (πœ‘ β†’ 𝐷 β‰  βˆ…)
1541533ad2ant1 1131 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝐷 β‰  βˆ…)
155 stoweidlem57.20 . . . . . 6 (πœ‘ β†’ 𝐸 ∈ ℝ+)
1561553ad2ant1 1131 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝐸 ∈ ℝ+)
15726simpld 494 . . . . . 6 (πœ‘ β†’ 𝐡 βŠ† 𝑇)
1581573ad2ant1 1131 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝐡 βŠ† 𝑇)
159663ad2ant1 1131 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝑉 ∈ V)
160 retop 24665 . . . . . . . . 9 (topGenβ€˜ran (,)) ∈ Top
1616, 160eqeltri 2824 . . . . . . . 8 𝐾 ∈ Top
162 cnfex 44313 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) β†’ (𝐽 Cn 𝐾) ∈ V)
16360, 161, 162sylancl 585 . . . . . . 7 (πœ‘ β†’ (𝐽 Cn 𝐾) ∈ V)
16411, 10sseqtrdi 4028 . . . . . . 7 (πœ‘ β†’ 𝐴 βŠ† (𝐽 Cn 𝐾))
165163, 164ssexd 5318 . . . . . 6 (πœ‘ β†’ 𝐴 ∈ V)
1661653ad2ant1 1131 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ 𝐴 ∈ V)
167120, 140, 149, 21, 150, 44, 151, 152, 154, 156, 158, 159, 166stoweidlem39 45350 . . . 4 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…)) β†’ βˆƒπ‘š ∈ β„• βˆƒπ‘£(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
168167rexlimdv3a 3154 . . 3 (πœ‘ β†’ (βˆƒπ‘Ÿ ∈ (𝒫 𝑉 ∩ Fin)(𝐷 βŠ† βˆͺ π‘Ÿ ∧ βˆ€π‘€ ∈ π‘Ÿ 𝑀 β‰  βˆ…) β†’ βˆƒπ‘š ∈ β„• βˆƒπ‘£(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))))
169107, 168mpd 15 . 2 (πœ‘ β†’ βˆƒπ‘š ∈ β„• βˆƒπ‘£(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
170 nfv 1910 . . . . . . 7 Ⅎ𝑖(πœ‘ ∧ π‘š ∈ β„•)
171 nfv 1910 . . . . . . . 8 Ⅎ𝑖 𝑣:(1...π‘š)βŸΆπ‘‰
172 nfv 1910 . . . . . . . 8 Ⅎ𝑖 𝐷 βŠ† βˆͺ ran 𝑣
173 nfv 1910 . . . . . . . . . 10 Ⅎ𝑖 𝑦:(1...π‘š)βŸΆπ‘Œ
174 nfra1 3276 . . . . . . . . . 10 β„²π‘–βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))
175173, 174nfan 1895 . . . . . . . . 9 Ⅎ𝑖(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
176175nfex 2312 . . . . . . . 8 β„²π‘–βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
177171, 172, 176nf3an 1897 . . . . . . 7 Ⅎ𝑖(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
178170, 177nfan 1895 . . . . . 6 Ⅎ𝑖((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
179 nfv 1910 . . . . . . . 8 Ⅎ𝑑 π‘š ∈ β„•
1802, 179nfan 1895 . . . . . . 7 Ⅎ𝑑(πœ‘ ∧ π‘š ∈ β„•)
181 nfcv 2898 . . . . . . . . 9 Ⅎ𝑑𝑣
182 nfcv 2898 . . . . . . . . 9 Ⅎ𝑑(1...π‘š)
183181, 182, 131nff 6712 . . . . . . . 8 Ⅎ𝑑 𝑣:(1...π‘š)βŸΆπ‘‰
184 nfcv 2898 . . . . . . . . 9 Ⅎ𝑑βˆͺ ran 𝑣
1853, 184nfss 3970 . . . . . . . 8 Ⅎ𝑑 𝐷 βŠ† βˆͺ ran 𝑣
186 nfcv 2898 . . . . . . . . . . 11 Ⅎ𝑑𝑦
187123, 122nfrabw 3463 . . . . . . . . . . . 12 Ⅎ𝑑{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}
188150, 187nfcxfr 2896 . . . . . . . . . . 11 β„²π‘‘π‘Œ
189186, 182, 188nff 6712 . . . . . . . . . 10 Ⅎ𝑑 𝑦:(1...π‘š)βŸΆπ‘Œ
190 nfra1 3276 . . . . . . . . . . . 12 β„²π‘‘βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š)
191 nfra1 3276 . . . . . . . . . . . 12 β„²π‘‘βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)
192190, 191nfan 1895 . . . . . . . . . . 11 Ⅎ𝑑(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))
193182, 192nfralw 3303 . . . . . . . . . 10 β„²π‘‘βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))
194189, 193nfan 1895 . . . . . . . . 9 Ⅎ𝑑(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
195194nfex 2312 . . . . . . . 8 β„²π‘‘βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
196183, 185, 195nf3an 1897 . . . . . . 7 Ⅎ𝑑(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
197180, 196nfan 1895 . . . . . 6 Ⅎ𝑑((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
198 nfv 1910 . . . . . . 7 Ⅎ𝑦(πœ‘ ∧ π‘š ∈ β„•)
199 nfv 1910 . . . . . . . 8 Ⅎ𝑦 𝑣:(1...π‘š)βŸΆπ‘‰
200 nfv 1910 . . . . . . . 8 Ⅎ𝑦 𝐷 βŠ† βˆͺ ran 𝑣
201 nfe1 2140 . . . . . . . 8 β„²π‘¦βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
202199, 200, 201nf3an 1897 . . . . . . 7 Ⅎ𝑦(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
203198, 202nfan 1895 . . . . . 6 Ⅎ𝑦((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
204 nfv 1910 . . . . . . 7 Ⅎ𝑀(πœ‘ ∧ π‘š ∈ β„•)
205 nfcv 2898 . . . . . . . . 9 Ⅎ𝑀𝑣
206 nfcv 2898 . . . . . . . . 9 Ⅎ𝑀(1...π‘š)
207205, 206, 53nff 6712 . . . . . . . 8 Ⅎ𝑀 𝑣:(1...π‘š)βŸΆπ‘‰
208 nfv 1910 . . . . . . . 8 Ⅎ𝑀 𝐷 βŠ† βˆͺ ran 𝑣
209 nfv 1910 . . . . . . . 8 β„²π‘€βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))
210207, 208, 209nf3an 1897 . . . . . . 7 Ⅎ𝑀(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
211204, 210nfan 1895 . . . . . 6 Ⅎ𝑀((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))))
212 eqid 2727 . . . . . 6 {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} = {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}
213 eqid 2727 . . . . . 6 (𝑓 ∈ {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}, 𝑔 ∈ {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ↦ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘)))) = (𝑓 ∈ {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}, 𝑔 ∈ {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ↦ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))))
214 eqid 2727 . . . . . 6 (𝑑 ∈ 𝑇 ↦ (𝑖 ∈ (1...π‘š) ↦ ((π‘¦β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝑖 ∈ (1...π‘š) ↦ ((π‘¦β€˜π‘–)β€˜π‘‘)))
215 eqid 2727 . . . . . 6 (𝑑 ∈ 𝑇 ↦ (seq1( Β· , ((𝑑 ∈ 𝑇 ↦ (𝑖 ∈ (1...π‘š) ↦ ((π‘¦β€˜π‘–)β€˜π‘‘)))β€˜π‘‘))β€˜π‘š)) = (𝑑 ∈ 𝑇 ↦ (seq1( Β· , ((𝑑 ∈ 𝑇 ↦ (𝑖 ∈ (1...π‘š) ↦ ((π‘¦β€˜π‘–)β€˜π‘‘)))β€˜π‘‘))β€˜π‘š))
216 simp1ll 1234 . . . . . . 7 ((((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ πœ‘)
217216, 15syld3an1 1408 . . . . . 6 ((((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
21811sselda 3978 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓 ∈ 𝐢)
2196, 9, 10, 218fcnre 44310 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
220219ad4ant14 751 . . . . . 6 ((((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
221 simplr 768 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ π‘š ∈ β„•)
222 simpr1 1192 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝑣:(1...π‘š)βŸΆπ‘‰)
2239cldss 22920 . . . . . . . 8 (𝐡 ∈ (Clsdβ€˜π½) β†’ 𝐡 βŠ† 𝑇)
22422, 223syl 17 . . . . . . 7 (πœ‘ β†’ 𝐡 βŠ† 𝑇)
225224ad2antrr 725 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝐡 βŠ† 𝑇)
226 simpr2 1193 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝐷 βŠ† βˆͺ ran 𝑣)
22732ad2antrr 725 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ 𝐷 βŠ† 𝑇)
228 feq3 6699 . . . . . . . . . . . 12 (π‘Œ = {β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} β†’ (𝑦:(1...π‘š)βŸΆπ‘Œ ↔ 𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)}))
229150, 228ax-mp 5 . . . . . . . . . . 11 (𝑦:(1...π‘š)βŸΆπ‘Œ ↔ 𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)})
230229biimpi 215 . . . . . . . . . 10 (𝑦:(1...π‘š)βŸΆπ‘Œ β†’ 𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)})
231230anim1i 614 . . . . . . . . 9 ((𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))) β†’ (𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
232231eximi 1830 . . . . . . . 8 (βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))) β†’ βˆƒπ‘¦(𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
2332323ad2ant3 1133 . . . . . . 7 ((𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))) β†’ βˆƒπ‘¦(𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
234233adantl 481 . . . . . 6 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ βˆƒπ‘¦(𝑦:(1...π‘š)⟢{β„Ž ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1)} ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))
2357uniexd 7741 . . . . . . . 8 (πœ‘ β†’ βˆͺ 𝐽 ∈ V)
2369, 235eqeltrid 2832 . . . . . . 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 45365 . . . . 5 (((πœ‘ ∧ π‘š ∈ β„•) ∧ (𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘))))) β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝐷 (π‘₯β€˜π‘‘) < 𝐸 ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ 𝐸) < (π‘₯β€˜π‘‘)))
242241ex 412 . . . 4 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))) β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝐷 (π‘₯β€˜π‘‘) < 𝐸 ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ 𝐸) < (π‘₯β€˜π‘‘))))
243242exlimdv 1929 . . 3 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (βˆƒπ‘£(𝑣:(1...π‘š)βŸΆπ‘‰ ∧ 𝐷 βŠ† βˆͺ ran 𝑣 ∧ βˆƒπ‘¦(𝑦:(1...π‘š)βŸΆπ‘Œ ∧ βˆ€π‘– ∈ (1...π‘š)(βˆ€π‘‘ ∈ (π‘£β€˜π‘–)((π‘¦β€˜π‘–)β€˜π‘‘) < (𝐸 / π‘š) ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ (𝐸 / π‘š)) < ((π‘¦β€˜π‘–)β€˜π‘‘)))) β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ 𝐷 (π‘₯β€˜π‘‘) < 𝐸 ∧ βˆ€π‘‘ ∈ 𝐡 (1 βˆ’ 𝐸) < (π‘₯β€˜π‘‘))))
244243rexlimdva 3150 . 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 395   ∧ w3a 1085   = wceq 1534  βˆƒwex 1774  β„²wnf 1778   ∈ wcel 2099  β„²wnfc 2878   β‰  wne 2935  βˆ€wral 3056  βˆƒwrex 3065  {crab 3427  Vcvv 3469   βˆ– cdif 3941   ∩ cin 3943   βŠ† wss 3944  βˆ…c0 4318  π’« cpw 4598  {csn 4624  βˆͺ cuni 4903   class class class wbr 5142   ↦ cmpt 5225  ran crn 5673  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414   ∈ cmpo 7416  Fincfn 8955  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   Β· cmul 11135   < clt 11270   ≀ cle 11271   βˆ’ cmin 11466   / cdiv 11893  β„•cn 12234  3c3 12290  β„+crp 12998  (,)cioo 13348  ...cfz 13508  seqcseq 13990   β†Ύt crest 17393  topGenctg 17410  Topctop 22782  Clsdccld 22907   Cn ccn 23115  Compccmp 23277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13352  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-fl 13781  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-clim 15456  df-rlim 15457  df-sum 15657  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-rest 17395  df-topn 17396  df-0g 17414  df-gsum 17415  df-topgen 17416  df-pt 17417  df-prds 17420  df-xrs 17475  df-qtop 17480  df-imas 17481  df-xps 17483  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-submnd 18732  df-mulg 19015  df-cntz 19259  df-cmn 19728  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-cnfld 21267  df-top 22783  df-topon 22800  df-topsp 22822  df-bases 22836  df-cld 22910  df-cn 23118  df-cnp 23119  df-cmp 23278  df-tx 23453  df-hmeo 23646  df-xms 24213  df-ms 24214  df-tms 24215
This theorem is referenced by:  stoweidlem58  45369
  Copyright terms: Public domain W3C validator