| Step | Hyp | Ref
| Expression |
| 1 | | dyadmbl.1 |
. . 3
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) |
| 2 | | dyadmbl.2 |
. . 3
⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)} |
| 3 | | dyadmbl.3 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ran 𝐹) |
| 4 | 1, 2, 3 | dyadmbllem 25634 |
. 2
⊢ (𝜑 → ∪ ([,] “ 𝐴) = ∪ ([,]
“ 𝐺)) |
| 5 | | isfinite 9692 |
. . . 4
⊢ (𝐺 ∈ Fin ↔ 𝐺 ≺
ω) |
| 6 | | iccf 13488 |
. . . . . 6
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
| 7 | | ffun 6739 |
. . . . . 6
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → Fun [,]) |
| 8 | | funiunfv 7268 |
. . . . . 6
⊢ (Fun [,]
→ ∪ 𝑛 ∈ 𝐺 ([,]‘𝑛) = ∪ ([,] “
𝐺)) |
| 9 | 6, 7, 8 | mp2b 10 |
. . . . 5
⊢ ∪ 𝑛 ∈ 𝐺 ([,]‘𝑛) = ∪ ([,] “
𝐺) |
| 10 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ∈ Fin) → 𝐺 ∈ Fin) |
| 11 | 2 | ssrab3 4082 |
. . . . . . . . . . . . . . 15
⊢ 𝐺 ⊆ 𝐴 |
| 12 | 11, 3 | sstrid 3995 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ⊆ ran 𝐹) |
| 13 | 1 | dyadf 25626 |
. . . . . . . . . . . . . . . 16
⊢ 𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ ×
ℝ)) |
| 14 | | frn 6743 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) → ran
𝐹 ⊆ ( ≤ ∩
(ℝ × ℝ))) |
| 15 | 13, 14 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ran 𝐹 ⊆ ( ≤ ∩ (ℝ
× ℝ)) |
| 16 | | inss2 4238 |
. . . . . . . . . . . . . . 15
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 17 | 15, 16 | sstri 3993 |
. . . . . . . . . . . . . 14
⊢ ran 𝐹 ⊆ (ℝ ×
ℝ) |
| 18 | 12, 17 | sstrdi 3996 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ⊆ (ℝ ×
ℝ)) |
| 19 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐺 ∈ Fin) → 𝐺 ⊆ (ℝ ×
ℝ)) |
| 20 | 19 | sselda 3983 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → 𝑛 ∈ (ℝ ×
ℝ)) |
| 21 | | 1st2nd2 8053 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℝ ×
ℝ) → 𝑛 =
〈(1st ‘𝑛), (2nd ‘𝑛)〉) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → 𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉) |
| 23 | 22 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → ([,]‘𝑛) = ([,]‘〈(1st
‘𝑛), (2nd
‘𝑛)〉)) |
| 24 | | df-ov 7434 |
. . . . . . . . 9
⊢
((1st ‘𝑛)[,](2nd ‘𝑛)) = ([,]‘〈(1st
‘𝑛), (2nd
‘𝑛)〉) |
| 25 | 23, 24 | eqtr4di 2795 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → ([,]‘𝑛) = ((1st ‘𝑛)[,](2nd ‘𝑛))) |
| 26 | | xp1st 8046 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℝ ×
ℝ) → (1st ‘𝑛) ∈ ℝ) |
| 27 | 20, 26 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → (1st ‘𝑛) ∈
ℝ) |
| 28 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℝ ×
ℝ) → (2nd ‘𝑛) ∈ ℝ) |
| 29 | 20, 28 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → (2nd ‘𝑛) ∈
ℝ) |
| 30 | | iccmbl 25601 |
. . . . . . . . 9
⊢
(((1st ‘𝑛) ∈ ℝ ∧ (2nd
‘𝑛) ∈ ℝ)
→ ((1st ‘𝑛)[,](2nd ‘𝑛)) ∈ dom vol) |
| 31 | 27, 29, 30 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → ((1st ‘𝑛)[,](2nd ‘𝑛)) ∈ dom
vol) |
| 32 | 25, 31 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → ([,]‘𝑛) ∈ dom vol) |
| 33 | 32 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ∈ Fin) → ∀𝑛 ∈ 𝐺 ([,]‘𝑛) ∈ dom vol) |
| 34 | | finiunmbl 25579 |
. . . . . 6
⊢ ((𝐺 ∈ Fin ∧ ∀𝑛 ∈ 𝐺 ([,]‘𝑛) ∈ dom vol) → ∪ 𝑛 ∈ 𝐺 ([,]‘𝑛) ∈ dom vol) |
| 35 | 10, 33, 34 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝐺 ∈ Fin) → ∪ 𝑛 ∈ 𝐺 ([,]‘𝑛) ∈ dom vol) |
| 36 | 9, 35 | eqeltrrid 2846 |
. . . 4
⊢ ((𝜑 ∧ 𝐺 ∈ Fin) → ∪ ([,] “ 𝐺) ∈ dom vol) |
| 37 | 5, 36 | sylan2br 595 |
. . 3
⊢ ((𝜑 ∧ 𝐺 ≺ ω) → ∪ ([,] “ 𝐺) ∈ dom vol) |
| 38 | | rnco2 6273 |
. . . . . . . . 9
⊢ ran ([,]
∘ 𝑓) = ([,] “
ran 𝑓) |
| 39 | | f1ofo 6855 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–1-1-onto→𝐺 → 𝑓:ℕ–onto→𝐺) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → 𝑓:ℕ–onto→𝐺) |
| 41 | | forn 6823 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐺 → ran 𝑓 = 𝐺) |
| 42 | 40, 41 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ran 𝑓 = 𝐺) |
| 43 | 42 | imaeq2d 6078 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ([,] “ ran 𝑓) = ([,] “ 𝐺)) |
| 44 | 38, 43 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ran ([,] ∘ 𝑓) = ([,] “ 𝐺)) |
| 45 | 44 | unieqd 4920 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ∪ ran ([,] ∘ 𝑓) = ∪ ([,] “
𝐺)) |
| 46 | | f1of 6848 |
. . . . . . . . 9
⊢ (𝑓:ℕ–1-1-onto→𝐺 → 𝑓:ℕ⟶𝐺) |
| 47 | 12, 15 | sstrdi 3996 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ⊆ ( ≤ ∩ (ℝ ×
ℝ))) |
| 48 | | fss 6752 |
. . . . . . . . 9
⊢ ((𝑓:ℕ⟶𝐺 ∧ 𝐺 ⊆ ( ≤ ∩ (ℝ ×
ℝ))) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
| 49 | 46, 47, 48 | syl2anr 597 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
| 50 | | fss 6752 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:ℕ⟶𝐺 ∧ 𝐺 ⊆ ran 𝐹) → 𝑓:ℕ⟶ran 𝐹) |
| 51 | 46, 12, 50 | syl2anr 597 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → 𝑓:ℕ⟶ran 𝐹) |
| 52 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ) → 𝑎 ∈
ℕ) |
| 53 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ⟶ran 𝐹 ∧ 𝑎 ∈ ℕ) → (𝑓‘𝑎) ∈ ran 𝐹) |
| 54 | 51, 52, 53 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑎) ∈ ran 𝐹) |
| 55 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ) → 𝑏 ∈
ℕ) |
| 56 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ⟶ran 𝐹 ∧ 𝑏 ∈ ℕ) → (𝑓‘𝑏) ∈ ran 𝐹) |
| 57 | 51, 55, 56 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑏) ∈ ran 𝐹) |
| 58 | 1 | dyaddisj 25631 |
. . . . . . . . . . . 12
⊢ (((𝑓‘𝑎) ∈ ran 𝐹 ∧ (𝑓‘𝑏) ∈ ran 𝐹) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) ∨ ([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
| 59 | 54, 57, 58 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) ∨ ([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
| 60 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑓‘𝑏) → ([,]‘𝑤) = ([,]‘(𝑓‘𝑏))) |
| 61 | 60 | sseq2d 4016 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑓‘𝑏) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) ↔ ([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)))) |
| 62 | | eqeq2 2749 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑓‘𝑏) → ((𝑓‘𝑎) = 𝑤 ↔ (𝑓‘𝑎) = (𝑓‘𝑏))) |
| 63 | 61, 62 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑓‘𝑏) → ((([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤) ↔ (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) → (𝑓‘𝑎) = (𝑓‘𝑏)))) |
| 64 | 46 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → 𝑓:ℕ⟶𝐺) |
| 65 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:ℕ⟶𝐺 ∧ 𝑎 ∈ ℕ) → (𝑓‘𝑎) ∈ 𝐺) |
| 66 | 64, 52, 65 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑎) ∈ 𝐺) |
| 67 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝑓‘𝑎) → ([,]‘𝑧) = ([,]‘(𝑓‘𝑎))) |
| 68 | 67 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑓‘𝑎) → (([,]‘𝑧) ⊆ ([,]‘𝑤) ↔ ([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤))) |
| 69 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑓‘𝑎) → (𝑧 = 𝑤 ↔ (𝑓‘𝑎) = 𝑤)) |
| 70 | 68, 69 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑓‘𝑎) → ((([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤))) |
| 71 | 70 | ralbidv 3178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑓‘𝑎) → (∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤))) |
| 72 | 71, 2 | elrab2 3695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑎) ∈ 𝐺 ↔ ((𝑓‘𝑎) ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤))) |
| 73 | 72 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑎) ∈ 𝐺 → ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤)) |
| 74 | 66, 73 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤)) |
| 75 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:ℕ⟶𝐺 ∧ 𝑏 ∈ ℕ) → (𝑓‘𝑏) ∈ 𝐺) |
| 76 | 64, 55, 75 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑏) ∈ 𝐺) |
| 77 | 11, 76 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑏) ∈ 𝐴) |
| 78 | 63, 74, 77 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) → (𝑓‘𝑎) = (𝑓‘𝑏))) |
| 79 | | f1of1 6847 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:ℕ–1-1-onto→𝐺 → 𝑓:ℕ–1-1→𝐺) |
| 80 | 79 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → 𝑓:ℕ–1-1→𝐺) |
| 81 | | f1fveq 7282 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:ℕ–1-1→𝐺 ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((𝑓‘𝑎) = (𝑓‘𝑏) ↔ 𝑎 = 𝑏)) |
| 82 | 80, 81 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((𝑓‘𝑎) = (𝑓‘𝑏) ↔ 𝑎 = 𝑏)) |
| 83 | | orc 868 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
| 84 | 82, 83 | biimtrdi 253 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((𝑓‘𝑎) = (𝑓‘𝑏) → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅))) |
| 85 | 78, 84 | syld 47 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅))) |
| 86 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑓‘𝑎) → ([,]‘𝑤) = ([,]‘(𝑓‘𝑎))) |
| 87 | 86 | sseq2d 4016 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑓‘𝑎) → (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) ↔ ([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)))) |
| 88 | | eqeq2 2749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑓‘𝑎) → ((𝑓‘𝑏) = 𝑤 ↔ (𝑓‘𝑏) = (𝑓‘𝑎))) |
| 89 | | eqcom 2744 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑏) = (𝑓‘𝑎) ↔ (𝑓‘𝑎) = (𝑓‘𝑏)) |
| 90 | 88, 89 | bitrdi 287 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑓‘𝑎) → ((𝑓‘𝑏) = 𝑤 ↔ (𝑓‘𝑎) = (𝑓‘𝑏))) |
| 91 | 87, 90 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑓‘𝑎) → ((([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤) ↔ (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) → (𝑓‘𝑎) = (𝑓‘𝑏)))) |
| 92 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝑓‘𝑏) → ([,]‘𝑧) = ([,]‘(𝑓‘𝑏))) |
| 93 | 92 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑓‘𝑏) → (([,]‘𝑧) ⊆ ([,]‘𝑤) ↔ ([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤))) |
| 94 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑓‘𝑏) → (𝑧 = 𝑤 ↔ (𝑓‘𝑏) = 𝑤)) |
| 95 | 93, 94 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑓‘𝑏) → ((([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤))) |
| 96 | 95 | ralbidv 3178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑓‘𝑏) → (∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤))) |
| 97 | 96, 2 | elrab2 3695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑏) ∈ 𝐺 ↔ ((𝑓‘𝑏) ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤))) |
| 98 | 97 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑏) ∈ 𝐺 → ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤)) |
| 99 | 76, 98 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤)) |
| 100 | 11, 66 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑎) ∈ 𝐴) |
| 101 | 91, 99, 100 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) → (𝑓‘𝑎) = (𝑓‘𝑏))) |
| 102 | 101, 84 | syld 47 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅))) |
| 103 | | olc 869 |
. . . . . . . . . . . . 13
⊢
((((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅ → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
| 104 | 103 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅ → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅))) |
| 105 | 85, 102, 104 | 3jaod 1431 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) ∨ ([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅) → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅))) |
| 106 | 59, 105 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
| 107 | 106 | ralrimivva 3202 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
| 108 | | 2fveq3 6911 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → ((,)‘(𝑓‘𝑎)) = ((,)‘(𝑓‘𝑏))) |
| 109 | 108 | disjor 5125 |
. . . . . . . . 9
⊢
(Disj 𝑎
∈ ℕ ((,)‘(𝑓‘𝑎)) ↔ ∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
| 110 | 107, 109 | sylibr 234 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → Disj 𝑎 ∈ ℕ
((,)‘(𝑓‘𝑎))) |
| 111 | | eqid 2737 |
. . . . . . . 8
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
| 112 | 49, 110, 111 | uniiccmbl 25625 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ∪ ran ([,] ∘ 𝑓) ∈ dom vol) |
| 113 | 45, 112 | eqeltrrd 2842 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ∪ ([,] “ 𝐺) ∈ dom vol) |
| 114 | 113 | ex 412 |
. . . . 5
⊢ (𝜑 → (𝑓:ℕ–1-1-onto→𝐺 → ∪ ([,] “ 𝐺) ∈ dom vol)) |
| 115 | 114 | exlimdv 1933 |
. . . 4
⊢ (𝜑 → (∃𝑓 𝑓:ℕ–1-1-onto→𝐺 → ∪ ([,] “ 𝐺) ∈ dom vol)) |
| 116 | | nnenom 14021 |
. . . . . 6
⊢ ℕ
≈ ω |
| 117 | | ensym 9043 |
. . . . . 6
⊢ (𝐺 ≈ ω → ω
≈ 𝐺) |
| 118 | | entr 9046 |
. . . . . 6
⊢ ((ℕ
≈ ω ∧ ω ≈ 𝐺) → ℕ ≈ 𝐺) |
| 119 | 116, 117,
118 | sylancr 587 |
. . . . 5
⊢ (𝐺 ≈ ω → ℕ
≈ 𝐺) |
| 120 | | bren 8995 |
. . . . 5
⊢ (ℕ
≈ 𝐺 ↔
∃𝑓 𝑓:ℕ–1-1-onto→𝐺) |
| 121 | 119, 120 | sylib 218 |
. . . 4
⊢ (𝐺 ≈ ω →
∃𝑓 𝑓:ℕ–1-1-onto→𝐺) |
| 122 | 115, 121 | impel 505 |
. . 3
⊢ ((𝜑 ∧ 𝐺 ≈ ω) → ∪ ([,] “ 𝐺) ∈ dom vol) |
| 123 | | reex 11246 |
. . . . . . . . 9
⊢ ℝ
∈ V |
| 124 | 123, 123 | xpex 7773 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ∈ V |
| 125 | 124 | inex2 5318 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
| 126 | 125, 15 | ssexi 5322 |
. . . . . 6
⊢ ran 𝐹 ∈ V |
| 127 | | ssdomg 9040 |
. . . . . 6
⊢ (ran
𝐹 ∈ V → (𝐺 ⊆ ran 𝐹 → 𝐺 ≼ ran 𝐹)) |
| 128 | 126, 12, 127 | mpsyl 68 |
. . . . 5
⊢ (𝜑 → 𝐺 ≼ ran 𝐹) |
| 129 | | omelon 9686 |
. . . . . . . 8
⊢ ω
∈ On |
| 130 | | znnen 16248 |
. . . . . . . . . . . 12
⊢ ℤ
≈ ℕ |
| 131 | 130, 116 | entri 9048 |
. . . . . . . . . . 11
⊢ ℤ
≈ ω |
| 132 | | nn0ennn 14020 |
. . . . . . . . . . . 12
⊢
ℕ0 ≈ ℕ |
| 133 | 132, 116 | entri 9048 |
. . . . . . . . . . 11
⊢
ℕ0 ≈ ω |
| 134 | | xpen 9180 |
. . . . . . . . . . 11
⊢ ((ℤ
≈ ω ∧ ℕ0 ≈ ω) → (ℤ
× ℕ0) ≈ (ω ×
ω)) |
| 135 | 131, 133,
134 | mp2an 692 |
. . . . . . . . . 10
⊢ (ℤ
× ℕ0) ≈ (ω × ω) |
| 136 | | xpomen 10055 |
. . . . . . . . . 10
⊢ (ω
× ω) ≈ ω |
| 137 | 135, 136 | entri 9048 |
. . . . . . . . 9
⊢ (ℤ
× ℕ0) ≈ ω |
| 138 | 137 | ensymi 9044 |
. . . . . . . 8
⊢ ω
≈ (ℤ × ℕ0) |
| 139 | | isnumi 9986 |
. . . . . . . 8
⊢ ((ω
∈ On ∧ ω ≈ (ℤ × ℕ0)) →
(ℤ × ℕ0) ∈ dom card) |
| 140 | 129, 138,
139 | mp2an 692 |
. . . . . . 7
⊢ (ℤ
× ℕ0) ∈ dom card |
| 141 | | ffn 6736 |
. . . . . . . . 9
⊢ (𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) →
𝐹 Fn (ℤ ×
ℕ0)) |
| 142 | 13, 141 | ax-mp 5 |
. . . . . . . 8
⊢ 𝐹 Fn (ℤ ×
ℕ0) |
| 143 | | dffn4 6826 |
. . . . . . . 8
⊢ (𝐹 Fn (ℤ ×
ℕ0) ↔ 𝐹:(ℤ ×
ℕ0)–onto→ran
𝐹) |
| 144 | 142, 143 | mpbi 230 |
. . . . . . 7
⊢ 𝐹:(ℤ ×
ℕ0)–onto→ran
𝐹 |
| 145 | | fodomnum 10097 |
. . . . . . 7
⊢ ((ℤ
× ℕ0) ∈ dom card → (𝐹:(ℤ ×
ℕ0)–onto→ran
𝐹 → ran 𝐹 ≼ (ℤ ×
ℕ0))) |
| 146 | 140, 144,
145 | mp2 9 |
. . . . . 6
⊢ ran 𝐹 ≼ (ℤ ×
ℕ0) |
| 147 | | domentr 9053 |
. . . . . 6
⊢ ((ran
𝐹 ≼ (ℤ ×
ℕ0) ∧ (ℤ × ℕ0) ≈
ω) → ran 𝐹
≼ ω) |
| 148 | 146, 137,
147 | mp2an 692 |
. . . . 5
⊢ ran 𝐹 ≼
ω |
| 149 | | domtr 9047 |
. . . . 5
⊢ ((𝐺 ≼ ran 𝐹 ∧ ran 𝐹 ≼ ω) → 𝐺 ≼ ω) |
| 150 | 128, 148,
149 | sylancl 586 |
. . . 4
⊢ (𝜑 → 𝐺 ≼ ω) |
| 151 | | brdom2 9022 |
. . . 4
⊢ (𝐺 ≼ ω ↔ (𝐺 ≺ ω ∨ 𝐺 ≈
ω)) |
| 152 | 150, 151 | sylib 218 |
. . 3
⊢ (𝜑 → (𝐺 ≺ ω ∨ 𝐺 ≈ ω)) |
| 153 | 37, 122, 152 | mpjaodan 961 |
. 2
⊢ (𝜑 → ∪ ([,] “ 𝐺) ∈ dom vol) |
| 154 | 4, 153 | eqeltrd 2841 |
1
⊢ (𝜑 → ∪ ([,] “ 𝐴) ∈ dom vol) |