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 ( [,] ∘ 𝐹 ) ⊆ ℝ )