Step | Hyp | Ref
| Expression |
1 | | stoweidlem35.8 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | stoweidlem35.6 |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
3 | 2 | rnmptfi 39351 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Fin → ran 𝐺 ∈ Fin) |
4 | 1, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
5 | | fnchoice 39188 |
. . . . . . . . . . 11
⊢ (ran
𝐺 ∈ Fin →
∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) |
6 | 5 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) |
7 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → 𝑔 Fn ran 𝐺) |
8 | | stoweidlem35.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤𝜑 |
9 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑤(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
10 | 2, 9 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑤𝐺 |
11 | 10 | nfrn 5368 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤ran
𝐺 |
12 | 11 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤 𝑘 ∈ ran 𝐺 |
13 | 8, 12 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑤(𝜑 ∧ 𝑘 ∈ ran 𝐺) |
14 | | stoweidlem35.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑋 ⊆ 𝑊) |
15 | 14 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑊) |
16 | | stoweidlem35.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
17 | 15, 16 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
18 | | rabid 3116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (𝑤 ∈ 𝐽 ∧ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
19 | 17, 18 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝑤 ∈ 𝐽 ∧ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
20 | 19 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}) |
21 | | df-rex 2918 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∃ℎ ∈
𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
22 | 20, 21 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
23 | | rabid 3116 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
24 | 23 | exbii 1774 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
25 | 22, 24 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
27 | | stoweidlem35.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ𝜑 |
28 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ 𝑤 ∈ 𝑋 |
29 | 27, 28 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎℎ(𝜑 ∧ 𝑤 ∈ 𝑋) |
30 | | nfrab1 3122 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ{ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
31 | 30 | nfeq2 2780 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎℎ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
32 | 29, 31 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎℎ((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
33 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → (ℎ ∈ 𝑘 ↔ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
34 | 33 | biimprd 238 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ℎ ∈ 𝑘)) |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ℎ ∈ 𝑘)) |
36 | 32, 35 | eximd 2085 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ∃ℎ ℎ ∈ 𝑘)) |
37 | 26, 36 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ 𝑘) |
38 | 37 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ 𝑘) |
39 | 2 | elrnmpt 5372 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ran 𝐺 → (𝑘 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
40 | 39 | ibi 256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ran 𝐺 → ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
41 | 40 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
42 | 13, 38, 41 | r19.29af 3076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → ∃ℎ ℎ ∈ 𝑘) |
43 | | n0 3931 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ≠ ∅ ↔
∃ℎ ℎ ∈ 𝑘) |
44 | 42, 43 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅) |
45 | 44 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅) |
46 | | simplrr 801 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) |
47 | | neeq1 2856 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑘 → (𝑙 ≠ ∅ ↔ 𝑘 ≠ ∅)) |
48 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 = 𝑘 → (𝑔‘𝑙) = (𝑔‘𝑘)) |
49 | 48 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑙) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑙)) |
50 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑘) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑘)) |
51 | 49, 50 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑙) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑘)) |
52 | 47, 51 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑘 → ((𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙) ↔ (𝑘 ≠ ∅ → (𝑔‘𝑘) ∈ 𝑘))) |
53 | 52 | rspccva 3308 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑙 ∈
ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔‘𝑘) ∈ 𝑘)) |
54 | 46, 53 | sylancom 701 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔‘𝑘) ∈ 𝑘)) |
55 | 45, 54 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
56 | 55 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → ∀𝑘 ∈ ran 𝐺(𝑔‘𝑘) ∈ 𝑘) |
57 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑙 → (𝑔‘𝑘) = (𝑔‘𝑙)) |
58 | 57 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑘) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑘)) |
59 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑙) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑙)) |
60 | 58, 59 | bitrd 268 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑘) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑙)) |
61 | 60 | cbvralv 3171 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
ran 𝐺(𝑔‘𝑘) ∈ 𝑘 ↔ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
62 | 56, 61 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
63 | 7, 62 | jca 554 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
64 | 63 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
65 | 64 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
66 | 65 | eximdv 1846 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
67 | 6, 66 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
68 | 4, 67 | mpdan 702 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
69 | 68 | ralrimivw 2967 |
. . . . . . 7
⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
70 | | stoweidlem35.10 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋) |
71 | | stoweidlem35.11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ∖ 𝑈) ≠ ∅) |
72 | | ssn0 3976 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∖ 𝑈) ⊆ ∪ 𝑋 ∧ (𝑇 ∖ 𝑈) ≠ ∅) → ∪ 𝑋
≠ ∅) |
73 | 70, 71, 72 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑋
≠ ∅) |
74 | 73 | neneqd 2799 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ ∪ 𝑋 =
∅) |
75 | | unieq 4444 |
. . . . . . . . . . . 12
⊢ (𝑋 = ∅ → ∪ 𝑋 =
∪ ∅) |
76 | | uni0 4465 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
77 | 75, 76 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → ∪ 𝑋 =
∅) |
78 | 74, 77 | nsyl 135 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 = ∅) |
79 | | dm0rn0 5342 |
. . . . . . . . . . 11
⊢ (dom
𝐺 = ∅ ↔ ran
𝐺 =
∅) |
80 | | stoweidlem35.4 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
81 | | stoweidlem35.7 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ V) |
82 | 80, 81 | rabexd 4814 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑄 ∈ V) |
83 | | nfrab1 3122 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎℎ{ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
84 | 80, 83 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎℎ𝑄 |
85 | 84 | rabexgf 39183 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ∈ V → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
86 | 82, 85 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
87 | 86 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
88 | 8, 87, 2 | fmptdf 6387 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑋⟶V) |
89 | | dffn2 6047 |
. . . . . . . . . . . . . 14
⊢ (𝐺 Fn 𝑋 ↔ 𝐺:𝑋⟶V) |
90 | 88, 89 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 Fn 𝑋) |
91 | | fndm 5990 |
. . . . . . . . . . . . 13
⊢ (𝐺 Fn 𝑋 → dom 𝐺 = 𝑋) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐺 = 𝑋) |
93 | 92 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝜑 → (dom 𝐺 = ∅ ↔ 𝑋 = ∅)) |
94 | 79, 93 | syl5bbr 274 |
. . . . . . . . . 10
⊢ (𝜑 → (ran 𝐺 = ∅ ↔ 𝑋 = ∅)) |
95 | 78, 94 | mtbird 315 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ran 𝐺 = ∅) |
96 | | fz1f1o 14441 |
. . . . . . . . . . 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 392 |
. . . . . . . . 9
⊢ (𝜑 → (¬ ran 𝐺 = ∅ → ((#‘ran
𝐺) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran
𝐺))) |
99 | 95, 98 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → ((#‘ran 𝐺) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran
𝐺)) |
100 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑚 = (#‘ran 𝐺) → (1...𝑚) = (1...(#‘ran 𝐺))) |
101 | | f1oeq2 6128 |
. . . . . . . . . . 11
⊢
((1...𝑚) =
(1...(#‘ran 𝐺))
→ (𝑓:(1...𝑚)–1-1-onto→ran
𝐺 ↔ 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran
𝐺)) |
102 | 100, 101 | syl 17 |
. . . . . . . . . 10
⊢ (𝑚 = (#‘ran 𝐺) → (𝑓:(1...𝑚)–1-1-onto→ran
𝐺 ↔ 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran
𝐺)) |
103 | 102 | exbidv 1850 |
. . . . . . . . 9
⊢ (𝑚 = (#‘ran 𝐺) → (∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 ↔ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran
𝐺)) |
104 | 103 | rspcev 3309 |
. . . . . . . 8
⊢
(((#‘ran 𝐺)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran
𝐺) → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
105 | 99, 104 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
106 | | r19.29 3072 |
. . . . . . 7
⊢
((∀𝑚 ∈
ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
107 | 69, 105, 106 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
108 | | eeanv 2182 |
. . . . . . . . 9
⊢
(∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
109 | 108 | biimpri 218 |
. . . . . . . 8
⊢
((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
110 | 109 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
111 | 110 | reximdv 3016 |
. . . . . 6
⊢ (𝜑 → (∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑚 ∈ ℕ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
112 | 107, 111 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
113 | | df-rex 2918 |
. . . . 5
⊢
(∃𝑚 ∈
ℕ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
114 | 112, 113 | sylib 208 |
. . . 4
⊢ (𝜑 → ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
115 | | ax-5 1839 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ →
∀𝑔 𝑚 ∈
ℕ) |
116 | | 19.29 1801 |
. . . . . . . . 9
⊢
((∀𝑔 𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
117 | 115, 116 | sylan 488 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
118 | | ax-5 1839 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ →
∀𝑓 𝑚 ∈
ℕ) |
119 | | 19.29 1801 |
. . . . . . . . . 10
⊢
((∀𝑓 𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
120 | 118, 119 | sylan 488 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
121 | 120 | eximi 1762 |
. . . . . . . 8
⊢
(∃𝑔(𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
122 | 117, 121 | syl 17 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
123 | | df-3an 1039 |
. . . . . . . . 9
⊢ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
124 | 123 | anbi2i 730 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) ↔ (𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
125 | 124 | 2exbii 1775 |
. . . . . . 7
⊢
(∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) ↔ ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
126 | 122, 125 | sylibr 224 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
127 | 126 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)))) |
128 | 127 | eximdv 1846 |
. . . 4
⊢ (𝜑 → (∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑚∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)))) |
129 | 114, 128 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑚∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
130 | 82 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑄 ∈ V) |
131 | | simprl 794 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑚 ∈
ℕ) |
132 | | simprr1 1109 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑔 Fn ran 𝐺) |
133 | | elex 3212 |
. . . . . . . . 9
⊢ (ran
𝐺 ∈ Fin → ran
𝐺 ∈
V) |
134 | 4, 133 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐺 ∈ V) |
135 | 134 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ran 𝐺 ∈ V) |
136 | | simprr2 1110 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
137 | 51 | rspccva 3308 |
. . . . . . . 8
⊢
((∀𝑙 ∈
ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
138 | 136, 137 | sylan 488 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
139 | | simprr3 1111 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
140 | 70 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋) |
141 | | stoweidlem35.1 |
. . . . . . . 8
⊢
Ⅎ𝑡𝜑 |
142 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑡 𝑚 ∈ ℕ |
143 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑔 |
144 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡𝑋 |
145 | | nfrab1 3122 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} |
146 | 145 | nfeq2 2780 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} |
147 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(ℎ‘𝑍) = 0 |
148 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) |
149 | 147, 148 | nfan 1828 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)) |
150 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝐴 |
151 | 149, 150 | nfrab 3123 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡{ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
152 | 80, 151 | nfcxfr 2762 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡𝑄 |
153 | 146, 152 | nfrab 3123 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡{ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
154 | 144, 153 | nfmpt 4746 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
155 | 2, 154 | nfcxfr 2762 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝐺 |
156 | 155 | nfrn 5368 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡ran
𝐺 |
157 | 143, 156 | nffn 5987 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑔 Fn ran 𝐺 |
158 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝑔‘𝑙) ∈ 𝑙 |
159 | 156, 158 | nfral 2945 |
. . . . . . . . . 10
⊢
Ⅎ𝑡∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 |
160 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑓 |
161 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(1...𝑚) |
162 | 160, 161,
156 | nff1o 6135 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 |
163 | 157, 159,
162 | nf3an 1831 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
164 | 142, 163 | nfan 1828 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
165 | 141, 164 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑡(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
166 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑚 ∈ ℕ |
167 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤𝑔 |
168 | 167, 11 | nffn 5987 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 𝑔 Fn ran 𝐺 |
169 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤(𝑔‘𝑙) ∈ 𝑙 |
170 | 11, 169 | nfral 2945 |
. . . . . . . . . 10
⊢
Ⅎ𝑤∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 |
171 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤𝑓 |
172 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤(1...𝑚) |
173 | 171, 172,
11 | nff1o 6135 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 |
174 | 168, 170,
173 | nf3an 1831 |
. . . . . . . . 9
⊢
Ⅎ𝑤(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
175 | 166, 174 | nfan 1828 |
. . . . . . . 8
⊢
Ⅎ𝑤(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
176 | 8, 175 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑤(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
177 | 2, 130, 131, 132, 135, 138, 139, 140, 165, 176, 84 | stoweidlem27 40244 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
178 | 177 | ex 450 |
. . . . 5
⊢ (𝜑 → ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
179 | 178 | 2eximdv 1848 |
. . . 4
⊢ (𝜑 → (∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
180 | 179 | eximdv 1846 |
. . 3
⊢ (𝜑 → (∃𝑚∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑚∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
181 | 129, 180 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑚∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
182 | | id 22 |
. . . 4
⊢
(∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
183 | 182 | exlimivv 1860 |
. . 3
⊢
(∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
184 | 183 | eximi 1762 |
. 2
⊢
(∃𝑚∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑚∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
185 | 181, 184 | syl 17 |
1
⊢ (𝜑 → ∃𝑚∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |