Theorem topgrpstr

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

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

Proof

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