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	imbitrrid	⊢ ( 𝐽 = ( MetOpen ‘ 𝐷 ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) )
32	28 31	impbid	⊢ ( 𝐽 = ( MetOpen ‘ 𝐷 ) → ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ↔ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) )
33	5 32	bitrid	⊢ ( 𝐽 = ( MetOpen ‘ 𝐷 ) → ( 𝐾 ∈ TopSp ↔ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) )
34	33	pm5.32ri	⊢ ( ( 𝐾 ∈ TopSp ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) )
35	4 34	bitri	⊢ ( 𝐾 ∈ ∞MetSp ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) )