topgrpstr

Description: A constructed topological group is a structure. (Contributed by Mario Carneiro, 29-Aug-2015)

		Ref	Expression
	Hypothesis	topgrpfn.w	$⊢ W = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), J⟩\}$
	Assertion	topgrpstr	$⊢ W Struct ⟨1, 9⟩$

Step	Hyp	Ref	Expression
1		topgrpfn.w	$⊢ W = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), J⟩\}$
2		1nn	$⊢ 1 \in ℕ$
3		basendx	$⊢ {Base}_{ndx} = 1$
4		1lt2	$⊢ 1 < 2$
5		2nn	$⊢ 2 \in ℕ$
6		plusgndx	$⊢ +_{ndx} = 2$
7		2lt9	$⊢ 2 < 9$
8		9nn	$⊢ 9 \in ℕ$
9		tsetndx	$⊢ TopSet (ndx) = 9$
10	2 3 4 5 6 7 8 9	strle3	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨TopSet (ndx), J⟩\} Struct ⟨1, 9⟩$
11	1 10	eqbrtri	$⊢ W Struct ⟨1, 9⟩$

Metamath Proof Explorer