ovolficcss

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

		Ref	Expression
	Assertion	ovolficcss	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃ ran ([.] \circ F) \subseteq ℝ$

Proof

Step	Hyp	Ref	Expression
1		rnco2	$⊢ ran ([.] \circ F) = [.] [ran F]$
2		ffvelcdm	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land y \in ℕ) \to F (y) \in (\leq \cap ℝ^{2})$
3	2	elin2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land y \in ℕ) \to F (y) \in ℝ^{2}$
4		1st2nd2	$⊢ F (y) \in ℝ^{2} \to F (y) = ⟨1^{st} (F (y)), 2^{nd} (F (y))⟩$
5	3 4	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land y \in ℕ) \to F (y) = ⟨1^{st} (F (y)), 2^{nd} (F (y))⟩$
6	5	fveq2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land y \in ℕ) \to [.] (F (y)) = [.] (⟨1^{st} (F (y)), 2^{nd} (F (y))⟩)$
7		df-ov	$⊢ [1^{st} (F (y)), 2^{nd} (F (y))] = [.] (⟨1^{st} (F (y)), 2^{nd} (F (y))⟩)$
8	6 7	eqtr4di	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land y \in ℕ) \to [.] (F (y)) = [1^{st} (F (y)), 2^{nd} (F (y))]$
9		xp1st	$⊢ F (y) \in ℝ^{2} \to 1^{st} (F (y)) \in ℝ$
10	3 9	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land y \in ℕ) \to 1^{st} (F (y)) \in ℝ$
11		xp2nd	$⊢ F (y) \in ℝ^{2} \to 2^{nd} (F (y)) \in ℝ$
12	3 11	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land y \in ℕ) \to 2^{nd} (F (y)) \in ℝ$
13		iccssre	$⊢ (1^{st} (F (y)) \in ℝ \land 2^{nd} (F (y)) \in ℝ) \to [1^{st} (F (y)), 2^{nd} (F (y))] \subseteq ℝ$
14	10 12 13	syl2anc	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land y \in ℕ) \to [1^{st} (F (y)), 2^{nd} (F (y))] \subseteq ℝ$
15	8 14	eqsstrd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land y \in ℕ) \to [.] (F (y)) \subseteq ℝ$
16		reex	$⊢ ℝ \in V$
17	16	elpw2	$⊢ [.] (F (y)) \in 𝒫 ℝ \leftrightarrow [.] (F (y)) \subseteq ℝ$
18	15 17	sylibr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land y \in ℕ) \to [.] (F (y)) \in 𝒫 ℝ$
19	18	ralrimiva	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to \forall y \in ℕ [.] (F (y)) \in 𝒫 ℝ$
20		ffn	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to F Fn ℕ$
21		fveq2	$⊢ x = F (y) \to [.] (x) = [.] (F (y))$
22	21	eleq1d	$⊢ x = F (y) \to ([.] (x) \in 𝒫 ℝ \leftrightarrow [.] (F (y)) \in 𝒫 ℝ)$
23	22	ralrn	$⊢ F Fn ℕ \to (\forall x \in ran F [.] (x) \in 𝒫 ℝ \leftrightarrow \forall y \in ℕ [.] (F (y)) \in 𝒫 ℝ)$
24	20 23	syl	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to (\forall x \in ran F [.] (x) \in 𝒫 ℝ \leftrightarrow \forall y \in ℕ [.] (F (y)) \in 𝒫 ℝ)$
25	19 24	mpbird	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to \forall x \in ran F [.] (x) \in 𝒫 ℝ$
26		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
27		ffun	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*} \to Fun [.]$
28	26 27	ax-mp	$⊢ Fun [.]$
29		frn	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ran F \subseteq \leq \cap ℝ^{2}$
30		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
31		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
32	30 31	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
33	26	fdmi	$⊢ dom [.] = ℝ^{} \times ℝ^{}$
34	32 33	sseqtrri	$⊢ \leq \cap ℝ^{2} \subseteq dom [.]$
35	29 34	sstrdi	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ran F \subseteq dom [.]$
36		funimass4	$⊢ (Fun [.] \land ran F \subseteq dom [.]) \to ([.] [ran F] \subseteq 𝒫 ℝ \leftrightarrow \forall x \in ran F [.] (x) \in 𝒫 ℝ)$
37	28 35 36	sylancr	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ([.] [ran F] \subseteq 𝒫 ℝ \leftrightarrow \forall x \in ran F [.] (x) \in 𝒫 ℝ)$
38	25 37	mpbird	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to [.] [ran F] \subseteq 𝒫 ℝ$
39	1 38	eqsstrid	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ran ([.] \circ F) \subseteq 𝒫 ℝ$
40		sspwuni	$⊢ ran ([.] \circ F) \subseteq 𝒫 ℝ \leftrightarrow ⋃ ran ([.] \circ F) \subseteq ℝ$
41	39 40	sylib	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃ ran ([.] \circ F) \subseteq ℝ$

Metamath Proof Explorer

Theorem ovolficcss

Proof