ovolficc

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

		Ref	Expression
	Assertion	ovolficc	$⊢ (A \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃ ran ([.] \circ F) \leftrightarrow \forall z \in A \exists n \in ℕ (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$

Proof

Step	Hyp	Ref	Expression
1		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
2		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
3		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
4	2 3	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
5		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
6	4 5	mpan2	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
7		fco	$⊢ ([.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{} \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ([.] \circ F) : ℕ ⟶ 𝒫 ℝ^{}$
8	1 6 7	sylancr	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ([.] \circ F) : ℕ ⟶ 𝒫 ℝ^{*}$
9		ffn	$⊢ ([.] \circ F) : ℕ ⟶ 𝒫 ℝ^{*} \to ([.] \circ F) Fn ℕ$
10		fniunfv	$⊢ ([.] \circ F) Fn ℕ \to ⋃_{n \in ℕ} ([.] \circ F) (n) = ⋃ ran ([.] \circ F)$
11	8 9 10	3syl	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃_{n \in ℕ} ([.] \circ F) (n) = ⋃ ran ([.] \circ F)$
12	11	sseq2d	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to (A \subseteq ⋃_{n \in ℕ} ([.] \circ F) (n) \leftrightarrow A \subseteq ⋃ ran ([.] \circ F))$
13	12	adantl	$⊢ (A \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃_{n \in ℕ} ([.] \circ F) (n) \leftrightarrow A \subseteq ⋃ ran ([.] \circ F))$
14		dfss3	$⊢ A \subseteq ⋃_{n \in ℕ} ([.] \circ F) (n) \leftrightarrow \forall z \in A z \in ⋃_{n \in ℕ} ([.] \circ F) (n)$
15		ssel2	$⊢ (A \subseteq ℝ \land z \in A) \to z \in ℝ$
16		eliun	$⊢ z \in ⋃_{n \in ℕ} ([.] \circ F) (n) \leftrightarrow \exists n \in ℕ z \in ([.] \circ F) (n)$
17		simpll	$⊢ ((z \in ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \land n \in ℕ) \to z \in ℝ$
18		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to ([.] \circ F) (n) = [.] (F (n))$
19		ffvelcdm	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to F (n) \in (\leq \cap ℝ^{2})$
20	19	elin2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to F (n) \in ℝ^{2}$
21		1st2nd2	$⊢ F (n) \in ℝ^{2} \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
22	20 21	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
23	22	fveq2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to [.] (F (n)) = [.] (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
24		df-ov	$⊢ [1^{st} (F (n)), 2^{nd} (F (n))] = [.] (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
25	23 24	eqtr4di	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to [.] (F (n)) = [1^{st} (F (n)), 2^{nd} (F (n))]$
26	18 25	eqtrd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to ([.] \circ F) (n) = [1^{st} (F (n)), 2^{nd} (F (n))]$
27	26	eleq2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (z \in ([.] \circ F) (n) \leftrightarrow z \in [1^{st} (F (n)), 2^{nd} (F (n))])$
28		ovolfcl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n)))$
29		elicc2	$⊢ (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ) \to (z \in [1^{st} (F (n)), 2^{nd} (F (n))] \leftrightarrow (z \in ℝ \land 1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$
30		3anass	$⊢ (z \in ℝ \land 1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))) \leftrightarrow (z \in ℝ \land (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$
31	29 30	bitrdi	$⊢ (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ) \to (z \in [1^{st} (F (n)), 2^{nd} (F (n))] \leftrightarrow (z \in ℝ \land (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n)))))$
32	31	3adant3	$⊢ (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n))) \to (z \in [1^{st} (F (n)), 2^{nd} (F (n))] \leftrightarrow (z \in ℝ \land (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n)))))$
33	28 32	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (z \in [1^{st} (F (n)), 2^{nd} (F (n))] \leftrightarrow (z \in ℝ \land (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n)))))$
34	27 33	bitrd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (z \in ([.] \circ F) (n) \leftrightarrow (z \in ℝ \land (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n)))))$
35	34	adantll	$⊢ ((z \in ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \land n \in ℕ) \to (z \in ([.] \circ F) (n) \leftrightarrow (z \in ℝ \land (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n)))))$
36	17 35	mpbirand	$⊢ ((z \in ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \land n \in ℕ) \to (z \in ([.] \circ F) (n) \leftrightarrow (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$
37	36	rexbidva	$⊢ (z \in ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (\exists n \in ℕ z \in ([.] \circ F) (n) \leftrightarrow \exists n \in ℕ (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$
38	16 37	bitrid	$⊢ (z \in ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (z \in ⋃_{n \in ℕ} ([.] \circ F) (n) \leftrightarrow \exists n \in ℕ (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$
39	15 38	sylan	$⊢ ((A \subseteq ℝ \land z \in A) \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (z \in ⋃_{n \in ℕ} ([.] \circ F) (n) \leftrightarrow \exists n \in ℕ (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$
40	39	an32s	$⊢ ((A \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \land z \in A) \to (z \in ⋃_{n \in ℕ} ([.] \circ F) (n) \leftrightarrow \exists n \in ℕ (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$
41	40	ralbidva	$⊢ (A \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (\forall z \in A z \in ⋃_{n \in ℕ} ([.] \circ F) (n) \leftrightarrow \forall z \in A \exists n \in ℕ (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$
42	14 41	bitrid	$⊢ (A \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃_{n \in ℕ} ([.] \circ F) (n) \leftrightarrow \forall z \in A \exists n \in ℕ (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$
43	13 42	bitr3d	$⊢ (A \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃ ran ([.] \circ F) \leftrightarrow \forall z \in A \exists n \in ℕ (1^{st} (F (n)) \leq z \land z \leq 2^{nd} (F (n))))$

Metamath Proof Explorer

Theorem ovolficc

Proof