Step | Hyp | Ref
| Expression |
1 | | stoweidlem35.8 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | stoweidlem35.6 |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
3 | 2 | rnmptfi 42380 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Fin → ran 𝐺 ∈ Fin) |
4 | 1, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
5 | | fnchoice 42245 |
. . . . . . . . . . 11
⊢ (ran
𝐺 ∈ Fin →
∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) |
6 | 5 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) |
7 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → 𝑔 Fn ran 𝐺) |
8 | | stoweidlem35.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤𝜑 |
9 | | nfmpt1 5153 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑤(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
10 | 2, 9 | nfcxfr 2902 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑤𝐺 |
11 | 10 | nfrn 5821 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤ran
𝐺 |
12 | 11 | nfcri 2891 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤 𝑘 ∈ ran 𝐺 |
13 | 8, 12 | nfan 1907 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑤(𝜑 ∧ 𝑘 ∈ ran 𝐺) |
14 | | stoweidlem35.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑋 ⊆ 𝑊) |
15 | 14 | sselda 3901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑊) |
16 | | stoweidlem35.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
17 | 15, 16 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
18 | | rabid 3290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (𝑤 ∈ 𝐽 ∧ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
19 | 17, 18 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝑤 ∈ 𝐽 ∧ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
20 | 19 | simprd 499 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}) |
21 | | df-rex 3067 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∃ℎ ∈
𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
22 | 20, 21 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
23 | | rabid 3290 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
24 | 23 | exbii 1855 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
25 | 22, 24 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
26 | 25 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
27 | | stoweidlem35.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ𝜑 |
28 | | nfv 1922 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ 𝑤 ∈ 𝑋 |
29 | 27, 28 | nfan 1907 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎℎ(𝜑 ∧ 𝑤 ∈ 𝑋) |
30 | | nfrab1 3296 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ{ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
31 | 30 | nfeq2 2921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎℎ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
32 | 29, 31 | nfan 1907 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎℎ((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
33 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → (ℎ ∈ 𝑘 ↔ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
34 | 33 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ℎ ∈ 𝑘)) |
35 | 34 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ℎ ∈ 𝑘)) |
36 | 32, 35 | eximd 2214 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ∃ℎ ℎ ∈ 𝑘)) |
37 | 26, 36 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ 𝑘) |
38 | 37 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ 𝑘) |
39 | 2 | elrnmpt 5825 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ran 𝐺 → (𝑘 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
40 | 39 | ibi 270 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ran 𝐺 → ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
41 | 40 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
42 | 13, 38, 41 | r19.29af 3249 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → ∃ℎ ℎ ∈ 𝑘) |
43 | | n0 4261 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ≠ ∅ ↔
∃ℎ ℎ ∈ 𝑘) |
44 | 42, 43 | sylibr 237 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅) |
45 | 44 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅) |
46 | | simplrr 778 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) |
47 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑘 → (𝑙 ≠ ∅ ↔ 𝑘 ≠ ∅)) |
48 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 = 𝑘 → (𝑔‘𝑙) = (𝑔‘𝑘)) |
49 | 48 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑙) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑙)) |
50 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑘) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑘)) |
51 | 49, 50 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑙) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑘)) |
52 | 47, 51 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑘 → ((𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙) ↔ (𝑘 ≠ ∅ → (𝑔‘𝑘) ∈ 𝑘))) |
53 | 52 | rspccva 3536 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑙 ∈
ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔‘𝑘) ∈ 𝑘)) |
54 | 46, 53 | sylancom 591 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔‘𝑘) ∈ 𝑘)) |
55 | 45, 54 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
56 | 55 | ralrimiva 3105 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → ∀𝑘 ∈ ran 𝐺(𝑔‘𝑘) ∈ 𝑘) |
57 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑙 → (𝑔‘𝑘) = (𝑔‘𝑙)) |
58 | 57 | eleq1d 2822 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑘) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑘)) |
59 | | eleq2 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑙) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑙)) |
60 | 58, 59 | bitrd 282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑘) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑙)) |
61 | 60 | cbvralvw 3358 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
ran 𝐺(𝑔‘𝑘) ∈ 𝑘 ↔ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
62 | 56, 61 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
63 | 7, 62 | jca 515 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
64 | 63 | ex 416 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
65 | 64 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
66 | 65 | eximdv 1925 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
67 | 6, 66 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
68 | 4, 67 | mpdan 687 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
69 | 68 | ralrimivw 3106 |
. . . . . . 7
⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
70 | | stoweidlem35.10 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋) |
71 | | stoweidlem35.11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ∖ 𝑈) ≠ ∅) |
72 | | ssn0 4315 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∖ 𝑈) ⊆ ∪ 𝑋 ∧ (𝑇 ∖ 𝑈) ≠ ∅) → ∪ 𝑋
≠ ∅) |
73 | 70, 71, 72 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑋
≠ ∅) |
74 | 73 | neneqd 2945 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ ∪ 𝑋 =
∅) |
75 | | unieq 4830 |
. . . . . . . . . . . 12
⊢ (𝑋 = ∅ → ∪ 𝑋 =
∪ ∅) |
76 | | uni0 4849 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
77 | 75, 76 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → ∪ 𝑋 =
∅) |
78 | 74, 77 | nsyl 142 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 = ∅) |
79 | | dm0rn0 5794 |
. . . . . . . . . . 11
⊢ (dom
𝐺 = ∅ ↔ ran
𝐺 =
∅) |
80 | | stoweidlem35.4 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
81 | | stoweidlem35.7 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ V) |
82 | 80, 81 | rabexd 5226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑄 ∈ V) |
83 | | nfrab1 3296 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎℎ{ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
84 | 80, 83 | nfcxfr 2902 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎℎ𝑄 |
85 | 84 | rabexgf 42240 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ∈ V → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
86 | 82, 85 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
87 | 86 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
88 | 8, 87, 2 | fmptdf 6934 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑋⟶V) |
89 | | dffn2 6547 |
. . . . . . . . . . . . . 14
⊢ (𝐺 Fn 𝑋 ↔ 𝐺:𝑋⟶V) |
90 | 88, 89 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 Fn 𝑋) |
91 | 90 | fndmd 6483 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐺 = 𝑋) |
92 | 91 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝜑 → (dom 𝐺 = ∅ ↔ 𝑋 = ∅)) |
93 | 79, 92 | bitr3id 288 |
. . . . . . . . . 10
⊢ (𝜑 → (ran 𝐺 = ∅ ↔ 𝑋 = ∅)) |
94 | 78, 93 | mtbird 328 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ran 𝐺 = ∅) |
95 | | fz1f1o 15274 |
. . . . . . . . . . 11
⊢ (ran
𝐺 ∈ Fin → (ran
𝐺 = ∅ ∨
((♯‘ran 𝐺)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺))) |
96 | 4, 95 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ran 𝐺 = ∅ ∨ ((♯‘ran 𝐺) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺))) |
97 | 96 | ord 864 |
. . . . . . . . 9
⊢ (𝜑 → (¬ ran 𝐺 = ∅ →
((♯‘ran 𝐺)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺))) |
98 | 94, 97 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘ran 𝐺) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺)) |
99 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑚 = (♯‘ran 𝐺) → (1...𝑚) = (1...(♯‘ran 𝐺))) |
100 | 99 | f1oeq2d 6657 |
. . . . . . . . . 10
⊢ (𝑚 = (♯‘ran 𝐺) → (𝑓:(1...𝑚)–1-1-onto→ran
𝐺 ↔ 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺)) |
101 | 100 | exbidv 1929 |
. . . . . . . . 9
⊢ (𝑚 = (♯‘ran 𝐺) → (∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 ↔ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺)) |
102 | 101 | rspcev 3537 |
. . . . . . . 8
⊢
(((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺) → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
103 | 98, 102 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
104 | | r19.29 3176 |
. . . . . . 7
⊢
((∀𝑚 ∈
ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
105 | 69, 103, 104 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
106 | | exdistrv 1964 |
. . . . . . . . 9
⊢
(∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
107 | 106 | biimpri 231 |
. . . . . . . 8
⊢
((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
108 | 107 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
109 | 108 | reximdv 3192 |
. . . . . 6
⊢ (𝜑 → (∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑚 ∈ ℕ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
110 | 105, 109 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
111 | | df-rex 3067 |
. . . . 5
⊢
(∃𝑚 ∈
ℕ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
112 | 110, 111 | sylib 221 |
. . . 4
⊢ (𝜑 → ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
113 | | ax-5 1918 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ →
∀𝑔 𝑚 ∈
ℕ) |
114 | | 19.29 1881 |
. . . . . . . . 9
⊢
((∀𝑔 𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
115 | 113, 114 | sylan 583 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
116 | | ax-5 1918 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ →
∀𝑓 𝑚 ∈
ℕ) |
117 | | 19.29 1881 |
. . . . . . . . . 10
⊢
((∀𝑓 𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
118 | 116, 117 | sylan 583 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
119 | 118 | eximi 1842 |
. . . . . . . 8
⊢
(∃𝑔(𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
120 | 115, 119 | syl 17 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
121 | | df-3an 1091 |
. . . . . . . . 9
⊢ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
122 | 121 | anbi2i 626 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) ↔ (𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
123 | 122 | 2exbii 1856 |
. . . . . . 7
⊢
(∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) ↔ ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
124 | 120, 123 | sylibr 237 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
125 | 124 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)))) |
126 | 125 | eximdv 1925 |
. . . 4
⊢ (𝜑 → (∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑚∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)))) |
127 | 112, 126 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑚∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
128 | 82 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑄 ∈ V) |
129 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑚 ∈
ℕ) |
130 | | simprr1 1223 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑔 Fn ran 𝐺) |
131 | | elex 3426 |
. . . . . . . . 9
⊢ (ran
𝐺 ∈ Fin → ran
𝐺 ∈
V) |
132 | 4, 131 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐺 ∈ V) |
133 | 132 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ran 𝐺 ∈ V) |
134 | | simprr2 1224 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
135 | 51 | rspccva 3536 |
. . . . . . . 8
⊢
((∀𝑙 ∈
ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
136 | 134, 135 | sylan 583 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
137 | | simprr3 1225 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
138 | 70 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋) |
139 | | stoweidlem35.1 |
. . . . . . . 8
⊢
Ⅎ𝑡𝜑 |
140 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑡 𝑚 ∈ ℕ |
141 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑔 |
142 | | nfcv 2904 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡𝑋 |
143 | | nfrab1 3296 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} |
144 | 143 | nfeq2 2921 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} |
145 | | nfv 1922 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(ℎ‘𝑍) = 0 |
146 | | nfra1 3140 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) |
147 | 145, 146 | nfan 1907 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)) |
148 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝐴 |
149 | 147, 148 | nfrabw 3297 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡{ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
150 | 80, 149 | nfcxfr 2902 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡𝑄 |
151 | 144, 150 | nfrabw 3297 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡{ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
152 | 142, 151 | nfmpt 5152 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
153 | 2, 152 | nfcxfr 2902 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝐺 |
154 | 153 | nfrn 5821 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡ran
𝐺 |
155 | 141, 154 | nffn 6478 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑔 Fn ran 𝐺 |
156 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝑔‘𝑙) ∈ 𝑙 |
157 | 154, 156 | nfralw 3147 |
. . . . . . . . . 10
⊢
Ⅎ𝑡∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 |
158 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑓 |
159 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(1...𝑚) |
160 | 158, 159,
154 | nff1o 6659 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 |
161 | 155, 157,
160 | nf3an 1909 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
162 | 140, 161 | nfan 1907 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
163 | 139, 162 | nfan 1907 |
. . . . . . 7
⊢
Ⅎ𝑡(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
164 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑚 ∈ ℕ |
165 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤𝑔 |
166 | 165, 11 | nffn 6478 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 𝑔 Fn ran 𝐺 |
167 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤(𝑔‘𝑙) ∈ 𝑙 |
168 | 11, 167 | nfralw 3147 |
. . . . . . . . . 10
⊢
Ⅎ𝑤∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 |
169 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤𝑓 |
170 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤(1...𝑚) |
171 | 169, 170,
11 | nff1o 6659 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 |
172 | 166, 168,
171 | nf3an 1909 |
. . . . . . . . 9
⊢
Ⅎ𝑤(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
173 | 164, 172 | nfan 1907 |
. . . . . . . 8
⊢
Ⅎ𝑤(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
174 | 8, 173 | nfan 1907 |
. . . . . . 7
⊢
Ⅎ𝑤(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
175 | 2, 128, 129, 130, 133, 136, 137, 138, 163, 174, 84 | stoweidlem27 43243 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
176 | 175 | ex 416 |
. . . . 5
⊢ (𝜑 → ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
177 | 176 | 2eximdv 1927 |
. . . 4
⊢ (𝜑 → (∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
178 | 177 | eximdv 1925 |
. . 3
⊢ (𝜑 → (∃𝑚∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑚∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
179 | 127, 178 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑚∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
180 | | id 22 |
. . . 4
⊢
(∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
181 | 180 | exlimivv 1940 |
. . 3
⊢
(∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
182 | 181 | eximi 1842 |
. 2
⊢
(∃𝑚∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑚∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
183 | 179, 182 | syl 17 |
1
⊢ (𝜑 → ∃𝑚∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |