| Step | Hyp | Ref
| Expression |
| 1 | | brdom2 9022 |
. . 3
⊢ (𝐴 ≼ ℕ ↔ (𝐴 ≺ ℕ ∨ 𝐴 ≈
ℕ)) |
| 2 | | nnenom 14021 |
. . . . . 6
⊢ ℕ
≈ ω |
| 3 | | sdomentr 9151 |
. . . . . 6
⊢ ((𝐴 ≺ ℕ ∧ ℕ
≈ ω) → 𝐴
≺ ω) |
| 4 | 2, 3 | mpan2 691 |
. . . . 5
⊢ (𝐴 ≺ ℕ → 𝐴 ≺
ω) |
| 5 | | isfinite 9692 |
. . . . . 6
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺
ω) |
| 6 | | finiunmbl 25579 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
| 7 | 6 | ex 412 |
. . . . . 6
⊢ (𝐴 ∈ Fin →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
| 8 | 5, 7 | sylbir 235 |
. . . . 5
⊢ (𝐴 ≺ ω →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
| 9 | 4, 8 | syl 17 |
. . . 4
⊢ (𝐴 ≺ ℕ →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
| 10 | | bren 8995 |
. . . . 5
⊢ (𝐴 ≈ ℕ ↔
∃𝑓 𝑓:𝐴–1-1-onto→ℕ) |
| 11 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛 𝑓:𝐴–1-1-onto→ℕ |
| 12 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛ℕ |
| 13 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 |
| 14 | 13 | nfcri 2897 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 |
| 15 | 12, 14 | nfrexw 3313 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 |
| 16 | | f1of 6848 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝐴–1-1-onto→ℕ → 𝑓:𝐴⟶ℕ) |
| 17 | 16 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴) → (𝑓‘𝑛) ∈ ℕ) |
| 18 | 17 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑓‘𝑛) ∈ ℕ) |
| 19 | | simp3 1139 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
| 20 | | f1ocnvfv1 7296 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴) → (◡𝑓‘(𝑓‘𝑛)) = 𝑛) |
| 21 | 20 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (◡𝑓‘(𝑓‘𝑛)) = 𝑛) |
| 22 | 21 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑛 = (◡𝑓‘(𝑓‘𝑛))) |
| 23 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (◡𝑓‘(𝑓‘𝑛)) → 𝐵 = ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝐵 = ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
| 25 | 19, 24 | eleqtrd 2843 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
| 26 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑓‘𝑛) → (◡𝑓‘𝑘) = (◡𝑓‘(𝑓‘𝑛))) |
| 27 | 26 | csbeq1d 3903 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑓‘𝑛) → ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 = ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) |
| 28 | 27 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑓‘𝑛) → (𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ↔ 𝑥 ∈ ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵)) |
| 29 | 28 | rspcev 3622 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑛) ∈ ℕ ∧ 𝑥 ∈ ⦋(◡𝑓‘(𝑓‘𝑛)) / 𝑛⦌𝐵) → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
| 30 | 18, 25, 29 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
| 31 | 30 | 3exp 1120 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–1-1-onto→ℕ → (𝑛 ∈ 𝐴 → (𝑥 ∈ 𝐵 → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵))) |
| 32 | 11, 15, 31 | rexlimd 3266 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 33 | | f1ocnvdm 7305 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) → (◡𝑓‘𝑘) ∈ 𝐴) |
| 34 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (◡𝑓‘𝑘) → 𝐵 = ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
| 35 | 34 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (◡𝑓‘𝑘) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 36 | 14, 35 | rspce 3611 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑓‘𝑘) ∈ 𝐴 ∧ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵) |
| 37 | 36 | ex 412 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑓‘𝑘) ∈ 𝐴 → (𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵)) |
| 38 | 33, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵)) |
| 39 | 38 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 → ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵)) |
| 40 | 32, 39 | impbid 212 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 41 | | eliun 4995 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝐴 𝐵 ↔ ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵) |
| 42 | | eliun 4995 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
| 43 | 40, 41, 42 | 3bitr4g 314 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1-onto→ℕ → (𝑥 ∈ ∪
𝑛 ∈ 𝐴 𝐵 ↔ 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 44 | 43 | eqrdv 2735 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1-onto→ℕ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
| 45 | 44 | adantr 480 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵) |
| 46 | | rspcsbela 4438 |
. . . . . . . . . . . 12
⊢ (((◡𝑓‘𝑘) ∈ 𝐴 ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) →
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
| 47 | 33, 46 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) →
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
| 48 | 47 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ ℕ) → ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
| 49 | 48 | ralrimiva 3146 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∀𝑘 ∈ ℕ
⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
| 50 | | iunmbl 25588 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol → ∪ 𝑘 ∈ ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
| 51 | 49, 50 | syl 17 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑘 ∈ ℕ ⦋(◡𝑓‘𝑘) / 𝑛⦌𝐵 ∈ dom vol) |
| 52 | 45, 51 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
| 53 | 52 | ex 412 |
. . . . . 6
⊢ (𝑓:𝐴–1-1-onto→ℕ → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
| 54 | 53 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑓 𝑓:𝐴–1-1-onto→ℕ → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
| 55 | 10, 54 | sylbi 217 |
. . . 4
⊢ (𝐴 ≈ ℕ →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
| 56 | 9, 55 | jaoi 858 |
. . 3
⊢ ((𝐴 ≺ ℕ ∨ 𝐴 ≈ ℕ) →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
| 57 | 1, 56 | sylbi 217 |
. 2
⊢ (𝐴 ≼ ℕ →
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)) |
| 58 | 57 | imp 406 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |