Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolficcss Structured version   Visualization version   GIF version

Theorem ovolficcss 24071
 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.
StepHypRef Expression
1 rnco2 6084 . . 3 ran ([,] ∘ 𝐹) = ([,] “ ran 𝐹)
2 ffvelrn 6831 . . . . . . . . . . . 12 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹𝑦) ∈ ( ≤ ∩ (ℝ × ℝ)))
32elin2d 4150 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹𝑦) ∈ (ℝ × ℝ))
4 1st2nd2 7714 . . . . . . . . . . 11 ((𝐹𝑦) ∈ (ℝ × ℝ) → (𝐹𝑦) = ⟨(1st ‘(𝐹𝑦)), (2nd ‘(𝐹𝑦))⟩)
53, 4syl 17 . . . . . . . . . 10 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹𝑦) = ⟨(1st ‘(𝐹𝑦)), (2nd ‘(𝐹𝑦))⟩)
65fveq2d 6656 . . . . . . . . 9 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹𝑦)) = ([,]‘⟨(1st ‘(𝐹𝑦)), (2nd ‘(𝐹𝑦))⟩))
7 df-ov 7143 . . . . . . . . 9 ((1st ‘(𝐹𝑦))[,](2nd ‘(𝐹𝑦))) = ([,]‘⟨(1st ‘(𝐹𝑦)), (2nd ‘(𝐹𝑦))⟩)
86, 7eqtr4di 2875 . . . . . . . 8 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹𝑦)) = ((1st ‘(𝐹𝑦))[,](2nd ‘(𝐹𝑦))))
9 xp1st 7707 . . . . . . . . . 10 ((𝐹𝑦) ∈ (ℝ × ℝ) → (1st ‘(𝐹𝑦)) ∈ ℝ)
103, 9syl 17 . . . . . . . . 9 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (1st ‘(𝐹𝑦)) ∈ ℝ)
11 xp2nd 7708 . . . . . . . . . 10 ((𝐹𝑦) ∈ (ℝ × ℝ) → (2nd ‘(𝐹𝑦)) ∈ ℝ)
123, 11syl 17 . . . . . . . . 9 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (2nd ‘(𝐹𝑦)) ∈ ℝ)
13 iccssre 12807 . . . . . . . . 9 (((1st ‘(𝐹𝑦)) ∈ ℝ ∧ (2nd ‘(𝐹𝑦)) ∈ ℝ) → ((1st ‘(𝐹𝑦))[,](2nd ‘(𝐹𝑦))) ⊆ ℝ)
1410, 12, 13syl2anc 587 . . . . . . . 8 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ((1st ‘(𝐹𝑦))[,](2nd ‘(𝐹𝑦))) ⊆ ℝ)
158, 14eqsstrd 3980 . . . . . . 7 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹𝑦)) ⊆ ℝ)
16 reex 10617 . . . . . . . 8 ℝ ∈ V
1716elpw2 5224 . . . . . . 7 (([,]‘(𝐹𝑦)) ∈ 𝒫 ℝ ↔ ([,]‘(𝐹𝑦)) ⊆ ℝ)
1815, 17sylibr 237 . . . . . 6 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹𝑦)) ∈ 𝒫 ℝ)
1918ralrimiva 3174 . . . . 5 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∀𝑦 ∈ ℕ ([,]‘(𝐹𝑦)) ∈ 𝒫 ℝ)
20 ffn 6494 . . . . . 6 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐹 Fn ℕ)
21 fveq2 6652 . . . . . . . 8 (𝑥 = (𝐹𝑦) → ([,]‘𝑥) = ([,]‘(𝐹𝑦)))
2221eleq1d 2898 . . . . . . 7 (𝑥 = (𝐹𝑦) → (([,]‘𝑥) ∈ 𝒫 ℝ ↔ ([,]‘(𝐹𝑦)) ∈ 𝒫 ℝ))
2322ralrn 6836 . . . . . 6 (𝐹 Fn ℕ → (∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ ↔ ∀𝑦 ∈ ℕ ([,]‘(𝐹𝑦)) ∈ 𝒫 ℝ))
2420, 23syl 17 . . . . 5 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → (∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ ↔ ∀𝑦 ∈ ℕ ([,]‘(𝐹𝑦)) ∈ 𝒫 ℝ))
2519, 24mpbird 260 . . . 4 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ)
26 iccf 12826 . . . . . 6 [,]:(ℝ* × ℝ*)⟶𝒫 ℝ*
27 ffun 6497 . . . . . 6 ([,]:(ℝ* × ℝ*)⟶𝒫 ℝ* → Fun [,])
2826, 27ax-mp 5 . . . . 5 Fun [,]
29 frn 6500 . . . . . 6 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran 𝐹 ⊆ ( ≤ ∩ (ℝ × ℝ)))
30 inss2 4180 . . . . . . . 8 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
31 rexpssxrxp 10675 . . . . . . . 8 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
3230, 31sstri 3951 . . . . . . 7 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
3326fdmi 6505 . . . . . . 7 dom [,] = (ℝ* × ℝ*)
3432, 33sseqtrri 3979 . . . . . 6 ( ≤ ∩ (ℝ × ℝ)) ⊆ dom [,]
3529, 34sstrdi 3954 . . . . 5 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran 𝐹 ⊆ dom [,])
36 funimass4 6712 . . . . 5 ((Fun [,] ∧ ran 𝐹 ⊆ dom [,]) → (([,] “ ran 𝐹) ⊆ 𝒫 ℝ ↔ ∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ))
3728, 35, 36sylancr 590 . . . 4 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → (([,] “ ran 𝐹) ⊆ 𝒫 ℝ ↔ ∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ))
3825, 37mpbird 260 . . 3 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ([,] “ ran 𝐹) ⊆ 𝒫 ℝ)
391, 38eqsstrid 3990 . 2 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐹) ⊆ 𝒫 ℝ)
40 sspwuni 4997 . 2 (ran ([,] ∘ 𝐹) ⊆ 𝒫 ℝ ↔ ran ([,] ∘ 𝐹) ⊆ ℝ)
4139, 40sylib 221 1 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐹) ⊆ ℝ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2114  ∀wral 3130   ∩ cin 3907   ⊆ wss 3908  𝒫 cpw 4511  ⟨cop 4545  ∪ cuni 4813   × cxp 5530  dom cdm 5532  ran crn 5533   “ cima 5535   ∘ ccom 5536  Fun wfun 6328   Fn wfn 6329  ⟶wf 6330  ‘cfv 6334  (class class class)co 7140  1st c1st 7673  2nd c2nd 7674  ℝcr 10525  ℝ*cxr 10663   ≤ cle 10665  ℕcn 11625  [,]cicc 12729 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-pre-lttri 10600  ax-pre-lttrn 10601 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-po 5451  df-so 5452  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-ov 7143  df-oprab 7144  df-mpo 7145  df-1st 7675  df-2nd 7676  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-icc 12733 This theorem is referenced by:  ovollb2lem  24090  ovollb2  24091  uniiccdif  24180  uniiccvol  24182  uniioombllem3  24187  uniioombllem4  24188  uniioombllem5  24189  uniiccmbl  24192
 Copyright terms: Public domain W3C validator