Step | Hyp | Ref
| Expression |
1 | | brdom2 7871 |
. . 3
⊢ (𝐴 ≼ ℕ ↔ (𝐴 ≺ ℕ ∨ 𝐴 ≈
ℕ)) |
2 | | nnenom 12641 |
. . . . . 6
⊢ ℕ
≈ ω |
3 | | sdomentr 7979 |
. . . . . 6
⊢ ((𝐴 ≺ ℕ ∧ ℕ
≈ ω) → 𝐴
≺ ω) |
4 | 2, 3 | mpan2 703 |
. . . . 5
⊢ (𝐴 ≺ ℕ → 𝐴 ≺
ω) |
5 | | isfinite 8432 |
. . . . . 6
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺
ω) |
6 | | finiunmbl 23119 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
7 | 6 | ex 449 |
. . . . . 6
⊢ (𝐴 ∈ Fin →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
8 | 5, 7 | sylbir 224 |
. . . . 5
⊢ (𝐴 ≺ ω →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
9 | 4, 8 | syl 17 |
. . . 4
⊢ (𝐴 ≺ ℕ →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
10 | | bren 7850 |
. . . . 5
⊢ (𝐴 ≈ ℕ ↔
∃𝑓 𝑓:𝐴–1-1-onto→ℕ) |
11 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛 𝑓:𝐴–1-1-onto→ℕ |
12 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛ℕ |
13 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 |
14 | 13 | nfcri 2745 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 |
15 | 12, 14 | nfrex 2990 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 |
16 | | f1of 6050 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝐴–1-1-onto→ℕ → 𝑓:𝐴⟶ℕ) |
17 | 16 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴) → (𝑓‘𝑛) ∈ ℕ) |
18 | 17 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑓‘𝑛) ∈ ℕ) |
19 | | simp3 1056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
20 | | f1ocnvfv1 6432 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴) → (◡𝑓‘(𝑓‘𝑛)) = 𝑛) |
21 | 20 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (◡𝑓‘(𝑓‘𝑛)) = 𝑛) |
22 | 21 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑛 = (◡𝑓‘(𝑓‘𝑛))) |
23 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (◡𝑓‘(𝑓‘𝑛)) → 𝐵 = ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝐵 = ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
25 | 19, 24 | eleqtrd 2690 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
26 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑓‘𝑛) → (◡𝑓‘𝑘) = (◡𝑓‘(𝑓‘𝑛))) |
27 | 26 | csbeq1d 3506 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑓‘𝑛) → ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 = ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
28 | 27 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑓‘𝑛) → (𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ↔ 𝑥 ∈ ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵)) |
29 | 28 | rspcev 3282 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑛) ∈ ℕ ∧ 𝑥 ∈ ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
30 | 18, 25, 29 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
31 | 30 | 3exp 1256 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–1-1-onto→ℕ → (𝑛 ∈ 𝐴 → (𝑥 ∈ 𝐵 → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵))) |
32 | 11, 15, 31 | rexlimd 3008 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
33 | | f1ocnvdm 6440 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) → (◡𝑓‘𝑘) ∈ 𝐴) |
34 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (◡𝑓‘𝑘) → 𝐵 = ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
35 | 34 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (◡𝑓‘𝑘) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
36 | 14, 35 | rspce 3277 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑓‘𝑘) ∈ 𝐴 ∧ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵) |
37 | 36 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑓‘𝑘) ∈ 𝐴 → (𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵)) |
38 | 33, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵)) |
39 | 38 | rexlimdva 3013 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵)) |
40 | 32, 39 | impbid 201 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
41 | | eliun 4460 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝐴 𝐵 ↔ ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵) |
42 | | eliun 4460 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
43 | 40, 41, 42 | 3bitr4g 302 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1-onto→ℕ → (𝑥 ∈ ∪
𝑛 ∈ 𝐴 𝐵 ↔ 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
44 | 43 | eqrdv 2608 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1-onto→ℕ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
45 | 44 | adantr 480 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
46 | | rspcsbela 3958 |
. . . . . . . . . . . 12
⊢ (((◡𝑓‘𝑘) ∈ 𝐴 ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) →
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
47 | 33, 46 | sylan 487 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) →
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
48 | 47 | an32s 842 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ ℕ) → ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
49 | 48 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∀𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
50 | | iunmbl 23128 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol → ∪ 𝑘 ∈ ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
51 | 49, 50 | syl 17 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑘 ∈ ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
52 | 45, 51 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
53 | 52 | ex 449 |
. . . . . 6
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
54 | 53 | exlimiv 1845 |
. . . . 5
⊢
(∃𝑓 𝑓:𝐴–1-1-onto→ℕ → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
55 | 10, 54 | sylbi 206 |
. . . 4
⊢ (𝐴 ≈ ℕ →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
56 | 9, 55 | jaoi 393 |
. . 3
⊢ ((𝐴 ≺ ℕ ∨ 𝐴 ≈ ℕ) →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
57 | 1, 56 | sylbi 206 |
. 2
⊢ (𝐴 ≼ ℕ →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
58 | 57 | imp 444 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |