Metamath Proof Explorer


Theorem ovolficc

Description: Unpack the interval covering property using closed intervals. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Assertion ovolficc ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ran ( [,] ∘ 𝐹 ) ↔ ∀ 𝑧𝐴𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iccf [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
2 inss2 ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
3 rexpssxrxp ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
4 2 3 sstri ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
5 fss ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
6 4 5 mpan2 ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
7 fco ( ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( [,] ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ* )
8 1 6 7 sylancr ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( [,] ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ* )
9 ffn ( ( [,] ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ* → ( [,] ∘ 𝐹 ) Fn ℕ )
10 fniunfv ( ( [,] ∘ 𝐹 ) Fn ℕ → 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) = ran ( [,] ∘ 𝐹 ) )
11 8 9 10 3syl ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) = ran ( [,] ∘ 𝐹 ) )
12 11 sseq2d ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( 𝐴 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ 𝐴 ran ( [,] ∘ 𝐹 ) ) )
13 12 adantl ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ 𝐴 ran ( [,] ∘ 𝐹 ) ) )
14 dfss3 ( 𝐴 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∀ 𝑧𝐴 𝑧 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) )
15 ssel2 ( ( 𝐴 ⊆ ℝ ∧ 𝑧𝐴 ) → 𝑧 ∈ ℝ )
16 eliun ( 𝑧 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) )
17 simpll ( ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝑧 ∈ ℝ )
18 fvco3 ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) = ( [,] ‘ ( 𝐹𝑛 ) ) )
19 ffvelrn ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
20 19 elin2d ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ∈ ( ℝ × ℝ ) )
21 1st2nd2 ( ( 𝐹𝑛 ) ∈ ( ℝ × ℝ ) → ( 𝐹𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
22 20 21 syl ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
23 22 fveq2d ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( [,] ‘ ( 𝐹𝑛 ) ) = ( [,] ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ ) )
24 df-ov ( ( 1st ‘ ( 𝐹𝑛 ) ) [,] ( 2nd ‘ ( 𝐹𝑛 ) ) ) = ( [,] ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
25 23 24 eqtr4di ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( [,] ‘ ( 𝐹𝑛 ) ) = ( ( 1st ‘ ( 𝐹𝑛 ) ) [,] ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
26 18 25 eqtrd ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 1st ‘ ( 𝐹𝑛 ) ) [,] ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
27 26 eleq2d ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ 𝑧 ∈ ( ( 1st ‘ ( 𝐹𝑛 ) ) [,] ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
28 ovolfcl ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
29 elicc2 ( ( ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ ) → ( 𝑧 ∈ ( ( 1st ‘ ( 𝐹𝑛 ) ) [,] ( 2nd ‘ ( 𝐹𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
30 3anass ( ( 𝑧 ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
31 29 30 bitrdi ( ( ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ ) → ( 𝑧 ∈ ( ( 1st ‘ ( 𝐹𝑛 ) ) [,] ( 2nd ‘ ( 𝐹𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) ) )
32 31 3adant3 ( ( ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) → ( 𝑧 ∈ ( ( 1st ‘ ( 𝐹𝑛 ) ) [,] ( 2nd ‘ ( 𝐹𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) ) )
33 28 32 syl ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( 1st ‘ ( 𝐹𝑛 ) ) [,] ( 2nd ‘ ( 𝐹𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) ) )
34 27 33 bitrd ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) ) )
35 34 adantll ( ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) ) )
36 17 35 mpbirand ( ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
37 36 rexbidva ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ∃ 𝑛 ∈ ℕ 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
38 16 37 syl5bb ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝑧 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
39 15 38 sylan ( ( ( 𝐴 ⊆ ℝ ∧ 𝑧𝐴 ) ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝑧 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
40 39 an32s ( ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑧𝐴 ) → ( 𝑧 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
41 40 ralbidva ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ∀ 𝑧𝐴 𝑧 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∀ 𝑧𝐴𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
42 14 41 syl5bb ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∀ 𝑧𝐴𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
43 13 42 bitr3d ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ran ( [,] ∘ 𝐹 ) ↔ ∀ 𝑧𝐴𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )