Metamath Proof Explorer

Theorem istgp

Description: The predicate "is a topological group". Definition 1 of BourbakiTop1 p. III.1. (Contributed by FL, 18-Apr-2010) (Revised by Mario Carneiro, 13-Aug-2015)

		Ref	Expression
	Hypotheses	istgp.1	$⊢ J = TopOpen (G)$
		istgp.2	$⊢ I = {inv}_{g} (G)$
	Assertion	istgp	$⊢ G \in TopGrp \leftrightarrow (G \in Grp \land G \in TopMnd \land I \in (J Cn J))$

Proof

Step	Hyp	Ref	Expression
1		istgp.1	$⊢ J = TopOpen (G)$
2		istgp.2	$⊢ I = {inv}_{g} (G)$
3		elin	$⊢ G \in (Grp \cap TopMnd) \leftrightarrow (G \in Grp \land G \in TopMnd)$
4	3	anbi1i	$⊢ (G \in (Grp \cap TopMnd) \land I \in (J Cn J)) \leftrightarrow ((G \in Grp \land G \in TopMnd) \land I \in (J Cn J))$
5		fvexd	$⊢ f = G \to TopOpen (f) \in V$
6		simpl	$⊢ (f = G \land j = TopOpen (f)) \to f = G$
7	6	fveq2d	$⊢ (f = G \land j = TopOpen (f)) \to {inv}_{g} (f) = {inv}_{g} (G)$
8	7 2	eqtr4di	$⊢ (f = G \land j = TopOpen (f)) \to {inv}_{g} (f) = I$
9		id	$⊢ j = TopOpen (f) \to j = TopOpen (f)$
10		fveq2	$⊢ f = G \to TopOpen (f) = TopOpen (G)$
11	10 1	eqtr4di	$⊢ f = G \to TopOpen (f) = J$
12	9 11	sylan9eqr	$⊢ (f = G \land j = TopOpen (f)) \to j = J$
13	12 12	oveq12d	$⊢ (f = G \land j = TopOpen (f)) \to j Cn j = J Cn J$
14	8 13	eleq12d	$⊢ (f = G \land j = TopOpen (f)) \to ({inv}_{g} (f) \in (j Cn j) \leftrightarrow I \in (J Cn J))$
15	5 14	sbcied	$⊢ f = G \to (\underset{˙}{[} TopOpen (f) / j \underset{˙}{]} {inv}_{g} (f) \in (j Cn j) \leftrightarrow I \in (J Cn J))$
16		df-tgp	$⊢ TopGrp = \{f \in (Grp \cap TopMnd) \| \underset{˙}{[} TopOpen (f) / j \underset{˙}{]} {inv}_{g} (f) \in (j Cn j)\}$
17	15 16	elrab2	$⊢ G \in TopGrp \leftrightarrow (G \in (Grp \cap TopMnd) \land I \in (J Cn J))$
18		df-3an	$⊢ (G \in Grp \land G \in TopMnd \land I \in (J Cn J)) \leftrightarrow ((G \in Grp \land G \in TopMnd) \land I \in (J Cn J))$
19	4 17 18	3bitr4i	$⊢ G \in TopGrp \leftrightarrow (G \in Grp \land G \in TopMnd \land I \in (J Cn J))$