ovolfioo

Description: Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014)

		Ref	Expression
	Assertion	ovolfioo	$⊢ (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)) < z \land z < 2^{nd} (F (n))))$

Proof

Step	Hyp	Ref	Expression
1		ioof	$⊢ (.) : ℝ^{} \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		rexr	$⊢ z \in ℝ \to z \in ℝ^{*}$
18	17	ad2antrr	$⊢ ((z \in ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \land n \in ℕ) \to z \in ℝ^{*}$
19		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to ((.) \circ F) (n) = (.) (F (n))$
20		ffvelcdm	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to F (n) \in (\leq \cap ℝ^{2})$
21	20	elin2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to F (n) \in ℝ^{2}$
22		1st2nd2	$⊢ F (n) \in ℝ^{2} \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
23	21 22	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
24	23	fveq2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (.) (F (n)) = (.) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
25		df-ov	$⊢ (1^{st} (F (n)), 2^{nd} (F (n))) = (.) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
26	24 25	eqtr4di	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (.) (F (n)) = (1^{st} (F (n)), 2^{nd} (F (n)))$
27	19 26	eqtrd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to ((.) \circ F) (n) = (1^{st} (F (n)), 2^{nd} (F (n)))$
28	27	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))))$
29		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)))$
30		rexr	$⊢ 1^{st} (F (n)) \in ℝ \to 1^{st} (F (n)) \in ℝ^{*}$
31		rexr	$⊢ 2^{nd} (F (n)) \in ℝ \to 2^{nd} (F (n)) \in ℝ^{*}$
32		elioo1	$⊢ (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)) < z \land z < 2^{nd} (F (n))))$
33	30 31 32	syl2an	$⊢ (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)) < z \land z < 2^{nd} (F (n))))$
34		3anass	$⊢ (z \in ℝ^{} \land 1^{st} (F (n)) < z \land z < 2^{nd} (F (n))) \leftrightarrow (z \in ℝ^{} \land (1^{st} (F (n)) < z \land z < 2^{nd} (F (n))))$
35	33 34	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)) < z \land z < 2^{nd} (F (n)))))$
36	35	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)) < z \land z < 2^{nd} (F (n)))))$
37	29 36	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)) < z \land z < 2^{nd} (F (n)))))$
38	28 37	bitrd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (z \in ((.) \circ F) (n) \leftrightarrow (z \in ℝ^{*} \land (1^{st} (F (n)) < z \land z < 2^{nd} (F (n)))))$
39	38	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)) < z \land z < 2^{nd} (F (n)))))$
40	18 39	mpbirand	$⊢ ((z \in ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \land n \in ℕ) \to (z \in ((.) \circ F) (n) \leftrightarrow (1^{st} (F (n)) < z \land z < 2^{nd} (F (n))))$
41	40	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)) < z \land z < 2^{nd} (F (n))))$
42	16 41	bitrid	$⊢ (z \in ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (z \in ⋃_{n \in ℕ} ((.) \circ F) (n) \leftrightarrow \exists n \in ℕ (1^{st} (F (n)) < z \land z < 2^{nd} (F (n))))$
43	15 42	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)) < z \land z < 2^{nd} (F (n))))$
44	43	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)) < z \land z < 2^{nd} (F (n))))$
45	44	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)) < z \land z < 2^{nd} (F (n))))$
46	14 45	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)) < z \land z < 2^{nd} (F (n))))$
47	13 46	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)) < z \land z < 2^{nd} (F (n))))$

Metamath Proof Explorer

Theorem ovolfioo

Proof