stoweidlem31 - Mathbox for Glauco Siliprandi

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

Theorem stoweidlem31 42673

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 𝑖 ranging in the finite indexing set, 0 ≤ x_i ≤ 1, x_i < ε / m on V(t_i), and x_i > 1 - ε / m on 𝐵. Here M is used to represent m in the paper, 𝐸 is used to represent ε in the paper, v_i is used to represent V(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.)

**Hypotheses**
Ref	Expression
stoweidlem31.1	⊢ Ⅎℎ𝜑
stoweidlem31.2	⊢ Ⅎ𝑡𝜑
stoweidlem31.3	⊢ Ⅎ𝑤𝜑
stoweidlem31.4	⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}
stoweidlem31.5	⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}
stoweidlem31.6	⊢ 𝐺 = (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
stoweidlem31.7	⊢ (𝜑 → 𝑅 ⊆ 𝑉)
stoweidlem31.8	⊢ (𝜑 → 𝑀 ∈ ℕ)
stoweidlem31.9	⊢ (𝜑 → 𝑣:(1...𝑀)–1-1-onto→𝑅)
stoweidlem31.10	⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
stoweidlem31.11	⊢ (𝜑 → 𝐵 ⊆ (𝑇 ∖ 𝑈))
stoweidlem31.12	⊢ (𝜑 → 𝑉 ∈ V)
stoweidlem31.13	⊢ (𝜑 → 𝐴 ∈ V)
stoweidlem31.14	⊢ (𝜑 → ran 𝐺 ∈ Fin)

**Assertion**
Ref	Expression
stoweidlem31	⊢ (𝜑 → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))))

Distinct variable groups: ℎ,𝑖,𝑡,𝑣,𝑤 𝑖,𝐺 𝑤,𝑌 𝜑,𝑖 𝑒,ℎ,𝑡,𝑤,𝐴 𝑒,𝐸,ℎ,𝑡,𝑤 𝑒,𝑀,ℎ,𝑡,𝑤 𝑇,𝑒,ℎ,𝑤 𝑈,𝑒,ℎ,𝑤 𝑅,ℎ,𝑡,𝑤 𝑥,𝑖,𝑡,𝑣 𝑖,𝑀 𝑥,𝐵 𝑥,𝐸 𝑥,𝐺 𝑥,𝑀 𝑥,𝑌 Allowed substitution hints: 𝜑(𝑥,𝑤,𝑣,𝑡,𝑒,ℎ) 𝐴(𝑥,𝑣,𝑖) 𝐵(𝑤,𝑣,𝑡,𝑒,ℎ,𝑖) 𝑅(𝑥,𝑣,𝑒,𝑖) 𝑇(𝑥,𝑣,𝑡,𝑖) 𝑈(𝑥,𝑣,𝑡,𝑖) 𝐸(𝑣,𝑖) 𝐺(𝑤,𝑣,𝑡,𝑒,ℎ) 𝐽(𝑥,𝑤,𝑣,𝑡,𝑒,ℎ,𝑖) 𝑀(𝑣) 𝑉(𝑥,𝑤,𝑣,𝑡,𝑒,ℎ,𝑖) 𝑌(𝑣,𝑡,𝑒,ℎ,𝑖)

