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

Metamath Proof Explorer

Theorem ovolficcss

Description: Any (closed) interval covering is a subset of the reals. (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Assertion ovolficcss ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )

Proof

Step Hyp Ref Expression
1 rnco2 ⊢ ran ( [,] ∘ 𝐹 ) = ( [,] “ ran 𝐹 )
2 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
3 2 elin2d ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ × ℝ ) )
4 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑦 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ⟩ )
5 3 4 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝐹 ‘ 𝑦 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ⟩ )
6 5 fveq2d ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) = ( [,] ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ⟩ ) )
7 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( [,] ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ⟩ )
8 6 7 eqtr4di ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
9 xp1st ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
10 3 9 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
11 xp2nd ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
12 3 11 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
13 iccssre ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ) ⊆ ℝ )
14 10 12 13 syl2anc ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ) ⊆ ℝ )
15 8 14 eqsstrd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )
16 reex ⊢ ℝ ∈ V
17 16 elpw2 ⊢ ( ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ ↔ ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )
18 15 17 sylibr ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ )
19 18 ralrimiva ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∀ 𝑦 ∈ ℕ ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ )
20 ffn ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 Fn ℕ )
21 fveq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( [,] ‘ 𝑥 ) = ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) )
22 21 eleq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ↔ ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ ) )
23 22 ralrn ⊢ ( 𝐹 Fn ℕ → ( ∀ 𝑥 ∈ ran 𝐹 ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ↔ ∀ 𝑦 ∈ ℕ ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ ) )
24 20 23 syl ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ∀ 𝑥 ∈ ran 𝐹 ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ↔ ∀ 𝑦 ∈ ℕ ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ ) )
25 19 24 mpbird ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∀ 𝑥 ∈ ran 𝐹 ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ )
26 iccf ⊢ [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
27 ffun ⊢ ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → Fun [,] )
28 26 27 ax-mp ⊢ Fun [,]
29 frn ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) )
30 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
31 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
32 30 31 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
33 26 fdmi ⊢ dom [,] = ( ℝ* × ℝ* )
34 32 33 sseqtrri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ dom [,]
35 29 34 sstrdi ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran 𝐹 ⊆ dom [,] )
36 funimass4 ⊢ ( ( Fun [,] ∧ ran 𝐹 ⊆ dom [,] ) → ( ( [,] “ ran 𝐹 ) ⊆ 𝒫 ℝ ↔ ∀ 𝑥 ∈ ran 𝐹 ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ) )
37 28 35 36 sylancr ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( [,] “ ran 𝐹 ) ⊆ 𝒫 ℝ ↔ ∀ 𝑥 ∈ ran 𝐹 ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ) )
38 25 37 mpbird ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( [,] “ ran 𝐹 ) ⊆ 𝒫 ℝ )
39 1 38 eqsstrid ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran ( [,] ∘ 𝐹 ) ⊆ 𝒫 ℝ )
40 sspwuni ⊢ ( ran ( [,] ∘ 𝐹 ) ⊆ 𝒫 ℝ ↔ ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
41 39 40 sylib ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )