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 43572

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 42572	. . 3 ⊢ (ran 𝐺 ∈ Fin → ∃𝑙(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → ∃𝑙(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
4		vex 3436	. . . . 5 ⊢ 𝑙 ∈ V
5		stoweidlem31.6	. . . . . . 7 ⊢ 𝐺 = (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
6		stoweidlem31.12	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ V)
7		stoweidlem31.7	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ⊆ 𝑉)
8	6, 7	ssexd 5248	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ V)
9		mptexg 7097	. . . . . . . 8 ⊢ (𝑅 ∈ V → (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) ∈ V)
10	8, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) ∈ V)
11	5, 10	eqeltrid 2843	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ V)
12		vex 3436	. . . . . 6 ⊢ 𝑣 ∈ V
13		coexg 7776	. . . . . 6 ⊢ ((𝐺 ∈ V ∧ 𝑣 ∈ V) → (𝐺 ∘ 𝑣) ∈ V)
14	11, 12, 13	sylancl 586	. . . . 5 ⊢ (𝜑 → (𝐺 ∘ 𝑣) ∈ V)
15		coexg 7776	. . . . 5 ⊢ ((𝑙 ∈ V ∧ (𝐺 ∘ 𝑣) ∈ V) → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
16	4, 14, 15	sylancr 587	. . . 4 ⊢ (𝜑 → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
17	16	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝑙 ∘ (𝐺 ∘ 𝑣)) ∈ V)
18		simprl 768	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑙 Fn ran 𝐺)
19		stoweidlem31.1	. . . . . . . . 9 ⊢ Ⅎℎ𝜑
20		nfcv 2907	. . . . . . . . . . 11 ⊢ Ⅎℎ𝑙
21		nfcv 2907	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ𝑅
22		nfrab1 3317	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}
23	21, 22	nfmpt 5181	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
24	5, 23	nfcxfr 2905	. . . . . . . . . . . 12 ⊢ Ⅎℎ𝐺
25	24	nfrn 5861	. . . . . . . . . . 11 ⊢ Ⅎℎran 𝐺
26	20, 25	nffn 6532	. . . . . . . . . 10 ⊢ Ⅎℎ 𝑙 Fn ran 𝐺
27		nfv 1917	. . . . . . . . . . 11 ⊢ Ⅎℎ(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
28	25, 27	nfralw 3151	. . . . . . . . . 10 ⊢ Ⅎℎ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
29	26, 28	nfan 1902	. . . . . . . . 9 ⊢ Ⅎℎ(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
30	19, 29	nfan 1902	. . . . . . . 8 ⊢ Ⅎℎ(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
31		fvelrnb 6830	. . . . . . . . . . . . 13 ⊢ (𝑙 Fn ran 𝐺 → (ℎ ∈ ran 𝑙 ↔ ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ))
32	18, 31	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (ℎ ∈ ran 𝑙 ↔ ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ))
33	32	biimpa 477	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ)
34		nfv 1917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏𝜑
35		nfv 1917	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏 𝑙 Fn ran 𝐺
36		nfra1 3144	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
37	35, 36	nfan 1902	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
38	34, 37	nfan 1902	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
39		nfv 1917	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏 ℎ ∈ ran 𝑙
40	38, 39	nfan 1902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙)
41		simp3 1137	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → (𝑙‘𝑏) = ℎ)
42		simp1ll 1235	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → 𝜑)
43		simplrr 775	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
44	43	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
45		simp2 1136	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → 𝑏 ∈ ran 𝐺)
46		simp3 1137	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ∈ ran 𝐺)
47		3simpc 1149	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺))
48		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ∈ ran 𝐺)
49		stoweidlem31.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤𝜑
50		stoweidlem31.13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ V)
51		rabexg 5255	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3141	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
55	5	fnmpt 6573	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑤 ∈ 𝑅 {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V → 𝐺 Fn 𝑅)
56	54, 55	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐺 Fn 𝑅)
57	56	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝐺 Fn 𝑅)
58		fvelrnb 6830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn 𝑅 → (𝑏 ∈ ran 𝐺 ↔ ∃𝑢 ∈ 𝑅 (𝐺‘𝑢) = 𝑏))
59		nfmpt1 5182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑤(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
60	5, 59	nfcxfr 2905	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤𝐺
61		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤𝑢
62	60, 61	nffv 6784	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤(𝐺‘𝑢)
63		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑤𝑏
64	62, 63	nfeq 2920	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑤(𝐺‘𝑢) = 𝑏
65		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑢(𝐺‘𝑤) = 𝑏
66		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = 𝑤 → (𝐺‘𝑢) = (𝐺‘𝑤))
67	66	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑤 → ((𝐺‘𝑢) = 𝑏 ↔ (𝐺‘𝑤) = 𝑏))
68	64, 65, 67	cbvrexw 3374	. . . . . . . . . . . . . . . . . . . . . . 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 5861	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑤ran 𝐺
73	72	nfcri 2894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑤 𝑏 ∈ ran 𝐺
74	49, 73	nfan 1902	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑏 ∈ ran 𝐺)
75		nfv 1917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤 𝑏 ≠ ∅
76		simp3 1137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → (𝐺‘𝑤) = 𝑏)
77		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝑤 ∈ 𝑅)
78	50	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝐴 ∈ V)
79	78, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
80	5	fvmpt2 6886	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ 𝑅 ∧ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
81	77, 79, 80	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐺‘𝑤) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
82	7	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝑤 ∈ 𝑉)
83		stoweidlem31.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}
84	83	rabeq2i 3422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 ∈ 𝑉 ↔ (𝑤 ∈ 𝐽 ∧ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))))
85	82, 84	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝑤 ∈ 𝐽 ∧ ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))))
86	85	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → ∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))
87		stoweidlem31.10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
88		stoweidlem31.8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑀 ∈ ℕ)
89	88	nnrpd 12770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
90	87, 89	rpdivcld 12789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐸 / 𝑀) ∈ ℝ⁺)
91	90	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐸 / 𝑀) ∈ ℝ⁺)
92		breq2 5078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 = (𝐸 / 𝑀) → ((ℎ‘𝑡) < 𝑒 ↔ (ℎ‘𝑡) < (𝐸 / 𝑀)))
93	92	ralbidv 3112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 = (𝐸 / 𝑀) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ↔ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀)))
94		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑒 = (𝐸 / 𝑀) → (1 − 𝑒) = (1 − (𝐸 / 𝑀)))
95	94	breq1d 5084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 = (𝐸 / 𝑀) → ((1 − 𝑒) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
96	95	ralbidv 3112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 = (𝐸 / 𝑀) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
97	93, 96	3anbi23d 1438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑒 = (𝐸 / 𝑀) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
98	97	rexbidv 3226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑒 = (𝐸 / 𝑀) → (∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ↔ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
99	98	rspccva 3560	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑒 ∈ ℝ⁺ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ∧ (𝐸 / 𝑀) ∈ ℝ⁺) → ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
100	86, 91, 99	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))
101		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎℎ 𝑤 ∈ 𝑅
102	19, 101	nfan 1902	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎℎ(𝜑 ∧ 𝑤 ∈ 𝑅)
103		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎℎ∅
104	22, 103	nfne 3045	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅
105		3simpc 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → (ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
106		rabid 3310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ (ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
107	105, 106	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
108		ne0i 4268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
110	109	3exp 1118	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (ℎ ∈ 𝐴 → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)))
111	102, 104, 110	rexlimd 3250	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅))
112	100, 111	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)
113	81, 112	eqnetrd 3011	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐺‘𝑤) ≠ ∅)
114	113	3adant3 1131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → (𝐺‘𝑤) ≠ ∅)
115	76, 114	eqnetrrd 3012	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → 𝑏 ≠ ∅)
116	115	3adant1r 1176	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → 𝑏 ≠ ∅)
117	116	3exp 1118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (𝑤 ∈ 𝑅 → ((𝐺‘𝑤) = 𝑏 → 𝑏 ≠ ∅)))
118	74, 75, 117	rexlimd 3250	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏 → 𝑏 ≠ ∅))
119	71, 118	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ≠ ∅)
120	119	3adant2 1130	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ≠ ∅)
121		rspa 3132	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
122	47, 120, 121	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑏)
123	46, 122	jca 512	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏))
124		vex 3436	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
125	5	elrnmpt 5865	. . . . . . . . . . . . . . . . . 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 1917	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤(𝑙‘𝑏) ∈ 𝑏
129	73, 128	nfan 1902	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏)
130		nfv 1917	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑙‘𝑏) ∈ 𝑌
131		simp1r 1197	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑏)
132		simp3 1137	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
133		simpl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑏)
134		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
135	133, 134	eleqtrd 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
136		elrabi 3618	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝐴)
137		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℎ = (𝑙‘𝑏) → (ℎ‘𝑡) = ((𝑙‘𝑏)‘𝑡))
138	137	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = (𝑙‘𝑏) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ ((𝑙‘𝑏)‘𝑡)))
139	137	breq1d 5084	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = (𝑙‘𝑏) → ((ℎ‘𝑡) ≤ 1 ↔ ((𝑙‘𝑏)‘𝑡) ≤ 1))
140	138, 139	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
141	140	ralbidv 3112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
142	137	breq1d 5084	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀)))
143	142	ralbidv 3112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀)))
144	137	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = (𝑙‘𝑏) → ((1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
145	144	ralbidv 3112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
146	141, 143, 145	3anbi123d 1435	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝑙‘𝑏) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡))))
147	146	elrab 3624	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ ((𝑙‘𝑏) ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡))))
148	147	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))
149	148	simp1d 1141	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1))
150	141	elrab 3624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ↔ ((𝑙‘𝑏) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1)))
151	136, 149, 150	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 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 2850	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑌)
155	131, 132, 154	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ 𝑌)
156	155	3exp 1118	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) → (𝑤 ∈ 𝑅 → (𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝑌)))
157	129, 130, 156	rexlimd 3250	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) → (∃𝑤 ∈ 𝑅 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝑌))
158	123, 127, 157	sylc 65	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑌)
159	42, 44, 45, 158	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → (𝑙‘𝑏) ∈ 𝑌)
160	41, 159	eqeltrrd 2840	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → ℎ ∈ 𝑌)
161	160	3exp 1118	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (𝑏 ∈ ran 𝐺 → ((𝑙‘𝑏) = ℎ → ℎ ∈ 𝑌)))
162	40, 161	reximdai 3244	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ → ∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌))
163	33, 162	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌)
164		nfv 1917	. . . . . . . . . . 11 ⊢ Ⅎ𝑏 ℎ ∈ 𝑌
165		idd 24	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ran 𝐺 → (ℎ ∈ 𝑌 → ℎ ∈ 𝑌))
166	165	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (𝑏 ∈ ran 𝐺 → (ℎ ∈ 𝑌 → ℎ ∈ 𝑌)))
167	40, 164, 166	rexlimd 3250	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌 → ℎ ∈ 𝑌))
168	163, 167	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ℎ ∈ 𝑌)
169	168	ex 413	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (ℎ ∈ ran 𝑙 → ℎ ∈ 𝑌))
170	30, 169	ralrimi 3141	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
171		dfss3 3909	. . . . . . . 8 ⊢ (ran 𝑙 ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌)
172		nfrab1 3317	. . . . . . . . . . 11 ⊢ Ⅎℎ{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}
173	153, 172	nfcxfr 2905	. . . . . . . . . 10 ⊢ Ⅎℎ𝑌
174	173	nfcri 2894	. . . . . . . . 9 ⊢ Ⅎℎ 𝑧 ∈ 𝑌
175		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑧 ℎ ∈ 𝑌
176		eleq1 2826	. . . . . . . . 9 ⊢ (𝑧 = ℎ → (𝑧 ∈ 𝑌 ↔ ℎ ∈ 𝑌))
177	174, 175, 176	cbvralw 3373	. . . . . . . 8 ⊢ (∀𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌 ↔ ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
178	171, 177	bitri 274	. . . . . . 7 ⊢ (ran 𝑙 ⊆ 𝑌 ↔ ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌)
179	170, 178	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ran 𝑙 ⊆ 𝑌)
180		df-f 6437	. . . . . 6 ⊢ (𝑙:ran 𝐺⟶𝑌 ↔ (𝑙 Fn ran 𝐺 ∧ ran 𝑙 ⊆ 𝑌))
181	18, 179, 180	sylanbrc 583	. . . . 5 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑙:ran 𝐺⟶𝑌)
182		dffn3 6613	. . . . . . . 8 ⊢ (𝐺 Fn 𝑅 ↔ 𝐺:𝑅⟶ran 𝐺)
183	56, 182	sylib 217	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑅⟶ran 𝐺)
184	183	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝐺:𝑅⟶ran 𝐺)
185		stoweidlem31.9	. . . . . . . 8 ⊢ (𝜑 → 𝑣:(1...𝑀)–1-1-onto→𝑅)
186		f1of 6716	. . . . . . . 8 ⊢ (𝑣:(1...𝑀)–1-1-onto→𝑅 → 𝑣:(1...𝑀)⟶𝑅)
187	185, 186	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑣:(1...𝑀)⟶𝑅)
188	187	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑣:(1...𝑀)⟶𝑅)
189		fco 6624	. . . . . 6 ⊢ ((𝐺:𝑅⟶ran 𝐺 ∧ 𝑣:(1...𝑀)⟶𝑅) → (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺)
190	184, 188, 189	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺)
191		fco 6624	. . . . 5 ⊢ ((𝑙:ran 𝐺⟶𝑌 ∧ (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺) → (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌)
192	181, 190, 191	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌)
193		fvco3 6867	. . . . . . . . 9 ⊢ (((𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
194	190, 193	sylan 580	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
195		simpll 764	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
196		simplrr 775	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
197	190	ffvelrnda 6961	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
198		simp3 1137	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
199		nfv 1917	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺
200	34, 36, 199	nf3an 1904	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏(𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)
201		nfv 1917	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏(𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)
202	200, 201	nfim 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑏((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
203		eleq1 2826	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (𝑏 ∈ ran 𝐺 ↔ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺))
204	203	3anbi3d 1441	. . . . . . . . . . . 12 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)))
205		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (𝑙‘𝑏) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)))
206		id 22	. . . . . . . . . . . . 13 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → 𝑏 = ((𝐺 ∘ 𝑣)‘𝑖))
207	205, 206	eleq12d 2833	. . . . . . . . . . . 12 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → ((𝑙‘𝑏) ∈ 𝑏 ↔ (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)))
208	204, 207	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑏) ↔ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))))
209	202, 208, 122	vtoclg1f 3504	. . . . . . . . . 10 ⊢ (((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺 → ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)))
210	198, 209	mpcom 38	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
211	195, 196, 197, 210	syl3anc 1370	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
212	194, 211	eqeltrd 2839	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖))
213		fvco3 6867	. . . . . . . . . . . 12 ⊢ ((𝑣:(1...𝑀)⟶𝑅 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = (𝐺‘(𝑣‘𝑖)))
214	187, 213	sylan 580	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = (𝐺‘(𝑣‘𝑖)))
215		raleq 3342	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑣‘𝑖) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀)))
216	215	3anbi2d 1440	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑣‘𝑖) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))))
217	216	rabbidv 3414	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑣‘𝑖) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
218	187	ffvelrnda 6961	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑣‘𝑖) ∈ 𝑅)
219	50	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐴 ∈ V)
220		rabexg 5255	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ V → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
221	219, 220	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V)
222	5, 217, 218, 221	fvmptd3 6898	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝑣‘𝑖)) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
223	214, 222	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
224	223	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
225	224	eleq2d 2824	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) ↔ ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}))
226		nfcv 2907	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ𝑣
227	24, 226	nfco 5774	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝐺 ∘ 𝑣)
228	20, 227	nfco 5774	. . . . . . . . . . . 12 ⊢ Ⅎℎ(𝑙 ∘ (𝐺 ∘ 𝑣))
229		nfcv 2907	. . . . . . . . . . . 12 ⊢ Ⅎℎ𝑖
230	228, 229	nffv 6784	. . . . . . . . . . 11 ⊢ Ⅎℎ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
231		nfcv 2907	. . . . . . . . . . 11 ⊢ Ⅎℎ𝐴
232		nfcv 2907	. . . . . . . . . . . . 13 ⊢ Ⅎℎ𝑇
233		nfcv 2907	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ0
234		nfcv 2907	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ ≤
235		nfcv 2907	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ𝑡
236	230, 235	nffv 6784	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
237	233, 234, 236	nfbr 5121	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
238		nfcv 2907	. . . . . . . . . . . . . . 15 ⊢ Ⅎℎ1
239	236, 234, 238	nfbr 5121	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1
240	237, 239	nfan 1902	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)
241	232, 240	nfralw 3151	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)
242		nfcv 2907	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑣‘𝑖)
243		nfcv 2907	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ <
244		nfcv 2907	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(𝐸 / 𝑀)
245	236, 243, 244	nfbr 5121	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)
246	242, 245	nfralw 3151	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)
247		nfcv 2907	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(𝑇 ∖ 𝑈)
248		nfcv 2907	. . . . . . . . . . . . . 14 ⊢ Ⅎℎ(1 − (𝐸 / 𝑀))
249	248, 243, 236	nfbr 5121	. . . . . . . . . . . . 13 ⊢ Ⅎℎ(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
250	247, 249	nfralw 3151	. . . . . . . . . . . 12 ⊢ Ⅎℎ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)
251	241, 246, 250	nf3an 1904	. . . . . . . . . . 11 ⊢ Ⅎℎ(∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
252		nfcv 2907	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡ℎ
253		nfcv 2907	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡𝑙
254		nfcv 2907	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡𝑅
255		nfra1 3144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)
256		nfra1 3144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀)
257		nfra1 3144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)
258	255, 256, 257	nf3an 1904	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))
259		nfcv 2907	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐴
260	258, 259	nfrabw 3318	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}
261	254, 260	nfmpt 5181	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})
262	5, 261	nfcxfr 2905	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝐺
263		nfcv 2907	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝑣
264	262, 263	nfco 5774	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝐺 ∘ 𝑣)
265	253, 264	nfco 5774	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡(𝑙 ∘ (𝐺 ∘ 𝑣))
266		nfcv 2907	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝑖
267	265, 266	nffv 6784	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
268	252, 267	nfeq 2920	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡 ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)
269		fveq1 6773	. . . . . . . . . . . . . . 15 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (ℎ‘𝑡) = (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
270	269	breq2d 5086	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
271	269	breq1d 5084	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((ℎ‘𝑡) ≤ 1 ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1))
272	270, 271	anbi12d 631	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)))
273	268, 272	ralbid 3161	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1)))
274	269	breq1d 5084	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((ℎ‘𝑡) < (𝐸 / 𝑀) ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
275	268, 274	ralbid 3161	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
276	269	breq2d 5086	. . . . . . . . . . . . 13 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
277	268, 276	ralbid 3161	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
278	273, 275, 277	3anbi123d 1435	. . . . . . . . . . 11 ⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
279	230, 231, 251, 278	elrabf 3620	. . . . . . . . . 10 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
280	279	simprbi 497	. . . . . . . . 9 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
281	280	simp2d 1142	. . . . . . . 8 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))
282	225, 281	syl6bi 252	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
283	212, 282	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))
284		stoweidlem31.2	. . . . . . . . 9 ⊢ Ⅎ𝑡𝜑
285	262	nfrn 5861	. . . . . . . . . . 11 ⊢ Ⅎ𝑡ran 𝐺
286	253, 285	nffn 6532	. . . . . . . . . 10 ⊢ Ⅎ𝑡 𝑙 Fn ran 𝐺
287		nfv 1917	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
288	285, 287	nfralw 3151	. . . . . . . . . 10 ⊢ Ⅎ𝑡∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)
289	286, 288	nfan 1902	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))
290	284, 289	nfan 1902	. . . . . . . 8 ⊢ Ⅎ𝑡(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)))
291		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑖 ∈ (1...𝑀)
292	290, 291	nfan 1902	. . . . . . 7 ⊢ Ⅎ𝑡((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀))
293		stoweidlem31.11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ⊆ (𝑇 ∖ 𝑈))
294	293	ad3antrrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝐵 ⊆ (𝑇 ∖ 𝑈))
295		simpr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ 𝐵)
296	294, 295	sseldd 3922	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ (𝑇 ∖ 𝑈))
297	280	simp3d 1143	. . . . . . . . . . . 12 ⊢ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
298	225, 297	syl6bi 252	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
299	212, 298	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
300	299	r19.21bi 3134	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
301	296, 300	syldan 591	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝐵) → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
302	301	ex 413	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (𝑡 ∈ 𝐵 → (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
303	292, 302	ralrimi 3141	. . . . . 6 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
304	283, 303	jca 512	. . . . 5 ⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
305	304	ralrimiva 3103	. . . 4 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
306	192, 305	jca 512	. . 3 ⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
307		feq1 6581	. . . . 5 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (𝑥:(1...𝑀)⟶𝑌 ↔ (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌))
308		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑡𝑥
309	308, 265	nfeq 2920	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣))
310		fveq1 6773	. . . . . . . . . 10 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (𝑥‘𝑖) = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖))
311	310	fveq1d 6776	. . . . . . . . 9 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((𝑥‘𝑖)‘𝑡) = (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))
312	311	breq1d 5084	. . . . . . . 8 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
313	309, 312	ralbid 3161	. . . . . . 7 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀)))
314	311	breq2d 5086	. . . . . . . 8 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
315	309, 314	ralbid 3161	. . . . . . 7 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡) ↔ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))
316	313, 315	anbi12d 631	. . . . . 6 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)) ↔ (∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
317	316	ralbidv 3112	. . . . 5 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)) ↔ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))
318	307, 317	anbi12d 631	. . . 4 ⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))) ↔ ((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))))
319	318	spcegv 3536	. . 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 1938	1 ⊢ (𝜑 → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∃wex 1782 Ⅎwnf 1786 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 {crab 3068 Vcvv 3432 ∖ cdif 3884 ⊆ wss 3887 ∅c0 4256 class class class wbr 5074 ↦ cmpt 5157 ran crn 5590 ∘ ccom 5593 Fn wfn 6428 ⟶wf 6429 –1-1-onto→wf1o 6432 ‘cfv 6433 (class class class)co 7275 Fincfn 8733 0cc0 10871 1c1 10872 < clt 11009 ≤ cle 11010 − cmin 11205 / cdiv 11632 ℕcn 11973 ℝ⁺crp 12730 ...cfz 13239

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-rp 12731

This theorem is referenced by: stoweidlem39 43580

W3C validator