Metamath Proof Explorer

Theorem elovolm

Description: Elementhood in the set M of approximations to the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypothesis elovolm.1 ⊢ M = y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
Assertion elovolm ⊢ B ∈ M ↔ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <

Proof

Step Hyp Ref Expression
1 elovolm.1 ⊢ M = y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
2 eqeq1 ⊢ y = B → y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ↔ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
3 2 anbi2d ⊢ y = B → A ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ↔ A ⊆ ⋃ ran ⁡ . ∘ f ∧ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
4 3 rexbidv ⊢ y = B → ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ↔ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
5 4 1 elrab2 ⊢ B ∈ M ↔ B ∈ ℝ * ∧ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
6 elovolmlem ⊢ f ∈ ≤ ∩ ℝ 2 ℕ ↔ f : ℕ ⟶ ≤ ∩ ℝ 2
7 eqid ⊢ abs ∘ − ∘ f = abs ∘ − ∘ f
8 eqid ⊢ seq 1 + abs ∘ − ∘ f = seq 1 + abs ∘ − ∘ f
9 7 8 ovolsf ⊢ f : ℕ ⟶ ≤ ∩ ℝ 2 → seq 1 + abs ∘ − ∘ f : ℕ ⟶ 0 +∞
10 6 9 sylbi ⊢ f ∈ ≤ ∩ ℝ 2 ℕ → seq 1 + abs ∘ − ∘ f : ℕ ⟶ 0 +∞
11 icossxr ⊢ 0 +∞ ⊆ ℝ *
12 fss ⊢ seq 1 + abs ∘ − ∘ f : ℕ ⟶ 0 +∞ ∧ 0 +∞ ⊆ ℝ * → seq 1 + abs ∘ − ∘ f : ℕ ⟶ ℝ *
13 10 11 12 sylancl ⊢ f ∈ ≤ ∩ ℝ 2 ℕ → seq 1 + abs ∘ − ∘ f : ℕ ⟶ ℝ *
14 frn ⊢ seq 1 + abs ∘ − ∘ f : ℕ ⟶ ℝ * → ran ⁡ seq 1 + abs ∘ − ∘ f ⊆ ℝ *
15 supxrcl ⊢ ran ⁡ seq 1 + abs ∘ − ∘ f ⊆ ℝ * → sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ∈ ℝ *
16 13 14 15 3syl ⊢ f ∈ ≤ ∩ ℝ 2 ℕ → sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ∈ ℝ *
17 eleq1 ⊢ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < → B ∈ ℝ * ↔ sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ∈ ℝ *
18 16 17 syl5ibrcom ⊢ f ∈ ≤ ∩ ℝ 2 ℕ → B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < → B ∈ ℝ *
19 18 imp ⊢ f ∈ ≤ ∩ ℝ 2 ℕ ∧ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < → B ∈ ℝ *
20 19 adantrl ⊢ f ∈ ≤ ∩ ℝ 2 ℕ ∧ A ⊆ ⋃ ran ⁡ . ∘ f ∧ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < → B ∈ ℝ *
21 20 rexlimiva ⊢ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < → B ∈ ℝ *
22 21 pm4.71ri ⊢ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ↔ B ∈ ℝ * ∧ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
23 5 22 bitr4i ⊢ B ∈ M ↔ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ B = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <