Step | Hyp | Ref
| Expression |
1 | | stoweidlem35.8 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | stoweidlem35.6 |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
3 | 2 | rnmptfi 40920 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Fin → ran 𝐺 ∈ Fin) |
4 | 1, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
5 | | fnchoice 40777 |
. . . . . . . . . . 11
⊢ (ran
𝐺 ∈ Fin →
∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) |
6 | 5 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) |
7 | | simprl 767 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → 𝑔 Fn ran 𝐺) |
8 | | stoweidlem35.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤𝜑 |
9 | | nfmpt1 5052 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑤(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
10 | 2, 9 | nfcxfr 2945 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑤𝐺 |
11 | 10 | nfrn 5698 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤ran
𝐺 |
12 | 11 | nfcri 2941 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤 𝑘 ∈ ran 𝐺 |
13 | 8, 12 | nfan 1879 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑤(𝜑 ∧ 𝑘 ∈ ran 𝐺) |
14 | | stoweidlem35.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑋 ⊆ 𝑊) |
15 | 14 | sselda 3884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑊) |
16 | | stoweidlem35.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
17 | 15, 16 | syl6eleq 2891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
18 | | rabid 3334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (𝑤 ∈ 𝐽 ∧ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
19 | 17, 18 | sylib 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝑤 ∈ 𝐽 ∧ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
20 | 19 | simprd 496 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}) |
21 | | df-rex 3109 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∃ℎ ∈
𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
22 | 20, 21 | sylib 219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
23 | | rabid 3334 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
24 | 23 | exbii 1827 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
25 | 22, 24 | sylibr 235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
27 | | stoweidlem35.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ𝜑 |
28 | | nfv 1890 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ 𝑤 ∈ 𝑋 |
29 | 27, 28 | nfan 1879 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎℎ(𝜑 ∧ 𝑤 ∈ 𝑋) |
30 | | nfrab1 3341 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ{ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
31 | 30 | nfeq2 2962 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎℎ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
32 | 29, 31 | nfan 1879 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎℎ((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
33 | | eleq2 2869 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → (ℎ ∈ 𝑘 ↔ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
34 | 33 | biimprd 249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ℎ ∈ 𝑘)) |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ℎ ∈ 𝑘)) |
36 | 32, 35 | eximd 2179 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ∃ℎ ℎ ∈ 𝑘)) |
37 | 26, 36 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ 𝑘) |
38 | 37 | adantllr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ 𝑘) |
39 | 2 | elrnmpt 5702 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ran 𝐺 → (𝑘 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
40 | 39 | ibi 268 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ran 𝐺 → ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
41 | 40 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
42 | 13, 38, 41 | r19.29af 3289 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → ∃ℎ ℎ ∈ 𝑘) |
43 | | n0 4224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ≠ ∅ ↔
∃ℎ ℎ ∈ 𝑘) |
44 | 42, 43 | sylibr 235 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅) |
45 | 44 | adantlr 711 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅) |
46 | | simplrr 774 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) |
47 | | neeq1 3044 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑘 → (𝑙 ≠ ∅ ↔ 𝑘 ≠ ∅)) |
48 | | fveq2 6530 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 = 𝑘 → (𝑔‘𝑙) = (𝑔‘𝑘)) |
49 | 48 | eleq1d 2865 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑙) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑙)) |
50 | | eleq2 2869 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑘) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑘)) |
51 | 49, 50 | bitrd 280 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑙) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑘)) |
52 | 47, 51 | imbi12d 346 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑘 → ((𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙) ↔ (𝑘 ≠ ∅ → (𝑔‘𝑘) ∈ 𝑘))) |
53 | 52 | rspccva 3553 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑙 ∈
ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔‘𝑘) ∈ 𝑘)) |
54 | 46, 53 | sylancom 588 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔‘𝑘) ∈ 𝑘)) |
55 | 45, 54 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
56 | 55 | ralrimiva 3147 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → ∀𝑘 ∈ ran 𝐺(𝑔‘𝑘) ∈ 𝑘) |
57 | | fveq2 6530 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑙 → (𝑔‘𝑘) = (𝑔‘𝑙)) |
58 | 57 | eleq1d 2865 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑘) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑘)) |
59 | | eleq2 2869 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑙) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑙)) |
60 | 58, 59 | bitrd 280 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑘) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑙)) |
61 | 60 | cbvralv 3400 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
ran 𝐺(𝑔‘𝑘) ∈ 𝑘 ↔ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
62 | 56, 61 | sylib 219 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
63 | 7, 62 | jca 512 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
64 | 63 | ex 413 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
65 | 64 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
66 | 65 | eximdv 1893 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
67 | 6, 66 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
68 | 4, 67 | mpdan 683 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
69 | 68 | ralrimivw 3148 |
. . . . . . 7
⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
70 | | stoweidlem35.10 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋) |
71 | | stoweidlem35.11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ∖ 𝑈) ≠ ∅) |
72 | | ssn0 4268 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∖ 𝑈) ⊆ ∪ 𝑋 ∧ (𝑇 ∖ 𝑈) ≠ ∅) → ∪ 𝑋
≠ ∅) |
73 | 70, 71, 72 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑋
≠ ∅) |
74 | 73 | neneqd 2987 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ ∪ 𝑋 =
∅) |
75 | | unieq 4747 |
. . . . . . . . . . . 12
⊢ (𝑋 = ∅ → ∪ 𝑋 =
∪ ∅) |
76 | | uni0 4766 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
77 | 75, 76 | syl6eq 2845 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → ∪ 𝑋 =
∅) |
78 | 74, 77 | nsyl 142 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 = ∅) |
79 | | dm0rn0 5671 |
. . . . . . . . . . 11
⊢ (dom
𝐺 = ∅ ↔ ran
𝐺 =
∅) |
80 | | stoweidlem35.4 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
81 | | stoweidlem35.7 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ V) |
82 | 80, 81 | rabexd 5120 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑄 ∈ V) |
83 | | nfrab1 3341 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎℎ{ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
84 | 80, 83 | nfcxfr 2945 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎℎ𝑄 |
85 | 84 | rabexgf 40772 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ∈ V → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
86 | 82, 85 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
87 | 86 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
88 | 8, 87, 2 | fmptdf 6735 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑋⟶V) |
89 | | dffn2 6376 |
. . . . . . . . . . . . . 14
⊢ (𝐺 Fn 𝑋 ↔ 𝐺:𝑋⟶V) |
90 | 88, 89 | sylibr 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 Fn 𝑋) |
91 | | fndm 6317 |
. . . . . . . . . . . . 13
⊢ (𝐺 Fn 𝑋 → dom 𝐺 = 𝑋) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐺 = 𝑋) |
93 | 92 | eqeq1d 2795 |
. . . . . . . . . . 11
⊢ (𝜑 → (dom 𝐺 = ∅ ↔ 𝑋 = ∅)) |
94 | 79, 93 | syl5bbr 286 |
. . . . . . . . . 10
⊢ (𝜑 → (ran 𝐺 = ∅ ↔ 𝑋 = ∅)) |
95 | 78, 94 | mtbird 326 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ran 𝐺 = ∅) |
96 | | fz1f1o 14888 |
. . . . . . . . . . 11
⊢ (ran
𝐺 ∈ Fin → (ran
𝐺 = ∅ ∨
((♯‘ran 𝐺)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺))) |
97 | 4, 96 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ran 𝐺 = ∅ ∨ ((♯‘ran 𝐺) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺))) |
98 | 97 | ord 859 |
. . . . . . . . 9
⊢ (𝜑 → (¬ ran 𝐺 = ∅ →
((♯‘ran 𝐺)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺))) |
99 | 95, 98 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘ran 𝐺) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺)) |
100 | | oveq2 7015 |
. . . . . . . . . . 11
⊢ (𝑚 = (♯‘ran 𝐺) → (1...𝑚) = (1...(♯‘ran 𝐺))) |
101 | 100 | f1oeq2d 6471 |
. . . . . . . . . 10
⊢ (𝑚 = (♯‘ran 𝐺) → (𝑓:(1...𝑚)–1-1-onto→ran
𝐺 ↔ 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺)) |
102 | 101 | exbidv 1897 |
. . . . . . . . 9
⊢ (𝑚 = (♯‘ran 𝐺) → (∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 ↔ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺)) |
103 | 102 | rspcev 3554 |
. . . . . . . 8
⊢
(((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺) → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
104 | 99, 103 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
105 | | r19.29 3215 |
. . . . . . 7
⊢
((∀𝑚 ∈
ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
106 | 69, 104, 105 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
107 | | exdistrv 1931 |
. . . . . . . . 9
⊢
(∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
108 | 107 | biimpri 229 |
. . . . . . . 8
⊢
((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
109 | 108 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
110 | 109 | reximdv 3233 |
. . . . . 6
⊢ (𝜑 → (∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑚 ∈ ℕ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
111 | 106, 110 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
112 | | df-rex 3109 |
. . . . 5
⊢
(∃𝑚 ∈
ℕ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
113 | 111, 112 | sylib 219 |
. . . 4
⊢ (𝜑 → ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
114 | | ax-5 1886 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ →
∀𝑔 𝑚 ∈
ℕ) |
115 | | 19.29 1853 |
. . . . . . . . 9
⊢
((∀𝑔 𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
116 | 114, 115 | sylan 580 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
117 | | ax-5 1886 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ →
∀𝑓 𝑚 ∈
ℕ) |
118 | | 19.29 1853 |
. . . . . . . . . 10
⊢
((∀𝑓 𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
119 | 117, 118 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
120 | 119 | eximi 1814 |
. . . . . . . 8
⊢
(∃𝑔(𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
121 | 116, 120 | syl 17 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
122 | | df-3an 1080 |
. . . . . . . . 9
⊢ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
123 | 122 | anbi2i 622 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) ↔ (𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
124 | 123 | 2exbii 1828 |
. . . . . . 7
⊢
(∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) ↔ ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
125 | 121, 124 | sylibr 235 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
126 | 125 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)))) |
127 | 126 | eximdv 1893 |
. . . 4
⊢ (𝜑 → (∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑚∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)))) |
128 | 113, 127 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑚∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
129 | 82 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑄 ∈ V) |
130 | | simprl 767 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑚 ∈
ℕ) |
131 | | simprr1 1212 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑔 Fn ran 𝐺) |
132 | | elex 3450 |
. . . . . . . . 9
⊢ (ran
𝐺 ∈ Fin → ran
𝐺 ∈
V) |
133 | 4, 132 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐺 ∈ V) |
134 | 133 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ran 𝐺 ∈ V) |
135 | | simprr2 1213 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
136 | 51 | rspccva 3553 |
. . . . . . . 8
⊢
((∀𝑙 ∈
ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
137 | 135, 136 | sylan 580 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
138 | | simprr3 1214 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
139 | 70 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋) |
140 | | stoweidlem35.1 |
. . . . . . . 8
⊢
Ⅎ𝑡𝜑 |
141 | | nfv 1890 |
. . . . . . . . 9
⊢
Ⅎ𝑡 𝑚 ∈ ℕ |
142 | | nfcv 2947 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑔 |
143 | | nfcv 2947 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡𝑋 |
144 | | nfrab1 3341 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} |
145 | 144 | nfeq2 2962 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} |
146 | | nfv 1890 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(ℎ‘𝑍) = 0 |
147 | | nfra1 3184 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) |
148 | 146, 147 | nfan 1879 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)) |
149 | | nfcv 2947 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝐴 |
150 | 148, 149 | nfrab 3342 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡{ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
151 | 80, 150 | nfcxfr 2945 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡𝑄 |
152 | 145, 151 | nfrab 3342 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡{ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
153 | 143, 152 | nfmpt 5051 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
154 | 2, 153 | nfcxfr 2945 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝐺 |
155 | 154 | nfrn 5698 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡ran
𝐺 |
156 | 142, 155 | nffn 6314 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑔 Fn ran 𝐺 |
157 | | nfv 1890 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝑔‘𝑙) ∈ 𝑙 |
158 | 155, 157 | nfral 3189 |
. . . . . . . . . 10
⊢
Ⅎ𝑡∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 |
159 | | nfcv 2947 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑓 |
160 | | nfcv 2947 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(1...𝑚) |
161 | 159, 160,
155 | nff1o 6473 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 |
162 | 156, 158,
161 | nf3an 1881 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
163 | 141, 162 | nfan 1879 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
164 | 140, 163 | nfan 1879 |
. . . . . . 7
⊢
Ⅎ𝑡(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
165 | | nfv 1890 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑚 ∈ ℕ |
166 | | nfcv 2947 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤𝑔 |
167 | 166, 11 | nffn 6314 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 𝑔 Fn ran 𝐺 |
168 | | nfv 1890 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤(𝑔‘𝑙) ∈ 𝑙 |
169 | 11, 168 | nfral 3189 |
. . . . . . . . . 10
⊢
Ⅎ𝑤∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 |
170 | | nfcv 2947 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤𝑓 |
171 | | nfcv 2947 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤(1...𝑚) |
172 | 170, 171,
11 | nff1o 6473 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 |
173 | 167, 169,
172 | nf3an 1881 |
. . . . . . . . 9
⊢
Ⅎ𝑤(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
174 | 165, 173 | nfan 1879 |
. . . . . . . 8
⊢
Ⅎ𝑤(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
175 | 8, 174 | nfan 1879 |
. . . . . . 7
⊢
Ⅎ𝑤(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
176 | 2, 129, 130, 131, 134, 137, 138, 139, 164, 175, 84 | stoweidlem27 41808 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
177 | 176 | ex 413 |
. . . . 5
⊢ (𝜑 → ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
178 | 177 | 2eximdv 1895 |
. . . 4
⊢ (𝜑 → (∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
179 | 178 | eximdv 1893 |
. . 3
⊢ (𝜑 → (∃𝑚∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑚∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
180 | 128, 179 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑚∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
181 | | id 22 |
. . . 4
⊢
(∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
182 | 181 | exlimivv 1908 |
. . 3
⊢
(∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
183 | 182 | eximi 1814 |
. 2
⊢
(∃𝑚∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑚∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
184 | 180, 183 | syl 17 |
1
⊢ (𝜑 → ∃𝑚∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |