Theorem issubg 18670

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

Hypothesis

Ref	Expression
issubg.b	⊢ 𝐵 = (Base‘𝐺)

Assertion

Ref	Expression
issubg	⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))

Proof of Theorem issubg

Dummy variables 𝑤 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-subg 18667	. . 3 ⊢ SubGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp})
2	1	mptrcl 6866	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
3		simp1 1134	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) → 𝐺 ∈ Grp)
4		fveq2 6756	. . . . . . . . . 10 ⊢ (𝑤 = 𝐺 → (Base‘𝑤) = (Base‘𝐺))
5		issubg.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐺)
6	4, 5	eqtr4di 2797	. . . . . . . . 9 ⊢ (𝑤 = 𝐺 → (Base‘𝑤) = 𝐵)
7	6	pweqd 4549	. . . . . . . 8 ⊢ (𝑤 = 𝐺 → 𝒫 (Base‘𝑤) = 𝒫 𝐵)
8		oveq1 7262	. . . . . . . . 9 ⊢ (𝑤 = 𝐺 → (𝑤 ↾s 𝑠) = (𝐺 ↾s 𝑠))
9	8	eleq1d 2823	. . . . . . . 8 ⊢ (𝑤 = 𝐺 → ((𝑤 ↾s 𝑠) ∈ Grp ↔ (𝐺 ↾s 𝑠) ∈ Grp))
10	7, 9	rabeqbidv 3410	. . . . . . 7 ⊢ (𝑤 = 𝐺 → {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp} = {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp})
11	5	fvexi 6770	. . . . . . . . 9 ⊢ 𝐵 ∈ V
12	11	pwex 5298	. . . . . . . 8 ⊢ 𝒫 𝐵 ∈ V
13	12	rabex 5251	. . . . . . 7 ⊢ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ∈ V
14	10, 1, 13	fvmpt 6857	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) = {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp})
15	14	eleq2d 2824	. . . . 5 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ 𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp}))
16		oveq2 7263	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (𝐺 ↾s 𝑠) = (𝐺 ↾s 𝑆))
17	16	eleq1d 2823	. . . . . . 7 ⊢ (𝑠 = 𝑆 → ((𝐺 ↾s 𝑠) ∈ Grp ↔ (𝐺 ↾s 𝑆) ∈ Grp))
18	17	elrab 3617	. . . . . 6 ⊢ (𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ↔ (𝑆 ∈ 𝒫 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
19	11	elpw2 5264	. . . . . . 7 ⊢ (𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵)
20	19	anbi1i 623	. . . . . 6 ⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
21	18, 20	bitri 274	. . . . 5 ⊢ (𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
22	15, 21	bitrdi 286	. . . 4 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))
23		ibar 528	. . . 4 ⊢ (𝐺 ∈ Grp → ((𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))))
24	22, 23	bitrd 278	. . 3 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))))
25		3anass 1093	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))
26	24, 25	bitr4di 288	. 2 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))
27	2, 3, 26	pm5.21nii 379	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  {crab 3067   ⊆ wss 3883  𝒫 cpw 4530  ‘cfv 6418  (class class class)co 7255  Basecbs 16840   ↾_s cress 16867  Grpcgrp 18492  SubGrpcsubg 18664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-subg 18667

This theorem is referenced by:  subgss  18671  subgid  18672  subggrp  18673  subgrcl  18675  issubg2  18685  resgrpisgrp  18691  subsubg  18693  pgrpsubgsymgbi  18931  opprsubg  19793  subrgsubg  19945  subdrgint  19986  cphsubrglem  24246  suborng  31416