# Metamath Proof Explorer

## Theorem ovolfioo

Description: Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Assertion ovolfioo $⊢ A ⊆ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 → A ⊆ ⋃ ran ⁡ . ∘ F ↔ ∀ z ∈ A ∃ n ∈ ℕ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$

### Proof

Step Hyp Ref Expression
1 ioof $⊢ . : ℝ * × ℝ * ⟶ 𝒫 ℝ$
2 inss2 $⊢ ≤ ∩ ℝ 2 ⊆ ℝ 2$
3 rexpssxrxp $⊢ ℝ 2 ⊆ ℝ * × ℝ *$
4 2 3 sstri $⊢ ≤ ∩ ℝ 2 ⊆ ℝ * × ℝ *$
5 fss $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ ≤ ∩ ℝ 2 ⊆ ℝ * × ℝ * → F : ℕ ⟶ ℝ * × ℝ *$
6 4 5 mpan2 $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 → F : ℕ ⟶ ℝ * × ℝ *$
7 fco $⊢ . : ℝ * × ℝ * ⟶ 𝒫 ℝ ∧ F : ℕ ⟶ ℝ * × ℝ * → . ∘ F : ℕ ⟶ 𝒫 ℝ$
8 1 6 7 sylancr $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 → . ∘ F : ℕ ⟶ 𝒫 ℝ$
9 ffn $⊢ . ∘ F : ℕ ⟶ 𝒫 ℝ → . ∘ F Fn ℕ$
10 fniunfv $⊢ . ∘ F Fn ℕ → ⋃ n ∈ ℕ . ∘ F ⁡ n = ⋃ ran ⁡ . ∘ F$
11 8 9 10 3syl $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 → ⋃ n ∈ ℕ . ∘ F ⁡ n = ⋃ ran ⁡ . ∘ F$
12 11 sseq2d $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 → A ⊆ ⋃ n ∈ ℕ . ∘ F ⁡ n ↔ A ⊆ ⋃ ran ⁡ . ∘ F$
13 12 adantl $⊢ A ⊆ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 → A ⊆ ⋃ n ∈ ℕ . ∘ F ⁡ n ↔ A ⊆ ⋃ ran ⁡ . ∘ F$
14 dfss3 $⊢ A ⊆ ⋃ n ∈ ℕ . ∘ F ⁡ n ↔ ∀ z ∈ A z ∈ ⋃ n ∈ ℕ . ∘ F ⁡ n$
15 ssel2 $⊢ A ⊆ ℝ ∧ z ∈ A → z ∈ ℝ$
16 eliun $⊢ z ∈ ⋃ n ∈ ℕ . ∘ F ⁡ n ↔ ∃ n ∈ ℕ z ∈ . ∘ F ⁡ n$
17 rexr $⊢ z ∈ ℝ → z ∈ ℝ *$
18 17 ad2antrr $⊢ z ∈ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → z ∈ ℝ *$
19 fvco3 $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → . ∘ F ⁡ n = . ⁡ F ⁡ n$
20 ffvelrn $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → F ⁡ n ∈ ≤ ∩ ℝ 2$
21 20 elin2d $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → F ⁡ n ∈ ℝ 2$
22 1st2nd2 $⊢ F ⁡ n ∈ ℝ 2 → F ⁡ n = 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n$
23 21 22 syl $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → F ⁡ n = 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n$
24 23 fveq2d $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → . ⁡ F ⁡ n = . ⁡ 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n$
25 df-ov $⊢ 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n = . ⁡ 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n$
26 24 25 eqtr4di $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → . ⁡ F ⁡ n = 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n$
27 19 26 eqtrd $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → . ∘ F ⁡ n = 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n$
28 27 eleq2d $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → z ∈ . ∘ F ⁡ n ↔ z ∈ 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n$
29 ovolfcl $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → 1 st ⁡ F ⁡ n ∈ ℝ ∧ 2 nd ⁡ F ⁡ n ∈ ℝ ∧ 1 st ⁡ F ⁡ n ≤ 2 nd ⁡ F ⁡ n$
30 rexr $⊢ 1 st ⁡ F ⁡ n ∈ ℝ → 1 st ⁡ F ⁡ n ∈ ℝ *$
31 rexr $⊢ 2 nd ⁡ F ⁡ n ∈ ℝ → 2 nd ⁡ F ⁡ n ∈ ℝ *$
32 elioo1 $⊢ 1 st ⁡ F ⁡ n ∈ ℝ * ∧ 2 nd ⁡ F ⁡ n ∈ ℝ * → z ∈ 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n ↔ z ∈ ℝ * ∧ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
33 30 31 32 syl2an $⊢ 1 st ⁡ F ⁡ n ∈ ℝ ∧ 2 nd ⁡ F ⁡ n ∈ ℝ → z ∈ 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n ↔ z ∈ ℝ * ∧ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
34 3anass $⊢ z ∈ ℝ * ∧ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n ↔ z ∈ ℝ * ∧ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
35 33 34 bitrdi $⊢ 1 st ⁡ F ⁡ n ∈ ℝ ∧ 2 nd ⁡ F ⁡ n ∈ ℝ → z ∈ 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n ↔ z ∈ ℝ * ∧ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
36 35 3adant3 $⊢ 1 st ⁡ F ⁡ n ∈ ℝ ∧ 2 nd ⁡ F ⁡ n ∈ ℝ ∧ 1 st ⁡ F ⁡ n ≤ 2 nd ⁡ F ⁡ n → z ∈ 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n ↔ z ∈ ℝ * ∧ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
37 29 36 syl $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → z ∈ 1 st ⁡ F ⁡ n 2 nd ⁡ F ⁡ n ↔ z ∈ ℝ * ∧ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
38 28 37 bitrd $⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → z ∈ . ∘ F ⁡ n ↔ z ∈ ℝ * ∧ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
39 38 adantll $⊢ z ∈ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → z ∈ . ∘ F ⁡ n ↔ z ∈ ℝ * ∧ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
40 18 39 mpbirand $⊢ z ∈ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → z ∈ . ∘ F ⁡ n ↔ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
41 40 rexbidva $⊢ z ∈ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 → ∃ n ∈ ℕ z ∈ . ∘ F ⁡ n ↔ ∃ n ∈ ℕ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
42 16 41 syl5bb $⊢ z ∈ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 → z ∈ ⋃ n ∈ ℕ . ∘ F ⁡ n ↔ ∃ n ∈ ℕ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
43 15 42 sylan $⊢ A ⊆ ℝ ∧ z ∈ A ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 → z ∈ ⋃ n ∈ ℕ . ∘ F ⁡ n ↔ ∃ n ∈ ℕ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
44 43 an32s $⊢ A ⊆ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ z ∈ A → z ∈ ⋃ n ∈ ℕ . ∘ F ⁡ n ↔ ∃ n ∈ ℕ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
45 44 ralbidva $⊢ A ⊆ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 → ∀ z ∈ A z ∈ ⋃ n ∈ ℕ . ∘ F ⁡ n ↔ ∀ z ∈ A ∃ n ∈ ℕ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
46 14 45 syl5bb $⊢ A ⊆ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 → A ⊆ ⋃ n ∈ ℕ . ∘ F ⁡ n ↔ ∀ z ∈ A ∃ n ∈ ℕ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$
47 13 46 bitr3d $⊢ A ⊆ ℝ ∧ F : ℕ ⟶ ≤ ∩ ℝ 2 → A ⊆ ⋃ ran ⁡ . ∘ F ↔ ∀ z ∈ A ∃ n ∈ ℕ 1 st ⁡ F ⁡ n < z ∧ z < 2 nd ⁡ F ⁡ n$