This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem symgtopn

Description: The topology of the symmetric group on A . (Contributed by Mario Carneiro, 29-Aug-2015)

	Ref	Expression
Hypotheses	symgga.g	$⊢ G = SymGrp (X)$
	symgga.b	$⊢ B = {Base}_{G}$
Assertion	symgtopn	$⊢ X \in V \to \prod_{𝑡} (X \times \{𝒫 X\}) ↾_{𝑡} B = TopOpen (G)$

Step	Hyp	Ref	Expression
1		symgga.g	$⊢ G = SymGrp (X)$
2		symgga.b	$⊢ B = {Base}_{G}$
3	1	symgtset	$⊢ X \in V \to \prod_{𝑡} (X \times \{𝒫 X\}) = TopSet (G)$
4	3	oveq1d	$⊢ X \in V \to \prod_{𝑡} (X \times \{𝒫 X\}) ↾_{𝑡} B = TopSet (G) ↾_{𝑡} B$
5		eqid	$⊢ TopSet (G) = TopSet (G)$
6	2 5	topnval	$⊢ TopSet (G) ↾_{𝑡} B = TopOpen (G)$
7	4 6	eqtrdi	$⊢ X \in V \to \prod_{𝑡} (X \times \{𝒫 X\}) ↾_{𝑡} B = TopOpen (G)$