Metamath Proof Explorer

Theorem issubg

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

Ref Expression
Hypothesis issubg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion issubg ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )

Proof

Step Hyp Ref Expression
1 issubg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 df-subg ⊢ SubGrp = ( 𝑤 ∈ Grp ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾s 𝑠 ) ∈ Grp } )
3 2 mptrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
4 simp1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) → 𝐺 ∈ Grp )
5 fveq2 ⊢ ( 𝑤 = 𝐺 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝐺 ) )
6 5 1 eqtr4di ⊢ ( 𝑤 = 𝐺 → ( Base ‘ 𝑤 ) = 𝐵 )
7 6 pweqd ⊢ ( 𝑤 = 𝐺 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 𝐵 )
8 oveq1 ⊢ ( 𝑤 = 𝐺 → ( 𝑤 ↾s 𝑠 ) = ( 𝐺 ↾s 𝑠 ) )
9 8 eleq1d ⊢ ( 𝑤 = 𝐺 → ( ( 𝑤 ↾s 𝑠 ) ∈ Grp ↔ ( 𝐺 ↾s 𝑠 ) ∈ Grp ) )
10 7 9 rabeqbidv ⊢ ( 𝑤 = 𝐺 → { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾s 𝑠 ) ∈ Grp } = { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺 ↾s 𝑠 ) ∈ Grp } )
11 1 fvexi ⊢ 𝐵 ∈ V
12 11 pwex ⊢ 𝒫 𝐵 ∈ V
13 12 rabex ⊢ { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺 ↾s 𝑠 ) ∈ Grp } ∈ V
14 10 2 13 fvmpt ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) = { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺 ↾s 𝑠 ) ∈ Grp } )
15 14 eleq2d ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺 ↾s 𝑠 ) ∈ Grp } ) )
16 oveq2 ⊢ ( 𝑠 = 𝑆 → ( 𝐺 ↾s 𝑠 ) = ( 𝐺 ↾s 𝑆 ) )
17 16 eleq1d ⊢ ( 𝑠 = 𝑆 → ( ( 𝐺 ↾s 𝑠 ) ∈ Grp ↔ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )
18 17 elrab ⊢ ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺 ↾s 𝑠 ) ∈ Grp } ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )
19 11 elpw2 ⊢ ( 𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵 )
20 19 anbi1i ⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ↔ ( 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )
21 18 20 bitri ⊢ ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺 ↾s 𝑠 ) ∈ Grp } ↔ ( 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )
22 15 21 bitrdi ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ) )
23 ibar ⊢ ( 𝐺 ∈ Grp → ( ( 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ) ) )
24 22 23 bitrd ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ) ) )
25 3anass ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ) )
26 24 25 bitr4di ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ) )
27 3 4 26 pm5.21nii ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )