Metamath Proof Explorer

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	$⊢ J = TopOpen (K)$
		isms.x	$⊢ X = {Base}_{K}$
		isms.d	$⊢ D = {dist (K) ↾}_{(X \times X)}$
	Assertion	isms2	$⊢ K \in MetSp \leftrightarrow (D \in Met (X) \land 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 \times X)}$
4	1 2 3	isxms2	$⊢ K \in ∞MetSp \leftrightarrow (D \in ∞Met (X) \land J = MetOpen (D))$
5	4	anbi1i	$⊢ (K \in ∞MetSp \land D \in Met (X)) \leftrightarrow ((D \in ∞Met (X) \land J = MetOpen (D)) \land D \in Met (X))$
6	1 2 3	isms	$⊢ K \in MetSp \leftrightarrow (K \in ∞MetSp \land D \in Met (X))$
7		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
8	7	pm4.71ri	$⊢ D \in Met (X) \leftrightarrow (D \in ∞Met (X) \land D \in Met (X))$
9	8	anbi1i	$⊢ (D \in Met (X) \land J = MetOpen (D)) \leftrightarrow ((D \in ∞Met (X) \land D \in Met (X)) \land J = MetOpen (D))$
10		an32	$⊢ ((D \in ∞Met (X) \land D \in Met (X)) \land J = MetOpen (D)) \leftrightarrow ((D \in ∞Met (X) \land J = MetOpen (D)) \land D \in Met (X))$
11	9 10	bitri	$⊢ (D \in Met (X) \land J = MetOpen (D)) \leftrightarrow ((D \in ∞Met (X) \land J = MetOpen (D)) \land D \in Met (X))$
12	5 6 11	3bitr4i	$⊢ K \in MetSp \leftrightarrow (D \in Met (X) \land J = MetOpen (D))$