| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bren 8995 | . . 3
⊢ (ℕ
≈ 𝐴 ↔
∃𝑓 𝑓:ℕ–1-1-onto→𝐴) | 
| 2 |  | simpll 767 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → 𝐴 ⊆ ℝ) | 
| 3 |  | f1of 6848 | . . . . . . . . . . . . . . . 16
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ⟶𝐴) | 
| 4 | 3 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ⟶𝐴) | 
| 5 | 4 | ffvelcdmda 7104 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (𝑓‘𝑥) ∈ 𝐴) | 
| 6 | 2, 5 | sseldd 3984 | . . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (𝑓‘𝑥) ∈ ℝ) | 
| 7 | 6 | leidd 11829 | . . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (𝑓‘𝑥) ≤ (𝑓‘𝑥)) | 
| 8 |  | df-br 5144 | . . . . . . . . . . . 12
⊢ ((𝑓‘𝑥) ≤ (𝑓‘𝑥) ↔ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ ≤ ) | 
| 9 | 7, 8 | sylib 218 | . . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ ≤ ) | 
| 10 | 6, 6 | opelxpd 5724 | . . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ (ℝ ×
ℝ)) | 
| 11 | 9, 10 | elind 4200 | . . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) | 
| 12 |  | df-ov 7434 | . . . . . . . . . . . 12
⊢ ((𝑓‘𝑥) I (𝑓‘𝑥)) = ( I ‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) | 
| 13 |  | opex 5469 | . . . . . . . . . . . . 13
⊢
〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ V | 
| 14 |  | fvi 6985 | . . . . . . . . . . . . 13
⊢
(〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ V → ( I
‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) | 
| 15 | 13, 14 | ax-mp 5 | . . . . . . . . . . . 12
⊢ ( I
‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 | 
| 16 | 12, 15 | eqtri 2765 | . . . . . . . . . . 11
⊢ ((𝑓‘𝑥) I (𝑓‘𝑥)) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 | 
| 17 | 16 | mpteq2i 5247 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℕ ↦ ((𝑓‘𝑥) I (𝑓‘𝑥))) = (𝑥 ∈ ℕ ↦ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) | 
| 18 | 11, 17 | fmptd 7134 | . . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑥 ∈ ℕ ↦ ((𝑓‘𝑥) I (𝑓‘𝑥))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 19 |  | nnex 12272 | . . . . . . . . . . . 12
⊢ ℕ
∈ V | 
| 20 | 19 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ℕ ∈
V) | 
| 21 | 6 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (𝑓‘𝑥) ∈ ℂ) | 
| 22 | 4 | feqmptd 6977 | . . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓 = (𝑥 ∈ ℕ ↦ (𝑓‘𝑥))) | 
| 23 | 20, 21, 21, 22, 22 | offval2 7717 | . . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑓 ∘f I 𝑓) = (𝑥 ∈ ℕ ↦ ((𝑓‘𝑥) I (𝑓‘𝑥)))) | 
| 24 | 23 | feq1d 6720 | . . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((𝑓 ∘f I 𝑓):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ↔ (𝑥
∈ ℕ ↦ ((𝑓‘𝑥) I (𝑓‘𝑥))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)))) | 
| 25 | 18, 24 | mpbird 257 | . . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑓 ∘f I 𝑓):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 26 |  | f1ofo 6855 | . . . . . . . . . . . . . . 15
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ–onto→𝐴) | 
| 27 | 26 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ–onto→𝐴) | 
| 28 |  | forn 6823 | . . . . . . . . . . . . . 14
⊢ (𝑓:ℕ–onto→𝐴 → ran 𝑓 = 𝐴) | 
| 29 | 27, 28 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ran 𝑓 = 𝐴) | 
| 30 | 29 | eleq2d 2827 | . . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑦 ∈ ran 𝑓 ↔ 𝑦 ∈ 𝐴)) | 
| 31 |  | f1ofn 6849 | . . . . . . . . . . . . . 14
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓 Fn ℕ) | 
| 32 | 31 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓 Fn ℕ) | 
| 33 |  | fvelrnb 6969 | . . . . . . . . . . . . 13
⊢ (𝑓 Fn ℕ → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ ℕ (𝑓‘𝑥) = 𝑦)) | 
| 34 | 32, 33 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ ℕ (𝑓‘𝑥) = 𝑦)) | 
| 35 | 30, 34 | bitr3d 281 | . . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ ℕ (𝑓‘𝑥) = 𝑦)) | 
| 36 | 23, 17 | eqtrdi 2793 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑓 ∘f I 𝑓) = (𝑥 ∈ ℕ ↦ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉)) | 
| 37 | 36 | fveq1d 6908 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((𝑓 ∘f I 𝑓)‘𝑥) = ((𝑥 ∈ ℕ ↦ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉)‘𝑥)) | 
| 38 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℕ ↦
〈(𝑓‘𝑥), (𝑓‘𝑥)〉) = (𝑥 ∈ ℕ ↦ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) | 
| 39 | 38 | fvmpt2 7027 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧
〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ V) → ((𝑥 ∈ ℕ ↦ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉)‘𝑥) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) | 
| 40 | 13, 39 | mpan2 691 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℕ → ((𝑥 ∈ ℕ ↦
〈(𝑓‘𝑥), (𝑓‘𝑥)〉)‘𝑥) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) | 
| 41 | 37, 40 | sylan9eq 2797 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → ((𝑓 ∘f I 𝑓)‘𝑥) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) | 
| 42 | 41 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (1st
‘((𝑓
∘f I 𝑓)‘𝑥)) = (1st ‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉)) | 
| 43 |  | fvex 6919 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓‘𝑥) ∈ V | 
| 44 | 43, 43 | op1st 8022 | . . . . . . . . . . . . . . . 16
⊢
(1st ‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) = (𝑓‘𝑥) | 
| 45 | 42, 44 | eqtrdi 2793 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (1st
‘((𝑓
∘f I 𝑓)‘𝑥)) = (𝑓‘𝑥)) | 
| 46 | 45, 7 | eqbrtrd 5165 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (1st
‘((𝑓
∘f I 𝑓)‘𝑥)) ≤ (𝑓‘𝑥)) | 
| 47 | 41 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (2nd
‘((𝑓
∘f I 𝑓)‘𝑥)) = (2nd ‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉)) | 
| 48 | 43, 43 | op2nd 8023 | . . . . . . . . . . . . . . . 16
⊢
(2nd ‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) = (𝑓‘𝑥) | 
| 49 | 47, 48 | eqtrdi 2793 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (2nd
‘((𝑓
∘f I 𝑓)‘𝑥)) = (𝑓‘𝑥)) | 
| 50 | 7, 49 | breqtrrd 5171 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (𝑓‘𝑥) ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥))) | 
| 51 | 46, 50 | jca 511 | . . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → ((1st
‘((𝑓
∘f I 𝑓)‘𝑥)) ≤ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥)))) | 
| 52 |  | breq2 5147 | . . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑥) = 𝑦 → ((1st ‘((𝑓 ∘f I 𝑓)‘𝑥)) ≤ (𝑓‘𝑥) ↔ (1st ‘((𝑓 ∘f I 𝑓)‘𝑥)) ≤ 𝑦)) | 
| 53 |  | breq1 5146 | . . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑥) = 𝑦 → ((𝑓‘𝑥) ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥)) ↔ 𝑦 ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥)))) | 
| 54 | 52, 53 | anbi12d 632 | . . . . . . . . . . . . 13
⊢ ((𝑓‘𝑥) = 𝑦 → (((1st ‘((𝑓 ∘f I 𝑓)‘𝑥)) ≤ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥))) ↔ ((1st ‘((𝑓 ∘f I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥))))) | 
| 55 | 51, 54 | syl5ibcom 245 | . . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → ((𝑓‘𝑥) = 𝑦 → ((1st ‘((𝑓 ∘f I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥))))) | 
| 56 | 55 | reximdva 3168 | . . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (∃𝑥 ∈ ℕ (𝑓‘𝑥) = 𝑦 → ∃𝑥 ∈ ℕ ((1st
‘((𝑓
∘f I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥))))) | 
| 57 | 35, 56 | sylbid 240 | . . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑦 ∈ 𝐴 → ∃𝑥 ∈ ℕ ((1st
‘((𝑓
∘f I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥))))) | 
| 58 | 57 | ralrimiv 3145 | . . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ∀𝑦 ∈ 𝐴 ∃𝑥 ∈ ℕ ((1st
‘((𝑓
∘f I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥)))) | 
| 59 |  | ovolficc 25503 | . . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ (𝑓 ∘f I 𝑓):ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
([,] ∘ (𝑓
∘f I 𝑓))
↔ ∀𝑦 ∈
𝐴 ∃𝑥 ∈ ℕ ((1st
‘((𝑓
∘f I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥))))) | 
| 60 | 25, 59 | syldan 591 | . . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝐴 ⊆ ∪ ran
([,] ∘ (𝑓
∘f I 𝑓))
↔ ∀𝑦 ∈
𝐴 ∃𝑥 ∈ ℕ ((1st
‘((𝑓
∘f I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘f I 𝑓)‘𝑥))))) | 
| 61 | 58, 60 | mpbird 257 | . . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝐴 ⊆ ∪ ran
([,] ∘ (𝑓
∘f I 𝑓))) | 
| 62 |  | eqid 2737 | . . . . . . . . 9
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑓 ∘f I 𝑓))) = seq1( + , ((abs ∘ − )
∘ (𝑓
∘f I 𝑓))) | 
| 63 | 62 | ovollb2 25524 | . . . . . . . 8
⊢ (((𝑓 ∘f I 𝑓):ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ (𝑓
∘f I 𝑓)))
→ (vol*‘𝐴) ≤
sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑓 ∘f I 𝑓))), ℝ*, <
)) | 
| 64 | 25, 61, 63 | syl2anc 584 | . . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (vol*‘𝐴) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑓 ∘f I 𝑓))), ℝ*, <
)) | 
| 65 | 21, 21 | opelxpd 5724 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ (ℂ ×
ℂ)) | 
| 66 |  | absf 15376 | . . . . . . . . . . . . . . . . . . 19
⊢
abs:ℂ⟶ℝ | 
| 67 |  | subf 11510 | . . . . . . . . . . . . . . . . . . 19
⊢  −
:(ℂ × ℂ)⟶ℂ | 
| 68 |  | fco 6760 | . . . . . . . . . . . . . . . . . . 19
⊢
((abs:ℂ⟶ℝ ∧ − :(ℂ ×
ℂ)⟶ℂ) → (abs ∘ − ):(ℂ ×
ℂ)⟶ℝ) | 
| 69 | 66, 67, 68 | mp2an 692 | . . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ):(ℂ × ℂ)⟶ℝ | 
| 70 | 69 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (abs ∘ −
):(ℂ × ℂ)⟶ℝ) | 
| 71 | 70 | feqmptd 6977 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (abs ∘ − )
= (𝑦 ∈ (ℂ
× ℂ) ↦ ((abs ∘ − )‘𝑦))) | 
| 72 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 → ((abs ∘ −
)‘𝑦) = ((abs ∘
− )‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉)) | 
| 73 |  | df-ov 7434 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥)) = ((abs ∘ −
)‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) | 
| 74 | 72, 73 | eqtr4di 2795 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 → ((abs ∘ −
)‘𝑦) = ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥))) | 
| 75 | 65, 36, 71, 74 | fmptco 7149 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((abs ∘ − )
∘ (𝑓
∘f I 𝑓)) =
(𝑥 ∈ ℕ ↦
((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥)))) | 
| 76 |  | cnmet 24792 | . . . . . . . . . . . . . . . . 17
⊢ (abs
∘ − ) ∈ (Met‘ℂ) | 
| 77 |  | met0 24353 | . . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ (𝑓‘𝑥) ∈ ℂ) → ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥)) = 0) | 
| 78 | 76, 21, 77 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥)) = 0) | 
| 79 | 78 | mpteq2dva 5242 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑥 ∈ ℕ ↦ ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥))) = (𝑥 ∈ ℕ ↦ 0)) | 
| 80 | 75, 79 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((abs ∘ − )
∘ (𝑓
∘f I 𝑓)) =
(𝑥 ∈ ℕ ↦
0)) | 
| 81 |  | fconstmpt 5747 | . . . . . . . . . . . . . 14
⊢ (ℕ
× {0}) = (𝑥 ∈
ℕ ↦ 0) | 
| 82 | 80, 81 | eqtr4di 2795 | . . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((abs ∘ − )
∘ (𝑓
∘f I 𝑓)) =
(ℕ × {0})) | 
| 83 | 82 | seqeq3d 14050 | . . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → seq1( + , ((abs ∘
− ) ∘ (𝑓
∘f I 𝑓)))
= seq1( + , (ℕ × {0}))) | 
| 84 |  | 1z 12647 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℤ | 
| 85 |  | nnuz 12921 | . . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) | 
| 86 | 85 | ser0f 14096 | . . . . . . . . . . . . 13
⊢ (1 ∈
ℤ → seq1( + , (ℕ × {0})) = (ℕ ×
{0})) | 
| 87 | 84, 86 | ax-mp 5 | . . . . . . . . . . . 12
⊢ seq1( + ,
(ℕ × {0})) = (ℕ × {0}) | 
| 88 | 83, 87 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → seq1( + , ((abs ∘
− ) ∘ (𝑓
∘f I 𝑓)))
= (ℕ × {0})) | 
| 89 | 88 | rneqd 5949 | . . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ran seq1( + , ((abs
∘ − ) ∘ (𝑓 ∘f I 𝑓))) = ran (ℕ ×
{0})) | 
| 90 |  | 1nn 12277 | . . . . . . . . . . 11
⊢ 1 ∈
ℕ | 
| 91 |  | ne0i 4341 | . . . . . . . . . . 11
⊢ (1 ∈
ℕ → ℕ ≠ ∅) | 
| 92 |  | rnxp 6190 | . . . . . . . . . . 11
⊢ (ℕ
≠ ∅ → ran (ℕ × {0}) = {0}) | 
| 93 | 90, 91, 92 | mp2b 10 | . . . . . . . . . 10
⊢ ran
(ℕ × {0}) = {0} | 
| 94 | 89, 93 | eqtrdi 2793 | . . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ran seq1( + , ((abs
∘ − ) ∘ (𝑓 ∘f I 𝑓))) = {0}) | 
| 95 | 94 | supeq1d 9486 | . . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑓 ∘f I 𝑓))), ℝ*, < ) = sup({0},
ℝ*, < )) | 
| 96 |  | xrltso 13183 | . . . . . . . . 9
⊢  < Or
ℝ* | 
| 97 |  | 0xr 11308 | . . . . . . . . 9
⊢ 0 ∈
ℝ* | 
| 98 |  | supsn 9512 | . . . . . . . . 9
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) | 
| 99 | 96, 97, 98 | mp2an 692 | . . . . . . . 8
⊢ sup({0},
ℝ*, < ) = 0 | 
| 100 | 95, 99 | eqtrdi 2793 | . . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑓 ∘f I 𝑓))), ℝ*, < ) =
0) | 
| 101 | 64, 100 | breqtrd 5169 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (vol*‘𝐴) ≤ 0) | 
| 102 |  | ovolge0 25516 | . . . . . . 7
⊢ (𝐴 ⊆ ℝ → 0 ≤
(vol*‘𝐴)) | 
| 103 | 102 | adantr 480 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 0 ≤
(vol*‘𝐴)) | 
| 104 |  | ovolcl 25513 | . . . . . . . 8
⊢ (𝐴 ⊆ ℝ →
(vol*‘𝐴) ∈
ℝ*) | 
| 105 | 104 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (vol*‘𝐴) ∈
ℝ*) | 
| 106 |  | xrletri3 13196 | . . . . . . 7
⊢
(((vol*‘𝐴)
∈ ℝ* ∧ 0 ∈ ℝ*) →
((vol*‘𝐴) = 0 ↔
((vol*‘𝐴) ≤ 0
∧ 0 ≤ (vol*‘𝐴)))) | 
| 107 | 105, 97, 106 | sylancl 586 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((vol*‘𝐴) = 0 ↔ ((vol*‘𝐴) ≤ 0 ∧ 0 ≤
(vol*‘𝐴)))) | 
| 108 | 101, 103,
107 | mpbir2and 713 | . . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (vol*‘𝐴) = 0) | 
| 109 | 108 | ex 412 | . . . 4
⊢ (𝐴 ⊆ ℝ → (𝑓:ℕ–1-1-onto→𝐴 → (vol*‘𝐴) = 0)) | 
| 110 | 109 | exlimdv 1933 | . . 3
⊢ (𝐴 ⊆ ℝ →
(∃𝑓 𝑓:ℕ–1-1-onto→𝐴 → (vol*‘𝐴) = 0)) | 
| 111 | 1, 110 | biimtrid 242 | . 2
⊢ (𝐴 ⊆ ℝ → (ℕ
≈ 𝐴 →
(vol*‘𝐴) =
0)) | 
| 112 |  | ensym 9043 | . 2
⊢ (𝐴 ≈ ℕ → ℕ
≈ 𝐴) | 
| 113 | 111, 112 | impel 505 | 1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≈ ℕ) →
(vol*‘𝐴) =
0) |