Metamath Proof Explorer

Theorem issubg

Description: The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypothesis issubg.b 
|- B = ( Base ` G )
Assertion issubg 
|- ( S e. ( SubGrp ` G ) <-> ( G e. Grp /\ S C_ B /\ ( G |`s S ) e. Grp ) )

Proof

Step Hyp Ref Expression
1 issubg.b 
 |-  B = ( Base ` G )
2 df-subg 
 |-  SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Grp } )
3 2 mptrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
4 simp1 
 |-  ( ( G e. Grp /\ S C_ B /\ ( G |`s S ) e. Grp ) -> G e. Grp )
5 fveq2 
 |-  ( w = G -> ( Base ` w ) = ( Base ` G ) )
6 5 1 eqtr4di 
 |-  ( w = G -> ( Base ` w ) = B )
7 6 pweqd 
 |-  ( w = G -> ~P ( Base ` w ) = ~P B )
8 oveq1 
 |-  ( w = G -> ( w |`s s ) = ( G |`s s ) )
9 8 eleq1d 
 |-  ( w = G -> ( ( w |`s s ) e. Grp <-> ( G |`s s ) e. Grp ) )
10 7 9 rabeqbidv 
 |-  ( w = G -> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Grp } = { s e. ~P B | ( G |`s s ) e. Grp } )
11 1 fvexi 
 |-  B e. _V
12 11 pwex 
 |-  ~P B e. _V
13 12 rabex 
 |-  { s e. ~P B | ( G |`s s ) e. Grp } e. _V
14 10 2 13 fvmpt 
 |-  ( G e. Grp -> ( SubGrp ` G ) = { s e. ~P B | ( G |`s s ) e. Grp } )
15 14 eleq2d 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> S e. { s e. ~P B | ( G |`s s ) e. Grp } ) )
16 oveq2 
 |-  ( s = S -> ( G |`s s ) = ( G |`s S ) )
17 16 eleq1d 
 |-  ( s = S -> ( ( G |`s s ) e. Grp <-> ( G |`s S ) e. Grp ) )
18 17 elrab 
 |-  ( S e. { s e. ~P B | ( G |`s s ) e. Grp } <-> ( S e. ~P B /\ ( G |`s S ) e. Grp ) )
19 11 elpw2 
 |-  ( S e. ~P B <-> S C_ B )
20 19 anbi1i 
 |-  ( ( S e. ~P B /\ ( G |`s S ) e. Grp ) <-> ( S C_ B /\ ( G |`s S ) e. Grp ) )
21 18 20 bitri 
 |-  ( S e. { s e. ~P B | ( G |`s s ) e. Grp } <-> ( S C_ B /\ ( G |`s S ) e. Grp ) )
22 15 21 bitrdi 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( S C_ B /\ ( G |`s S ) e. Grp ) ) )
23 ibar 
 |-  ( G e. Grp -> ( ( S C_ B /\ ( G |`s S ) e. Grp ) <-> ( G e. Grp /\ ( S C_ B /\ ( G |`s S ) e. Grp ) ) ) )
24 22 23 bitrd 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( G e. Grp /\ ( S C_ B /\ ( G |`s S ) e. Grp ) ) ) )
25 3anass 
 |-  ( ( G e. Grp /\ S C_ B /\ ( G |`s S ) e. Grp ) <-> ( G e. Grp /\ ( S C_ B /\ ( G |`s S ) e. Grp ) ) )
26 24 25 bitr4di 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( G e. Grp /\ S C_ B /\ ( G |`s S ) e. Grp ) ) )
27 3 4 26 pm5.21nii 
 |-  ( S e. ( SubGrp ` G ) <-> ( G e. Grp /\ S C_ B /\ ( G |`s S ) e. Grp ) )