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 23173 |
. 2
⊢ (𝜑 → ∪ ([,] “ 𝐴) = ∪ ([,]
“ 𝐺)) |
5 | | isfinite 8432 |
. . . 4
⊢ (𝐺 ∈ Fin ↔ 𝐺 ≺
ω) |
6 | | iccf 12143 |
. . . . . 6
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
7 | | ffun 5961 |
. . . . . 6
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → Fun [,]) |
8 | | funiunfv 6410 |
. . . . . 6
⊢ (Fun [,]
→ ∪ 𝑛 ∈ 𝐺 ([,]‘𝑛) = ∪ ([,] “
𝐺)) |
9 | 6, 7, 8 | mp2b 10 |
. . . . 5
⊢ ∪ 𝑛 ∈ 𝐺 ([,]‘𝑛) = ∪ ([,] “
𝐺) |
10 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ∈ Fin) → 𝐺 ∈ Fin) |
11 | | ssrab2 3650 |
. . . . . . . . . . . . . . . 16
⊢ {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)} ⊆ 𝐴 |
12 | 2, 11 | eqsstri 3598 |
. . . . . . . . . . . . . . 15
⊢ 𝐺 ⊆ 𝐴 |
13 | 12, 3 | syl5ss 3579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ⊆ ran 𝐹) |
14 | 1 | dyadf 23165 |
. . . . . . . . . . . . . . . 16
⊢ 𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ ×
ℝ)) |
15 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) → ran
𝐹 ⊆ ( ≤ ∩
(ℝ × ℝ))) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ran 𝐹 ⊆ ( ≤ ∩ (ℝ
× ℝ)) |
17 | | inss2 3796 |
. . . . . . . . . . . . . . 15
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
18 | 16, 17 | sstri 3577 |
. . . . . . . . . . . . . 14
⊢ ran 𝐹 ⊆ (ℝ ×
ℝ) |
19 | 13, 18 | syl6ss 3580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ⊆ (ℝ ×
ℝ)) |
20 | 19 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐺 ∈ Fin) → 𝐺 ⊆ (ℝ ×
ℝ)) |
21 | 20 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → 𝑛 ∈ (ℝ ×
ℝ)) |
22 | | 1st2nd2 7096 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℝ ×
ℝ) → 𝑛 =
〈(1st ‘𝑛), (2nd ‘𝑛)〉) |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → 𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉) |
24 | 23 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → ([,]‘𝑛) = ([,]‘〈(1st
‘𝑛), (2nd
‘𝑛)〉)) |
25 | | df-ov 6552 |
. . . . . . . . 9
⊢
((1st ‘𝑛)[,](2nd ‘𝑛)) = ([,]‘〈(1st
‘𝑛), (2nd
‘𝑛)〉) |
26 | 24, 25 | syl6eqr 2662 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → ([,]‘𝑛) = ((1st ‘𝑛)[,](2nd ‘𝑛))) |
27 | | xp1st 7089 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℝ ×
ℝ) → (1st ‘𝑛) ∈ ℝ) |
28 | 21, 27 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → (1st ‘𝑛) ∈
ℝ) |
29 | | xp2nd 7090 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℝ ×
ℝ) → (2nd ‘𝑛) ∈ ℝ) |
30 | 21, 29 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → (2nd ‘𝑛) ∈
ℝ) |
31 | | iccmbl 23141 |
. . . . . . . . 9
⊢
(((1st ‘𝑛) ∈ ℝ ∧ (2nd
‘𝑛) ∈ ℝ)
→ ((1st ‘𝑛)[,](2nd ‘𝑛)) ∈ dom vol) |
32 | 28, 30, 31 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → ((1st ‘𝑛)[,](2nd ‘𝑛)) ∈ dom
vol) |
33 | 26, 32 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐺 ∈ Fin) ∧ 𝑛 ∈ 𝐺) → ([,]‘𝑛) ∈ dom vol) |
34 | 33 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ∈ Fin) → ∀𝑛 ∈ 𝐺 ([,]‘𝑛) ∈ dom vol) |
35 | | finiunmbl 23119 |
. . . . . 6
⊢ ((𝐺 ∈ Fin ∧ ∀𝑛 ∈ 𝐺 ([,]‘𝑛) ∈ dom vol) → ∪ 𝑛 ∈ 𝐺 ([,]‘𝑛) ∈ dom vol) |
36 | 10, 34, 35 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝐺 ∈ Fin) → ∪ 𝑛 ∈ 𝐺 ([,]‘𝑛) ∈ dom vol) |
37 | 9, 36 | syl5eqelr 2693 |
. . . 4
⊢ ((𝜑 ∧ 𝐺 ∈ Fin) → ∪ ([,] “ 𝐺) ∈ dom vol) |
38 | 5, 37 | sylan2br 492 |
. . 3
⊢ ((𝜑 ∧ 𝐺 ≺ ω) → ∪ ([,] “ 𝐺) ∈ dom vol) |
39 | | nnenom 12641 |
. . . . . . 7
⊢ ℕ
≈ ω |
40 | | ensym 7891 |
. . . . . . 7
⊢ (𝐺 ≈ ω → ω
≈ 𝐺) |
41 | | entr 7894 |
. . . . . . 7
⊢ ((ℕ
≈ ω ∧ ω ≈ 𝐺) → ℕ ≈ 𝐺) |
42 | 39, 40, 41 | sylancr 694 |
. . . . . 6
⊢ (𝐺 ≈ ω → ℕ
≈ 𝐺) |
43 | | bren 7850 |
. . . . . 6
⊢ (ℕ
≈ 𝐺 ↔
∃𝑓 𝑓:ℕ–1-1-onto→𝐺) |
44 | 42, 43 | sylib 207 |
. . . . 5
⊢ (𝐺 ≈ ω →
∃𝑓 𝑓:ℕ–1-1-onto→𝐺) |
45 | | rnco2 5559 |
. . . . . . . . . 10
⊢ ran ([,]
∘ 𝑓) = ([,] “
ran 𝑓) |
46 | | f1ofo 6057 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–1-1-onto→𝐺 → 𝑓:ℕ–onto→𝐺) |
47 | 46 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → 𝑓:ℕ–onto→𝐺) |
48 | | forn 6031 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐺 → ran 𝑓 = 𝐺) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ran 𝑓 = 𝐺) |
50 | 49 | imaeq2d 5385 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ([,] “ ran 𝑓) = ([,] “ 𝐺)) |
51 | 45, 50 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ran ([,] ∘ 𝑓) = ([,] “ 𝐺)) |
52 | 51 | unieqd 4382 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ∪ ran ([,] ∘ 𝑓) = ∪ ([,] “
𝐺)) |
53 | | f1of 6050 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–1-1-onto→𝐺 → 𝑓:ℕ⟶𝐺) |
54 | 13, 16 | syl6ss 3580 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ⊆ ( ≤ ∩ (ℝ ×
ℝ))) |
55 | | fss 5969 |
. . . . . . . . . 10
⊢ ((𝑓:ℕ⟶𝐺 ∧ 𝐺 ⊆ ( ≤ ∩ (ℝ ×
ℝ))) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
56 | 53, 54, 55 | syl2anr 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
57 | | fss 5969 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:ℕ⟶𝐺 ∧ 𝐺 ⊆ ran 𝐹) → 𝑓:ℕ⟶ran 𝐹) |
58 | 53, 13, 57 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → 𝑓:ℕ⟶ran 𝐹) |
59 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ) → 𝑎 ∈
ℕ) |
60 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:ℕ⟶ran 𝐹 ∧ 𝑎 ∈ ℕ) → (𝑓‘𝑎) ∈ ran 𝐹) |
61 | 58, 59, 60 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑎) ∈ ran 𝐹) |
62 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ) → 𝑏 ∈
ℕ) |
63 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:ℕ⟶ran 𝐹 ∧ 𝑏 ∈ ℕ) → (𝑓‘𝑏) ∈ ran 𝐹) |
64 | 58, 62, 63 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑏) ∈ ran 𝐹) |
65 | 1 | dyaddisj 23170 |
. . . . . . . . . . . . 13
⊢ (((𝑓‘𝑎) ∈ ran 𝐹 ∧ (𝑓‘𝑏) ∈ ran 𝐹) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) ∨ ([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
66 | 61, 64, 65 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) ∨ ([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
67 | 53 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → 𝑓:ℕ⟶𝐺) |
68 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:ℕ⟶𝐺 ∧ 𝑏 ∈ ℕ) → (𝑓‘𝑏) ∈ 𝐺) |
69 | 67, 62, 68 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑏) ∈ 𝐺) |
70 | 12, 69 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑏) ∈ 𝐴) |
71 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:ℕ⟶𝐺 ∧ 𝑎 ∈ ℕ) → (𝑓‘𝑎) ∈ 𝐺) |
72 | 67, 59, 71 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑎) ∈ 𝐺) |
73 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = (𝑓‘𝑎) → ([,]‘𝑧) = ([,]‘(𝑓‘𝑎))) |
74 | 73 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝑓‘𝑎) → (([,]‘𝑧) ⊆ ([,]‘𝑤) ↔ ([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤))) |
75 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝑓‘𝑎) → (𝑧 = 𝑤 ↔ (𝑓‘𝑎) = 𝑤)) |
76 | 74, 75 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑓‘𝑎) → ((([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤))) |
77 | 76 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑓‘𝑎) → (∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤))) |
78 | 77, 2 | elrab2 3333 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑎) ∈ 𝐺 ↔ ((𝑓‘𝑎) ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤))) |
79 | 78 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑎) ∈ 𝐺 → ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤)) |
80 | 72, 79 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤)) |
81 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (𝑓‘𝑏) → ([,]‘𝑤) = ([,]‘(𝑓‘𝑏))) |
82 | 81 | sseq2d 3596 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝑓‘𝑏) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) ↔ ([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)))) |
83 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝑓‘𝑏) → ((𝑓‘𝑎) = 𝑤 ↔ (𝑓‘𝑎) = (𝑓‘𝑏))) |
84 | 82, 83 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑓‘𝑏) → ((([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤) ↔ (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) → (𝑓‘𝑎) = (𝑓‘𝑏)))) |
85 | 84 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑏) ∈ 𝐴 → (∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘𝑤) → (𝑓‘𝑎) = 𝑤) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) → (𝑓‘𝑎) = (𝑓‘𝑏)))) |
86 | 70, 80, 85 | sylc 63 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) → (𝑓‘𝑎) = (𝑓‘𝑏))) |
87 | | f1of1 6049 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:ℕ–1-1-onto→𝐺 → 𝑓:ℕ–1-1→𝐺) |
88 | 87 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → 𝑓:ℕ–1-1→𝐺) |
89 | | f1fveq 6420 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:ℕ–1-1→𝐺 ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((𝑓‘𝑎) = (𝑓‘𝑏) ↔ 𝑎 = 𝑏)) |
90 | 88, 89 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((𝑓‘𝑎) = (𝑓‘𝑏) ↔ 𝑎 = 𝑏)) |
91 | | orc 399 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
92 | 90, 91 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((𝑓‘𝑎) = (𝑓‘𝑏) → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅))) |
93 | 86, 92 | syld 46 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅))) |
94 | 12, 72 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑓‘𝑎) ∈ 𝐴) |
95 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = (𝑓‘𝑏) → ([,]‘𝑧) = ([,]‘(𝑓‘𝑏))) |
96 | 95 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝑓‘𝑏) → (([,]‘𝑧) ⊆ ([,]‘𝑤) ↔ ([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤))) |
97 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝑓‘𝑏) → (𝑧 = 𝑤 ↔ (𝑓‘𝑏) = 𝑤)) |
98 | 96, 97 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑓‘𝑏) → ((([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤))) |
99 | 98 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑓‘𝑏) → (∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤))) |
100 | 99, 2 | elrab2 3333 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑏) ∈ 𝐺 ↔ ((𝑓‘𝑏) ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤))) |
101 | 100 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑏) ∈ 𝐺 → ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤)) |
102 | 69, 101 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤)) |
103 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (𝑓‘𝑎) → ([,]‘𝑤) = ([,]‘(𝑓‘𝑎))) |
104 | 103 | sseq2d 3596 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝑓‘𝑎) → (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) ↔ ([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)))) |
105 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (𝑓‘𝑎) → ((𝑓‘𝑏) = 𝑤 ↔ (𝑓‘𝑏) = (𝑓‘𝑎))) |
106 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓‘𝑏) = (𝑓‘𝑎) ↔ (𝑓‘𝑎) = (𝑓‘𝑏)) |
107 | 105, 106 | syl6bb 275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝑓‘𝑎) → ((𝑓‘𝑏) = 𝑤 ↔ (𝑓‘𝑎) = (𝑓‘𝑏))) |
108 | 104, 107 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑓‘𝑎) → ((([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤) ↔ (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) → (𝑓‘𝑎) = (𝑓‘𝑏)))) |
109 | 108 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑎) ∈ 𝐴 → (∀𝑤 ∈ 𝐴 (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘𝑤) → (𝑓‘𝑏) = 𝑤) → (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) → (𝑓‘𝑎) = (𝑓‘𝑏)))) |
110 | 94, 102, 109 | sylc 63 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) → (𝑓‘𝑎) = (𝑓‘𝑏))) |
111 | 110, 92 | syld 46 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅))) |
112 | | olc 398 |
. . . . . . . . . . . . . 14
⊢
((((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅ → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
113 | 112 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅ → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅))) |
114 | 93, 111, 113 | 3jaod 1384 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((([,]‘(𝑓‘𝑎)) ⊆ ([,]‘(𝑓‘𝑏)) ∨ ([,]‘(𝑓‘𝑏)) ⊆ ([,]‘(𝑓‘𝑎)) ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅) → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅))) |
115 | 66, 114 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
116 | 115 | ralrimivva 2954 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
117 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (𝑓‘𝑎) = (𝑓‘𝑏)) |
118 | 117 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → ((,)‘(𝑓‘𝑎)) = ((,)‘(𝑓‘𝑏))) |
119 | 118 | disjor 4567 |
. . . . . . . . . 10
⊢
(Disj 𝑎
∈ ℕ ((,)‘(𝑓‘𝑎)) ↔ ∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ (𝑎 = 𝑏 ∨ (((,)‘(𝑓‘𝑎)) ∩ ((,)‘(𝑓‘𝑏))) = ∅)) |
120 | 116, 119 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → Disj 𝑎 ∈ ℕ
((,)‘(𝑓‘𝑎))) |
121 | | eqid 2610 |
. . . . . . . . 9
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
122 | 56, 120, 121 | uniiccmbl 23164 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ∪ ran ([,] ∘ 𝑓) ∈ dom vol) |
123 | 52, 122 | eqeltrrd 2689 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:ℕ–1-1-onto→𝐺) → ∪ ([,] “ 𝐺) ∈ dom vol) |
124 | 123 | ex 449 |
. . . . . 6
⊢ (𝜑 → (𝑓:ℕ–1-1-onto→𝐺 → ∪ ([,] “ 𝐺) ∈ dom vol)) |
125 | 124 | exlimdv 1848 |
. . . . 5
⊢ (𝜑 → (∃𝑓 𝑓:ℕ–1-1-onto→𝐺 → ∪ ([,] “ 𝐺) ∈ dom vol)) |
126 | 44, 125 | syl5 33 |
. . . 4
⊢ (𝜑 → (𝐺 ≈ ω → ∪ ([,] “ 𝐺) ∈ dom vol)) |
127 | 126 | imp 444 |
. . 3
⊢ ((𝜑 ∧ 𝐺 ≈ ω) → ∪ ([,] “ 𝐺) ∈ dom vol) |
128 | | reex 9906 |
. . . . . . . . 9
⊢ ℝ
∈ V |
129 | 128, 128 | xpex 6860 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ∈ V |
130 | 129 | inex2 4728 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
131 | 130, 16 | ssexi 4731 |
. . . . . 6
⊢ ran 𝐹 ∈ V |
132 | | ssdomg 7887 |
. . . . . 6
⊢ (ran
𝐹 ∈ V → (𝐺 ⊆ ran 𝐹 → 𝐺 ≼ ran 𝐹)) |
133 | 131, 13, 132 | mpsyl 66 |
. . . . 5
⊢ (𝜑 → 𝐺 ≼ ran 𝐹) |
134 | | omelon 8426 |
. . . . . . . 8
⊢ ω
∈ On |
135 | | znnen 14780 |
. . . . . . . . . . . 12
⊢ ℤ
≈ ℕ |
136 | 135, 39 | entri 7896 |
. . . . . . . . . . 11
⊢ ℤ
≈ ω |
137 | | nn0ennn 12640 |
. . . . . . . . . . . 12
⊢
ℕ0 ≈ ℕ |
138 | 137, 39 | entri 7896 |
. . . . . . . . . . 11
⊢
ℕ0 ≈ ω |
139 | | xpen 8008 |
. . . . . . . . . . 11
⊢ ((ℤ
≈ ω ∧ ℕ0 ≈ ω) → (ℤ
× ℕ0) ≈ (ω ×
ω)) |
140 | 136, 138,
139 | mp2an 704 |
. . . . . . . . . 10
⊢ (ℤ
× ℕ0) ≈ (ω × ω) |
141 | | xpomen 8721 |
. . . . . . . . . 10
⊢ (ω
× ω) ≈ ω |
142 | 140, 141 | entri 7896 |
. . . . . . . . 9
⊢ (ℤ
× ℕ0) ≈ ω |
143 | 142 | ensymi 7892 |
. . . . . . . 8
⊢ ω
≈ (ℤ × ℕ0) |
144 | | isnumi 8655 |
. . . . . . . 8
⊢ ((ω
∈ On ∧ ω ≈ (ℤ × ℕ0)) →
(ℤ × ℕ0) ∈ dom card) |
145 | 134, 143,
144 | mp2an 704 |
. . . . . . 7
⊢ (ℤ
× ℕ0) ∈ dom card |
146 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) →
𝐹 Fn (ℤ ×
ℕ0)) |
147 | 14, 146 | ax-mp 5 |
. . . . . . . 8
⊢ 𝐹 Fn (ℤ ×
ℕ0) |
148 | | dffn4 6034 |
. . . . . . . 8
⊢ (𝐹 Fn (ℤ ×
ℕ0) ↔ 𝐹:(ℤ ×
ℕ0)–onto→ran
𝐹) |
149 | 147, 148 | mpbi 219 |
. . . . . . 7
⊢ 𝐹:(ℤ ×
ℕ0)–onto→ran
𝐹 |
150 | | fodomnum 8763 |
. . . . . . 7
⊢ ((ℤ
× ℕ0) ∈ dom card → (𝐹:(ℤ ×
ℕ0)–onto→ran
𝐹 → ran 𝐹 ≼ (ℤ ×
ℕ0))) |
151 | 145, 149,
150 | mp2 9 |
. . . . . 6
⊢ ran 𝐹 ≼ (ℤ ×
ℕ0) |
152 | | domentr 7901 |
. . . . . 6
⊢ ((ran
𝐹 ≼ (ℤ ×
ℕ0) ∧ (ℤ × ℕ0) ≈
ω) → ran 𝐹
≼ ω) |
153 | 151, 142,
152 | mp2an 704 |
. . . . 5
⊢ ran 𝐹 ≼
ω |
154 | | domtr 7895 |
. . . . 5
⊢ ((𝐺 ≼ ran 𝐹 ∧ ran 𝐹 ≼ ω) → 𝐺 ≼ ω) |
155 | 133, 153,
154 | sylancl 693 |
. . . 4
⊢ (𝜑 → 𝐺 ≼ ω) |
156 | | brdom2 7871 |
. . . 4
⊢ (𝐺 ≼ ω ↔ (𝐺 ≺ ω ∨ 𝐺 ≈
ω)) |
157 | 155, 156 | sylib 207 |
. . 3
⊢ (𝜑 → (𝐺 ≺ ω ∨ 𝐺 ≈ ω)) |
158 | 38, 127, 157 | mpjaodan 823 |
. 2
⊢ (𝜑 → ∪ ([,] “ 𝐺) ∈ dom vol) |
159 | 4, 158 | eqeltrd 2688 |
1
⊢ (𝜑 → ∪ ([,] “ 𝐴) ∈ dom vol) |