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

Theorem metustss 22549
Description: Range of the elements of the filter base generated by the metric 𝐷. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
Hypothesis
Ref Expression
metust.1 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
Assertion
Ref Expression
metustss ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝐹) → 𝐴 ⊆ (𝑋 × 𝑋))
Distinct variable groups:   𝐷,𝑎   𝑋,𝑎   𝐴,𝑎   𝐹,𝑎

Proof of Theorem metustss
StepHypRef Expression
1 metust.1 . . . 4 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
2 cnvimass 5635 . . . . . . . . 9 (𝐷 “ (0[,)𝑎)) ⊆ dom 𝐷
3 psmetf 22304 . . . . . . . . . 10 (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
4 fdm 6204 . . . . . . . . . 10 (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom 𝐷 = (𝑋 × 𝑋))
53, 4syl 17 . . . . . . . . 9 (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
62, 5syl5sseq 3786 . . . . . . . 8 (𝐷 ∈ (PsMet‘𝑋) → (𝐷 “ (0[,)𝑎)) ⊆ (𝑋 × 𝑋))
76ad2antrr 764 . . . . . . 7 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) → (𝐷 “ (0[,)𝑎)) ⊆ (𝑋 × 𝑋))
8 cnvexg 7269 . . . . . . . . 9 (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ V)
9 imaexg 7260 . . . . . . . . 9 (𝐷 ∈ V → (𝐷 “ (0[,)𝑎)) ∈ V)
10 elpwg 4302 . . . . . . . . 9 ((𝐷 “ (0[,)𝑎)) ∈ V → ((𝐷 “ (0[,)𝑎)) ∈ 𝒫 (𝑋 × 𝑋) ↔ (𝐷 “ (0[,)𝑎)) ⊆ (𝑋 × 𝑋)))
118, 9, 103syl 18 . . . . . . . 8 (𝐷 ∈ (PsMet‘𝑋) → ((𝐷 “ (0[,)𝑎)) ∈ 𝒫 (𝑋 × 𝑋) ↔ (𝐷 “ (0[,)𝑎)) ⊆ (𝑋 × 𝑋)))
1211ad2antrr 764 . . . . . . 7 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) → ((𝐷 “ (0[,)𝑎)) ∈ 𝒫 (𝑋 × 𝑋) ↔ (𝐷 “ (0[,)𝑎)) ⊆ (𝑋 × 𝑋)))
137, 12mpbird 247 . . . . . 6 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) → (𝐷 “ (0[,)𝑎)) ∈ 𝒫 (𝑋 × 𝑋))
1413ralrimiva 3096 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝐹) → ∀𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑎)) ∈ 𝒫 (𝑋 × 𝑋))
15 eqid 2752 . . . . . 6 (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) = (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
1615rnmptss 6547 . . . . 5 (∀𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑎)) ∈ 𝒫 (𝑋 × 𝑋) → ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) ⊆ 𝒫 (𝑋 × 𝑋))
1714, 16syl 17 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝐹) → ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) ⊆ 𝒫 (𝑋 × 𝑋))
181, 17syl5eqss 3782 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝐹) → 𝐹 ⊆ 𝒫 (𝑋 × 𝑋))
19 simpr 479 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝐹) → 𝐴𝐹)
2018, 19sseldd 3737 . 2 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝐹) → 𝐴 ∈ 𝒫 (𝑋 × 𝑋))
2120elpwid 4306 1 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴𝐹) → 𝐴 ⊆ (𝑋 × 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1624  wcel 2131  wral 3042  Vcvv 3332  wss 3707  𝒫 cpw 4294  cmpt 4873   × cxp 5256  ccnv 5257  dom cdm 5258  ran crn 5259  cima 5261  wf 6037  cfv 6041  (class class class)co 6805  0cc0 10120  *cxr 10257  +crp 12017  [,)cico 12362  PsMetcpsmet 19924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-cnex 10176  ax-resscn 10177
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-fv 6049  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-map 8017  df-xr 10262  df-psmet 19932
This theorem is referenced by:  metustrel  22550  metustsym  22553
  Copyright terms: Public domain W3C validator