Theorem 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 >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. }
Assertion	topgrpstr	|- W Struct <. 1 , 9 >.

Proof

Step	Hyp	Ref	Expression
1		topgrpfn.w	|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. }
2		1nn	|- 1 e. NN
3		basendx	|- ( Base ` ndx ) = 1
4		1lt2	|- 1 < 2
5		2nn	|- 2 e. NN
6		plusgndx	|- ( +g ` ndx ) = 2
7		2lt9	|- 2 < 9
8		9nn	|- 9 e. NN
9		tsetndx	|- ( TopSet ` ndx ) = 9
10	2 3 4 5 6 7 8 9	strle3	|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } Struct <. 1 , 9 >.
11	1 10	eqbrtri	|- W Struct <. 1 , 9 >.