Theorem topgrpstr

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

	Ref	Expression
Hypothesis	topgrpfn.w	⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ }
Assertion	topgrpstr	⊢ 𝑊 Struct ⟨ 1 , 9 ⟩

Proof

Step	Hyp	Ref	Expression
1		topgrpfn.w	⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ }
2		1nn	⊢ 1 ∈ ℕ
3		basendx	⊢ ( Base ‘ ndx ) = 1
4		1lt2	⊢ 1 < 2
5		2nn	⊢ 2 ∈ ℕ
6		plusgndx	⊢ ( +g ‘ ndx ) = 2
7		2lt9	⊢ 2 < 9
8		9nn	⊢ 9 ∈ ℕ
9		tsetndx	⊢ ( TopSet ‘ ndx ) = 9
10	2 3 4 5 6 7 8 9	strle3	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } Struct ⟨ 1 , 9 ⟩
11	1 10	eqbrtri	⊢ 𝑊 Struct ⟨ 1 , 9 ⟩