Proof of Theorem stoweidlem31 Dummy variables 𝑏 𝑙 𝑢 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		stoweidlem31.14	. . 3 ⊢ (𝜑 → ran 𝐺 ∈ Fin)
2		fnchoice 41658	. . 3 ⊢ (ran 𝐺 ∈ Fin → ∃𝑙(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → ∃𝑙(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
4		vex 3444	. . . . 5 ⊢ 𝑙 ∈ V
5		stoweidlem31.6	. . . . . . 7 ⊢ 𝐺 = (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
6		stoweidlem31.12	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ V)
7		stoweidlem31.7	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ⊆ 𝑉)
8	6, 7	ssexd 5192	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ V)
9		mptexg 6961	. . . . . . . 8 ⊢ (𝑅 ∈ V → (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) ∈ V)
10	8, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) ∈ V)
11	5, 10	eqeltrid 2894	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ V)
12		vex 3444	. . . . . 6 ⊢ 𝑣 ∈ V
13		coexg 7616	. . . . . 6 ⊢ ((𝐺 ∈ V ∧ 𝑣 ∈ V) → (𝐺 ∘ 𝑣) ∈ V)
14	11, 12, 13	sylancl 589	. . . . 5 ⊢ (𝜑 → (𝐺 ∘ 𝑣) ∈ V)
15		coexg 7616	. . . . 5 ⊢ ((𝑙 ∈ V ∧ (𝐺 ∘ 𝑣) ∈ V) → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
16	4, 14, 15	sylancr 590	. . . 4 ⊢ (𝜑 → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
17	16	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
18		simprl 770	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑙 Fn ran 𝐺)
19		stoweidlem31.1	. . . . . . . . 9 ⊢ Ⅎℎ𝜑
20		nfcv 2955	. . . . . . . . . . 11 ⊢ Ⅎℎ𝑙
21		nfcv 2955	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ𝑅
22		nfrab1 3337	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}
23	21, 22	nfmpt 5127	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
24	5, 23	nfcxfr 2953	. . . . . . . . . . . 12 ⊢ Ⅎℎ𝐺
25	24	nfrn 5788	. . . . . . . . . . 11 ⊢ Ⅎℎran 𝐺
26	20, 25	nffn 6422	. . . . . . . . . 10 ⊢ Ⅎℎ 𝑙 Fn ran 𝐺
27		nfv 1915	. . . . . . . . . . 11 ⊢ Ⅎℎ(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
28	25, 27	nfralw 3189	. . . . . . . . . 10 ⊢ Ⅎℎ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
29	26, 28	nfan 1900	. . . . . . . . 9 ⊢ Ⅎℎ(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
30	19, 29	nfan 1900	. . . . . . . 8 ⊢ Ⅎℎ(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
31		fvelrnb 6701	. . . . . . . . . . . . 13 ⊢ (𝑙 Fn ran 𝐺 → (ℎ ∈ ran 𝑙 ↔ ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ))
32	18, 31	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (ℎ ∈ ran 𝑙 ↔ ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ))
33	32	biimpa 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ)
34		nfv 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏𝜑
35		nfv 1915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏 𝑙 Fn ran 𝐺
36		nfra1 3183	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
37	35, 36	nfan 1900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
38	34, 37	nfan 1900	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
39		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏 ℎ ∈ ran 𝑙
40	38, 39	nfan 1900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙)
41		simp3 1135	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → (𝑙‘𝑏) = ℎ)
42		simp1ll 1233	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → 𝜑)
43		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
44	43	3ad2ant1 1130	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
45		simp2 1134	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → 𝑏 ∈ ran 𝐺)
46		simp3 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ∈ ran 𝐺)
47		3simpc 1147	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺))
48		simpr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ∈ ran 𝐺)
49		stoweidlem31.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤𝜑
50		stoweidlem31.13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ V)
51		rabexg 5198	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ V → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
53	52	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑤 ∈ 𝑅 → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V))
54	49, 53	ralrimi 3180	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
55	5	fnmpt 6460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑤 ∈ 𝑅 {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V → 𝐺 Fn 𝑅)
56	54, 55	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐺 Fn 𝑅)
57	56	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝐺 Fn 𝑅)
58		fvelrnb 6701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn 𝑅 → (𝑏 ∈ ran 𝐺 ↔ ∃𝑢 ∈ 𝑅 (𝐺‘𝑢) = 𝑏))
59		nfmpt1 5128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑤(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
60	5, 59	nfcxfr 2953	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤𝐺
61		nfcv 2955	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤𝑢
62	60, 61	nffv 6655	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤(𝐺‘𝑢)
63		nfcv 2955	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤𝑏
64	62, 63	nfeq 2968	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑤(𝐺‘𝑢) = 𝑏
65		nfv 1915	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑢(𝐺‘𝑤) = 𝑏
66		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = 𝑤 → (𝐺‘𝑢) = (𝐺‘𝑤))
67	66	eqeq1d 2800	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑤 → ((𝐺‘𝑢) = 𝑏 ↔ (𝐺‘𝑤) = 𝑏))
68	64, 65, 67	cbvrexw 3388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑢 ∈ 𝑅 (𝐺‘𝑢) = 𝑏 ↔ ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏)
69	58, 68	syl6bb 290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 Fn 𝑅 → (𝑏 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏))
70	57, 69	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏))
71	48, 70	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏)
72	60	nfrn 5788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑤ran 𝐺
73	72	nfcri 2943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑤 𝑏 ∈ ran 𝐺
74	49, 73	nfan 1900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑏 ∈ ran 𝐺)
75		nfv 1915	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤 𝑏 ≠ ∅
76		simp3 1135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → (𝐺‘𝑤) = 𝑏)
77		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝑤 ∈ 𝑅)
78	50	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝐴 ∈ V)
79	78, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
80	5	fvmpt2 6756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ 𝑅 ∧ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
81	77, 79, 80	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐺‘𝑤) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
82	7	sselda 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝑤 ∈ 𝑉)
83		stoweidlem31.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}
84	83	rabeq2i 3435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 ∈ 𝑉 ↔ (𝑤 ∈ 𝐽 ∧ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))))
85	82, 84	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝑤 ∈ 𝐽 ∧ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))))
86	85	simprd 499	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))
87		stoweidlem31.10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
88		stoweidlem31.8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑀 ∈ ℕ)
89	88	nnrpd 12417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
90	87, 89	rpdivcld 12436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐸 / 𝑀) ∈ ℝ⁺)
91	90	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐸 / 𝑀) ∈ ℝ⁺)
92		breq2 5034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 = (𝐸 / 𝑀) → ((ℎ‘𝑡) < 𝑒 ↔ (ℎ‘𝑡) < (𝐸 / 𝑀)))
93	92	ralbidv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 = (𝐸 / 𝑀) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ↔ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀)))
94		oveq2 7143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑒 = (𝐸 / 𝑀) → (1 − 𝑒) = (1 − (𝐸 / 𝑀)))
95	94	breq1d 5040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 = (𝐸 / 𝑀) → ((1 − 𝑒) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
96	95	ralbidv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 = (𝐸 / 𝑀) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
97	93, 96	3anbi23d 1436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑒 = (𝐸 / 𝑀) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
98	97	rexbidv 3256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑒 = (𝐸 / 𝑀) → (∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ↔ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
99	98	rspccva 3570	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ∧ (𝐸 / 𝑀) ∈ ℝ⁺) → ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
100	86, 91, 99	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
101		nfv 1915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎℎ 𝑤 ∈ 𝑅
102	19, 101	nfan 1900	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎℎ(𝜑 ∧ 𝑤 ∈ 𝑅)
103		nfcv 2955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎℎ∅
104	22, 103	nfne 3087	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅
105		3simpc 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → (ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
106		rabid 3331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ (ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
107	105, 106	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
108		ne0i 4250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
110	109	3exp 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (ℎ ∈ 𝐴 → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)))
111	102, 104, 110	rexlimd 3276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅))
112	100, 111	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
113	81, 112	eqnetrd 3054	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐺‘𝑤) ≠ ∅)
114	113	3adant3 1129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → (𝐺‘𝑤) ≠ ∅)
115	76, 114	eqnetrrd 3055	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → 𝑏 ≠ ∅)
116	115	3adant1r 1174	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → 𝑏 ≠ ∅)
117	116	3exp 1116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (𝑤 ∈ 𝑅 → ((𝐺‘𝑤) = 𝑏 → 𝑏 ≠ ∅)))
118	74, 75, 117	rexlimd 3276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏 → 𝑏 ≠ ∅))
119	71, 118	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ≠ ∅)
120	119	3adant2 1128	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ≠ ∅)
121		rspa 3171	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
122	47, 120, 121	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑏)
123	46, 122	jca 515	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏))
124		vex 3444	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
125	5	elrnmpt 5792	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ V → (𝑏 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑅 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}))
126	124, 125	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑅 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
127	46, 126	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑅 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
128		nfv 1915	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤(𝑙‘𝑏) ∈ 𝑏
129	73, 128	nfan 1900	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏)
130		nfv 1915	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑙‘𝑏) ∈ 𝑌
131		simp1r 1195	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑏)
132		simp3 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
133		simpl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑏)
134		simpr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
135	133, 134	eleqtrd 2892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
136		elrabi 3623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝐴)
137		fveq1 6644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℎ = (𝑙‘𝑏) → (ℎ‘𝑡) = ((𝑙‘𝑏)‘𝑡))
138	137	breq2d 5042	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = (𝑙‘𝑏) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ ((𝑙‘𝑏)‘𝑡)))
139	137	breq1d 5040	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = (𝑙‘𝑏) → ((ℎ‘𝑡) ≤ 1 ↔ ((𝑙‘𝑏)‘𝑡) ≤ 1))
140	138, 139	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
141	140	ralbidv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
142	137	breq1d 5040	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀)))
143	142	ralbidv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀)))
144	137	breq2d 5042	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
145	144	ralbidv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
146	141, 143, 145	3anbi123d 1433	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝑙‘𝑏) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡))))
147	146	elrab 3628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ ((𝑙‘𝑏) ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡))))
148	147	simprbi 500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
149	148	simp1d 1139	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1))
150	141	elrab 3628	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ↔ ((𝑙‘𝑏) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
151	136, 149, 150	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)})
152	135, 151	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)})
153		stoweidlem31.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}
154	152, 153	eleqtrrdi 2901	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑌)
155	131, 132, 154	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑌)
156	155	3exp 1116	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) → (𝑤 ∈ 𝑅 → (𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝑌)))
157	129, 130, 156	rexlimd 3276	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) → (∃𝑤 ∈ 𝑅 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝑌))
158	123, 127, 157	sylc 65	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑌)
159	42, 44, 45, 158	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → (𝑙‘𝑏) ∈ 𝑌)
160	41, 159	eqeltrrd 2891	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → ℎ ∈ 𝑌)
161	160	3exp 1116	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (𝑏 ∈ ran 𝐺 → ((𝑙‘𝑏) = ℎ → ℎ ∈ 𝑌)))
162	40, 161	reximdai 3270	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ → ∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌))
163	33, 162	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌)
164		nfv 1915	. . . . . . . . . . 11 ⊢ Ⅎ𝑏 ℎ ∈ 𝑌
165		idd 24	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ran 𝐺 → (ℎ ∈ 𝑌 → ℎ ∈ 𝑌))
166	165	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (𝑏 ∈ ran 𝐺 → (ℎ ∈ 𝑌 → ℎ ∈ 𝑌)))
167	40, 164, 166	rexlimd 3276	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌 → ℎ ∈ 𝑌))
168	163, 167	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ℎ ∈ 𝑌)
169	168	ex 416	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (ℎ ∈ ran 𝑙 → ℎ ∈ 𝑌))
170	30, 169	ralrimi 3180	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
171		dfss3 3903	. . . . . . . 8 ⊢ (ran 𝑙 ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌)
172		nfrab1 3337	. . . . . . . . . . 11 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}
173	153, 172	nfcxfr 2953	. . . . . . . . . 10 ⊢ Ⅎℎ𝑌
174	173	nfcri 2943	. . . . . . . . 9 ⊢ Ⅎℎ 𝑧 ∈ 𝑌
175		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑧 ℎ ∈ 𝑌
176		eleq1 2877	. . . . . . . . 9 ⊢ (𝑧 = ℎ → (𝑧 ∈ 𝑌 ↔ ℎ ∈ 𝑌))
177	174, 175, 176	cbvralw 3387	. . . . . . . 8 ⊢ (∀𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌 ↔ ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
178	171, 177	bitri 278	. . . . . . 7 ⊢ (ran 𝑙 ⊆ 𝑌 ↔ ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
179	170, 178	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ran 𝑙 ⊆ 𝑌)
180		df-f 6328	. . . . . 6 ⊢ (𝑙:ran 𝐺⟶𝑌 ↔ (𝑙 Fn ran 𝐺 ∧ ran 𝑙 ⊆ 𝑌))
181	18, 179, 180	sylanbrc 586	. . . . 5 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑙:ran 𝐺⟶𝑌)
182		dffn3 6499	. . . . . . . 8 ⊢ (𝐺 Fn 𝑅 ↔ 𝐺:𝑅⟶ran 𝐺)
183	56, 182	sylib 221	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑅⟶ran 𝐺)
184	183	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝐺:𝑅⟶ran 𝐺)
185		stoweidlem31.9	. . . . . . . 8 ⊢ (𝜑 → 𝑣:(1...𝑀)–1-1-onto→𝑅)
186		f1of 6590	. . . . . . . 8 ⊢ (𝑣:(1...𝑀)–1-1-onto→𝑅 → 𝑣:(1...𝑀)⟶𝑅)
187	185, 186	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑣:(1...𝑀)⟶𝑅)
188	187	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑣:(1...𝑀)⟶𝑅)
189		fco 6505	. . . . . 6 ⊢ ((𝐺:𝑅⟶ran 𝐺 ∧ 𝑣:(1...𝑀)⟶𝑅) → (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺)
190	184, 188, 189	syl2anc 587	. . . . 5 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺)
191		fco 6505	. . . . 5 ⊢ ((𝑙:ran 𝐺⟶𝑌 ∧ (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺) → (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌)
192	181, 190, 191	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌)
193		fvco3 6737	. . . . . . . . 9 ⊢ (((𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
194	190, 193	sylan 583	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
195		simpll 766	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
196		simplrr 777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
197	190	ffvelrnda 6828	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
198		simp3 1135	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
199		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺
200	34, 36, 199	nf3an 1902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏(𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
201		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏(𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)
202	200, 201	nfim 1897	. . . . . . . . . . 11 ⊢ Ⅎ𝑏((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
203		eleq1 2877	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (𝑏 ∈ ran 𝐺 ↔ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺))
204	203	3anbi3d 1439	. . . . . . . . . . . 12 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)))
205		fveq2 6645	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (𝑙‘𝑏) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
206		id 22	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → 𝑏 = ((𝐺 ∘ 𝑣)‘𝑖))
207	205, 206	eleq12d 2884	. . . . . . . . . . . 12 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → ((𝑙‘𝑏) ∈ 𝑏 ↔ (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)))
208	204, 207	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑏) ↔ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))))
209	202, 208, 122	vtoclg1f 3514	. . . . . . . . . 10 ⊢ (((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺 → ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)))
210	198, 209	mpcom 38	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
211	195, 196, 197, 210	syl3anc 1368	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
212	194, 211	eqeltrd 2890	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
213		fvco3 6737	. . . . . . . . . . . 12 ⊢ ((𝑣:(1...𝑀)⟶𝑅 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = (𝐺‘(𝑣‘𝑖)))
214	187, 213	sylan 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = (𝐺‘(𝑣‘𝑖)))
215		raleq 3358	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑣‘𝑖) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀)))
216	215	3anbi2d 1438	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑣‘𝑖) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
217	216	rabbidv 3427	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑣‘𝑖) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
218	187	ffvelrnda 6828	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑣‘𝑖) ∈ 𝑅)
219	50	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐴 ∈ V)
220		rabexg 5198	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ V → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
221	219, 220	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
222	5, 217, 218, 221	fvmptd3 6768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝑣‘𝑖)) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
223	214, 222	eqtrd 2833	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
224	223	adantlr 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
225	224	eleq2d 2875	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) ↔ ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}))
226		nfcv 2955	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ𝑣
227	24, 226	nfco 5700	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝐺 ∘ 𝑣)
228	20, 227	nfco 5700	. . . . . . . . . . . 12 ⊢ Ⅎℎ(𝑙 ∘ (𝐺 ∘ 𝑣))
229		nfcv 2955	. . . . . . . . . . . 12 ⊢ Ⅎℎ𝑖
230	228, 229	nffv 6655	. . . . . . . . . . 11 ⊢ Ⅎℎ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
231		nfcv 2955	. . . . . . . . . . 11 ⊢ Ⅎℎ𝐴
232		nfcv 2955	. . . . . . . . . . . . 13 ⊢ Ⅎℎ𝑇
233		nfcv 2955	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ0
234		nfcv 2955	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ ≤
235		nfcv 2955	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ𝑡
236	230, 235	nffv 6655	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
237	233, 234, 236	nfbr 5077	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
238		nfcv 2955	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ1
239	236, 234, 238	nfbr 5077	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1
240	237, 239	nfan 1900	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)
241	232, 240	nfralw 3189	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)
242		nfcv 2955	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑣‘𝑖)
243		nfcv 2955	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ <
244		nfcv 2955	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(𝐸 / 𝑀)
245	236, 243, 244	nfbr 5077	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)
246	242, 245	nfralw 3189	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)
247		nfcv 2955	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑇 ∖ 𝑈)
248		nfcv 2955	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(1 − (𝐸 / 𝑀))
249	248, 243, 236	nfbr 5077	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
250	247, 249	nfralw 3189	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
251	241, 246, 250	nf3an 1902	. . . . . . . . . . 11 ⊢ Ⅎℎ(∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
252		nfcv 2955	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡ℎ
253		nfcv 2955	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡𝑙
254		nfcv 2955	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡𝑅
255		nfra1 3183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)
256		nfra1 3183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀)
257		nfra1 3183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)
258	255, 256, 257	nf3an 1902	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))
259		nfcv 2955	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐴
260	258, 259	nfrabw 3338	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}
261	254, 260	nfmpt 5127	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
262	5, 261	nfcxfr 2953	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝐺
263		nfcv 2955	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝑣
264	262, 263	nfco 5700	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝐺 ∘ 𝑣)
265	253, 264	nfco 5700	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡(𝑙 ∘ (𝐺 ∘ 𝑣))
266		nfcv 2955	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝑖
267	265, 266	nffv 6655	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
268	252, 267	nfeq 2968	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡 ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
269		fveq1 6644	. . . . . . . . . . . . . . 15 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (ℎ‘𝑡) = (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
270	269	breq2d 5042	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
271	269	breq1d 5040	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((ℎ‘𝑡) ≤ 1 ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1))
272	270, 271	anbi12d 633	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)))
273	268, 272	ralbid 3195	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)))
274	269	breq1d 5040	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((ℎ‘𝑡) < (𝐸 / 𝑀) ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
275	268, 274	ralbid 3195	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
276	269	breq2d 5042	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
277	268, 276	ralbid 3195	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
278	273, 275, 277	3anbi123d 1433	. . . . . . . . . . 11 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
279	230, 231, 251, 278	elrabf 3624	. . . . . . . . . 10 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
280	279	simprbi 500	. . . . . . . . 9 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
281	280	simp2d 1140	. . . . . . . 8 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))
282	225, 281	syl6bi 256	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
283	212, 282	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))
284		stoweidlem31.2	. . . . . . . . 9 ⊢ Ⅎ𝑡𝜑
285	262	nfrn 5788	. . . . . . . . . . 11 ⊢ Ⅎ𝑡ran 𝐺
286	253, 285	nffn 6422	. . . . . . . . . 10 ⊢ Ⅎ𝑡 𝑙 Fn ran 𝐺
287		nfv 1915	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
288	285, 287	nfralw 3189	. . . . . . . . . 10 ⊢ Ⅎ𝑡∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
289	286, 288	nfan 1900	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
290	284, 289	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑡(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
291		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑖 ∈ (1...𝑀)
292	290, 291	nfan 1900	. . . . . . 7 ⊢ Ⅎ𝑡((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀))
293		stoweidlem31.11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ⊆ (𝑇 ∖ 𝑈))
294	293	ad3antrrr 729	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝐵 ⊆ (𝑇 ∖ 𝑈))
295		simpr 488	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ 𝐵)
296	294, 295	sseldd 3916	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ (𝑇 ∖ 𝑈))
297	280	simp3d 1141	. . . . . . . . . . . 12 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
298	225, 297	syl6bi 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
299	212, 298	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
300	299	r19.21bi 3173	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
301	296, 300	syldan 594	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
302	301	ex 416	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (𝑡 ∈ 𝐵 → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
303	292, 302	ralrimi 3180	. . . . . 6 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
304	283, 303	jca 515	. . . . 5 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
305	304	ralrimiva 3149	. . . 4 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
306	192, 305	jca 515	. . 3 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
307		feq1 6468	. . . . 5 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (𝑥:(1...𝑀)⟶𝑌 ↔ (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌))
308		nfcv 2955	. . . . . . . . 9 ⊢ Ⅎ𝑡𝑥
309	308, 265	nfeq 2968	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣))
310		fveq1 6644	. . . . . . . . . 10 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (𝑥‘𝑖) = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖))
311	310	fveq1d 6647	. . . . . . . . 9 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((𝑥‘𝑖)‘𝑡) = (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
312	311	breq1d 5040	. . . . . . . 8 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
313	309, 312	ralbid 3195	. . . . . . 7 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
314	311	breq2d 5042	. . . . . . . 8 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
315	309, 314	ralbid 3195	. . . . . . 7 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡) ↔ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
316	313, 315	anbi12d 633	. . . . . 6 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)) ↔ (∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
317	316	ralbidv 3162	. . . . 5 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)) ↔ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
318	307, 317	anbi12d 633	. . . 4 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))) ↔ ((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))))
319	318	spcegv 3545	. . 3 ⊢ ((𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V → (((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))) → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)))))
320	17, 306, 319	sylc 65	. 2 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))))
321	3, 320	exlimddv 1936	1 ⊢ (𝜑 → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∃wex 1781 Ⅎwnf 1785 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 ∃wrex 3107 {crab 3110 Vcvv 3441 ∖ cdif 3878 ⊆ wss 3881 ∅c0 4243 class class class wbr 5030 ↦ cmpt 5110 ran crn 5520 ∘ ccom 5523 Fn wfn 6319 ⟶wf 6320 –1-1-onto→wf1o 6323 ‘cfv 6324 (class class class)co 7135 Fincfn 8492 0cc0 10526 1c1 10527 < clt 10664 ≤ cle 10665 − cmin 10859 / cdiv 11286 ℕcn 11625 ℝ⁺crp 12377 ...cfz 12885

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-er 8272 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-rp 12378

This theorem is referenced by: stoweidlem39 42681

W3C validator