Metamath Proof Explorer

Theorem isxms2

Description: Express the predicate " <. X , D >. is an extended metric space" with underlying set X and distance function D . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses isms.j ⊢ J = TopOpen ⁡ K
isms.x ⊢ X = Base K
isms.d ⊢ D = dist ⁡ K ↾ X × X
Assertion isxms2 ⊢ K ∈ ∞MetSp ↔ D ∈ ∞Met ⁡ X ∧ J = MetOpen ⁡ D

Proof

Step Hyp Ref Expression
1 isms.j ⊢ J = TopOpen ⁡ K
2 isms.x ⊢ X = Base K
3 isms.d ⊢ D = dist ⁡ K ↾ X × X
4 1 2 3 isxms ⊢ K ∈ ∞MetSp ↔ K ∈ TopSp ∧ J = MetOpen ⁡ D
5 2 1 istps ⊢ K ∈ TopSp ↔ J ∈ TopOn ⁡ X
6 df-mopn ⊢ MetOpen = x ∈ ⋃ ran ⁡ ∞Met ⟼ topGen ⁡ ran ⁡ ball ⁡ x
7 6 dmmptss ⊢ dom ⁡ MetOpen ⊆ ⋃ ran ⁡ ∞Met
8 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
9 8 adantl ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → X ∈ J
10 simpl ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → J = MetOpen ⁡ D
11 9 10 eleqtrd ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → X ∈ MetOpen ⁡ D
12 elfvdm ⊢ X ∈ MetOpen ⁡ D → D ∈ dom ⁡ MetOpen
13 11 12 syl ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → D ∈ dom ⁡ MetOpen
14 7 13 sselid ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → D ∈ ⋃ ran ⁡ ∞Met
15 xmetunirn ⊢ D ∈ ⋃ ran ⁡ ∞Met ↔ D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D
16 14 15 sylib ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D
17 eqid ⊢ MetOpen ⁡ D = MetOpen ⁡ D
18 17 mopntopon ⊢ D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D → MetOpen ⁡ D ∈ TopOn ⁡ dom ⁡ dom ⁡ D
19 16 18 syl ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → MetOpen ⁡ D ∈ TopOn ⁡ dom ⁡ dom ⁡ D
20 10 19 eqeltrd ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → J ∈ TopOn ⁡ dom ⁡ dom ⁡ D
21 toponuni ⊢ J ∈ TopOn ⁡ dom ⁡ dom ⁡ D → dom ⁡ dom ⁡ D = ⋃ J
22 20 21 syl ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → dom ⁡ dom ⁡ D = ⋃ J
23 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
24 23 adantl ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → X = ⋃ J
25 22 24 eqtr4d ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → dom ⁡ dom ⁡ D = X
26 25 fveq2d ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → ∞Met ⁡ dom ⁡ dom ⁡ D = ∞Met ⁡ X
27 16 26 eleqtrd ⊢ J = MetOpen ⁡ D ∧ J ∈ TopOn ⁡ X → D ∈ ∞Met ⁡ X
28 27 ex ⊢ J = MetOpen ⁡ D → J ∈ TopOn ⁡ X → D ∈ ∞Met ⁡ X
29 17 mopntopon ⊢ D ∈ ∞Met ⁡ X → MetOpen ⁡ D ∈ TopOn ⁡ X
30 eleq1 ⊢ J = MetOpen ⁡ D → J ∈ TopOn ⁡ X ↔ MetOpen ⁡ D ∈ TopOn ⁡ X
31 29 30 imbitrrid ⊢ J = MetOpen ⁡ D → D ∈ ∞Met ⁡ X → J ∈ TopOn ⁡ X
32 28 31 impbid ⊢ J = MetOpen ⁡ D → J ∈ TopOn ⁡ X ↔ D ∈ ∞Met ⁡ X
33 5 32 bitrid ⊢ J = MetOpen ⁡ D → K ∈ TopSp ↔ D ∈ ∞Met ⁡ X
34 33 pm5.32ri ⊢ K ∈ TopSp ∧ J = MetOpen ⁡ D ↔ D ∈ ∞Met ⁡ X ∧ J = MetOpen ⁡ D
35 4 34 bitri ⊢ K ∈ ∞MetSp ↔ D ∈ ∞Met ⁡ X ∧ J = MetOpen ⁡ D