This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
Assertion elovolm ( 𝐵 ∈ 𝑀 ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) )

Proof

Step Hyp Ref Expression
1 elovolm.1 ⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
2 eqeq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ↔ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) )
3 2 anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) )
4 3 rexbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) )
5 4 1 elrab2 ⊢ ( 𝐵 ∈ 𝑀 ↔ ( 𝐵 ∈ ℝ* ∧ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) )
6 elovolmlem ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
7 eqid ⊢ ( ( abs ∘ − ) ∘ 𝑓 ) = ( ( abs ∘ − ) ∘ 𝑓 )
8 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
9 7 8 ovolsf ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
10 6 9 sylbi ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
11 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
12 fss ⊢ ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ* ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) : ℕ ⟶ ℝ* )
13 10 11 12 sylancl ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) : ℕ ⟶ ℝ* )
14 frn ⊢ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) : ℕ ⟶ ℝ* → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ⊆ ℝ* )
15 supxrcl ⊢ ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ⊆ ℝ* → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ∈ ℝ* )
16 13 14 15 3syl ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ∈ ℝ* )
17 eleq1 ⊢ ( 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) → ( 𝐵 ∈ ℝ* ↔ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ∈ ℝ* ) )
18 16 17 syl5ibrcom ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) → 𝐵 ∈ ℝ* ) )
19 18 imp ⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) → 𝐵 ∈ ℝ* )
20 19 adantrl ⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) → 𝐵 ∈ ℝ* )
21 20 rexlimiva ⊢ ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) → 𝐵 ∈ ℝ* )
22 21 pm4.71ri ⊢ ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ↔ ( 𝐵 ∈ ℝ* ∧ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) )
23 5 22 bitr4i ⊢ ( 𝐵 ∈ 𝑀 ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) )