ovolficc

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

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

Proof

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

Metamath Proof Explorer

Theorem ovolficc

Proof