Theorem ovolficcss 25538

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

Assertion

Ref	Expression
ovolficcss	⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)

Proof of Theorem ovolficcss

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rnco2 6241	. . 3 ⊢ ran ([,] ∘ 𝐹) = ([,] “ ran 𝐹)
2		ffvelcdm 7062	. . . . . . . . . . . 12 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) ∈ ( ≤ ∩ (ℝ × ℝ)))
3	2	elin2d 4158	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) ∈ (ℝ × ℝ))
4		1st2nd2 8009	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑦) ∈ (ℝ × ℝ) → (𝐹‘𝑦) = ⟨(1st ‘(𝐹‘𝑦)), (2nd ‘(𝐹‘𝑦))⟩)
5	3, 4	syl 17	. . . . . . . . . 10 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) = ⟨(1st ‘(𝐹‘𝑦)), (2nd ‘(𝐹‘𝑦))⟩)
6	5	fveq2d 6871	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) = ([,]‘⟨(1st ‘(𝐹‘𝑦)), (2nd ‘(𝐹‘𝑦))⟩))
7		df-ov 7399	. . . . . . . . 9 ⊢ ((1st ‘(𝐹‘𝑦))[,](2nd ‘(𝐹‘𝑦))) = ([,]‘⟨(1st ‘(𝐹‘𝑦)), (2nd ‘(𝐹‘𝑦))⟩)
8	6, 7	eqtr4di 2816	. . . . . . . 8 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) = ((1st ‘(𝐹‘𝑦))[,](2nd ‘(𝐹‘𝑦))))
9		xp1st 8002	. . . . . . . . . 10 ⊢ ((𝐹‘𝑦) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘𝑦)) ∈ ℝ)
10	3, 9	syl 17	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (1st ‘(𝐹‘𝑦)) ∈ ℝ)
11		xp2nd 8003	. . . . . . . . . 10 ⊢ ((𝐹‘𝑦) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘𝑦)) ∈ ℝ)
12	3, 11	syl 17	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (2nd ‘(𝐹‘𝑦)) ∈ ℝ)
13		iccssre 13443	. . . . . . . . 9 ⊢ (((1st ‘(𝐹‘𝑦)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑦)) ∈ ℝ) → ((1st ‘(𝐹‘𝑦))[,](2nd ‘(𝐹‘𝑦))) ⊆ ℝ)
14	10, 12, 13	syl2anc 593	. . . . . . . 8 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ((1st ‘(𝐹‘𝑦))[,](2nd ‘(𝐹‘𝑦))) ⊆ ℝ)
15	8, 14	eqsstrd 3971	. . . . . . 7 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) ⊆ ℝ)
16		reex 11175	. . . . . . . 8 ⊢ ℝ ∈ V
17	16	elpw2 5291	. . . . . . 7 ⊢ (([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ ↔ ([,]‘(𝐹‘𝑦)) ⊆ ℝ)
18	15, 17	sylibr 236	. . . . . 6 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ)
19	18	ralrimiva 3155	. . . . 5 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∀𝑦 ∈ ℕ ([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ)
20		ffn 6691	. . . . . 6 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐹 Fn ℕ)
21		fveq2 6867	. . . . . . . 8 ⊢ (𝑥 = (𝐹‘𝑦) → ([,]‘𝑥) = ([,]‘(𝐹‘𝑦)))
22	21	eleq1d 2848	. . . . . . 7 ⊢ (𝑥 = (𝐹‘𝑦) → (([,]‘𝑥) ∈ 𝒫 ℝ ↔ ([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ))
23	22	ralrn 7069	. . . . . 6 ⊢ (𝐹 Fn ℕ → (∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ ↔ ∀𝑦 ∈ ℕ ([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ))
24	20, 23	syl 17	. . . . 5 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → (∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ ↔ ∀𝑦 ∈ ℕ ([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ))
25	19, 24	mpbird 259	. . . 4 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ)
26		iccf 13462	. . . . . 6 ⊢ [,]:(ℝ* × ℝ*)⟶𝒫 ℝ*
27		ffun 6694	. . . . . 6 ⊢ ([,]:(ℝ* × ℝ*)⟶𝒫 ℝ* → Fun [,])
28	26, 27	ax-mp 5	. . . . 5 ⊢ Fun [,]
29		frn 6699	. . . . . 6 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran 𝐹 ⊆ ( ≤ ∩ (ℝ × ℝ)))
30		inss2 4190	. . . . . . . 8 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
31		rexpssxrxp 11238	. . . . . . . 8 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
32	30, 31	sstri 3946	. . . . . . 7 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
33	26	fdmi 6703	. . . . . . 7 ⊢ dom [,] = (ℝ* × ℝ*)
34	32, 33	sseqtrri 3986	. . . . . 6 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ dom [,]
35	29, 34	sstrdi 3949	. . . . 5 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran 𝐹 ⊆ dom [,])
36		funimass4 6931	. . . . 5 ⊢ ((Fun [,] ∧ ran 𝐹 ⊆ dom [,]) → (([,] “ ran 𝐹) ⊆ 𝒫 ℝ ↔ ∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ))
37	28, 35, 36	sylancr 596	. . . 4 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → (([,] “ ran 𝐹) ⊆ 𝒫 ℝ ↔ ∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ))
38	25, 37	mpbird 259	. . 3 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ([,] “ ran 𝐹) ⊆ 𝒫 ℝ)
39	1, 38	eqsstrid 3975	. 2 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐹) ⊆ 𝒫 ℝ)
40		sspwuni 5058	. 2 ⊢ (ran ([,] ∘ 𝐹) ⊆ 𝒫 ℝ ↔ ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
41	39, 40	sylib 220	1 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1561   ∈ wcel 2143  ∀wral 3077   ∩ cin 3904   ⊆ wss 3905  𝒫 cpw 4556  ⟨cop 4589  ∪ cuni 4866   × cxp 5646  dom cdm 5648  ran crn 5649   “ cima 5651   ∘ ccom 5652  Fun wfun 6515   Fn wfn 6516  ⟶wf 6517  ‘cfv 6521  (class class class)co 7396  1^st c1st 7968  2^nd c2nd 7969  ℝcr 11083  ℝ^*cxr 11226   ≤ cle 11228  ℕcn 12220  [,]cicc 13362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718  ax-cnex 11140  ax-resscn 11141  ax-pre-lttri 11158  ax-pre-lttrn 11159

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11229  df-mnf 11230  df-xr 11231  df-ltxr 11232  df-le 11233  df-icc 13366

This theorem is referenced by:  ovollb2lem  25557  ovollb2  25558  uniiccdif  25647  uniiccvol  25649  uniioombllem3  25654  uniioombllem4  25655  uniioombllem5  25656  uniiccmbl  25659