Step | Hyp | Ref
| Expression |
1 | | stoweidlem31.14 |
. . 3
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
2 | | fnchoice 42542 |
. . 3
⊢ (ran
𝐺 ∈ Fin →
∃𝑙(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑙(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) |
4 | | vex 3435 |
. . . . 5
⊢ 𝑙 ∈ V |
5 | | stoweidlem31.6 |
. . . . . . 7
⊢ 𝐺 = (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
6 | | stoweidlem31.12 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈ V) |
7 | | stoweidlem31.7 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ⊆ 𝑉) |
8 | 6, 7 | ssexd 5252 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ V) |
9 | | mptexg 7094 |
. . . . . . . 8
⊢ (𝑅 ∈ V → (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) ∈ V) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) ∈ V) |
11 | 5, 10 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ V) |
12 | | vex 3435 |
. . . . . 6
⊢ 𝑣 ∈ V |
13 | | coexg 7770 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑣 ∈ V) → (𝐺 ∘ 𝑣) ∈ V) |
14 | 11, 12, 13 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (𝐺 ∘ 𝑣) ∈ V) |
15 | | coexg 7770 |
. . . . 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 2909 |
. . . . . . . . . . 11
⊢
Ⅎℎ𝑙 |
21 | | nfcv 2909 |
. . . . . . . . . . . . . 14
⊢
Ⅎℎ𝑅 |
22 | | nfrab1 3316 |
. . . . . . . . . . . . . 14
⊢
Ⅎℎ{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} |
23 | 21, 22 | nfmpt 5186 |
. . . . . . . . . . . . 13
⊢
Ⅎℎ(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
24 | 5, 23 | nfcxfr 2907 |
. . . . . . . . . . . 12
⊢
Ⅎℎ𝐺 |
25 | 24 | nfrn 5860 |
. . . . . . . . . . 11
⊢
Ⅎℎran
𝐺 |
26 | 20, 25 | nffn 6530 |
. . . . . . . . . 10
⊢
Ⅎℎ 𝑙 Fn ran 𝐺 |
27 | | nfv 1921 |
. . . . . . . . . . 11
⊢
Ⅎℎ(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) |
28 | 25, 27 | nfralw 3152 |
. . . . . . . . . 10
⊢
Ⅎℎ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) |
29 | 26, 28 | nfan 1906 |
. . . . . . . . 9
⊢
Ⅎℎ(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)) |
30 | 19, 29 | nfan 1906 |
. . . . . . . 8
⊢
Ⅎℎ(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) |
31 | | fvelrnb 6827 |
. . . . . . . . . . . . 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 1921 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑏𝜑 |
35 | | nfv 1921 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑏 𝑙 Fn ran 𝐺 |
36 | | nfra1 3145 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑏∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) |
37 | 35, 36 | nfan 1906 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑏(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)) |
38 | 34, 37 | nfan 1906 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑏(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) |
39 | | nfv 1921 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑏 ℎ ∈ ran 𝑙 |
40 | 38, 39 | nfan 1906 |
. . . . . . . . . . . 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 5259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3142 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ∀𝑤 ∈ 𝑅 {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V) |
55 | 5 | fnmpt 6571 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑤 ∈
𝑅 {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V → 𝐺 Fn 𝑅) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐺 Fn 𝑅) |
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝐺 Fn 𝑅) |
58 | | fvelrnb 6827 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 Fn 𝑅 → (𝑏 ∈ ran 𝐺 ↔ ∃𝑢 ∈ 𝑅 (𝐺‘𝑢) = 𝑏)) |
59 | | nfmpt1 5187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
Ⅎ𝑤(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
60 | 5, 59 | nfcxfr 2907 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑤𝐺 |
61 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑤𝑢 |
62 | 60, 61 | nffv 6781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑤(𝐺‘𝑢) |
63 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑤𝑏 |
64 | 62, 63 | nfeq 2922 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑤(𝐺‘𝑢) = 𝑏 |
65 | | nfv 1921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑢(𝐺‘𝑤) = 𝑏 |
66 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = 𝑤 → (𝐺‘𝑢) = (𝐺‘𝑤)) |
67 | 66 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = 𝑤 → ((𝐺‘𝑢) = 𝑏 ↔ (𝐺‘𝑤) = 𝑏)) |
68 | 64, 65, 67 | cbvrexw 3373 |
. . . . . . . . . . . . . . . . . . . . . . 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 5860 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑤ran
𝐺 |
73 | 72 | nfcri 2896 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤 𝑏 ∈ ran 𝐺 |
74 | 49, 73 | nfan 1906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤(𝜑 ∧ 𝑏 ∈ ran 𝐺) |
75 | | nfv 1921 |
. . . . . . . . . . . . . . . . . . . . 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 6883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑤 ∈ 𝑅 ∧ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
81 | 77, 79, 80 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐺‘𝑤) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
82 | 7 | sselda 3926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → 𝑤 ∈ 𝑉) |
83 | | stoweidlem31.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} |
84 | 83 | rabeq2i 3421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 12769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
90 | 87, 89 | rpdivcld 12788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (𝐸 / 𝑀) ∈
ℝ+) |
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐸 / 𝑀) ∈
ℝ+) |
92 | | breq2 5083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑒 = (𝐸 / 𝑀) → ((ℎ‘𝑡) < 𝑒 ↔ (ℎ‘𝑡) < (𝐸 / 𝑀))) |
93 | 92 | ralbidv 3123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑒 = (𝐸 / 𝑀) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ↔ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀))) |
94 | | oveq2 7279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑒 = (𝐸 / 𝑀) → (1 − 𝑒) = (1 − (𝐸 / 𝑀))) |
95 | 94 | breq1d 5089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑒 = (𝐸 / 𝑀) → ((1 − 𝑒) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) |
96 | 95 | ralbidv 3123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑒 = (𝐸 / 𝑀) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) |
97 | 93, 96 | 3anbi23d 1438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑒 = (𝐸 / 𝑀) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))) |
98 | 97 | rexbidv 3228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Ⅎℎ 𝑤 ∈ 𝑅 |
102 | 19, 101 | nfan 1906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
Ⅎℎ(𝜑 ∧ 𝑤 ∈ 𝑅) |
103 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Ⅎℎ∅ |
104 | 22, 103 | nfne 3047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
Ⅎℎ{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅ |
105 | | 3simpc 1149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → (ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))) |
106 | | rabid 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ↔ (ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))) |
107 | 105, 106 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑅) ∧ ℎ ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))) → ℎ ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
108 | | ne0i 4274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 3248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅)) |
112 | 100, 111 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ≠ ∅) |
113 | 81, 112 | eqnetrd 3013 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅) → (𝐺‘𝑤) ≠ ∅) |
114 | 113 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → (𝐺‘𝑤) ≠ ∅) |
115 | 76, 114 | eqnetrrd 3014 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → 𝑏 ≠ ∅) |
116 | 115 | 3adant1r 1176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑏 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑅 ∧ (𝐺‘𝑤) = 𝑏) → 𝑏 ≠ ∅) |
117 | 116 | 3exp 1118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (𝑤 ∈ 𝑅 → ((𝐺‘𝑤) = 𝑏 → 𝑏 ≠ ∅))) |
118 | 74, 75, 117 | rexlimd 3248 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → (∃𝑤 ∈ 𝑅 (𝐺‘𝑤) = 𝑏 → 𝑏 ≠ ∅)) |
119 | 71, 118 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ≠ ∅) |
120 | 119 | 3adant2 1130 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → 𝑏 ≠ ∅) |
121 | | rspa 3133 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑏 ∈
ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)) |
122 | 47, 120, 121 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑏) |
123 | 46, 122 | jca 512 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏)) |
124 | | vex 3435 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑏 ∈ V |
125 | 5 | elrnmpt 5864 |
. . . . . . . . . . . . . . . . . 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 1921 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑤(𝑙‘𝑏) ∈ 𝑏 |
129 | 73, 128 | nfan 1906 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑤(𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) ∈ 𝑏) |
130 | | nfv 1921 |
. . . . . . . . . . . . . . . . 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 2843 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑙‘𝑏) ∈ 𝑏 ∧ 𝑏 = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) → (𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
136 | | elrabi 3620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑙‘𝑏) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} → (𝑙‘𝑏) ∈ 𝐴) |
137 | | fveq1 6770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (ℎ = (𝑙‘𝑏) → (ℎ‘𝑡) = ((𝑙‘𝑏)‘𝑡)) |
138 | 137 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ℎ = (𝑙‘𝑏) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ ((𝑙‘𝑏)‘𝑡))) |
139 | 137 | breq1d 5089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ℎ = (𝑙‘𝑏) → ((ℎ‘𝑡) ≤ 1 ↔ ((𝑙‘𝑏)‘𝑡) ≤ 1)) |
140 | 138, 139 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℎ = (𝑙‘𝑏) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1))) |
141 | 140 | ralbidv 3123 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1))) |
142 | 137 | breq1d 5089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℎ = (𝑙‘𝑏) → ((ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀))) |
143 | 142 | ralbidv 3123 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀))) |
144 | 137 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℎ = (𝑙‘𝑏) → ((1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡))) |
145 | 144 | ralbidv 3123 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ = (𝑙‘𝑏) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡))) |
146 | 141, 143,
145 | 3anbi123d 1435 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ = (𝑙‘𝑏) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑙‘𝑏)‘𝑡) ∧ ((𝑙‘𝑏)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 ((𝑙‘𝑏)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < ((𝑙‘𝑏)‘𝑡)))) |
147 | 146 | elrab 3626 |
. . . . . . . . . . . . . . . . . . . . . . . 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 3626 |
. . . . . . . . . . . . . . . . . . . . . 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 2852 |
. . . . . . . . . . . . . . . . . . 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 3248 |
. . . . . . . . . . . . . . . 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 2842 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) ∧ 𝑏 ∈ ran 𝐺 ∧ (𝑙‘𝑏) = ℎ) → ℎ ∈ 𝑌) |
161 | 160 | 3exp 1118 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (𝑏 ∈ ran 𝐺 → ((𝑙‘𝑏) = ℎ → ℎ ∈ 𝑌))) |
162 | 40, 161 | reximdai 3242 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (∃𝑏 ∈ ran 𝐺(𝑙‘𝑏) = ℎ → ∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌)) |
163 | 33, 162 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → ∃𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌) |
164 | | nfv 1921 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏 ℎ ∈ 𝑌 |
165 | | idd 24 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ran 𝐺 → (ℎ ∈ 𝑌 → ℎ ∈ 𝑌)) |
166 | 165 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ ℎ ∈ ran 𝑙) → (𝑏 ∈ ran 𝐺 → (ℎ ∈ 𝑌 → ℎ ∈ 𝑌))) |
167 | 40, 164, 166 | rexlimd 3248 |
. . . . . . . . . 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 3142 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌) |
171 | | dfss3 3914 |
. . . . . . . 8
⊢ (ran
𝑙 ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌) |
172 | | nfrab1 3316 |
. . . . . . . . . . 11
⊢
Ⅎℎ{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
173 | 153, 172 | nfcxfr 2907 |
. . . . . . . . . 10
⊢
Ⅎℎ𝑌 |
174 | 173 | nfcri 2896 |
. . . . . . . . 9
⊢
Ⅎℎ 𝑧 ∈ 𝑌 |
175 | | nfv 1921 |
. . . . . . . . 9
⊢
Ⅎ𝑧 ℎ ∈ 𝑌 |
176 | | eleq1 2828 |
. . . . . . . . 9
⊢ (𝑧 = ℎ → (𝑧 ∈ 𝑌 ↔ ℎ ∈ 𝑌)) |
177 | 174, 175,
176 | cbvralw 3372 |
. . . . . . . 8
⊢
(∀𝑧 ∈
ran 𝑙 𝑧 ∈ 𝑌 ↔ ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌) |
178 | 171, 177 | bitri 274 |
. . . . . . 7
⊢ (ran
𝑙 ⊆ 𝑌 ↔ ∀ℎ ∈ ran 𝑙 ℎ ∈ 𝑌) |
179 | 170, 178 | sylibr 233 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ran 𝑙 ⊆ 𝑌) |
180 | | df-f 6436 |
. . . . . 6
⊢ (𝑙:ran 𝐺⟶𝑌 ↔ (𝑙 Fn ran 𝐺 ∧ ran 𝑙 ⊆ 𝑌)) |
181 | 18, 179, 180 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑙:ran 𝐺⟶𝑌) |
182 | | dffn3 6611 |
. . . . . . . 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 6714 |
. . . . . . . 8
⊢ (𝑣:(1...𝑀)–1-1-onto→𝑅 → 𝑣:(1...𝑀)⟶𝑅) |
187 | 185, 186 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑣:(1...𝑀)⟶𝑅) |
188 | 187 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → 𝑣:(1...𝑀)⟶𝑅) |
189 | | fco 6622 |
. . . . . 6
⊢ ((𝐺:𝑅⟶ran 𝐺 ∧ 𝑣:(1...𝑀)⟶𝑅) → (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺) |
190 | 184, 188,
189 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺) |
191 | | fco 6622 |
. . . . 5
⊢ ((𝑙:ran 𝐺⟶𝑌 ∧ (𝐺 ∘ 𝑣):(1...𝑀)⟶ran 𝐺) → (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌) |
192 | 181, 190,
191 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌) |
193 | | fvco3 6864 |
. . . . . . . . 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 6958 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) |
198 | | simp3 1137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) |
199 | | nfv 1921 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑏((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺 |
200 | 34, 36, 199 | nf3an 1908 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑏(𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) |
201 | | nfv 1921 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑏(𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖) |
202 | 200, 201 | nfim 1903 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)) |
203 | | eleq1 2828 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (𝑏 ∈ ran 𝐺 ↔ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺)) |
204 | 203 | 3anbi3d 1441 |
. . . . . . . . . . . 12
⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺))) |
205 | | fveq2 6771 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (𝑙‘𝑏) = (𝑙‘((𝐺 ∘ 𝑣)‘𝑖))) |
206 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → 𝑏 = ((𝐺 ∘ 𝑣)‘𝑖)) |
207 | 205, 206 | eleq12d 2835 |
. . . . . . . . . . . 12
⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → ((𝑙‘𝑏) ∈ 𝑏 ↔ (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖))) |
208 | 204, 207 | imbi12d 345 |
. . . . . . . . . . 11
⊢ (𝑏 = ((𝐺 ∘ 𝑣)‘𝑖) → (((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ 𝑏 ∈ ran 𝐺) → (𝑙‘𝑏) ∈ 𝑏) ↔ ((𝜑 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) ∧ ((𝐺 ∘ 𝑣)‘𝑖) ∈ ran 𝐺) → (𝑙‘((𝐺 ∘ 𝑣)‘𝑖)) ∈ ((𝐺 ∘ 𝑣)‘𝑖)))) |
209 | 202, 208,
122 | vtoclg1f 3503 |
. . . . . . . . . 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 2841 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖)) |
213 | | fvco3 6864 |
. . . . . . . . . . . 12
⊢ ((𝑣:(1...𝑀)⟶𝑅 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = (𝐺‘(𝑣‘𝑖))) |
214 | 187, 213 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = (𝐺‘(𝑣‘𝑖))) |
215 | | raleq 3341 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑣‘𝑖) → (∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀))) |
216 | 215 | 3anbi2d 1440 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑣‘𝑖) → ((∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)))) |
217 | 216 | rabbidv 3413 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑣‘𝑖) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
218 | 187 | ffvelrnda 6958 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑣‘𝑖) ∈ 𝑅) |
219 | 50 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐴 ∈ V) |
220 | | rabexg 5259 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ V → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V) |
221 | 219, 220 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} ∈ V) |
222 | 5, 217, 218, 221 | fvmptd3 6895 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝑣‘𝑖)) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
223 | 214, 222 | eqtrd 2780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
224 | 223 | adantlr 712 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝑣)‘𝑖) = {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
225 | 224 | eleq2d 2826 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ ((𝐺 ∘ 𝑣)‘𝑖) ↔ ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) ∈ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})) |
226 | | nfcv 2909 |
. . . . . . . . . . . . . 14
⊢
Ⅎℎ𝑣 |
227 | 24, 226 | nfco 5773 |
. . . . . . . . . . . . 13
⊢
Ⅎℎ(𝐺 ∘ 𝑣) |
228 | 20, 227 | nfco 5773 |
. . . . . . . . . . . 12
⊢
Ⅎℎ(𝑙 ∘ (𝐺 ∘ 𝑣)) |
229 | | nfcv 2909 |
. . . . . . . . . . . 12
⊢
Ⅎℎ𝑖 |
230 | 228, 229 | nffv 6781 |
. . . . . . . . . . 11
⊢
Ⅎℎ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) |
231 | | nfcv 2909 |
. . . . . . . . . . 11
⊢
Ⅎℎ𝐴 |
232 | | nfcv 2909 |
. . . . . . . . . . . . 13
⊢
Ⅎℎ𝑇 |
233 | | nfcv 2909 |
. . . . . . . . . . . . . . 15
⊢
Ⅎℎ0 |
234 | | nfcv 2909 |
. . . . . . . . . . . . . . 15
⊢
Ⅎℎ
≤ |
235 | | nfcv 2909 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎℎ𝑡 |
236 | 230, 235 | nffv 6781 |
. . . . . . . . . . . . . . 15
⊢
Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) |
237 | 233, 234,
236 | nfbr 5126 |
. . . . . . . . . . . . . 14
⊢
Ⅎℎ0 ≤
(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) |
238 | | nfcv 2909 |
. . . . . . . . . . . . . . 15
⊢
Ⅎℎ1 |
239 | 236, 234,
238 | nfbr 5126 |
. . . . . . . . . . . . . 14
⊢
Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1 |
240 | 237, 239 | nfan 1906 |
. . . . . . . . . . . . 13
⊢
Ⅎℎ(0 ≤
(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) |
241 | 232, 240 | nfralw 3152 |
. . . . . . . . . . . 12
⊢
Ⅎℎ∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) |
242 | | nfcv 2909 |
. . . . . . . . . . . . 13
⊢
Ⅎℎ(𝑣‘𝑖) |
243 | | nfcv 2909 |
. . . . . . . . . . . . . 14
⊢
Ⅎℎ
< |
244 | | nfcv 2909 |
. . . . . . . . . . . . . 14
⊢
Ⅎℎ(𝐸 / 𝑀) |
245 | 236, 243,
244 | nfbr 5126 |
. . . . . . . . . . . . 13
⊢
Ⅎℎ(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) |
246 | 242, 245 | nfralw 3152 |
. . . . . . . . . . . 12
⊢
Ⅎℎ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) |
247 | | nfcv 2909 |
. . . . . . . . . . . . 13
⊢
Ⅎℎ(𝑇 ∖ 𝑈) |
248 | | nfcv 2909 |
. . . . . . . . . . . . . 14
⊢
Ⅎℎ(1
− (𝐸 / 𝑀)) |
249 | 248, 243,
236 | nfbr 5126 |
. . . . . . . . . . . . 13
⊢
Ⅎℎ(1 −
(𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) |
250 | 247, 249 | nfralw 3152 |
. . . . . . . . . . . 12
⊢
Ⅎℎ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) |
251 | 241, 246,
250 | nf3an 1908 |
. . . . . . . . . . 11
⊢
Ⅎℎ(∀𝑡 ∈ 𝑇 (0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ∧ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)) |
252 | | nfcv 2909 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡ℎ |
253 | | nfcv 2909 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡𝑙 |
254 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡𝑅 |
255 | | nfra1 3145 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) |
256 | | nfra1 3145 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) |
257 | | nfra1 3145 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑡∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡) |
258 | 255, 256,
257 | nf3an 1908 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡(∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡)) |
259 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡𝐴 |
260 | 258, 259 | nfrabw 3317 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡{ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))} |
261 | 254, 260 | nfmpt 5186 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))}) |
262 | 5, 261 | nfcxfr 2907 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝐺 |
263 | | nfcv 2909 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝑣 |
264 | 262, 263 | nfco 5773 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡(𝐺 ∘ 𝑣) |
265 | 253, 264 | nfco 5773 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡(𝑙 ∘ (𝐺 ∘ 𝑣)) |
266 | | nfcv 2909 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡𝑖 |
267 | 265, 266 | nffv 6781 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) |
268 | 252, 267 | nfeq 2922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡 ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) |
269 | | fveq1 6770 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (ℎ‘𝑡) = (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)) |
270 | 269 | breq2d 5091 |
. . . . . . . . . . . . . 14
⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))) |
271 | 269 | breq1d 5089 |
. . . . . . . . . . . . . 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 5089 |
. . . . . . . . . . . . 13
⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → ((ℎ‘𝑡) < (𝐸 / 𝑀) ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))) |
275 | 268, 274 | ralbid 3161 |
. . . . . . . . . . . 12
⊢ (ℎ = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖) → (∀𝑡 ∈ (𝑣‘𝑖)(ℎ‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))) |
276 | 269 | breq2d 5091 |
. . . . . . . . . . . . 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 3622 |
. . . . . . . . . 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 5860 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡ran
𝐺 |
286 | 253, 285 | nffn 6530 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑙 Fn ran 𝐺 |
287 | | nfv 1921 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) |
288 | 285, 287 | nfralw 3152 |
. . . . . . . . . 10
⊢
Ⅎ𝑡∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏) |
289 | 286, 288 | nfan 1906 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏)) |
290 | 284, 289 | nfan 1906 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) |
291 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑖 ∈ (1...𝑀) |
292 | 290, 291 | nfan 1906 |
. . . . . . 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 3927 |
. . . . . . . . 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 3135 |
. . . . . . . . 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 3142 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)) |
304 | 283, 303 | jca 512 |
. . . . 5
⊢ (((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) ∧ 𝑖 ∈ (1...𝑀)) → (∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))) |
305 | 304 | ralrimiva 3110 |
. . . 4
⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))) |
306 | 192, 305 | jca 512 |
. . 3
⊢ ((𝜑 ∧ (𝑙 Fn ran 𝐺 ∧ ∀𝑏 ∈ ran 𝐺(𝑏 ≠ ∅ → (𝑙‘𝑏) ∈ 𝑏))) → ((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))) |
307 | | feq1 6579 |
. . . . 5
⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (𝑥:(1...𝑀)⟶𝑌 ↔ (𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌)) |
308 | | nfcv 2909 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝑥 |
309 | 308, 265 | nfeq 2922 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) |
310 | | fveq1 6770 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (𝑥‘𝑖) = ((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)) |
311 | 310 | fveq1d 6773 |
. . . . . . . . 9
⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((𝑥‘𝑖)‘𝑡) = (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)) |
312 | 311 | breq1d 5089 |
. . . . . . . 8
⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ↔ (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))) |
313 | 309, 312 | ralbid 3161 |
. . . . . . 7
⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ↔ ∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀))) |
314 | 311 | breq2d 5091 |
. . . . . . . 8
⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))) |
315 | 309, 314 | ralbid 3161 |
. . . . . . 7
⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡) ↔ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))) |
316 | 313, 315 | anbi12d 631 |
. . . . . 6
⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)) ↔ (∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))) |
317 | 316 | ralbidv 3123 |
. . . . 5
⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → (∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)) ↔ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡)))) |
318 | 307, 317 | anbi12d 631 |
. . . 4
⊢ (𝑥 = (𝑙 ∘ (𝐺 ∘ 𝑣)) → ((𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))) ↔ ((𝑙 ∘ (𝐺 ∘ 𝑣)):(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)(((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < (((𝑙 ∘ (𝐺 ∘ 𝑣))‘𝑖)‘𝑡))))) |
319 | 318 | spcegv 3535 |
. . 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 1942 |
1
⊢ (𝜑 → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡)))) |