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