ovolfioo

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

		Ref	Expression
	Assertion	ovolfioo	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
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		rexr	⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ℝ^* )
18	17	ad2antrr	⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝑧 ∈ ℝ^* )
19		fvco3	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) )
20		ffvelrn	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
21	20	elin2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
22		1st2nd2	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
23	21 22	syl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
24	23	fveq2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) )
25		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
26	24 25	eqtr4di	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
27	19 26	eqtrd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
28	27	eleq2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ↔ 𝑧 ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
29		ovolfcl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
30		rexr	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ^* )
31		rexr	⊢ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ^* )
32		elioo1	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ^* ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ^* ) → ( 𝑧 ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ^* ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
33	30 31 32	syl2an	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ) → ( 𝑧 ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ^* ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
34		3anass	⊢ ( ( 𝑧 ∈ ℝ^* ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ^* ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
35	33 34	bitrdi	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ) → ( 𝑧 ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ^* ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) )
36	35	3adant3	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝑧 ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ^* ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) )
37	29 36	syl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ^* ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) )
38	28 37	bitrd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ↔ ( 𝑧 ∈ ℝ^* ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) )
39	38	adantll	⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ↔ ( 𝑧 ∈ ℝ^* ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) )
40	18 39	mpbirand	⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
41	40	rexbidva	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ∃ 𝑛 ∈ ℕ 𝑧 ∈ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
42	16 41	syl5bb	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝑧 ∈ ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
43	15 42	sylan	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝑧 ∈ ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
44	43	an32s	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
45	44	ralbidva	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ∀ 𝑧 ∈ 𝐴 𝑧 ∈ ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
46	14 45	syl5bb	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
47	13 46	bitr3d	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )

Metamath Proof Explorer

Theorem ovolfioo

Proof