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

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 = ( 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 ) ) )