Metamath Proof Explorer


Theorem topgrpstr

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

Ref Expression
Hypothesis topgrpfn.w W=BasendxB+ndx+˙TopSetndxJ
Assertion topgrpstr WStruct19

Proof

Step Hyp Ref Expression
1 topgrpfn.w W=BasendxB+ndx+˙TopSetndxJ
2 1nn 1
3 basendx Basendx=1
4 1lt2 1<2
5 2nn 2
6 plusgndx +ndx=2
7 2lt9 2<9
8 9nn 9
9 tsetndx TopSetndx=9
10 2 3 4 5 6 7 8 9 strle3 BasendxB+ndx+˙TopSetndxJStruct19
11 1 10 eqbrtri WStruct19