Theorem issubg 13594

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 13591	. . 3 ⊢ SubGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp})
2	1	mptrcl 5680	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
3		simp1 1000	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) → 𝐺 ∈ Grp)
4		fveq2 5594	. . . . . . . . 9 ⊢ (𝑤 = 𝐺 → (Base‘𝑤) = (Base‘𝐺))
5		issubg.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐺)
6	4, 5	eqtr4di 2257	. . . . . . . 8 ⊢ (𝑤 = 𝐺 → (Base‘𝑤) = 𝐵)
7	6	pweqd 3626	. . . . . . 7 ⊢ (𝑤 = 𝐺 → 𝒫 (Base‘𝑤) = 𝒫 𝐵)
8		oveq1 5969	. . . . . . . 8 ⊢ (𝑤 = 𝐺 → (𝑤 ↾s 𝑠) = (𝐺 ↾s 𝑠))
9	8	eleq1d 2275	. . . . . . 7 ⊢ (𝑤 = 𝐺 → ((𝑤 ↾s 𝑠) ∈ Grp ↔ (𝐺 ↾s 𝑠) ∈ Grp))
10	7, 9	rabeqbidv 2768	. . . . . 6 ⊢ (𝑤 = 𝐺 → {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp} = {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp})
11		id 19	. . . . . 6 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Grp)
12		basfn 12975	. . . . . . . . . 10 ⊢ Base Fn V
13		elex 2785	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ V)
14		funfvex 5611	. . . . . . . . . . 11 ⊢ ((Fun Base ∧ 𝐺 ∈ dom Base) → (Base‘𝐺) ∈ V)
15	14	funfni 5390	. . . . . . . . . 10 ⊢ ((Base Fn V ∧ 𝐺 ∈ V) → (Base‘𝐺) ∈ V)
16	12, 13, 15	sylancr 414	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → (Base‘𝐺) ∈ V)
17	5, 16	eqeltrid 2293	. . . . . . . 8 ⊢ (𝐺 ∈ Grp → 𝐵 ∈ V)
18	17	pwexd 4236	. . . . . . 7 ⊢ (𝐺 ∈ Grp → 𝒫 𝐵 ∈ V)
19		rabexg 4198	. . . . . . 7 ⊢ (𝒫 𝐵 ∈ V → {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ∈ V)
20	18, 19	syl 14	. . . . . 6 ⊢ (𝐺 ∈ Grp → {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ∈ V)
21	1, 10, 11, 20	fvmptd3 5691	. . . . 5 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) = {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp})
22	21	eleq2d 2276	. . . 4 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ 𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp}))
23		oveq2 5970	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (𝐺 ↾s 𝑠) = (𝐺 ↾s 𝑆))
24	23	eleq1d 2275	. . . . . 6 ⊢ (𝑠 = 𝑆 → ((𝐺 ↾s 𝑠) ∈ Grp ↔ (𝐺 ↾s 𝑆) ∈ Grp))
25	24	elrab 2933	. . . . 5 ⊢ (𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ↔ (𝑆 ∈ 𝒫 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
26		elpw2g 4211	. . . . . . 7 ⊢ (𝐵 ∈ V → (𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵))
27	17, 26	syl 14	. . . . . 6 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵))
28	27	anbi1d 465	. . . . 5 ⊢ (𝐺 ∈ Grp → ((𝑆 ∈ 𝒫 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))
29	25, 28	bitrid 192	. . . 4 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))
30		ibar 301	. . . 4 ⊢ (𝐺 ∈ Grp → ((𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))))
31	22, 29, 30	3bitrd 214	. . 3 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))))
32		3anass 985	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))
33	31, 32	bitr4di 198	. 2 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))
34	2, 3, 33	pm5.21nii 706	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 981   = wceq 1373   ∈ wcel 2177  {crab 2489  Vcvv 2773   ⊆ wss 3170  𝒫 cpw 3621   Fn wfn 5280  ‘cfv 5285  (class class class)co 5962  Basecbs 12917   ↾_s cress 12918  Grpcgrp 13417  SubGrpcsubg 13588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4173  ax-pow 4229  ax-pr 4264  ax-un 4493  ax-cnex 8046  ax-resscn 8047  ax-1re 8049  ax-addrcl 8052

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-sbc 3003  df-csb 3098  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-int 3895  df-br 4055  df-opab 4117  df-mpt 4118  df-id 4353  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-iota 5246  df-fun 5287  df-fn 5288  df-fv 5293  df-ov 5965  df-inn 9067  df-ndx 12920  df-slot 12921  df-base 12923  df-subg 13591

This theorem is referenced by:  subgss  13595  subgid  13596  subggrp  13598  subgbas  13599  subgrcl  13600  issubg2m  13610  resgrpisgrp  13616  subsubg  13618  opprsubgg  13931  subrngsubg  14051  subrgsubg  14074