| Step | Hyp | Ref
| Expression |
| 1 | | stoweidlem35.8 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 2 | | stoweidlem35.6 |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
| 3 | 2 | rnmptfi 45176 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Fin → ran 𝐺 ∈ Fin) |
| 4 | 1, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
| 5 | | fnchoice 45034 |
. . . . . . . . . . 11
⊢ (ran
𝐺 ∈ Fin →
∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) |
| 6 | 5 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) |
| 7 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → 𝑔 Fn ran 𝐺) |
| 8 | | stoweidlem35.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤𝜑 |
| 9 | | nfmpt1 5250 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑤(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
| 10 | 2, 9 | nfcxfr 2903 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑤𝐺 |
| 11 | 10 | nfrn 5963 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤ran
𝐺 |
| 12 | 11 | nfcri 2897 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤 𝑘 ∈ ran 𝐺 |
| 13 | 8, 12 | nfan 1899 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑤(𝜑 ∧ 𝑘 ∈ ran 𝐺) |
| 14 | | stoweidlem35.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑋 ⊆ 𝑊) |
| 15 | 14 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑊) |
| 16 | | stoweidlem35.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
| 17 | 15, 16 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
| 18 | | rabid 3458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (𝑤 ∈ 𝐽 ∧ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
| 19 | 17, 18 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝑤 ∈ 𝐽 ∧ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
| 20 | 19 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}) |
| 21 | | df-rex 3071 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∃ℎ ∈
𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
| 22 | 20, 21 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
| 23 | | rabid 3458 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
| 24 | 23 | exbii 1848 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ∃ℎ(ℎ ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
| 25 | 22, 24 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
| 27 | | stoweidlem35.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ𝜑 |
| 28 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ 𝑤 ∈ 𝑋 |
| 29 | 27, 28 | nfan 1899 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎℎ(𝜑 ∧ 𝑤 ∈ 𝑋) |
| 30 | | nfrab1 3457 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎℎ{ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
| 31 | 30 | nfeq2 2923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎℎ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
| 32 | 29, 31 | nfan 1899 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎℎ((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
| 33 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → (ℎ ∈ 𝑘 ↔ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
| 34 | 33 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ℎ ∈ 𝑘)) |
| 35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ℎ ∈ 𝑘)) |
| 36 | 32, 35 | eximd 2216 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (∃ℎ ℎ ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} → ∃ℎ ℎ ∈ 𝑘)) |
| 37 | 26, 36 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ 𝑘) |
| 38 | 37 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ∃ℎ ℎ ∈ 𝑘) |
| 39 | 2 | elrnmpt 5969 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ran 𝐺 → (𝑘 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
| 40 | 39 | ibi 267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ran 𝐺 → ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
| 41 | 40 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑋 𝑘 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
| 42 | 13, 38, 41 | r19.29af 3268 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐺) → ∃ℎ ℎ ∈ 𝑘) |
| 43 | | n0 4353 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ≠ ∅ ↔
∃ℎ ℎ ∈ 𝑘) |
| 44 | 42, 43 | sylibr 234 |
. . . . . . . . . . . . . . . . . 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 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 = 𝑘 → (𝑔‘𝑙) = (𝑔‘𝑘)) |
| 49 | 48 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑙) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑙)) |
| 50 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑘) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑘)) |
| 51 | 49, 50 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑘 → ((𝑔‘𝑙) ∈ 𝑙 ↔ (𝑔‘𝑘) ∈ 𝑘)) |
| 52 | 47, 51 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑘 → ((𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙) ↔ (𝑘 ≠ ∅ → (𝑔‘𝑘) ∈ 𝑘))) |
| 53 | 52 | rspccva 3621 |
. . . . . . . . . . . . . . . . . 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 3146 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → ∀𝑘 ∈ ran 𝐺(𝑔‘𝑘) ∈ 𝑘) |
| 57 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑙 → (𝑔‘𝑘) = (𝑔‘𝑙)) |
| 58 | 57 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑘) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑘)) |
| 59 | | eleq2 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑙) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑙)) |
| 60 | 58, 59 | bitrd 279 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑙 → ((𝑔‘𝑘) ∈ 𝑘 ↔ (𝑔‘𝑙) ∈ 𝑙)) |
| 61 | 60 | cbvralvw 3237 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
ran 𝐺(𝑔‘𝑘) ∈ 𝑘 ↔ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
| 62 | 56, 61 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
| 63 | 7, 62 | jca 511 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙))) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
| 64 | 63 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
| 65 | 64 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ran 𝐺 ∈ Fin) → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔‘𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙))) |
| 66 | 65 | eximdv 1917 |
. . . . . . . . . 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 3150 |
. . . . . . 7
⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙)) |
| 70 | | stoweidlem35.10 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋) |
| 71 | | stoweidlem35.11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ∖ 𝑈) ≠ ∅) |
| 72 | | ssn0 4404 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∖ 𝑈) ⊆ ∪ 𝑋 ∧ (𝑇 ∖ 𝑈) ≠ ∅) → ∪ 𝑋
≠ ∅) |
| 73 | 70, 71, 72 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑋
≠ ∅) |
| 74 | 73 | neneqd 2945 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ ∪ 𝑋 =
∅) |
| 75 | | unieq 4918 |
. . . . . . . . . . . 12
⊢ (𝑋 = ∅ → ∪ 𝑋 =
∪ ∅) |
| 76 | | uni0 4935 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
| 77 | 75, 76 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → ∪ 𝑋 =
∅) |
| 78 | 74, 77 | nsyl 140 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 = ∅) |
| 79 | | dm0rn0 5935 |
. . . . . . . . . . 11
⊢ (dom
𝐺 = ∅ ↔ ran
𝐺 =
∅) |
| 80 | | stoweidlem35.4 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
| 81 | | stoweidlem35.7 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ V) |
| 82 | 80, 81 | rabexd 5340 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑄 ∈ V) |
| 83 | | nfrab1 3457 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎℎ{ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
| 84 | 80, 83 | nfcxfr 2903 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎℎ𝑄 |
| 85 | 84 | rabexgf 45029 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ∈ V → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
| 86 | 82, 85 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
| 87 | 86 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
| 88 | 8, 87, 2 | fmptdf 7137 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑋⟶V) |
| 89 | | dffn2 6738 |
. . . . . . . . . . . . . 14
⊢ (𝐺 Fn 𝑋 ↔ 𝐺:𝑋⟶V) |
| 90 | 88, 89 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 Fn 𝑋) |
| 91 | 90 | fndmd 6673 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐺 = 𝑋) |
| 92 | 91 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝜑 → (dom 𝐺 = ∅ ↔ 𝑋 = ∅)) |
| 93 | 79, 92 | bitr3id 285 |
. . . . . . . . . 10
⊢ (𝜑 → (ran 𝐺 = ∅ ↔ 𝑋 = ∅)) |
| 94 | 78, 93 | mtbird 325 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ran 𝐺 = ∅) |
| 95 | | fz1f1o 15746 |
. . . . . . . . . . 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 865 |
. . . . . . . . 9
⊢ (𝜑 → (¬ ran 𝐺 = ∅ →
((♯‘ran 𝐺)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺))) |
| 98 | 94, 97 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘ran 𝐺) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺)) |
| 99 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑚 = (♯‘ran 𝐺) → (1...𝑚) = (1...(♯‘ran 𝐺))) |
| 100 | 99 | f1oeq2d 6844 |
. . . . . . . . . 10
⊢ (𝑚 = (♯‘ran 𝐺) → (𝑓:(1...𝑚)–1-1-onto→ran
𝐺 ↔ 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺)) |
| 101 | 100 | exbidv 1921 |
. . . . . . . . 9
⊢ (𝑚 = (♯‘ran 𝐺) → (∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 ↔ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran
𝐺)) |
| 102 | 101 | rspcev 3622 |
. . . . . . . 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 3114 |
. . . . . . 7
⊢
((∀𝑚 ∈
ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
| 105 | 69, 103, 104 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
| 106 | | exdistrv 1955 |
. . . . . . . . 9
⊢
(∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
| 107 | 106 | biimpri 228 |
. . . . . . . 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 3170 |
. . . . . 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 3071 |
. . . . 5
⊢
(∃𝑚 ∈
ℕ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
| 112 | 110, 111 | sylib 218 |
. . . 4
⊢ (𝜑 → ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
| 113 | | ax-5 1910 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ →
∀𝑔 𝑚 ∈
ℕ) |
| 114 | | 19.29 1873 |
. . . . . . . . 9
⊢
((∀𝑔 𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
| 115 | 113, 114 | sylan 580 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧
∃𝑔∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
| 116 | | ax-5 1910 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ →
∀𝑓 𝑚 ∈
ℕ) |
| 117 | | 19.29 1873 |
. . . . . . . . . 10
⊢
((∀𝑓 𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
| 118 | 116, 117 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧
∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
| 119 | 118 | eximi 1835 |
. . . . . . . 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 1089 |
. . . . . . . . 9
⊢ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) ↔ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
| 122 | 121 | anbi2i 623 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) ↔ (𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
| 123 | 122 | 2exbii 1849 |
. . . . . . 7
⊢
(∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) ↔ ∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
| 124 | 120, 123 | sylibr 234 |
. . . . . 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 1917 |
. . . 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 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑄 ∈ V) |
| 129 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑚 ∈
ℕ) |
| 130 | | simprr1 1222 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑔 Fn ran 𝐺) |
| 131 | | elex 3501 |
. . . . . . . . 9
⊢ (ran
𝐺 ∈ Fin → ran
𝐺 ∈
V) |
| 132 | 4, 131 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐺 ∈ V) |
| 133 | 132 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ran 𝐺 ∈ V) |
| 134 | | simprr2 1223 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙) |
| 135 | 51 | rspccva 3621 |
. . . . . . . 8
⊢
((∀𝑙 ∈
ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
| 136 | 134, 135 | sylan 580 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔‘𝑘) ∈ 𝑘) |
| 137 | | simprr3 1224 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
| 138 | 70 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋) |
| 139 | | stoweidlem35.1 |
. . . . . . . 8
⊢
Ⅎ𝑡𝜑 |
| 140 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑡 𝑚 ∈ ℕ |
| 141 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑔 |
| 142 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡𝑋 |
| 143 | | nfrab1 3457 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} |
| 144 | 143 | nfeq2 2923 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} |
| 145 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(ℎ‘𝑍) = 0 |
| 146 | | nfra1 3284 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) |
| 147 | 145, 146 | nfan 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)) |
| 148 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝐴 |
| 149 | 147, 148 | nfrabw 3475 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡{ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
| 150 | 80, 149 | nfcxfr 2903 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡𝑄 |
| 151 | 144, 150 | nfrabw 3475 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡{ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
| 152 | 142, 151 | nfmpt 5249 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
| 153 | 2, 152 | nfcxfr 2903 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝐺 |
| 154 | 153 | nfrn 5963 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡ran
𝐺 |
| 155 | 141, 154 | nffn 6667 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑔 Fn ran 𝐺 |
| 156 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝑔‘𝑙) ∈ 𝑙 |
| 157 | 154, 156 | nfralw 3311 |
. . . . . . . . . 10
⊢
Ⅎ𝑡∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 |
| 158 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑓 |
| 159 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(1...𝑚) |
| 160 | 158, 159,
154 | nff1o 6846 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 |
| 161 | 155, 157,
160 | nf3an 1901 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
| 162 | 140, 161 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
| 163 | 139, 162 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑡(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
| 164 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑚 ∈ ℕ |
| 165 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤𝑔 |
| 166 | 165, 11 | nffn 6667 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 𝑔 Fn ran 𝐺 |
| 167 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤(𝑔‘𝑙) ∈ 𝑙 |
| 168 | 11, 167 | nfralw 3311 |
. . . . . . . . . 10
⊢
Ⅎ𝑤∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 |
| 169 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤𝑓 |
| 170 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤(1...𝑚) |
| 171 | 169, 170,
11 | nff1o 6846 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 𝑓:(1...𝑚)–1-1-onto→ran
𝐺 |
| 172 | 166, 168,
171 | nf3an 1901 |
. . . . . . . . 9
⊢
Ⅎ𝑤(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺) |
| 173 | 164, 172 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑤(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) |
| 174 | 8, 173 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑤(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) |
| 175 | 2, 128, 129, 130, 133, 136, 137, 138, 163, 174, 84 | stoweidlem27 46042 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
| 176 | 175 | ex 412 |
. . . . 5
⊢ (𝜑 → ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
| 177 | 176 | 2eximdv 1919 |
. . . 4
⊢ (𝜑 → (∃𝑔∃𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔‘𝑙) ∈ 𝑙 ∧ 𝑓:(1...𝑚)–1-1-onto→ran
𝐺)) → ∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))) |
| 178 | 177 | eximdv 1917 |
. . 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 1932 |
. . 3
⊢
(∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
| 182 | 181 | eximi 1835 |
. 2
⊢
(∃𝑚∃𝑔∃𝑓∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))) → ∃𝑚∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |
| 183 | 179, 182 | syl 17 |
1
⊢ (𝜑 → ∃𝑚∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡)))) |