Theorem stoweidlem39 40755

Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that 𝑟 is a finite subset of 𝑊, 𝑥 indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ x_i ≤ 1, x_i < ε / m on V(t_i), and x_i > 1 - ε / m on 𝐵. Here 𝐷 is used to represent A in the paper's Lemma 2 (because 𝐴 is used for the subalgebra), 𝑀 is used to represent m in the paper, 𝐸 is used to represent ε, and v_i is used to represent V(t_i). 𝑊 is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Hypotheses

Ref	Expression
stoweidlem39.1	⊢ Ⅎℎ𝜑
stoweidlem39.2	⊢ Ⅎ𝑡𝜑
stoweidlem39.3	⊢ Ⅎ𝑤𝜑
stoweidlem39.4	⊢ 𝑈 = (𝑇 ∖ 𝐵)
stoweidlem39.5	⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}
stoweidlem39.6	⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}
stoweidlem39.7	⊢ (𝜑 → 𝑟 ∈ (𝒫 𝑊 ∩ Fin))
stoweidlem39.8	⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑟)
stoweidlem39.9	⊢ (𝜑 → 𝐷 ≠ ∅)
stoweidlem39.10	⊢ (𝜑 → 𝐸 ∈ ℝ+)
stoweidlem39.11	⊢ (𝜑 → 𝐵 ⊆ 𝑇)
stoweidlem39.12	⊢ (𝜑 → 𝑊 ∈ V)
stoweidlem39.13	⊢ (𝜑 → 𝐴 ∈ V)

Assertion

Ref	Expression
stoweidlem39	⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))

Distinct variable groups:   𝑒,ℎ,𝑚,𝑡,𝑤   𝐴,𝑒,ℎ,𝑡,𝑤   𝑒,𝐸,ℎ,𝑡,𝑤   𝑇,𝑒,ℎ,𝑤   𝑈,𝑒,ℎ,𝑤   ℎ,𝑖,𝑟,𝑣,𝑥,𝑚,𝑡,𝑤   𝐴,𝑖,𝑥   𝑖,𝐸,𝑥   𝑇,𝑖,𝑥   𝑈,𝑖,𝑥   𝜑,𝑖,𝑚,𝑣   𝑤,𝑌,𝑥   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥,𝑤,𝑡,𝑒,ℎ,𝑟)   𝐴(𝑣,𝑚,𝑟)   𝐵(𝑤,𝑣,𝑡,𝑒,ℎ,𝑖,𝑚,𝑟)   𝐷(𝑥,𝑤,𝑣,𝑡,𝑒,ℎ,𝑖,𝑚,𝑟)   𝑇(𝑣,𝑡,𝑚,𝑟)   𝑈(𝑣,𝑡,𝑚,𝑟)   𝐸(𝑣,𝑚,𝑟)   𝐽(𝑥,𝑤,𝑣,𝑡,𝑒,ℎ,𝑖,𝑚,𝑟)   𝑊(𝑥,𝑤,𝑣,𝑡,𝑒,ℎ,𝑖,𝑚,𝑟)   𝑌(𝑣,𝑡,𝑒,ℎ,𝑖,𝑚,𝑟)

Proof of Theorem stoweidlem39

