Step | Hyp | Ref
| Expression |
1 | | stoweidlem39.8 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑟) |
2 | | stoweidlem39.9 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ≠ ∅) |
3 | 1, 2 | jca 515 |
. . . . . 6
⊢ (𝜑 → (𝐷 ⊆ ∪ 𝑟 ∧ 𝐷 ≠ ∅)) |
4 | | ssn0 4315 |
. . . . . 6
⊢ ((𝐷 ⊆ ∪ 𝑟
∧ 𝐷 ≠ ∅)
→ ∪ 𝑟 ≠ ∅) |
5 | | unieq 4830 |
. . . . . . . 8
⊢ (𝑟 = ∅ → ∪ 𝑟 =
∪ ∅) |
6 | | uni0 4849 |
. . . . . . . 8
⊢ ∪ ∅ = ∅ |
7 | 5, 6 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑟 = ∅ → ∪ 𝑟 =
∅) |
8 | 7 | necon3i 2973 |
. . . . . 6
⊢ (∪ 𝑟
≠ ∅ → 𝑟 ≠
∅) |
9 | 3, 4, 8 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝑟 ≠ ∅) |
10 | 9 | neneqd 2945 |
. . . 4
⊢ (𝜑 → ¬ 𝑟 = ∅) |
11 | | stoweidlem39.7 |
. . . . . 6
⊢ (𝜑 → 𝑟 ∈ (𝒫 𝑊 ∩ Fin)) |
12 | | elinel2 4110 |
. . . . . 6
⊢ (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ∈ Fin) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑟 ∈ Fin) |
14 | | fz1f1o 15274 |
. . . . 5
⊢ (𝑟 ∈ Fin → (𝑟 = ∅ ∨
((♯‘𝑟) ∈
ℕ ∧ ∃𝑣
𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟))) |
15 | | pm2.53 851 |
. . . . 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 7221 |
. . . . . 6
⊢ (𝑚 = (♯‘𝑟) → (1...𝑚) = (1...(♯‘𝑟))) |
19 | 18 | f1oeq2d 6657 |
. . . . 5
⊢ (𝑚 = (♯‘𝑟) → (𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟)) |
20 | 19 | exbidv 1929 |
. . . 4
⊢ (𝑚 = (♯‘𝑟) → (∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟)) |
21 | 20 | rspcev 3537 |
. . 3
⊢
(((♯‘𝑟)
∈ ℕ ∧ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto→𝑟) → ∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟) |
22 | 17, 21 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟) |
23 | | f1of 6661 |
. . . . . . . 8
⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 → 𝑣:(1...𝑚)⟶𝑟) |
24 | 23 | adantl 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑣:(1...𝑚)⟶𝑟) |
25 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝜑) |
26 | | elinel1 4109 |
. . . . . . . . 9
⊢ (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ∈ 𝒫 𝑊) |
27 | 26 | elpwid 4524 |
. . . . . . . 8
⊢ (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ⊆ 𝑊) |
28 | 25, 11, 27 | 3syl 18 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑟 ⊆ 𝑊) |
29 | 24, 28 | fssd 6563 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑣:(1...𝑚)⟶𝑊) |
30 | 1 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐷 ⊆ ∪ 𝑟) |
31 | | dff1o2 6666 |
. . . . . . . . . 10
⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 ↔ (𝑣 Fn (1...𝑚) ∧ Fun ◡𝑣 ∧ ran 𝑣 = 𝑟)) |
32 | 31 | simp3bi 1149 |
. . . . . . . . 9
⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 → ran 𝑣 = 𝑟) |
33 | 32 | unieqd 4833 |
. . . . . . . 8
⊢ (𝑣:(1...𝑚)–1-1-onto→𝑟 → ∪ ran 𝑣 = ∪ 𝑟) |
34 | 33 | adantl 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → ∪ ran 𝑣 = ∪ 𝑟) |
35 | 30, 34 | sseqtrrd 3942 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐷 ⊆ ∪ ran
𝑣) |
36 | | stoweidlem39.1 |
. . . . . . . . 9
⊢
Ⅎℎ𝜑 |
37 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎℎ 𝑚 ∈ ℕ |
38 | 36, 37 | nfan 1907 |
. . . . . . . 8
⊢
Ⅎℎ(𝜑 ∧ 𝑚 ∈ ℕ) |
39 | | nfv 1922 |
. . . . . . . 8
⊢
Ⅎℎ 𝑣:(1...𝑚)–1-1-onto→𝑟 |
40 | 38, 39 | nfan 1907 |
. . . . . . 7
⊢
Ⅎℎ((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) |
41 | | stoweidlem39.2 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝜑 |
42 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑡 𝑚 ∈ ℕ |
43 | 41, 42 | nfan 1907 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝜑 ∧ 𝑚 ∈ ℕ) |
44 | | nfv 1922 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑣:(1...𝑚)–1-1-onto→𝑟 |
45 | 43, 44 | nfan 1907 |
. . . . . . 7
⊢
Ⅎ𝑡((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) |
46 | | stoweidlem39.3 |
. . . . . . . . 9
⊢
Ⅎ𝑤𝜑 |
47 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑚 ∈ ℕ |
48 | 46, 47 | nfan 1907 |
. . . . . . . 8
⊢
Ⅎ𝑤(𝜑 ∧ 𝑚 ∈ ℕ) |
49 | | nfv 1922 |
. . . . . . . 8
⊢
Ⅎ𝑤 𝑣:(1...𝑚)–1-1-onto→𝑟 |
50 | 48, 49 | nfan 1907 |
. . . . . . 7
⊢
Ⅎ𝑤((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) |
51 | | stoweidlem39.5 |
. . . . . . 7
⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
52 | | stoweidlem39.6 |
. . . . . . 7
⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} |
53 | | eqid 2737 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) = (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) |
54 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑚 ∈ ℕ) |
55 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑣:(1...𝑚)–1-1-onto→𝑟) |
56 | | stoweidlem39.10 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
57 | 56 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐸 ∈
ℝ+) |
58 | | stoweidlem39.11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ⊆ 𝑇) |
59 | 58 | sselda 3901 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝑇) |
60 | | notnot 144 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ 𝐵 → ¬ ¬ 𝑏 ∈ 𝐵) |
61 | 60 | intnand 492 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝐵 → ¬ (𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵)) |
62 | 61 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵)) |
63 | | eldif 3876 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (𝑇 ∖ 𝐵) ↔ (𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵)) |
64 | 62, 63 | sylnibr 332 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ (𝑇 ∖ 𝐵)) |
65 | | stoweidlem39.4 |
. . . . . . . . . . . . 13
⊢ 𝑈 = (𝑇 ∖ 𝐵) |
66 | 65 | eleq2i 2829 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ (𝑇 ∖ 𝐵)) |
67 | 64, 66 | sylnibr 332 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝑈) |
68 | 59, 67 | eldifd 3877 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ (𝑇 ∖ 𝑈)) |
69 | 68 | ralrimiva 3105 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑏 ∈ 𝐵 𝑏 ∈ (𝑇 ∖ 𝑈)) |
70 | | dfss3 3888 |
. . . . . . . . 9
⊢ (𝐵 ⊆ (𝑇 ∖ 𝑈) ↔ ∀𝑏 ∈ 𝐵 𝑏 ∈ (𝑇 ∖ 𝑈)) |
71 | 69, 70 | sylibr 237 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ (𝑇 ∖ 𝑈)) |
72 | 71 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐵 ⊆ (𝑇 ∖ 𝑈)) |
73 | | stoweidlem39.12 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ V) |
74 | 73 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑊 ∈ V) |
75 | | stoweidlem39.13 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ V) |
76 | 75 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝐴 ∈ V) |
77 | 13 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → 𝑟 ∈ Fin) |
78 | | mptfi 8975 |
. . . . . . . 8
⊢ (𝑟 ∈ Fin → (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin) |
79 | | rnfi 8959 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin → ran (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin) |
80 | 77, 78, 79 | 3syl 18 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → ran (𝑤 ∈ 𝑟 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑚)) < (ℎ‘𝑡))}) ∈ Fin) |
81 | 40, 45, 50, 51, 52, 53, 28, 54, 55, 57, 72, 74, 76, 80 | stoweidlem31 43247 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))) |
82 | 29, 35, 81 | 3jca 1130 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto→𝑟) → (𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡))))) |
83 | 82 | ex 416 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑣:(1...𝑚)–1-1-onto→𝑟 → (𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))) |
84 | 83 | eximdv 1925 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟 → ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))) |
85 | 84 | reximdva 3193 |
. 2
⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto→𝑟 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))) |
86 | 22, 85 | mpd 15 |
1
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡))))) |