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 44747

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 43713	. . 3 ⊢ (ran 𝐺 ∈ Fin → ∃𝑙(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → ∃𝑙(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
4		vex 3479	. . . . 5 ⊢ 𝑙 ∈ V
5		stoweidlem31.6	. . . . . . 7 ⊢ 𝐺 = (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
6		stoweidlem31.12	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ V)
7		stoweidlem31.7	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ⊆ 𝑉)
8	6, 7	ssexd 5325	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ V)
9		mptexg 7223	. . . . . . . 8 ⊢ (𝑅 ∈ V → (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) ∈ V)
10	8, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) ∈ V)
11	5, 10	eqeltrid 2838	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ V)
12		vex 3479	. . . . . 6 ⊢ 𝑣 ∈ V
13		coexg 7920	. . . . . 6 ⊢ ((𝐺 ∈ V ∧ 𝑣 ∈ V) → (𝐺 ∘ 𝑣) ∈ V)
14	11, 12, 13	sylancl 587	. . . . 5 ⊢ (𝜑 → (𝐺 ∘ 𝑣) ∈ V)
15		coexg 7920	. . . . 5 ⊢ ((𝑙 ∈ V ∧ (𝐺 ∘ 𝑣) ∈ V) → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
16	4, 14, 15	sylancr 588	. . . 4 ⊢ (𝜑 → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
17	16	adantr 482	. . 3 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
18		simprl 770	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑙 Fn ran 𝐺)
19		stoweidlem31.1	. . . . . . . . 9 ⊢ Ⅎℎ𝜑
20		nfcv 2904	. . . . . . . . . . 11 ⊢ Ⅎℎ𝑙
21		nfcv 2904	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ𝑅
22		nfrab1 3452	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}
23	21, 22	nfmpt 5256	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
24	5, 23	nfcxfr 2902	. . . . . . . . . . . 12 ⊢ Ⅎℎ𝐺
25	24	nfrn 5952	. . . . . . . . . . 11 ⊢ Ⅎℎran 𝐺
26	20, 25	nffn 6649	. . . . . . . . . 10 ⊢ Ⅎℎ 𝑙 Fn ran 𝐺
27		nfv 1918	. . . . . . . . . . 11 ⊢ Ⅎℎ(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
28	25, 27	nfralw 3309	. . . . . . . . . 10 ⊢ Ⅎℎ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
29	26, 28	nfan 1903	. . . . . . . . 9 ⊢ Ⅎℎ(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
30	19, 29	nfan 1903	. . . . . . . 8 ⊢ Ⅎℎ(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
31		fvelrnb 6953	. . . . . . . . . . . . 13 ⊢ (𝑙 Fn ran 𝐺 → (ℎ ∈ ran 𝑙 ↔ ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ))
32	18, 31	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (ℎ ∈ ran 𝑙 ↔ ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ))
33	32	biimpa 478	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ)
34		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏𝜑
35		nfv 1918	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏 𝑙 Fn ran 𝐺
36		nfra1 3282	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
37	35, 36	nfan 1903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
38	34, 37	nfan 1903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
39		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏 ℎ ∈ ran 𝑙
40	38, 39	nfan 1903	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙)
41		simp3 1139	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → (𝑙‘𝑏) = ℎ)
42		simp1ll 1237	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → 𝜑)
43		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
44	43	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
45		simp2 1138	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → 𝑏 ∈ ran 𝐺)
46		simp3 1139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ∈ ran 𝐺)
47		3simpc 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺))
48		simpr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ∈ ran 𝐺)
49		stoweidlem31.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤𝜑
50		stoweidlem31.13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ V)
51		rabexg 5332	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3255	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
55	5	fnmpt 6691	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑤 ∈ 𝑅 {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V → 𝐺 Fn 𝑅)
56	54, 55	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐺 Fn 𝑅)
57	56	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝐺 Fn 𝑅)
58		fvelrnb 6953	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn 𝑅 → (𝑏 ∈ ran 𝐺 ↔ ∃𝑢 ∈ 𝑅 (𝐺‘𝑢) = 𝑏))
59		nfmpt1 5257	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑤(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
60	5, 59	nfcxfr 2902	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤𝐺
61		nfcv 2904	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤𝑢
62	60, 61	nffv 6902	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤(𝐺‘𝑢)
63		nfcv 2904	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤𝑏
64	62, 63	nfeq 2917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑤(𝐺‘𝑢) = 𝑏
65		nfv 1918	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑢(𝐺‘𝑤) = 𝑏
66		fveq2 6892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = 𝑤 → (𝐺‘𝑢) = (𝐺‘𝑤))
67	66	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑤 → ((𝐺‘𝑢) = 𝑏 ↔ (𝐺‘𝑤) = 𝑏))
68	64, 65, 67	cbvrexw 3305	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑢 ∈ 𝑅 (𝐺‘𝑢) = 𝑏 ↔ ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏)
69	58, 68	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 Fn 𝑅 → (𝑏 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏))
70	57, 69	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏))
71	48, 70	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏)
72	60	nfrn 5952	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑤ran 𝐺
73	72	nfcri 2891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑤 𝑏 ∈ ran 𝐺
74	49, 73	nfan 1903	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑏 ∈ ran 𝐺)
75		nfv 1918	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤 𝑏 ≠ ∅
76		simp3 1139	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → (𝐺‘𝑤) = 𝑏)
77		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝑤 ∈ 𝑅)
78	50	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝐴 ∈ V)
79	78, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
80	5	fvmpt2 7010	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ 𝑅 ∧ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
81	77, 79, 80	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐺‘𝑤) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
82	7	sselda 3983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝑤 ∈ 𝑉)
83		stoweidlem31.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}
84	83	reqabi 3455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 ∈ 𝑉 ↔ (𝑤 ∈ 𝐽 ∧ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))))
85	82, 84	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝑤 ∈ 𝐽 ∧ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))))
86	85	simprd 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))
87		stoweidlem31.10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
88		stoweidlem31.8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑀 ∈ ℕ)
89	88	nnrpd 13014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
90	87, 89	rpdivcld 13033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐸 / 𝑀) ∈ ℝ⁺)
91	90	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐸 / 𝑀) ∈ ℝ⁺)
92		breq2 5153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 = (𝐸 / 𝑀) → ((ℎ‘𝑡) < 𝑒 ↔ (ℎ‘𝑡) < (𝐸 / 𝑀)))
93	92	ralbidv 3178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 = (𝐸 / 𝑀) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ↔ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀)))
94		oveq2 7417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑒 = (𝐸 / 𝑀) → (1 − 𝑒) = (1 − (𝐸 / 𝑀)))
95	94	breq1d 5159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 = (𝐸 / 𝑀) → ((1 − 𝑒) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
96	95	ralbidv 3178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 = (𝐸 / 𝑀) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
97	93, 96	3anbi23d 1440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑒 = (𝐸 / 𝑀) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
98	97	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑒 = (𝐸 / 𝑀) → (∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ↔ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
99	98	rspccva 3612	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ∧ (𝐸 / 𝑀) ∈ ℝ⁺) → ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
100	86, 91, 99	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
101		nfv 1918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎℎ 𝑤 ∈ 𝑅
102	19, 101	nfan 1903	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎℎ(𝜑 ∧ 𝑤 ∈ 𝑅)
103		nfcv 2904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎℎ∅
104	22, 103	nfne 3044	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅
105		3simpc 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → (ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
106		rabid 3453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ (ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
107	105, 106	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
108		ne0i 4335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
110	109	3exp 1120	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (ℎ ∈ 𝐴 → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)))
111	102, 104, 110	rexlimd 3264	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅))
112	100, 111	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
113	81, 112	eqnetrd 3009	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐺‘𝑤) ≠ ∅)
114	113	3adant3 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → (𝐺‘𝑤) ≠ ∅)
115	76, 114	eqnetrrd 3010	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → 𝑏 ≠ ∅)
116	115	3adant1r 1178	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → 𝑏 ≠ ∅)
117	116	3exp 1120	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (𝑤 ∈ 𝑅 → ((𝐺‘𝑤) = 𝑏 → 𝑏 ≠ ∅)))
118	74, 75, 117	rexlimd 3264	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏 → 𝑏 ≠ ∅))
119	71, 118	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ≠ ∅)
120	119	3adant2 1132	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ≠ ∅)
121		rspa 3246	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
122	47, 120, 121	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑏)
123	46, 122	jca 513	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏))
124		vex 3479	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
125	5	elrnmpt 5956	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ V → (𝑏 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑅 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}))
126	124, 125	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑅 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
127	46, 126	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑅 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
128		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤(𝑙‘𝑏) ∈ 𝑏
129	73, 128	nfan 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏)
130		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑙‘𝑏) ∈ 𝑌
131		simp1r 1199	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑏)
132		simp3 1139	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
133		simpl 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑏)
134		simpr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
135	133, 134	eleqtrd 2836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
136		elrabi 3678	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝐴)
137		fveq1 6891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℎ = (𝑙‘𝑏) → (ℎ‘𝑡) = ((𝑙‘𝑏)‘𝑡))
138	137	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = (𝑙‘𝑏) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ ((𝑙‘𝑏)‘𝑡)))
139	137	breq1d 5159	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = (𝑙‘𝑏) → ((ℎ‘𝑡) ≤ 1 ↔ ((𝑙‘𝑏)‘𝑡) ≤ 1))
140	138, 139	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
141	140	ralbidv 3178	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
142	137	breq1d 5159	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀)))
143	142	ralbidv 3178	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀)))
144	137	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
145	144	ralbidv 3178	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
146	141, 143, 145	3anbi123d 1437	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝑙‘𝑏) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡))))
147	146	elrab 3684	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ ((𝑙‘𝑏) ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡))))
148	147	simprbi 498	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
149	148	simp1d 1143	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1))
150	141	elrab 3684	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ↔ ((𝑙‘𝑏) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
151	136, 149, 150	sylanbrc 584	. . . . . . . . . . . . . . . . . . . . 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 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑌)
155	131, 132, 154	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑌)
156	155	3exp 1120	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) → (𝑤 ∈ 𝑅 → (𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝑌)))
157	129, 130, 156	rexlimd 3264	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) → (∃𝑤 ∈ 𝑅 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝑌))
158	123, 127, 157	sylc 65	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑌)
159	42, 44, 45, 158	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → (𝑙‘𝑏) ∈ 𝑌)
160	41, 159	eqeltrrd 2835	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → ℎ ∈ 𝑌)
161	160	3exp 1120	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (𝑏 ∈ ran 𝐺 → ((𝑙‘𝑏) = ℎ → ℎ ∈ 𝑌)))
162	40, 161	reximdai 3259	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ → ∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌))
163	33, 162	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌)
164		nfv 1918	. . . . . . . . . . 11 ⊢ Ⅎ𝑏 ℎ ∈ 𝑌
165		idd 24	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ran 𝐺 → (ℎ ∈ 𝑌 → ℎ ∈ 𝑌))
166	165	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (𝑏 ∈ ran 𝐺 → (ℎ ∈ 𝑌 → ℎ ∈ 𝑌)))
167	40, 164, 166	rexlimd 3264	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌 → ℎ ∈ 𝑌))
168	163, 167	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ℎ ∈ 𝑌)
169	168	ex 414	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (ℎ ∈ ran 𝑙 → ℎ ∈ 𝑌))
170	30, 169	ralrimi 3255	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
171		dfss3 3971	. . . . . . . 8 ⊢ (ran 𝑙 ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌)
172		nfrab1 3452	. . . . . . . . . . 11 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}
173	153, 172	nfcxfr 2902	. . . . . . . . . 10 ⊢ Ⅎℎ𝑌
174	173	nfcri 2891	. . . . . . . . 9 ⊢ Ⅎℎ 𝑧 ∈ 𝑌
175		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑧 ℎ ∈ 𝑌
176		eleq1 2822	. . . . . . . . 9 ⊢ (𝑧 = ℎ → (𝑧 ∈ 𝑌 ↔ ℎ ∈ 𝑌))
177	174, 175, 176	cbvralw 3304	. . . . . . . 8 ⊢ (∀𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌 ↔ ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
178	171, 177	bitri 275	. . . . . . 7 ⊢ (ran 𝑙 ⊆ 𝑌 ↔ ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
179	170, 178	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ran 𝑙 ⊆ 𝑌)
180		df-f 6548	. . . . . 6 ⊢ (𝑙:ran 𝐺⟶𝑌 ↔ (𝑙 Fn ran 𝐺 ∧ ran 𝑙 ⊆ 𝑌))
181	18, 179, 180	sylanbrc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑙:ran 𝐺⟶𝑌)
182		dffn3 6731	. . . . . . . 8 ⊢ (𝐺 Fn 𝑅 ↔ 𝐺:𝑅⟶ran 𝐺)
183	56, 182	sylib 217	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑅⟶ran 𝐺)
184	183	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝐺:𝑅⟶ran 𝐺)
185		stoweidlem31.9	. . . . . . . 8 ⊢ (𝜑 → 𝑣:(1...𝑀)–1-1-onto→𝑅)
186		f1of 6834	. . . . . . . 8 ⊢ (𝑣:(1...𝑀)–1-1-onto→𝑅 → 𝑣:(1...𝑀)⟶𝑅)
187	185, 186	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑣:(1...𝑀)⟶𝑅)
188	187	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑣:(1...𝑀)⟶𝑅)
189		fco 6742	. . . . . 6 ⊢ ((𝐺:𝑅⟶ran 𝐺 ∧ 𝑣:(1...𝑀)⟶𝑅) → (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺)
190	184, 188, 189	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺)
191		fco 6742	. . . . 5 ⊢ ((𝑙:ran 𝐺⟶𝑌 ∧ (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺) → (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌)
192	181, 190, 191	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌)
193		fvco3 6991	. . . . . . . . 9 ⊢ (((𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
194	190, 193	sylan 581	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
195		simpll 766	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
196		simplrr 777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
197	190	ffvelcdmda 7087	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
198		simp3 1139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
199		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺
200	34, 36, 199	nf3an 1905	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏(𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
201		nfv 1918	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏(𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)
202	200, 201	nfim 1900	. . . . . . . . . . 11 ⊢ Ⅎ𝑏((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
203		eleq1 2822	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (𝑏 ∈ ran 𝐺 ↔ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺))
204	203	3anbi3d 1443	. . . . . . . . . . . 12 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)))
205		fveq2 6892	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (𝑙‘𝑏) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
206		id 22	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → 𝑏 = ((𝐺 ∘ 𝑣)‘𝑖))
207	205, 206	eleq12d 2828	. . . . . . . . . . . 12 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → ((𝑙‘𝑏) ∈ 𝑏 ↔ (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)))
208	204, 207	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑏) ↔ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))))
209	202, 208, 122	vtoclg1f 3556	. . . . . . . . . 10 ⊢ (((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺 → ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)))
210	198, 209	mpcom 38	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
211	195, 196, 197, 210	syl3anc 1372	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
212	194, 211	eqeltrd 2834	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
213		fvco3 6991	. . . . . . . . . . . 12 ⊢ ((𝑣:(1...𝑀)⟶𝑅 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = (𝐺‘(𝑣‘𝑖)))
214	187, 213	sylan 581	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = (𝐺‘(𝑣‘𝑖)))
215		raleq 3323	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑣‘𝑖) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀)))
216	215	3anbi2d 1442	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑣‘𝑖) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
217	216	rabbidv 3441	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑣‘𝑖) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
218	187	ffvelcdmda 7087	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑣‘𝑖) ∈ 𝑅)
219	50	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐴 ∈ V)
220		rabexg 5332	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ V → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
221	219, 220	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
222	5, 217, 218, 221	fvmptd3 7022	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝑣‘𝑖)) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
223	214, 222	eqtrd 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
224	223	adantlr 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
225	224	eleq2d 2820	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) ↔ ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}))
226		nfcv 2904	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ𝑣
227	24, 226	nfco 5866	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝐺 ∘ 𝑣)
228	20, 227	nfco 5866	. . . . . . . . . . . 12 ⊢ Ⅎℎ(𝑙 ∘ (𝐺 ∘ 𝑣))
229		nfcv 2904	. . . . . . . . . . . 12 ⊢ Ⅎℎ𝑖
230	228, 229	nffv 6902	. . . . . . . . . . 11 ⊢ Ⅎℎ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
231		nfcv 2904	. . . . . . . . . . 11 ⊢ Ⅎℎ𝐴
232		nfcv 2904	. . . . . . . . . . . . 13 ⊢ Ⅎℎ𝑇
233		nfcv 2904	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ0
234		nfcv 2904	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ ≤
235		nfcv 2904	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ𝑡
236	230, 235	nffv 6902	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
237	233, 234, 236	nfbr 5196	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
238		nfcv 2904	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ1
239	236, 234, 238	nfbr 5196	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1
240	237, 239	nfan 1903	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)
241	232, 240	nfralw 3309	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)
242		nfcv 2904	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑣‘𝑖)
243		nfcv 2904	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ <
244		nfcv 2904	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(𝐸 / 𝑀)
245	236, 243, 244	nfbr 5196	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)
246	242, 245	nfralw 3309	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)
247		nfcv 2904	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑇 ∖ 𝑈)
248		nfcv 2904	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(1 − (𝐸 / 𝑀))
249	248, 243, 236	nfbr 5196	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
250	247, 249	nfralw 3309	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
251	241, 246, 250	nf3an 1905	. . . . . . . . . . 11 ⊢ Ⅎℎ(∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
252		nfcv 2904	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡ℎ
253		nfcv 2904	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡𝑙
254		nfcv 2904	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡𝑅
255		nfra1 3282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)
256		nfra1 3282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀)
257		nfra1 3282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)
258	255, 256, 257	nf3an 1905	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))
259		nfcv 2904	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐴
260	258, 259	nfrabw 3469	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}
261	254, 260	nfmpt 5256	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
262	5, 261	nfcxfr 2902	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝐺
263		nfcv 2904	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝑣
264	262, 263	nfco 5866	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝐺 ∘ 𝑣)
265	253, 264	nfco 5866	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡(𝑙 ∘ (𝐺 ∘ 𝑣))
266		nfcv 2904	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝑖
267	265, 266	nffv 6902	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
268	252, 267	nfeq 2917	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡 ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
269		fveq1 6891	. . . . . . . . . . . . . . 15 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (ℎ‘𝑡) = (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
270	269	breq2d 5161	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
271	269	breq1d 5159	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((ℎ‘𝑡) ≤ 1 ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1))
272	270, 271	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)))
273	268, 272	ralbid 3271	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)))
274	269	breq1d 5159	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((ℎ‘𝑡) < (𝐸 / 𝑀) ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
275	268, 274	ralbid 3271	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
276	269	breq2d 5161	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
277	268, 276	ralbid 3271	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
278	273, 275, 277	3anbi123d 1437	. . . . . . . . . . 11 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
279	230, 231, 251, 278	elrabf 3680	. . . . . . . . . 10 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
280	279	simprbi 498	. . . . . . . . 9 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
281	280	simp2d 1144	. . . . . . . 8 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))
282	225, 281	syl6bi 253	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
283	212, 282	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))
284		stoweidlem31.2	. . . . . . . . 9 ⊢ Ⅎ𝑡𝜑
285	262	nfrn 5952	. . . . . . . . . . 11 ⊢ Ⅎ𝑡ran 𝐺
286	253, 285	nffn 6649	. . . . . . . . . 10 ⊢ Ⅎ𝑡 𝑙 Fn ran 𝐺
287		nfv 1918	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
288	285, 287	nfralw 3309	. . . . . . . . . 10 ⊢ Ⅎ𝑡∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
289	286, 288	nfan 1903	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
290	284, 289	nfan 1903	. . . . . . . 8 ⊢ Ⅎ𝑡(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
291		nfv 1918	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑖 ∈ (1...𝑀)
292	290, 291	nfan 1903	. . . . . . 7 ⊢ Ⅎ𝑡((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀))
293		stoweidlem31.11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ⊆ (𝑇 ∖ 𝑈))
294	293	ad3antrrr 729	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝐵 ⊆ (𝑇 ∖ 𝑈))
295		simpr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ 𝐵)
296	294, 295	sseldd 3984	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ (𝑇 ∖ 𝑈))
297	280	simp3d 1145	. . . . . . . . . . . 12 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
298	225, 297	syl6bi 253	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
299	212, 298	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
300	299	r19.21bi 3249	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
301	296, 300	syldan 592	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
302	301	ex 414	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (𝑡 ∈ 𝐵 → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
303	292, 302	ralrimi 3255	. . . . . 6 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
304	283, 303	jca 513	. . . . 5 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
305	304	ralrimiva 3147	. . . 4 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
306	192, 305	jca 513	. . 3 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
307		feq1 6699	. . . . 5 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (𝑥:(1...𝑀)⟶𝑌 ↔ (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌))
308		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑡𝑥
309	308, 265	nfeq 2917	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣))
310		fveq1 6891	. . . . . . . . . 10 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (𝑥‘𝑖) = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖))
311	310	fveq1d 6894	. . . . . . . . 9 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((𝑥‘𝑖)‘𝑡) = (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
312	311	breq1d 5159	. . . . . . . 8 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
313	309, 312	ralbid 3271	. . . . . . 7 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
314	311	breq2d 5161	. . . . . . . 8 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
315	309, 314	ralbid 3271	. . . . . . 7 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡) ↔ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
316	313, 315	anbi12d 632	. . . . . 6 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)) ↔ (∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
317	316	ralbidv 3178	. . . . 5 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)) ↔ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
318	307, 317	anbi12d 632	. . . 4 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))) ↔ ((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))))
319	318	spcegv 3588	. . 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 1939	1 ⊢ (𝜑 → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∃wex 1782 Ⅎwnf 1786 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 {crab 3433 Vcvv 3475 ∖ cdif 3946 ⊆ wss 3949 ∅c0 4323 class class class wbr 5149 ↦ cmpt 5232 ran crn 5678 ∘ ccom 5681 Fn wfn 6539 ⟶wf 6540 –1-1-onto→wf1o 6543 ‘cfv 6544 (class class class)co 7409 Fincfn 8939 0cc0 11110 1c1 11111 < clt 11248 ≤ cle 11249 − cmin 11444 / cdiv 11871 ℕcn 12212 ℝ⁺crp 12974 ...cfz 13484

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-rp 12975

This theorem is referenced by: stoweidlem39 44755

W3C validator