Dummy variable 𝑏 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		stoweidlem39.8	. . . . . . 7 ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑟)
2		stoweidlem39.9	. . . . . . 7 ⊢ (𝜑 → 𝐷 ≠ ∅)
3	1, 2	jca 555	. . . . . 6 ⊢ (𝜑 → (𝐷 ⊆ ∪ 𝑟 ∧ 𝐷 ≠ ∅))
4		ssn0 4115	. . . . . 6 ⊢ ((𝐷 ⊆ ∪ 𝑟 ∧ 𝐷 ≠ ∅) → ∪ 𝑟 ≠ ∅)
5		unieq 4592	. . . . . . . 8 ⊢ (𝑟 = ∅ → ∪ 𝑟 = ∪ ∅)
6		uni0 4613	. . . . . . . 8 ⊢ ∪ ∅ = ∅
7	5, 6	syl6eq 2806	. . . . . . 7 ⊢ (𝑟 = ∅ → ∪ 𝑟 = ∅)
8	7	necon3i 2960	. . . . . 6 ⊢ (∪ 𝑟 ≠ ∅ → 𝑟 ≠ ∅)
9	3, 4, 8	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑟 ≠ ∅)
10	9	neneqd 2933	. . . 4 ⊢ (𝜑 → ¬ 𝑟 = ∅)
11		stoweidlem39.7	. . . . . 6 ⊢ (𝜑 → 𝑟 ∈ (𝒫 𝑊 ∩ Fin))
12		elinel2 3939	. . . . . 6 ⊢ (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ∈ Fin)
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → 𝑟 ∈ Fin)
14		fz1f1o 14636	. . . . 5 ⊢ (𝑟 ∈ Fin → (𝑟 = ∅ ∨ ((♯‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟)))
15		pm2.53 387	. . . . 5 ⊢ ((𝑟 = ∅ ∨ ((♯‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟)) → (¬ 𝑟 = ∅ → ((♯‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟)))
16	13, 14, 15	3syl 18	. . . 4 ⊢ (𝜑 → (¬ 𝑟 = ∅ → ((♯‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟)))
17	10, 16	mpd 15	. . 3 ⊢ (𝜑 → ((♯‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟))
18		oveq2 6817	. . . . . 6 ⊢ (𝑚 = (♯‘𝑟) → (1...𝑚) = (1...(♯‘𝑟)))
19		f1oeq2 6285	. . . . . 6 ⊢ ((1...𝑚) = (1...(♯‘𝑟)) → (𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟))
20	18, 19	syl 17	. . . . 5 ⊢ (𝑚 = (♯‘𝑟) → (𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟))
21	20	exbidv 1995	. . . 4 ⊢ (𝑚 = (♯‘𝑟) → (∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟))
22	21	rspcev 3445	. . 3 ⊢ (((♯‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟) → ∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟)
23	17, 22	syl 17	. 2 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟)
24		f1of 6294	. . . . . . . 8 ⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 → 𝑣:(1...𝑚)⟶𝑟)
25	24	adantl 473	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑣:(1...𝑚)⟶𝑟)
26		simpll 807	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝜑)
27		elinel1 3938	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ∈ 𝒫 𝑊)
28	27	elpwid 4310	. . . . . . . 8 ⊢ (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ⊆ 𝑊)
29	26, 11, 28	3syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑟 ⊆ 𝑊)
30	25, 29	fssd 6214	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑣:(1...𝑚)⟶𝑊)
31	1	ad2antrr 764	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐷 ⊆ ∪ 𝑟)
32		dff1o2 6299	. . . . . . . . . 10 ⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ (𝑣 Fn (1...𝑚) ∧ Fun ◡𝑣 ∧ ran 𝑣 = 𝑟))
33	32	simp3bi 1142	. . . . . . . . 9 ⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 → ran 𝑣 = 𝑟)
34	33	unieqd 4594	. . . . . . . 8 ⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 → ∪ ran 𝑣 = ∪ 𝑟)
35	34	adantl 473	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → ∪ ran 𝑣 = ∪ 𝑟)
36	31, 35	sseqtr4d 3779	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐷 ⊆ ∪ ran 𝑣)
37		stoweidlem39.1	. . . . . . . . 9 ⊢ Ⅎℎ𝜑
38		nfv 1988	. . . . . . . . 9 ⊢ Ⅎℎ 𝑚 ∈ ℕ
39	37, 38	nfan 1973	. . . . . . . 8 ⊢ Ⅎℎ(𝜑 ∧ 𝑚 ∈ ℕ)
40		nfv 1988	. . . . . . . 8 ⊢ Ⅎℎ 𝑣:(1...𝑚)–1-1-onto→𝑟
41	39, 40	nfan 1973	. . . . . . 7 ⊢ Ⅎℎ((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟)
42		stoweidlem39.2	. . . . . . . . 9 ⊢ Ⅎ𝑡𝜑
43		nfv 1988	. . . . . . . . 9 ⊢ Ⅎ𝑡 𝑚 ∈ ℕ
44	42, 43	nfan 1973	. . . . . . . 8 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑚 ∈ ℕ)
45		nfv 1988	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑣:(1...𝑚)–1-1-onto→𝑟
46	44, 45	nfan 1973	. . . . . . 7 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟)
47		stoweidlem39.3	. . . . . . . . 9 ⊢ Ⅎ𝑤𝜑
48		nfv 1988	. . . . . . . . 9 ⊢ Ⅎ𝑤 𝑚 ∈ ℕ
49	47, 48	nfan 1973	. . . . . . . 8 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑚 ∈ ℕ)
50		nfv 1988	. . . . . . . 8 ⊢ Ⅎ𝑤 𝑣:(1...𝑚)–1-1-onto→𝑟
51	49, 50	nfan 1973	. . . . . . 7 ⊢ Ⅎ𝑤((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟)
52		stoweidlem39.5	. . . . . . 7 ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}
53		stoweidlem39.6	. . . . . . 7 ⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}
54		eqid 2756	. . . . . . 7 ⊢ (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) = (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))})
55		simplr 809	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑚 ∈ ℕ)
56		simpr 479	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑣:(1...𝑚)–1-1-onto→𝑟)
57		stoweidlem39.10	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ℝ+)
58	57	ad2antrr 764	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐸 ∈ ℝ+)
59		stoweidlem39.11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ⊆ 𝑇)
60	59	sselda 3740	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝑇)
61		notnot 136	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝐵 → ¬ ¬ 𝑏 ∈ 𝐵)
62	61	intnand 1000	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝐵 → ¬ (𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵))
63	62	adantl 473	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵))
64		eldif 3721	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (𝑇 ∖ 𝐵) ↔ (𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵))
65	63, 64	sylnibr 318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ (𝑇 ∖ 𝐵))
66		stoweidlem39.4	. . . . . . . . . . . . 13 ⊢ 𝑈 = (𝑇 ∖ 𝐵)
67	66	eleq2i 2827	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ (𝑇 ∖ 𝐵))
68	65, 67	sylnibr 318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝑈)
69	60, 68	eldifd 3722	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ (𝑇 ∖ 𝑈))
70	69	ralrimiva 3100	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 𝑏 ∈ (𝑇 ∖ 𝑈))
71		dfss3 3729	. . . . . . . . 9 ⊢ (𝐵 ⊆ (𝑇 ∖ 𝑈) ↔ ∀𝑏 ∈ 𝐵 𝑏 ∈ (𝑇 ∖ 𝑈))
72	70, 71	sylibr 224	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ (𝑇 ∖ 𝑈))
73	72	ad2antrr 764	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐵 ⊆ (𝑇 ∖ 𝑈))
74		stoweidlem39.12	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ V)
75	74	ad2antrr 764	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑊 ∈ V)
76		stoweidlem39.13	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ V)
77	76	ad2antrr 764	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐴 ∈ V)
78	13	ad2antrr 764	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑟 ∈ Fin)
79		mptfi 8426	. . . . . . . 8 ⊢ (𝑟 ∈ Fin → (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin)
80		rnfi 8410	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin → ran (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin)
81	78, 79, 80	3syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → ran (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin)
82	41, 46, 51, 52, 53, 54, 29, 55, 56, 58, 73, 75, 77, 81	stoweidlem31 40747	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡))))
83	30, 36, 82	3jca 1123	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → (𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))
84	83	ex 449	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑣:(1...𝑚)–1-1-onto→𝑟 → (𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡))))))
85	84	eximdv 1991	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟 → ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡))))))
86	85	reximdva 3151	. 2 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡))))))
87	23, 86	mpd 15	1 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1072   = wceq 1628  ∃wex 1849  Ⅎwnf 1853   ∈ wcel 2135   ≠ wne 2928  ∀wral 3046  ∃wrex 3047  {crab 3050  Vcvv 3336   ∖ cdif 3708   ∩ cin 3710   ⊆ wss 3711  ∅c0 4054  𝒫 cpw 4298  ∪ cuni 4584   class class class wbr 4800   ↦ cmpt 4877  ^◡ccnv 5261  ran crn 5263  Fun wfun 6039   Fn wfn 6040  ⟶wf 6041  –1-1-onto→wf1o 6044  ‘cfv 6045  (class class class)co 6809  Fincfn 8117  0cc0 10124  1c1 10125   < clt 10262   ≤ cle 10263   − cmin 10454   / cdiv 10872  ℕcn 11208  ℝ⁺crp 12021  ...cfz 12515  ♯chash 13307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-oadd 7729  df-er 7907  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-card 8951  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-div 10873  df-nn 11209  df-n0 11481  df-z 11566  df-uz 11876  df-rp 12022  df-fz 12516  df-hash 13308

This theorem is referenced by:  stoweidlem57  40773