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 ⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
isms.x ⊢ 𝑋 = ( Base ‘ 𝐾 )
isms.d ⊢ 𝐷 = ( ( dist ‘ 𝐾 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion isxms2 ( 𝐾 ∈ ∞MetSp ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) )

Proof

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