Step | Hyp | Ref
| Expression |
1 | | brdom2 8533 |
. . 3
⊢ (𝐴 ≼ ℕ ↔ (𝐴 ≺ ℕ ∨ 𝐴 ≈
ℕ)) |
2 | | nnenom 13342 |
. . . . . 6
⊢ ℕ
≈ ω |
3 | | sdomentr 8645 |
. . . . . 6
⊢ ((𝐴 ≺ ℕ ∧ ℕ
≈ ω) → 𝐴
≺ ω) |
4 | 2, 3 | mpan2 689 |
. . . . 5
⊢ (𝐴 ≺ ℕ → 𝐴 ≺
ω) |
5 | | isfinite 9109 |
. . . . . 6
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺
ω) |
6 | | finiunmbl 24139 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
7 | 6 | ex 415 |
. . . . . 6
⊢ (𝐴 ∈ Fin →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
8 | 5, 7 | sylbir 237 |
. . . . 5
⊢ (𝐴 ≺ ω →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
9 | 4, 8 | syl 17 |
. . . 4
⊢ (𝐴 ≺ ℕ →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
10 | | bren 8512 |
. . . . 5
⊢ (𝐴 ≈ ℕ ↔
∃𝑓 𝑓:𝐴–1-1-onto→ℕ) |
11 | | nfv 1911 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛 𝑓:𝐴–1-1-onto→ℕ |
12 | | nfcv 2977 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛ℕ |
13 | | nfcsb1v 3907 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 |
14 | 13 | nfcri 2971 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 |
15 | 12, 14 | nfrex 3309 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 |
16 | | f1of 6610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝐴–1-1-onto→ℕ → 𝑓:𝐴⟶ℕ) |
17 | 16 | ffvelrnda 6846 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴) → (𝑓‘𝑛) ∈ ℕ) |
18 | 17 | 3adant3 1128 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑓‘𝑛) ∈ ℕ) |
19 | | simp3 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
20 | | f1ocnvfv1 7027 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴) → (◡𝑓‘(𝑓‘𝑛)) = 𝑛) |
21 | 20 | 3adant3 1128 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (◡𝑓‘(𝑓‘𝑛)) = 𝑛) |
22 | 21 | eqcomd 2827 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑛 = (◡𝑓‘(𝑓‘𝑛))) |
23 | | csbeq1a 3897 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (◡𝑓‘(𝑓‘𝑛)) → 𝐵 = ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝐵 = ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
25 | 19, 24 | eleqtrd 2915 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
26 | | fveq2 6665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑓‘𝑛) → (◡𝑓‘𝑘) = (◡𝑓‘(𝑓‘𝑛))) |
27 | 26 | csbeq1d 3887 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑓‘𝑛) → ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 = ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
28 | 27 | eleq2d 2898 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑓‘𝑛) → (𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ↔ 𝑥 ∈ ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵)) |
29 | 28 | rspcev 3623 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑛) ∈ ℕ ∧ 𝑥 ∈ ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
30 | 18, 25, 29 | syl2anc 586 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
31 | 30 | 3exp 1115 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–1-1-onto→ℕ → (𝑛 ∈ 𝐴 → (𝑥 ∈ 𝐵 → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵))) |
32 | 11, 15, 31 | rexlimd 3317 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
33 | | f1ocnvdm 7035 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) → (◡𝑓‘𝑘) ∈ 𝐴) |
34 | | csbeq1a 3897 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (◡𝑓‘𝑘) → 𝐵 = ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
35 | 34 | eleq2d 2898 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (◡𝑓‘𝑘) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
36 | 14, 35 | rspce 3612 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑓‘𝑘) ∈ 𝐴 ∧ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵) |
37 | 36 | ex 415 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑓‘𝑘) ∈ 𝐴 → (𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵)) |
38 | 33, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵)) |
39 | 38 | rexlimdva 3284 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵)) |
40 | 32, 39 | impbid 214 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
41 | | eliun 4916 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝐴 𝐵 ↔ ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵) |
42 | | eliun 4916 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
43 | 40, 41, 42 | 3bitr4g 316 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1-onto→ℕ → (𝑥 ∈ ∪
𝑛 ∈ 𝐴 𝐵 ↔ 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
44 | 43 | eqrdv 2819 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1-onto→ℕ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
45 | 44 | adantr 483 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
46 | | rspcsbela 4387 |
. . . . . . . . . . . 12
⊢ (((◡𝑓‘𝑘) ∈ 𝐴 ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) →
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
47 | 33, 46 | sylan 582 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) →
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
48 | 47 | an32s 650 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ ℕ) → ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
49 | 48 | ralrimiva 3182 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∀𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
50 | | iunmbl 24148 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol → ∪ 𝑘 ∈ ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
51 | 49, 50 | syl 17 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑘 ∈ ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
52 | 45, 51 | eqeltrd 2913 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
53 | 52 | ex 415 |
. . . . . 6
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
54 | 53 | exlimiv 1927 |
. . . . 5
⊢
(∃𝑓 𝑓:𝐴–1-1-onto→ℕ → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
55 | 10, 54 | sylbi 219 |
. . . 4
⊢ (𝐴 ≈ ℕ →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
56 | 9, 55 | jaoi 853 |
. . 3
⊢ ((𝐴 ≺ ℕ ∨ 𝐴 ≈ ℕ) →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
57 | 1, 56 | sylbi 219 |
. 2
⊢ (𝐴 ≼ ℕ →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
58 | 57 | imp 409 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |