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 46671

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 45675	. . 3 ⊢ (ran 𝐺 ∈ Fin → ∃𝑙(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
3	1, 2	syl 18	. 2 ⊢ (𝜑 → ∃𝑙(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
4		vex 3467	. . . . 5 ⊢ 𝑙 ∈ V
5		stoweidlem31.6	. . . . . . 7 ⊢ 𝐺 = (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
6		stoweidlem31.12	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ V)
7		stoweidlem31.7	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ⊆ 𝑉)
8	6, 7	ssexd 5295	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ V)
9		mptexg 7220	. . . . . . . 8 ⊢ (𝑅 ∈ V → (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) ∈ V)
10	8, 9	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) ∈ V)
11	5, 10	eqeltrid 2873	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ V)
12		vex 3467	. . . . . 6 ⊢ 𝑣 ∈ V
13		coexg 7926	. . . . . 6 ⊢ ((𝐺 ∈ V ∧ 𝑣 ∈ V) → (𝐺 ∘ 𝑣) ∈ V)
14	11, 12, 13	sylancl 597	. . . . 5 ⊢ (𝜑 → (𝐺 ∘ 𝑣) ∈ V)
15		coexg 7926	. . . . 5 ⊢ ((𝑙 ∈ V ∧ (𝐺 ∘ 𝑣) ∈ V) → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
16	4, 14, 15	sylancr 598	. . . 4 ⊢ (𝜑 → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
17	16	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
18		simprl 782	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑙 Fn ran 𝐺)
19		stoweidlem31.1	. . . . . . . . 9 ⊢ Ⅎℎ𝜑
20		nfcv 2931	. . . . . . . . . . 11 ⊢ Ⅎℎ𝑙
21		nfcv 2931	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ𝑅
22		nfrab1 3443	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}
23	21, 22	nfmpt 5213	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
24	5, 23	nfcxfr 2929	. . . . . . . . . . . 12 ⊢ Ⅎℎ𝐺
25	24	nfrn 5943	. . . . . . . . . . 11 ⊢ Ⅎℎran 𝐺
26	20, 25	nffn 6635	. . . . . . . . . 10 ⊢ Ⅎℎ 𝑙 Fn ran 𝐺
27		nfv 1941	. . . . . . . . . . 11 ⊢ Ⅎℎ(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
28	25, 27	nfralw 3318	. . . . . . . . . 10 ⊢ Ⅎℎ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
29	26, 28	nfan 1926	. . . . . . . . 9 ⊢ Ⅎℎ(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
30	19, 29	nfan 1926	. . . . . . . 8 ⊢ Ⅎℎ(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
31		fvelrnb 6942	. . . . . . . . . . . . 13 ⊢ (𝑙 Fn ran 𝐺 → (ℎ ∈ ran 𝑙 ↔ ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ))
32	18, 31	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (ℎ ∈ ran 𝑙 ↔ ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ))
33	32	biimpa 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ)
34		nfv 1941	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏𝜑
35		nfv 1941	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏 𝑙 Fn ran 𝐺
36		nfra1 3295	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
37	35, 36	nfan 1926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
38	34, 37	nfan 1926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
39		nfv 1941	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏 ℎ ∈ ran 𝑙
40	38, 39	nfan 1926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙)
41		simp3 1154	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → (𝑙‘𝑏) = ℎ)
42		simp1ll 1253	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → 𝜑)
43		simplrr 789	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
44	43	3ad2ant1 1149	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
45		simp2 1153	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → 𝑏 ∈ ran 𝐺)
46		simp3 1154	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ∈ ran 𝐺)
47		3simpc 1166	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺))
48		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ∈ ran 𝐺)
49		stoweidlem31.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤𝜑
50		stoweidlem31.13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ V)
51		rabexg 5308	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ V → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
52	50, 51	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
53	52	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑤 ∈ 𝑅 → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V))
54	49, 53	ralrimi 3269	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
55	5	fnmpt 6676	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑤 ∈ 𝑅 {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V → 𝐺 Fn 𝑅)
56	54, 55	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐺 Fn 𝑅)
57	56	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝐺 Fn 𝑅)
58		fvelrnb 6942	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn 𝑅 → (𝑏 ∈ ran 𝐺 ↔ ∃𝑢 ∈ 𝑅 (𝐺‘𝑢) = 𝑏))
59		nfmpt1 5214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑤(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
60	5, 59	nfcxfr 2929	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤𝐺
61		nfcv 2931	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤𝑢
62	60, 61	nffv 6892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤(𝐺‘𝑢)
63		nfcv 2931	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤𝑏
64	62, 63	nfeq 2944	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑤(𝐺‘𝑢) = 𝑏
65		nfv 1941	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑢(𝐺‘𝑤) = 𝑏
66		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = 𝑤 → (𝐺‘𝑢) = (𝐺‘𝑤))
67	66	eqeq1d 2771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑤 → ((𝐺‘𝑢) = 𝑏 ↔ (𝐺‘𝑤) = 𝑏))
68	64, 65, 67	cbvrexw 3314	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑢 ∈ 𝑅 (𝐺‘𝑢) = 𝑏 ↔ ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏)
69	58, 68	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 Fn 𝑅 → (𝑏 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏))
70	57, 69	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏))
71	48, 70	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏)
72	60	nfrn 5943	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑤ran 𝐺
73	72	nfcri 2923	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑤 𝑏 ∈ ran 𝐺
74	49, 73	nfan 1926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑏 ∈ ran 𝐺)
75		nfv 1941	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤 𝑏 ≠ ∅
76		simp3 1154	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → (𝐺‘𝑤) = 𝑏)
77		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝑤 ∈ 𝑅)
78	50	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝐴 ∈ V)
79	78, 51	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
80	5	fvmpt2 7002	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ 𝑅 ∧ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
81	77, 79, 80	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐺‘𝑤) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
82	7	sselda 3945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝑤 ∈ 𝑉)
83		stoweidlem31.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}
84	83	reqabi 3446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 ∈ 𝑉 ↔ (𝑤 ∈ 𝐽 ∧ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))))
85	82, 84	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝑤 ∈ 𝐽 ∧ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))))
86	85	simprd 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))
87		stoweidlem31.10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
88		stoweidlem31.8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑀 ∈ ℕ)
89	88	nnrpd 13058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
90	87, 89	rpdivcld 13077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐸 / 𝑀) ∈ ℝ⁺)
91	90	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐸 / 𝑀) ∈ ℝ⁺)
92		breq2 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 = (𝐸 / 𝑀) → ((ℎ‘𝑡) < 𝑒 ↔ (ℎ‘𝑡) < (𝐸 / 𝑀)))
93	92	ralbidv 3194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 = (𝐸 / 𝑀) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ↔ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀)))
94		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑒 = (𝐸 / 𝑀) → (1 − 𝑒) = (1 − (𝐸 / 𝑀)))
95	94	breq1d 5123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 = (𝐸 / 𝑀) → ((1 − 𝑒) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
96	95	ralbidv 3194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 = (𝐸 / 𝑀) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
97	93, 96	3anbi23d 1465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑒 = (𝐸 / 𝑀) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
98	97	rexbidv 3195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑒 = (𝐸 / 𝑀) → (∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ↔ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
99	98	rspccva 3589	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ∧ (𝐸 / 𝑀) ∈ ℝ⁺) → ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
100	86, 91, 99	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
101		nfv 1941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎℎ 𝑤 ∈ 𝑅
102	19, 101	nfan 1926	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎℎ(𝜑 ∧ 𝑤 ∈ 𝑅)
103		nfcv 2931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎℎ∅
104	22, 103	nfne 3067	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅
105		3simpc 1166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → (ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
106		rabid 3444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ (ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
107	105, 106	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
108		ne0i 4302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
109	107, 108	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
110	109	3exp 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (ℎ ∈ 𝐴 → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)))
111	102, 104, 110	rexlimd 3278	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅))
112	100, 111	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
113	81, 112	eqnetrd 3031	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐺‘𝑤) ≠ ∅)
114	113	3adant3 1148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → (𝐺‘𝑤) ≠ ∅)
115	76, 114	eqnetrrd 3032	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → 𝑏 ≠ ∅)
116	115	3adant1r 1194	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → 𝑏 ≠ ∅)
117	116	3exp 1135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (𝑤 ∈ 𝑅 → ((𝐺‘𝑤) = 𝑏 → 𝑏 ≠ ∅)))
118	74, 75, 117	rexlimd 3278	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏 → 𝑏 ≠ ∅))
119	71, 118	mpd 16	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ≠ ∅)
120	119	3adant2 1147	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ≠ ∅)
121		rspa 3260	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
122	47, 120, 121	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑏)
123	46, 122	jca 520	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏))
124		vex 3467	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
125	5	elrnmpt 5949	. . . . . . . . . . . . . . . . . 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 1941	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤(𝑙‘𝑏) ∈ 𝑏
129	73, 128	nfan 1926	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏)
130		nfv 1941	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑙‘𝑏) ∈ 𝑌
131		simp1r 1215	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑏)
132		simp3 1154	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
133		simpl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑏)
134		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
135	133, 134	eleqtrd 2871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
136		elrabi 3655	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝐴)
137		fveq1 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℎ = (𝑙‘𝑏) → (ℎ‘𝑡) = ((𝑙‘𝑏)‘𝑡))
138	137	breq2d 5125	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = (𝑙‘𝑏) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ ((𝑙‘𝑏)‘𝑡)))
139	137	breq1d 5123	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = (𝑙‘𝑏) → ((ℎ‘𝑡) ≤ 1 ↔ ((𝑙‘𝑏)‘𝑡) ≤ 1))
140	138, 139	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
141	140	ralbidv 3194	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
142	137	breq1d 5123	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀)))
143	142	ralbidv 3194	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀)))
144	137	breq2d 5125	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
145	144	ralbidv 3194	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
146	141, 143, 145	3anbi123d 1462	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝑙‘𝑏) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡))))
147	146	elrab 3659	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ ((𝑙‘𝑏) ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡))))
148	147	simprbi 502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
149	148	simp1d 1158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1))
150	141	elrab 3659	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ↔ ((𝑙‘𝑏) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
151	136, 149, 150	sylanbrc 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)})
152	135, 151	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)})
153		stoweidlem31.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}
154	152, 153	eleqtrrdi 2880	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑌)
155	131, 132, 154	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑌)
156	155	3exp 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) → (𝑤 ∈ 𝑅 → (𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝑌)))
157	129, 130, 156	rexlimd 3278	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) → (∃𝑤 ∈ 𝑅 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝑌))
158	123, 127, 157	sylc 66	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑌)
159	42, 44, 45, 158	syl3anc 1396	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → (𝑙‘𝑏) ∈ 𝑌)
160	41, 159	eqeltrrd 2870	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → ℎ ∈ 𝑌)
161	160	3exp 1135	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (𝑏 ∈ ran 𝐺 → ((𝑙‘𝑏) = ℎ → ℎ ∈ 𝑌)))
162	40, 161	reximdai 3273	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ → ∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌))
163	33, 162	mpd 16	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌)
164		nfv 1941	. . . . . . . . . . 11 ⊢ Ⅎ𝑏 ℎ ∈ 𝑌
165		idd 25	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ran 𝐺 → (ℎ ∈ 𝑌 → ℎ ∈ 𝑌))
166	165	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (𝑏 ∈ ran 𝐺 → (ℎ ∈ 𝑌 → ℎ ∈ 𝑌)))
167	40, 164, 166	rexlimd 3278	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌 → ℎ ∈ 𝑌))
168	163, 167	mpd 16	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ℎ ∈ 𝑌)
169	168	ex 417	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (ℎ ∈ ran 𝑙 → ℎ ∈ 𝑌))
170	30, 169	ralrimi 3269	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
171		dfss3 3934	. . . . . . . 8 ⊢ (ran 𝑙 ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌)
172		nfrab1 3443	. . . . . . . . . . 11 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}
173	153, 172	nfcxfr 2929	. . . . . . . . . 10 ⊢ Ⅎℎ𝑌
174	173	nfcri 2923	. . . . . . . . 9 ⊢ Ⅎℎ 𝑧 ∈ 𝑌
175		nfv 1941	. . . . . . . . 9 ⊢ Ⅎ𝑧 ℎ ∈ 𝑌
176		eleq1 2857	. . . . . . . . 9 ⊢ (𝑧 = ℎ → (𝑧 ∈ 𝑌 ↔ ℎ ∈ 𝑌))
177	174, 175, 176	cbvralw 3313	. . . . . . . 8 ⊢ (∀𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌 ↔ ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
178	171, 177	bitri 278	. . . . . . 7 ⊢ (ran 𝑙 ⊆ 𝑌 ↔ ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
179	170, 178	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ran 𝑙 ⊆ 𝑌)
180		df-f 6541	. . . . . 6 ⊢ (𝑙:ran 𝐺⟶𝑌 ↔ (𝑙 Fn ran 𝐺 ∧ ran 𝑙 ⊆ 𝑌))
181	18, 179, 180	sylanbrc 594	. . . . 5 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑙:ran 𝐺⟶𝑌)
182		dffn3 6719	. . . . . . . 8 ⊢ (𝐺 Fn 𝑅 ↔ 𝐺:𝑅⟶ran 𝐺)
183	56, 182	sylib 221	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑅⟶ran 𝐺)
184	183	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝐺:𝑅⟶ran 𝐺)
185		stoweidlem31.9	. . . . . . . 8 ⊢ (𝜑 → 𝑣:(1...𝑀)–1-1-onto→𝑅)
186		f1of 6821	. . . . . . . 8 ⊢ (𝑣:(1...𝑀)–1-1-onto→𝑅 → 𝑣:(1...𝑀)⟶𝑅)
187	185, 186	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑣:(1...𝑀)⟶𝑅)
188	187	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑣:(1...𝑀)⟶𝑅)
189		fco 6731	. . . . . 6 ⊢ ((𝐺:𝑅⟶ran 𝐺 ∧ 𝑣:(1...𝑀)⟶𝑅) → (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺)
190	184, 188, 189	syl2anc 595	. . . . 5 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺)
191		fco 6731	. . . . 5 ⊢ ((𝑙:ran 𝐺⟶𝑌 ∧ (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺) → (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌)
192	181, 190, 191	syl2anc 595	. . . 4 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌)
193		fvco3 6982	. . . . . . . . 9 ⊢ (((𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
194	190, 193	sylan 591	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
195		simpll 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
196		simplrr 789	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
197	190	ffvelcdmda 7080	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
198		simp3 1154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
199		nfv 1941	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺
200	34, 36, 199	nf3an 1928	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏(𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
201		nfv 1941	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏(𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)
202	200, 201	nfim 1923	. . . . . . . . . . 11 ⊢ Ⅎ𝑏((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
203		eleq1 2857	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (𝑏 ∈ ran 𝐺 ↔ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺))
204	203	3anbi3d 1468	. . . . . . . . . . . 12 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)))
205		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (𝑙‘𝑏) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
206		id 23	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → 𝑏 = ((𝐺 ∘ 𝑣)‘𝑖))
207	205, 206	eleq12d 2863	. . . . . . . . . . . 12 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → ((𝑙‘𝑏) ∈ 𝑏 ↔ (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)))
208	204, 207	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑏) ↔ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))))
209	202, 208, 122	vtoclg1f 3544	. . . . . . . . . 10 ⊢ (((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺 → ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)))
210	198, 209	mpcom 39	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
211	195, 196, 197, 210	syl3anc 1396	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
212	194, 211	eqeltrd 2869	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
213		fvco3 6982	. . . . . . . . . . . 12 ⊢ ((𝑣:(1...𝑀)⟶𝑅 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = (𝐺‘(𝑣‘𝑖)))
214	187, 213	sylan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = (𝐺‘(𝑣‘𝑖)))
215		raleq 3326	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑣‘𝑖) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀)))
216	215	3anbi2d 1467	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑣‘𝑖) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
217	216	rabbidv 3430	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑣‘𝑖) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
218	187	ffvelcdmda 7080	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑣‘𝑖) ∈ 𝑅)
219	50	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐴 ∈ V)
220		rabexg 5308	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ V → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
221	219, 220	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
222	5, 217, 218, 221	fvmptd3 7014	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝑣‘𝑖)) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
223	214, 222	eqtrd 2804	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
224	223	adantlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
225	224	eleq2d 2855	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) ↔ ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}))
226		nfcv 2931	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ𝑣
227	24, 226	nfco 5852	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝐺 ∘ 𝑣)
228	20, 227	nfco 5852	. . . . . . . . . . . 12 ⊢ Ⅎℎ(𝑙 ∘ (𝐺 ∘ 𝑣))
229		nfcv 2931	. . . . . . . . . . . 12 ⊢ Ⅎℎ𝑖
230	228, 229	nffv 6892	. . . . . . . . . . 11 ⊢ Ⅎℎ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
231		nfcv 2931	. . . . . . . . . . 11 ⊢ Ⅎℎ𝐴
232		nfcv 2931	. . . . . . . . . . . . 13 ⊢ Ⅎℎ𝑇
233		nfcv 2931	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ0
234		nfcv 2931	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ ≤
235		nfcv 2931	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ𝑡
236	230, 235	nffv 6892	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
237	233, 234, 236	nfbr 5162	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
238		nfcv 2931	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ1
239	236, 234, 238	nfbr 5162	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1
240	237, 239	nfan 1926	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)
241	232, 240	nfralw 3318	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)
242		nfcv 2931	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑣‘𝑖)
243		nfcv 2931	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ <
244		nfcv 2931	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(𝐸 / 𝑀)
245	236, 243, 244	nfbr 5162	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)
246	242, 245	nfralw 3318	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)
247		nfcv 2931	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑇 ∖ 𝑈)
248		nfcv 2931	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(1 − (𝐸 / 𝑀))
249	248, 243, 236	nfbr 5162	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
250	247, 249	nfralw 3318	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
251	241, 246, 250	nf3an 1928	. . . . . . . . . . 11 ⊢ Ⅎℎ(∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
252		nfcv 2931	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡ℎ
253		nfcv 2931	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡𝑙
254		nfcv 2931	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡𝑅
255		nfra1 3295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)
256		nfra1 3295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀)
257		nfra1 3295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)
258	255, 256, 257	nf3an 1928	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))
259		nfcv 2931	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐴
260	258, 259	nfrabw 3460	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}
261	254, 260	nfmpt 5213	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
262	5, 261	nfcxfr 2929	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝐺
263		nfcv 2931	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝑣
264	262, 263	nfco 5852	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝐺 ∘ 𝑣)
265	253, 264	nfco 5852	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡(𝑙 ∘ (𝐺 ∘ 𝑣))
266		nfcv 2931	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝑖
267	265, 266	nffv 6892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
268	252, 267	nfeq 2944	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡 ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
269		fveq1 6881	. . . . . . . . . . . . . . 15 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (ℎ‘𝑡) = (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
270	269	breq2d 5125	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
271	269	breq1d 5123	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((ℎ‘𝑡) ≤ 1 ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1))
272	270, 271	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)))
273	268, 272	ralbid 3284	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)))
274	269	breq1d 5123	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((ℎ‘𝑡) < (𝐸 / 𝑀) ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
275	268, 274	ralbid 3284	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
276	269	breq2d 5125	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
277	268, 276	ralbid 3284	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
278	273, 275, 277	3anbi123d 1462	. . . . . . . . . . 11 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
279	230, 231, 251, 278	elrabf 3656	. . . . . . . . . 10 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
280	279	simprbi 502	. . . . . . . . 9 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
281	280	simp2d 1159	. . . . . . . 8 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))
282	225, 281	biimtrdi 256	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
283	212, 282	mpd 16	. . . . . 6 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))
284		stoweidlem31.2	. . . . . . . . 9 ⊢ Ⅎ𝑡𝜑
285	262	nfrn 5943	. . . . . . . . . . 11 ⊢ Ⅎ𝑡ran 𝐺
286	253, 285	nffn 6635	. . . . . . . . . 10 ⊢ Ⅎ𝑡 𝑙 Fn ran 𝐺
287		nfv 1941	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
288	285, 287	nfralw 3318	. . . . . . . . . 10 ⊢ Ⅎ𝑡∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
289	286, 288	nfan 1926	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
290	284, 289	nfan 1926	. . . . . . . 8 ⊢ Ⅎ𝑡(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
291		nfv 1941	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑖 ∈ (1...𝑀)
292	290, 291	nfan 1926	. . . . . . 7 ⊢ Ⅎ𝑡((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀))
293		stoweidlem31.11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ⊆ (𝑇 ∖ 𝑈))
294	293	ad3antrrr 742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝐵 ⊆ (𝑇 ∖ 𝑈))
295		simpr 489	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ 𝐵)
296	294, 295	sseldd 3946	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ (𝑇 ∖ 𝑈))
297	280	simp3d 1160	. . . . . . . . . . . 12 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
298	225, 297	biimtrdi 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
299	212, 298	mpd 16	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
300	299	r19.21bi 3263	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
301	296, 300	syldan 602	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
302	301	ex 417	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (𝑡 ∈ 𝐵 → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
303	292, 302	ralrimi 3269	. . . . . 6 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
304	283, 303	jca 520	. . . . 5 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
305	304	ralrimiva 3163	. . . 4 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
306	192, 305	jca 520	. . 3 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
307		feq1 6684	. . . . 5 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (𝑥:(1...𝑀)⟶𝑌 ↔ (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌))
308		nfcv 2931	. . . . . . . . 9 ⊢ Ⅎ𝑡𝑥
309	308, 265	nfeq 2944	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣))
310		fveq1 6881	. . . . . . . . . 10 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (𝑥‘𝑖) = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖))
311	310	fveq1d 6884	. . . . . . . . 9 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((𝑥‘𝑖)‘𝑡) = (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
312	311	breq1d 5123	. . . . . . . 8 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
313	309, 312	ralbid 3284	. . . . . . 7 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
314	311	breq2d 5125	. . . . . . . 8 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
315	309, 314	ralbid 3284	. . . . . . 7 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡) ↔ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
316	313, 315	anbi12d 643	. . . . . 6 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)) ↔ (∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
317	316	ralbidv 3194	. . . . 5 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)) ↔ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
318	307, 317	anbi12d 643	. . . 4 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))) ↔ ((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))))
319	318	spcegv 3565	. . 3 ⊢ ((𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V → (((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))) → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)))))
320	17, 306, 319	sylc 66	. 2 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))))
321	3, 320	exlimddv 1962	1 ⊢ (𝜑 → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∃wex 1806 Ⅎwnf 1810 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 {crab 3423 Vcvv 3463 ∖ cdif 3910 ⊆ wss 3913 ∅c0 4294 class class class wbr 5113 ↦ cmpt 5196 ran crn 5663 ∘ ccom 5666 Fn wfn 6532 ⟶wf 6533 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7411 Fincfn 8943 0cc0 11100 1c1 11101 < clt 11243 ≤ cle 11244 − cmin 11441 / cdiv 11871 ℕcn 12233 ℝ⁺crp 13016 ...cfz 13535

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-er 8694 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-rp 13017

This theorem is referenced by: stoweidlem39 46679

W3C validator