setsmsbas

Description: The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015) (Proof shortened by AV, 12-Nov-2024)

	Ref	Expression
Hypotheses	setsms.x	$⊢ φ \to X = {Base}_{M}$
	setsms.d	$⊢ φ \to D = {dist (M) ↾}_{(X \times X)}$
	setsms.k	$⊢ φ \to K = M sSet ⟨TopSet (ndx), MetOpen (D)⟩$
Assertion	setsmsbas	$⊢ φ \to X = {Base}_{K}$

Step	Hyp	Ref	Expression
1		setsms.x	$⊢ φ \to X = {Base}_{M}$
2		setsms.d	$⊢ φ \to D = {dist (M) ↾}_{(X \times X)}$
3		setsms.k	$⊢ φ \to K = M sSet ⟨TopSet (ndx), MetOpen (D)⟩$
4		baseid	$⊢ Base = Slot {Base}_{ndx}$
5		tsetndxnbasendx	$⊢ TopSet (ndx) \neq {Base}_{ndx}$
6	5	necomi	$⊢ {Base}_{ndx} \neq TopSet (ndx)$
7	4 6	setsnid	$⊢ {Base}_{M} = {Base}_{(M sSet ⟨TopSet (ndx), MetOpen (D)⟩)}$
8	3	fveq2d	$⊢ φ \to {Base}_{K} = {Base}_{(M sSet ⟨TopSet (ndx), MetOpen (D)⟩)}$
9	7 1 8	3eqtr4a	$⊢ φ \to X = {Base}_{K}$

Metamath Proof Explorer