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 = ( invg ` G )
Assertion	istgp	|- ( G e. TopGrp <-> ( G e. Grp /\ G e. TopMnd /\ I e. ( J Cn J ) ) )

Proof

Step	Hyp	Ref	Expression
1		istgp.1	|- J = ( TopOpen ` G )
2		istgp.2	|- I = ( invg ` G )
3		elin	|- ( G e. ( Grp i^i TopMnd ) <-> ( G e. Grp /\ G e. TopMnd ) )
4	3	anbi1i	|- ( ( G e. ( Grp i^i TopMnd ) /\ I e. ( J Cn J ) ) <-> ( ( G e. Grp /\ G e. TopMnd ) /\ I e. ( J Cn J ) ) )
5		fvexd	|- ( f = G -> ( TopOpen ` f ) e. _V )
6		simpl	|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> f = G )
7	6	fveq2d	|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> ( invg ` f ) = ( invg ` G ) )
8	7 2	eqtr4di	|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> ( invg ` f ) = I )
9		id	|- ( j = ( TopOpen ` f ) -> j = ( TopOpen ` f ) )
10		fveq2	|- ( f = G -> ( TopOpen ` f ) = ( TopOpen ` G ) )
11	10 1	eqtr4di	|- ( f = G -> ( TopOpen ` f ) = J )
12	9 11	sylan9eqr	|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> j = J )
13	12 12	oveq12d	|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> ( j Cn j ) = ( J Cn J ) )
14	8 13	eleq12d	|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> ( ( invg ` f ) e. ( j Cn j ) <-> I e. ( J Cn J ) ) )
15	5 14	sbcied	|- ( f = G -> ( [. ( TopOpen ` f ) / j ]. ( invg ` f ) e. ( j Cn j ) <-> I e. ( J Cn J ) ) )
16		df-tgp	|- TopGrp = { f e. ( Grp i^i TopMnd ) | [. ( TopOpen ` f ) / j ]. ( invg ` f ) e. ( j Cn j ) }
17	15 16	elrab2	|- ( G e. TopGrp <-> ( G e. ( Grp i^i TopMnd ) /\ I e. ( J Cn J ) ) )
18		df-3an	|- ( ( G e. Grp /\ G e. TopMnd /\ I e. ( J Cn J ) ) <-> ( ( G e. Grp /\ G e. TopMnd ) /\ I e. ( J Cn J ) ) )
19	4 17 18	3bitr4i	|- ( G e. TopGrp <-> ( G e. Grp /\ G e. TopMnd /\ I e. ( J Cn J ) ) )