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 ffvelrn ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝐹𝑦 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
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 ( [,] ∘ 𝐹 ) ⊆ ℝ )