Theorem isms2

Description: Express the predicate " <. X , D >. is a metric space" with underlying set X and distance function D . (Contributed by NM, 27-Aug-2006) (Revised by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Hypotheses	isms.j	⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
	isms.x	⊢ 𝑋 = ( Base ‘ 𝐾 )
	isms.d	⊢ 𝐷 = ( ( dist ‘ 𝐾 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion	isms2	⊢ ( 𝐾 ∈ MetSp ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isms.j	⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
2		isms.x	⊢ 𝑋 = ( Base ‘ 𝐾 )
3		isms.d	⊢ 𝐷 = ( ( dist ‘ 𝐾 ) ↾ ( 𝑋 × 𝑋 ) )
4	1 2 3	isxms2	⊢ ( 𝐾 ∈ ∞MetSp ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) )
5	4	anbi1i	⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ↔ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
6	1 2 3	isms	⊢ ( 𝐾 ∈ MetSp ↔ ( 𝐾 ∈ ∞MetSp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
7		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
8	7	pm4.71ri	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
9	8	anbi1i	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) )
10		an32	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
11	9 10	bitri	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
12	5 6 11	3bitr4i	⊢ ( 𝐾 ∈ MetSp ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) )