Step | Hyp | Ref
| Expression |
1 | | stoweidlem39.8 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑟) |
2 | | stoweidlem39.9 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ≠ ∅) |
3 | 1, 2 | jca 553 |
. . . . . 6
⊢ (𝜑 → (𝐷 ⊆ ∪ 𝑟 ∧ 𝐷 ≠ ∅)) |
4 | | ssn0 3928 |
. . . . . 6
⊢ ((𝐷 ⊆ ∪ 𝑟
∧ 𝐷 ≠ ∅)
→ ∪ 𝑟 ≠ ∅) |
5 | | unieq 4380 |
. . . . . . . 8
⊢ (𝑟 = ∅ → ∪ 𝑟 =
∪ ∅) |
6 | | uni0 4401 |
. . . . . . . 8
⊢ ∪ ∅ = ∅ |
7 | 5, 6 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑟 = ∅ → ∪ 𝑟 =
∅) |
8 | 7 | necon3i 2814 |
. . . . . 6
⊢ (∪ 𝑟
≠ ∅ → 𝑟 ≠
∅) |
9 | 3, 4, 8 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝑟 ≠ ∅) |
10 | 9 | neneqd 2787 |
. . . 4
⊢ (𝜑 → ¬ 𝑟 = ∅) |
11 | | stoweidlem39.7 |
. . . . . 6
⊢ (𝜑 → 𝑟 ∈ (𝒫 𝑊 ∩ Fin)) |
12 | | elinel2 3762 |
. . . . . 6
⊢ (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ∈ Fin) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑟 ∈ Fin) |
14 | | fz1f1o 14288 |
. . . . 5
⊢ (𝑟 ∈ Fin → (𝑟 = ∅ ∨ ((#‘𝑟) ∈ ℕ ∧
∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto→𝑟))) |
15 | | pm2.53 387 |
. . . . 5
⊢ ((𝑟 = ∅ ∨ ((#‘𝑟) ∈ ℕ ∧
∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto→𝑟)) → (¬ 𝑟 = ∅ →
((#‘𝑟) ∈ ℕ
∧ ∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto→𝑟))) |
16 | 13, 14, 15 | 3syl 18 |
. . . 4
⊢ (𝜑 → (¬ 𝑟 = ∅ → ((#‘𝑟) ∈ ℕ ∧
∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto→𝑟))) |
17 | 10, 16 | mpd 15 |
. . 3
⊢ (𝜑 → ((#‘𝑟) ∈ ℕ ∧
∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto→𝑟)) |
18 | | oveq2 6557 |
. . . . . 6
⊢ (𝑚 = (#‘𝑟) → (1...𝑚) = (1...(#‘𝑟))) |
19 | | f1oeq2 6041 |
. . . . . 6
⊢
((1...𝑚) =
(1...(#‘𝑟)) →
(𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ 𝑣:(1...(#‘𝑟))–1-1-onto→𝑟)) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (𝑚 = (#‘𝑟) → (𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ 𝑣:(1...(#‘𝑟))–1-1-onto→𝑟)) |
21 | 20 | exbidv 1837 |
. . . 4
⊢ (𝑚 = (#‘𝑟) → (∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ ∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto→𝑟)) |
22 | 21 | rspcev 3282 |
. . 3
⊢
(((#‘𝑟) ∈
ℕ ∧ ∃𝑣
𝑣:(1...(#‘𝑟))–1-1-onto→𝑟) → ∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟) |
23 | 17, 22 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟) |
24 | | f1of 6050 |
. . . . . . . 8
⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 → 𝑣:(1...𝑚)⟶𝑟) |
25 | 24 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑣:(1...𝑚)⟶𝑟) |
26 | | simpll 786 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝜑) |
27 | | elinel1 3761 |
. . . . . . . . 9
⊢ (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ∈ 𝒫 𝑊) |
28 | 27 | elpwid 4118 |
. . . . . . . 8
⊢ (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ⊆ 𝑊) |
29 | 26, 11, 28 | 3syl 18 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑟 ⊆ 𝑊) |
30 | 25, 29 | fssd 5970 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑣:(1...𝑚)⟶𝑊) |
31 | 1 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐷 ⊆ ∪ 𝑟) |
32 | | dff1o2 6055 |
. . . . . . . . . 10
⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ (𝑣 Fn (1...𝑚) ∧ Fun ◡𝑣 ∧ ran 𝑣 = 𝑟)) |
33 | 32 | simp3bi 1071 |
. . . . . . . . 9
⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 → ran 𝑣 = 𝑟) |
34 | 33 | unieqd 4382 |
. . . . . . . 8
⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 → ∪ ran 𝑣 = ∪ 𝑟) |
35 | 34 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → ∪ ran 𝑣 = ∪ 𝑟) |
36 | 31, 35 | sseqtr4d 3605 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐷 ⊆ ∪ ran
𝑣) |
37 | | stoweidlem39.1 |
. . . . . . . . 9
⊢
Ⅎℎ𝜑 |
38 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎℎ 𝑚 ∈ ℕ |
39 | 37, 38 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎℎ(𝜑 ∧ 𝑚 ∈ ℕ) |
40 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎℎ 𝑣:(1...𝑚)–1-1-onto→𝑟 |
41 | 39, 40 | nfan 1816 |
. . . . . . 7
⊢
Ⅎℎ((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) |
42 | | stoweidlem39.2 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝜑 |
43 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑡 𝑚 ∈ ℕ |
44 | 42, 43 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝜑 ∧ 𝑚 ∈ ℕ) |
45 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑣:(1...𝑚)–1-1-onto→𝑟 |
46 | 44, 45 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑡((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) |
47 | | stoweidlem39.3 |
. . . . . . . . 9
⊢
Ⅎ𝑤𝜑 |
48 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑚 ∈ ℕ |
49 | 47, 48 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑤(𝜑 ∧ 𝑚 ∈ ℕ) |
50 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑤 𝑣:(1...𝑚)–1-1-onto→𝑟 |
51 | 49, 50 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑤((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) |
52 | | stoweidlem39.5 |
. . . . . . 7
⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
53 | | stoweidlem39.6 |
. . . . . . 7
⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} |
54 | | eqid 2610 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) = (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) |
55 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑚 ∈ ℕ) |
56 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑣:(1...𝑚)–1-1-onto→𝑟) |
57 | | stoweidlem39.10 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
58 | 57 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐸 ∈
ℝ+) |
59 | | stoweidlem39.11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ⊆ 𝑇) |
60 | 59 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝑇) |
61 | | notnot 135 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ 𝐵 → ¬ ¬ 𝑏 ∈ 𝐵) |
62 | 61 | intnand 953 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝐵 → ¬ (𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵)) |
63 | 62 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵)) |
64 | | eldif 3550 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (𝑇 ∖ 𝐵) ↔ (𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵)) |
65 | 63, 64 | sylnibr 318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ (𝑇 ∖ 𝐵)) |
66 | | stoweidlem39.4 |
. . . . . . . . . . . . 13
⊢ 𝑈 = (𝑇 ∖ 𝐵) |
67 | 66 | eleq2i 2680 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ (𝑇 ∖ 𝐵)) |
68 | 65, 67 | sylnibr 318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝑈) |
69 | 60, 68 | eldifd 3551 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ (𝑇 ∖ 𝑈)) |
70 | 69 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑏 ∈ 𝐵 𝑏 ∈ (𝑇 ∖ 𝑈)) |
71 | | dfss3 3558 |
. . . . . . . . 9
⊢ (𝐵 ⊆ (𝑇 ∖ 𝑈) ↔ ∀𝑏 ∈ 𝐵 𝑏 ∈ (𝑇 ∖ 𝑈)) |
72 | 70, 71 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ (𝑇 ∖ 𝑈)) |
73 | 72 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐵 ⊆ (𝑇 ∖ 𝑈)) |
74 | | stoweidlem39.12 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ V) |
75 | 74 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑊 ∈ V) |
76 | | stoweidlem39.13 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ V) |
77 | 76 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐴 ∈ V) |
78 | 13 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑟 ∈ Fin) |
79 | | mptfi 8148 |
. . . . . . . 8
⊢ (𝑟 ∈ Fin → (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin) |
80 | | rnfi 8132 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin → ran (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin) |
81 | 78, 79, 80 | 3syl 18 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → ran (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin) |
82 | 41, 46, 51, 52, 53, 54, 29, 55, 56, 58, 73, 75, 77, 81 | stoweidlem31 38924 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))) |
83 | 30, 36, 82 | 3jca 1235 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → (𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡))))) |
84 | 83 | ex 449 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑣:(1...𝑚)–1-1-onto→𝑟 → (𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))) |
85 | 84 | eximdv 1833 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟 → ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))) |
86 | 85 | reximdva 3000 |
. 2
⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))) |
87 | 23, 86 | mpd 15 |
1
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡))))) |