Step |
Hyp |
Ref |
Expression |
1 |
|
dyadmbl.1 |
⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ 〈 ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) 〉 ) |
2 |
|
dyadmbl.2 |
⊢ 𝐺 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) } |
3 |
|
dyadmbl.3 |
⊢ ( 𝜑 → 𝐴 ⊆ ran 𝐹 ) |
4 |
1 2 3
|
dyadmbllem |
⊢ ( 𝜑 → ∪ ( [,] “ 𝐴 ) = ∪ ( [,] “ 𝐺 ) ) |
5 |
|
isfinite |
⊢ ( 𝐺 ∈ Fin ↔ 𝐺 ≺ ω ) |
6 |
|
iccf |
⊢ [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* |
7 |
|
ffun |
⊢ ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → Fun [,] ) |
8 |
|
funiunfv |
⊢ ( Fun [,] → ∪ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) = ∪ ( [,] “ 𝐺 ) ) |
9 |
6 7 8
|
mp2b |
⊢ ∪ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) = ∪ ( [,] “ 𝐺 ) |
10 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ Fin ) → 𝐺 ∈ Fin ) |
11 |
2
|
ssrab3 |
⊢ 𝐺 ⊆ 𝐴 |
12 |
11 3
|
sstrid |
⊢ ( 𝜑 → 𝐺 ⊆ ran 𝐹 ) |
13 |
1
|
dyadf |
⊢ 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) |
14 |
|
frn |
⊢ ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
15 |
13 14
|
ax-mp |
⊢ ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) |
16 |
|
inss2 |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) |
17 |
15 16
|
sstri |
⊢ ran 𝐹 ⊆ ( ℝ × ℝ ) |
18 |
12 17
|
sstrdi |
⊢ ( 𝜑 → 𝐺 ⊆ ( ℝ × ℝ ) ) |
19 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ Fin ) → 𝐺 ⊆ ( ℝ × ℝ ) ) |
20 |
19
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → 𝑛 ∈ ( ℝ × ℝ ) ) |
21 |
|
1st2nd2 |
⊢ ( 𝑛 ∈ ( ℝ × ℝ ) → 𝑛 = 〈 ( 1st ‘ 𝑛 ) , ( 2nd ‘ 𝑛 ) 〉 ) |
22 |
20 21
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → 𝑛 = 〈 ( 1st ‘ 𝑛 ) , ( 2nd ‘ 𝑛 ) 〉 ) |
23 |
22
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( [,] ‘ 𝑛 ) = ( [,] ‘ 〈 ( 1st ‘ 𝑛 ) , ( 2nd ‘ 𝑛 ) 〉 ) ) |
24 |
|
df-ov |
⊢ ( ( 1st ‘ 𝑛 ) [,] ( 2nd ‘ 𝑛 ) ) = ( [,] ‘ 〈 ( 1st ‘ 𝑛 ) , ( 2nd ‘ 𝑛 ) 〉 ) |
25 |
23 24
|
eqtr4di |
⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( [,] ‘ 𝑛 ) = ( ( 1st ‘ 𝑛 ) [,] ( 2nd ‘ 𝑛 ) ) ) |
26 |
|
xp1st |
⊢ ( 𝑛 ∈ ( ℝ × ℝ ) → ( 1st ‘ 𝑛 ) ∈ ℝ ) |
27 |
20 26
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( 1st ‘ 𝑛 ) ∈ ℝ ) |
28 |
|
xp2nd |
⊢ ( 𝑛 ∈ ( ℝ × ℝ ) → ( 2nd ‘ 𝑛 ) ∈ ℝ ) |
29 |
20 28
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( 2nd ‘ 𝑛 ) ∈ ℝ ) |
30 |
|
iccmbl |
⊢ ( ( ( 1st ‘ 𝑛 ) ∈ ℝ ∧ ( 2nd ‘ 𝑛 ) ∈ ℝ ) → ( ( 1st ‘ 𝑛 ) [,] ( 2nd ‘ 𝑛 ) ) ∈ dom vol ) |
31 |
27 29 30
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( ( 1st ‘ 𝑛 ) [,] ( 2nd ‘ 𝑛 ) ) ∈ dom vol ) |
32 |
25 31
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( [,] ‘ 𝑛 ) ∈ dom vol ) |
33 |
32
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ Fin ) → ∀ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) ∈ dom vol ) |
34 |
|
finiunmbl |
⊢ ( ( 𝐺 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) ∈ dom vol ) → ∪ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) ∈ dom vol ) |
35 |
10 33 34
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ Fin ) → ∪ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) ∈ dom vol ) |
36 |
9 35
|
eqeltrrid |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ Fin ) → ∪ ( [,] “ 𝐺 ) ∈ dom vol ) |
37 |
5 36
|
sylan2br |
⊢ ( ( 𝜑 ∧ 𝐺 ≺ ω ) → ∪ ( [,] “ 𝐺 ) ∈ dom vol ) |
38 |
|
rnco2 |
⊢ ran ( [,] ∘ 𝑓 ) = ( [,] “ ran 𝑓 ) |
39 |
|
f1ofo |
⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐺 → 𝑓 : ℕ –onto→ 𝐺 ) |
40 |
39
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → 𝑓 : ℕ –onto→ 𝐺 ) |
41 |
|
forn |
⊢ ( 𝑓 : ℕ –onto→ 𝐺 → ran 𝑓 = 𝐺 ) |
42 |
40 41
|
syl |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ran 𝑓 = 𝐺 ) |
43 |
42
|
imaeq2d |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ( [,] “ ran 𝑓 ) = ( [,] “ 𝐺 ) ) |
44 |
38 43
|
syl5eq |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ran ( [,] ∘ 𝑓 ) = ( [,] “ 𝐺 ) ) |
45 |
44
|
unieqd |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ∪ ran ( [,] ∘ 𝑓 ) = ∪ ( [,] “ 𝐺 ) ) |
46 |
|
f1of |
⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐺 → 𝑓 : ℕ ⟶ 𝐺 ) |
47 |
12 15
|
sstrdi |
⊢ ( 𝜑 → 𝐺 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
48 |
|
fss |
⊢ ( ( 𝑓 : ℕ ⟶ 𝐺 ∧ 𝐺 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
49 |
46 47 48
|
syl2anr |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
50 |
|
fss |
⊢ ( ( 𝑓 : ℕ ⟶ 𝐺 ∧ 𝐺 ⊆ ran 𝐹 ) → 𝑓 : ℕ ⟶ ran 𝐹 ) |
51 |
46 12 50
|
syl2anr |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → 𝑓 : ℕ ⟶ ran 𝐹 ) |
52 |
|
simpl |
⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) → 𝑎 ∈ ℕ ) |
53 |
|
ffvelrn |
⊢ ( ( 𝑓 : ℕ ⟶ ran 𝐹 ∧ 𝑎 ∈ ℕ ) → ( 𝑓 ‘ 𝑎 ) ∈ ran 𝐹 ) |
54 |
51 52 53
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑎 ) ∈ ran 𝐹 ) |
55 |
|
simpr |
⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) → 𝑏 ∈ ℕ ) |
56 |
|
ffvelrn |
⊢ ( ( 𝑓 : ℕ ⟶ ran 𝐹 ∧ 𝑏 ∈ ℕ ) → ( 𝑓 ‘ 𝑏 ) ∈ ran 𝐹 ) |
57 |
51 55 56
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑏 ) ∈ ran 𝐹 ) |
58 |
1
|
dyaddisj |
⊢ ( ( ( 𝑓 ‘ 𝑎 ) ∈ ran 𝐹 ∧ ( 𝑓 ‘ 𝑏 ) ∈ ran 𝐹 ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ∨ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) |
59 |
54 57 58
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ∨ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) |
60 |
|
fveq2 |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑏 ) → ( [,] ‘ 𝑤 ) = ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ) |
61 |
60
|
sseq2d |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑏 ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ) ) |
62 |
|
eqeq2 |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑏 ) → ( ( 𝑓 ‘ 𝑎 ) = 𝑤 ↔ ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) ) |
63 |
61 62
|
imbi12d |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑏 ) → ( ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ↔ ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) ) ) |
64 |
46
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → 𝑓 : ℕ ⟶ 𝐺 ) |
65 |
|
ffvelrn |
⊢ ( ( 𝑓 : ℕ ⟶ 𝐺 ∧ 𝑎 ∈ ℕ ) → ( 𝑓 ‘ 𝑎 ) ∈ 𝐺 ) |
66 |
64 52 65
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑎 ) ∈ 𝐺 ) |
67 |
|
fveq2 |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑎 ) → ( [,] ‘ 𝑧 ) = ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ) |
68 |
67
|
sseq1d |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑎 ) → ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) ) ) |
69 |
|
eqeq1 |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑎 ) → ( 𝑧 = 𝑤 ↔ ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ) |
70 |
68 69
|
imbi12d |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑎 ) → ( ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ) ) |
71 |
70
|
ralbidv |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑎 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ) ) |
72 |
71 2
|
elrab2 |
⊢ ( ( 𝑓 ‘ 𝑎 ) ∈ 𝐺 ↔ ( ( 𝑓 ‘ 𝑎 ) ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ) ) |
73 |
72
|
simprbi |
⊢ ( ( 𝑓 ‘ 𝑎 ) ∈ 𝐺 → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ) |
74 |
66 73
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ) |
75 |
|
ffvelrn |
⊢ ( ( 𝑓 : ℕ ⟶ 𝐺 ∧ 𝑏 ∈ ℕ ) → ( 𝑓 ‘ 𝑏 ) ∈ 𝐺 ) |
76 |
64 55 75
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑏 ) ∈ 𝐺 ) |
77 |
11 76
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑏 ) ∈ 𝐴 ) |
78 |
63 74 77
|
rspcdva |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) ) |
79 |
|
f1of1 |
⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐺 → 𝑓 : ℕ –1-1→ 𝐺 ) |
80 |
79
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → 𝑓 : ℕ –1-1→ 𝐺 ) |
81 |
|
f1fveq |
⊢ ( ( 𝑓 : ℕ –1-1→ 𝐺 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) ) |
82 |
80 81
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) ) |
83 |
|
orc |
⊢ ( 𝑎 = 𝑏 → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) |
84 |
82 83
|
syl6bi |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) ) |
85 |
78 84
|
syld |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) ) |
86 |
|
fveq2 |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑎 ) → ( [,] ‘ 𝑤 ) = ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ) |
87 |
86
|
sseq2d |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑎 ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ) ) |
88 |
|
eqeq2 |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑎 ) → ( ( 𝑓 ‘ 𝑏 ) = 𝑤 ↔ ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ 𝑎 ) ) ) |
89 |
|
eqcom |
⊢ ( ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ 𝑎 ) ↔ ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) |
90 |
88 89
|
bitrdi |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑎 ) → ( ( 𝑓 ‘ 𝑏 ) = 𝑤 ↔ ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) ) |
91 |
87 90
|
imbi12d |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑎 ) → ( ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ↔ ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) ) ) |
92 |
|
fveq2 |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑏 ) → ( [,] ‘ 𝑧 ) = ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ) |
93 |
92
|
sseq1d |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑏 ) → ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) ) ) |
94 |
|
eqeq1 |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑏 ) → ( 𝑧 = 𝑤 ↔ ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ) |
95 |
93 94
|
imbi12d |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑏 ) → ( ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ) ) |
96 |
95
|
ralbidv |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑏 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ) ) |
97 |
96 2
|
elrab2 |
⊢ ( ( 𝑓 ‘ 𝑏 ) ∈ 𝐺 ↔ ( ( 𝑓 ‘ 𝑏 ) ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ) ) |
98 |
97
|
simprbi |
⊢ ( ( 𝑓 ‘ 𝑏 ) ∈ 𝐺 → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ) |
99 |
76 98
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ) |
100 |
11 66
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑎 ) ∈ 𝐴 ) |
101 |
91 99 100
|
rspcdva |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) ) |
102 |
101 84
|
syld |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) ) |
103 |
|
olc |
⊢ ( ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) |
104 |
103
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) ) |
105 |
85 102 104
|
3jaod |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ∨ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) ) |
106 |
59 105
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) |
107 |
106
|
ralrimivva |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) |
108 |
|
2fveq3 |
⊢ ( 𝑎 = 𝑏 → ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) = ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) |
109 |
108
|
disjor |
⊢ ( Disj 𝑎 ∈ ℕ ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ↔ ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) |
110 |
107 109
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → Disj 𝑎 ∈ ℕ ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ) |
111 |
|
eqid |
⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) |
112 |
49 110 111
|
uniiccmbl |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ∪ ran ( [,] ∘ 𝑓 ) ∈ dom vol ) |
113 |
45 112
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ∪ ( [,] “ 𝐺 ) ∈ dom vol ) |
114 |
113
|
ex |
⊢ ( 𝜑 → ( 𝑓 : ℕ –1-1-onto→ 𝐺 → ∪ ( [,] “ 𝐺 ) ∈ dom vol ) ) |
115 |
114
|
exlimdv |
⊢ ( 𝜑 → ( ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐺 → ∪ ( [,] “ 𝐺 ) ∈ dom vol ) ) |
116 |
|
nnenom |
⊢ ℕ ≈ ω |
117 |
|
ensym |
⊢ ( 𝐺 ≈ ω → ω ≈ 𝐺 ) |
118 |
|
entr |
⊢ ( ( ℕ ≈ ω ∧ ω ≈ 𝐺 ) → ℕ ≈ 𝐺 ) |
119 |
116 117 118
|
sylancr |
⊢ ( 𝐺 ≈ ω → ℕ ≈ 𝐺 ) |
120 |
|
bren |
⊢ ( ℕ ≈ 𝐺 ↔ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐺 ) |
121 |
119 120
|
sylib |
⊢ ( 𝐺 ≈ ω → ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐺 ) |
122 |
115 121
|
impel |
⊢ ( ( 𝜑 ∧ 𝐺 ≈ ω ) → ∪ ( [,] “ 𝐺 ) ∈ dom vol ) |
123 |
|
reex |
⊢ ℝ ∈ V |
124 |
123 123
|
xpex |
⊢ ( ℝ × ℝ ) ∈ V |
125 |
124
|
inex2 |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ∈ V |
126 |
125 15
|
ssexi |
⊢ ran 𝐹 ∈ V |
127 |
|
ssdomg |
⊢ ( ran 𝐹 ∈ V → ( 𝐺 ⊆ ran 𝐹 → 𝐺 ≼ ran 𝐹 ) ) |
128 |
126 12 127
|
mpsyl |
⊢ ( 𝜑 → 𝐺 ≼ ran 𝐹 ) |
129 |
|
omelon |
⊢ ω ∈ On |
130 |
|
znnen |
⊢ ℤ ≈ ℕ |
131 |
130 116
|
entri |
⊢ ℤ ≈ ω |
132 |
|
nn0ennn |
⊢ ℕ0 ≈ ℕ |
133 |
132 116
|
entri |
⊢ ℕ0 ≈ ω |
134 |
|
xpen |
⊢ ( ( ℤ ≈ ω ∧ ℕ0 ≈ ω ) → ( ℤ × ℕ0 ) ≈ ( ω × ω ) ) |
135 |
131 133 134
|
mp2an |
⊢ ( ℤ × ℕ0 ) ≈ ( ω × ω ) |
136 |
|
xpomen |
⊢ ( ω × ω ) ≈ ω |
137 |
135 136
|
entri |
⊢ ( ℤ × ℕ0 ) ≈ ω |
138 |
137
|
ensymi |
⊢ ω ≈ ( ℤ × ℕ0 ) |
139 |
|
isnumi |
⊢ ( ( ω ∈ On ∧ ω ≈ ( ℤ × ℕ0 ) ) → ( ℤ × ℕ0 ) ∈ dom card ) |
140 |
129 138 139
|
mp2an |
⊢ ( ℤ × ℕ0 ) ∈ dom card |
141 |
|
ffn |
⊢ ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 Fn ( ℤ × ℕ0 ) ) |
142 |
13 141
|
ax-mp |
⊢ 𝐹 Fn ( ℤ × ℕ0 ) |
143 |
|
dffn4 |
⊢ ( 𝐹 Fn ( ℤ × ℕ0 ) ↔ 𝐹 : ( ℤ × ℕ0 ) –onto→ ran 𝐹 ) |
144 |
142 143
|
mpbi |
⊢ 𝐹 : ( ℤ × ℕ0 ) –onto→ ran 𝐹 |
145 |
|
fodomnum |
⊢ ( ( ℤ × ℕ0 ) ∈ dom card → ( 𝐹 : ( ℤ × ℕ0 ) –onto→ ran 𝐹 → ran 𝐹 ≼ ( ℤ × ℕ0 ) ) ) |
146 |
140 144 145
|
mp2 |
⊢ ran 𝐹 ≼ ( ℤ × ℕ0 ) |
147 |
|
domentr |
⊢ ( ( ran 𝐹 ≼ ( ℤ × ℕ0 ) ∧ ( ℤ × ℕ0 ) ≈ ω ) → ran 𝐹 ≼ ω ) |
148 |
146 137 147
|
mp2an |
⊢ ran 𝐹 ≼ ω |
149 |
|
domtr |
⊢ ( ( 𝐺 ≼ ran 𝐹 ∧ ran 𝐹 ≼ ω ) → 𝐺 ≼ ω ) |
150 |
128 148 149
|
sylancl |
⊢ ( 𝜑 → 𝐺 ≼ ω ) |
151 |
|
brdom2 |
⊢ ( 𝐺 ≼ ω ↔ ( 𝐺 ≺ ω ∨ 𝐺 ≈ ω ) ) |
152 |
150 151
|
sylib |
⊢ ( 𝜑 → ( 𝐺 ≺ ω ∨ 𝐺 ≈ ω ) ) |
153 |
37 122 152
|
mpjaodan |
⊢ ( 𝜑 → ∪ ( [,] “ 𝐺 ) ∈ dom vol ) |
154 |
4 153
|
eqeltrd |
⊢ ( 𝜑 → ∪ ( [,] “ 𝐴 ) ∈ dom vol ) |