This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem topgrpbas

Description: The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015)

		Ref	Expression
	Hypothesis	topgrpfn.w	$⊢ W = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), J⟩\}$
	Assertion	topgrpbas	$⊢ B \in X \to B = {Base}_{W}$

Step	Hyp	Ref	Expression
1		topgrpfn.w	$⊢ W = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), J⟩\}$
2	1	topgrpstr	$⊢ W Struct ⟨1, 9⟩$
3		baseid	$⊢ Base = Slot {Base}_{ndx}$
4		snsstp1	$⊢ \{⟨{Base}_{ndx}, B⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), J⟩\}$
5	4 1	sseqtrri	$⊢ \{⟨{Base}_{ndx}, B⟩\} \subseteq W$
6	2 3 5	strfv	$⊢ B \in X \to B = {Base}_{W}$