Metamath Proof Explorer

Theorem ovolctb

Description: The volume of a denumerable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014) (Proof shortened by Mario Carneiro, 25-Mar-2015)

Ref Expression
Assertion ovolctb ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≈ ℕ ) → ( vol* ‘ 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 bren ⊢ ( ℕ ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐴 )
2 simpll ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → 𝐴 ⊆ ℝ )
3 f1of ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → 𝑓 : ℕ ⟶ 𝐴 )
4 3 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → 𝑓 : ℕ ⟶ 𝐴 )
5 4 ffvelrnda ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 )
6 2 5 sseldd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
7 6 leidd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑥 ) )
8 df-br ⊢ ( ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑥 ) ↔ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ∈ ≤ )
9 7 8 sylib ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ∈ ≤ )
10 6 6 opelxpd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ∈ ( ℝ × ℝ ) )
11 9 10 elind ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
12 df-ov ⊢ ( ( 𝑓 ‘ 𝑥 ) I ( 𝑓 ‘ 𝑥 ) ) = ( I ‘ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ )
13 opex ⊢ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ∈ V
14 fvi ⊢ ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ∈ V → ( I ‘ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) = ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ )
15 13 14 ax-mp ⊢ ( I ‘ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) = ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩
16 12 15 eqtri ⊢ ( ( 𝑓 ‘ 𝑥 ) I ( 𝑓 ‘ 𝑥 ) ) = ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩
17 16 mpteq2i ⊢ ( 𝑥 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑥 ) I ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℕ ↦ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ )
18 11 17 fmptd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝑥 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑥 ) I ( 𝑓 ‘ 𝑥 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
19 nnex ⊢ ℕ ∈ V
20 19 a1i ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ℕ ∈ V )
21 6 recnd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
22 4 feqmptd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → 𝑓 = ( 𝑥 ∈ ℕ ↦ ( 𝑓 ‘ 𝑥 ) ) )
23 20 21 21 22 22 offval2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝑓 ∘f I 𝑓 ) = ( 𝑥 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑥 ) I ( 𝑓 ‘ 𝑥 ) ) ) )
24 23 feq1d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( ( 𝑓 ∘f I 𝑓 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ↔ ( 𝑥 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑥 ) I ( 𝑓 ‘ 𝑥 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) )
25 18 24 mpbird ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝑓 ∘f I 𝑓 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
26 f1ofo ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → 𝑓 : ℕ –onto→ 𝐴 )
27 26 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → 𝑓 : ℕ –onto→ 𝐴 )
28 forn ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ran 𝑓 = 𝐴 )
29 27 28 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ran 𝑓 = 𝐴 )
30 29 eleq2d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝑦 ∈ ran 𝑓 ↔ 𝑦 ∈ 𝐴 ) )
31 f1ofn ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → 𝑓 Fn ℕ )
32 31 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → 𝑓 Fn ℕ )
33 fvelrnb ⊢ ( 𝑓 Fn ℕ → ( 𝑦 ∈ ran 𝑓 ↔ ∃ 𝑥 ∈ ℕ ( 𝑓 ‘ 𝑥 ) = 𝑦 ) )
34 32 33 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝑦 ∈ ran 𝑓 ↔ ∃ 𝑥 ∈ ℕ ( 𝑓 ‘ 𝑥 ) = 𝑦 ) )
35 30 34 bitr3d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝑦 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ℕ ( 𝑓 ‘ 𝑥 ) = 𝑦 ) )
36 23 17 eqtrdi ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝑓 ∘f I 𝑓 ) = ( 𝑥 ∈ ℕ ↦ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) )
37 36 fveq1d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℕ ↦ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) ‘ 𝑥 ) )
38 eqid ⊢ ( 𝑥 ∈ ℕ ↦ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ ℕ ↦ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ )
39 38 fvmpt2 ⊢ ( ( 𝑥 ∈ ℕ ∧ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ∈ V ) → ( ( 𝑥 ∈ ℕ ↦ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) ‘ 𝑥 ) = ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ )
40 13 39 mpan2 ⊢ ( 𝑥 ∈ ℕ → ( ( 𝑥 ∈ ℕ ↦ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) ‘ 𝑥 ) = ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ )
41 37 40 sylan9eq ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) = ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ )
42 41 fveq2d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) = ( 1st ‘ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) )
43 fvex ⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
44 43 43 op1st ⊢ ( 1st ‘ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) = ( 𝑓 ‘ 𝑥 )
45 42 44 eqtrdi ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) = ( 𝑓 ‘ 𝑥 ) )
46 45 7 eqbrtrd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ ( 𝑓 ‘ 𝑥 ) )
47 41 fveq2d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) = ( 2nd ‘ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) )
48 43 43 op2nd ⊢ ( 2nd ‘ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) = ( 𝑓 ‘ 𝑥 )
49 47 48 eqtrdi ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) = ( 𝑓 ‘ 𝑥 ) )
50 7 49 breqtrrd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑓 ‘ 𝑥 ) ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) )
51 46 50 jca ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ) )
52 breq2 ⊢ ( ( 𝑓 ‘ 𝑥 ) = 𝑦 → ( ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ ( 𝑓 ‘ 𝑥 ) ↔ ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ 𝑦 ) )
53 breq1 ⊢ ( ( 𝑓 ‘ 𝑥 ) = 𝑦 → ( ( 𝑓 ‘ 𝑥 ) ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ↔ 𝑦 ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ) )
54 52 53 anbi12d ⊢ ( ( 𝑓 ‘ 𝑥 ) = 𝑦 → ( ( ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ) ↔ ( ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ 𝑦 ∧ 𝑦 ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ) ) )
55 51 54 syl5ibcom ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑓 ‘ 𝑥 ) = 𝑦 → ( ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ 𝑦 ∧ 𝑦 ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ) ) )
56 55 reximdva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( ∃ 𝑥 ∈ ℕ ( 𝑓 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ ℕ ( ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ 𝑦 ∧ 𝑦 ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ) ) )
57 35 56 sylbid ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝑦 ∈ 𝐴 → ∃ 𝑥 ∈ ℕ ( ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ 𝑦 ∧ 𝑦 ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ) ) )
58 57 ralrimiv ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ ℕ ( ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ 𝑦 ∧ 𝑦 ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ) )
59 ovolficc ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑓 ∘f I 𝑓 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( [,] ∘ ( 𝑓 ∘f I 𝑓 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ ℕ ( ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ 𝑦 ∧ 𝑦 ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ) ) )
60 25 59 syldan ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝐴 ⊆ ∪ ran ( [,] ∘ ( 𝑓 ∘f I 𝑓 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ ℕ ( ( 1st ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ≤ 𝑦 ∧ 𝑦 ≤ ( 2nd ‘ ( ( 𝑓 ∘f I 𝑓 ) ‘ 𝑥 ) ) ) ) )
61 58 60 mpbird ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → 𝐴 ⊆ ∪ ran ( [,] ∘ ( 𝑓 ∘f I 𝑓 ) ) )
62 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) )
63 62 ovollb2 ⊢ ( ( ( 𝑓 ∘f I 𝑓 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ ( 𝑓 ∘f I 𝑓 ) ) ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) ) , ℝ* , < ) )
64 25 61 63 syl2anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) ) , ℝ* , < ) )
65 21 21 opelxpd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ∈ ( ℂ × ℂ ) )
66 absf ⊢ abs : ℂ ⟶ ℝ
67 subf ⊢ − : ( ℂ × ℂ ) ⟶ ℂ
68 fco ⊢ ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
69 66 67 68 mp2an ⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
70 69 a1i ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
71 70 feqmptd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( abs ∘ − ) = ( 𝑦 ∈ ( ℂ × ℂ ) ↦ ( ( abs ∘ − ) ‘ 𝑦 ) ) )
72 fveq2 ⊢ ( 𝑦 = ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ → ( ( abs ∘ − ) ‘ 𝑦 ) = ( ( abs ∘ − ) ‘ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ ) )
73 df-ov ⊢ ( ( 𝑓 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑓 ‘ 𝑥 ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ )
74 72 73 eqtr4di ⊢ ( 𝑦 = ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑥 ) ⟩ → ( ( abs ∘ − ) ‘ 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑓 ‘ 𝑥 ) ) )
75 65 36 71 74 fmptco ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) = ( 𝑥 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑓 ‘ 𝑥 ) ) ) )
76 cnmet ⊢ ( abs ∘ − ) ∈ ( Met ‘ ℂ )
77 met0 ⊢ ( ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) ∧ ( 𝑓 ‘ 𝑥 ) ∈ ℂ ) → ( ( 𝑓 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑓 ‘ 𝑥 ) ) = 0 )
78 76 21 77 sylancr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑓 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑓 ‘ 𝑥 ) ) = 0 )
79 78 mpteq2dva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝑥 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℕ ↦ 0 ) )
80 75 79 eqtrd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) = ( 𝑥 ∈ ℕ ↦ 0 ) )
81 fconstmpt ⊢ ( ℕ × { 0 } ) = ( 𝑥 ∈ ℕ ↦ 0 )
82 80 81 eqtr4di ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) = ( ℕ × { 0 } ) )
83 82 seqeq3d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) ) = seq 1 ( + , ( ℕ × { 0 } ) ) )
84 1z ⊢ 1 ∈ ℤ
85 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
86 85 ser0f ⊢ ( 1 ∈ ℤ → seq 1 ( + , ( ℕ × { 0 } ) ) = ( ℕ × { 0 } ) )
87 84 86 ax-mp ⊢ seq 1 ( + , ( ℕ × { 0 } ) ) = ( ℕ × { 0 } )
88 83 87 eqtrdi ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) ) = ( ℕ × { 0 } ) )
89 88 rneqd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) ) = ran ( ℕ × { 0 } ) )
90 1nn ⊢ 1 ∈ ℕ
91 ne0i ⊢ ( 1 ∈ ℕ → ℕ ≠ ∅ )
92 rnxp ⊢ ( ℕ ≠ ∅ → ran ( ℕ × { 0 } ) = { 0 } )
93 90 91 92 mp2b ⊢ ran ( ℕ × { 0 } ) = { 0 }
94 89 93 eqtrdi ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) ) = { 0 } )
95 94 supeq1d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) ) , ℝ* , < ) = sup ( { 0 } , ℝ* , < ) )
96 xrltso ⊢ < Or ℝ*
97 0xr ⊢ 0 ∈ ℝ*
98 supsn ⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
99 96 97 98 mp2an ⊢ sup ( { 0 } , ℝ* , < ) = 0
100 95 99 eqtrdi ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑓 ∘f I 𝑓 ) ) ) , ℝ* , < ) = 0 )
101 64 100 breqtrd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( vol* ‘ 𝐴 ) ≤ 0 )
102 ovolge0 ⊢ ( 𝐴 ⊆ ℝ → 0 ≤ ( vol* ‘ 𝐴 ) )
103 102 adantr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → 0 ≤ ( vol* ‘ 𝐴 ) )
104 ovolcl ⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) ∈ ℝ* )
105 104 adantr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( vol* ‘ 𝐴 ) ∈ ℝ* )
106 xrletri3 ⊢ ( ( ( vol* ‘ 𝐴 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( vol* ‘ 𝐴 ) = 0 ↔ ( ( vol* ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( vol* ‘ 𝐴 ) ) ) )
107 105 97 106 sylancl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( ( vol* ‘ 𝐴 ) = 0 ↔ ( ( vol* ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( vol* ‘ 𝐴 ) ) ) )
108 101 103 107 mpbir2and ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( vol* ‘ 𝐴 ) = 0 )
109 108 ex ⊢ ( 𝐴 ⊆ ℝ → ( 𝑓 : ℕ –1-1-onto→ 𝐴 → ( vol* ‘ 𝐴 ) = 0 ) )
110 109 exlimdv ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐴 → ( vol* ‘ 𝐴 ) = 0 ) )
111 1 110 syl5bi ⊢ ( 𝐴 ⊆ ℝ → ( ℕ ≈ 𝐴 → ( vol* ‘ 𝐴 ) = 0 ) )
112 ensym ⊢ ( 𝐴 ≈ ℕ → ℕ ≈ 𝐴 )
113 111 112 impel ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≈ ℕ ) → ( vol* ‘ 𝐴 ) = 0 )