Theorem issubg 9425

Description: The predicate "is a subgroup of G." (Contributed by Paul Chapman, 3-Mar-2008.)

Assertion

Ref	Expression
issubg	|- (H e. (SubGrp` G) <-> (G e. Grp /\ H e. Grp /\ H C_ G))

Proof of Theorem issubg

Step	Hyp	Ref	Expression
1		3anass 862	. . 3 |- ((G e. Grp /\ H e. Grp /\ H C_ G) <-> (G e. Grp /\ (H e. Grp /\ H C_ G)))
2		df-rab 2112	. . . . . . . . . 10 |- {h e. Grp | h C_ g} = {h | (h e. Grp /\ h C_ g)}
3		df-pw 3035	. . . . . . . . . . . 12 |- ~Pg = {h | h C_ g}
4		visset 2295	. . . . . . . . . . . . 13 |- g e. _V
5	4	pwex 3487	. . . . . . . . . . . 12 |- ~Pg e. _V
6	3, 5	eqeltrri 1968	. . . . . . . . . . 11 |- {h | h C_ g} e. _V
7		simpr 350	. . . . . . . . . . . 12 |- ((h e. Grp /\ h C_ g) -> h C_ g)
8	7	ss2abi 2679	. . . . . . . . . . 11 |- {h | (h e. Grp /\ h C_ g)} C_ {h | h C_ g}
9	6, 8	ssexi 3456	. . . . . . . . . 10 |- {h | (h e. Grp /\ h C_ g)} e. _V
10	2, 9	eqeltri 1967	. . . . . . . . 9 |- {h e. Grp | h C_ g} e. _V
11		df-subg 9424	. . . . . . . . 9 |- SubGrp = {<.g, s>. | (g e. Grp /\ s = {h e. Grp | h C_ g})}
12	10, 11	dmopab2 4550	. . . . . . . 8 |- dom SubGrp = Grp
13	12	eleq2i 1961	. . . . . . 7 |- (G e. dom SubGrp <-> G e. Grp)
14	13	biimpi 168	. . . . . 6 |- (G e. dom SubGrp -> G e. Grp)
15	14	con3i 114	. . . . 5 |- (-. G e. Grp -> -. G e. dom SubGrp)
16		ndmfv 4702	. . . . 5 |- (-. G e. dom SubGrp -> (SubGrp` G) = (/))
17		n0i 2880	. . . . . 6 |- (H e. (SubGrp` G) -> -. (SubGrp` G) = (/))
18	17	con2i 113	. . . . 5 |- ((SubGrp` G) = (/) -> -. H e. (SubGrp` G))
19	15, 16, 18	3syl 24	. . . 4 |- (-. G e. Grp -> -. H e. (SubGrp` G))
20	19	con4i 90	. . 3 |- (H e. (SubGrp` G) -> G e. Grp)
21		abssexg 3490	. . . . . . . . 9 |- (G e. Grp -> {h | (h C_ G /\ h e. Grp)} e. _V)
22		df-rab 2112	. . . . . . . . . 10 |- {h e. Grp | h C_ G} = {h | (h e. Grp /\ h C_ G)}
23		ancom 482	. . . . . . . . . . 11 |- ((h e. Grp /\ h C_ G) <-> (h C_ G /\ h e. Grp))
24	23	abbii 2006	. . . . . . . . . 10 |- {h | (h e. Grp /\ h C_ G)} = {h | (h C_ G /\ h e. Grp)}
25	22, 24	eqtri 1908	. . . . . . . . 9 |- {h e. Grp | h C_ G} = {h | (h C_ G /\ h e. Grp)}
26	21, 25	syl5eqel 1975	. . . . . . . 8 |- (G e. Grp -> {h e. Grp | h C_ G} e. _V)
27		sseq2 2639	. . . . . . . . . 10 |- (g = G -> (h C_ g <-> h C_ G))
28	27	rabbidv 2287	. . . . . . . . 9 |- (g = G -> {h e. Grp | h C_ g} = {h e. Grp | h C_ G})
29	28, 11	fvopab4g 4742	. . . . . . . 8 |- ((G e. Grp /\ {h e. Grp | h C_ G} e. _V) -> (SubGrp` G) = {h e. Grp | h C_ G})
30	26, 29	mpdan 768	. . . . . . 7 |- (G e. Grp -> (SubGrp` G) = {h e. Grp | h C_ G})
31	30	eleq2d 1964	. . . . . 6 |- (G e. Grp -> (H e. (SubGrp` G) <-> H e. {h e. Grp | h C_ G}))
32		sseq1 2637	. . . . . . 7 |- (h = H -> (h C_ G <-> H C_ G))
33	32	elrab 2414	. . . . . 6 |- (H e. {h e. Grp | h C_ G} <-> (H e. Grp /\ H C_ G))
34	31, 33	syl6bb 595	. . . . 5 |- (G e. Grp -> (H e. (SubGrp` G) <-> (H e. Grp /\ H C_ G)))
35	34	biimpd 170	. . . 4 |- (G e. Grp -> (H e. (SubGrp` G) -> (H e. Grp /\ H C_ G)))
36	20, 35	mpcom 60	. . 3 |- (H e. (SubGrp` G) -> (H e. Grp /\ H C_ G))
37	1, 20, 36	sylanbrc 527	. 2 |- (H e. (SubGrp` G) -> (G e. Grp /\ H e. Grp /\ H C_ G))
38	34	biimpar 461	. . 3 |- ((G e. Grp /\ (H e. Grp /\ H C_ G)) -> H e. (SubGrp` G))
39	38	3impb 1063	. 2 |- ((G e. Grp /\ H e. Grp /\ H C_ G) -> H e. (SubGrp` G))
40	37, 39	impbii 174	1 |- (H e. (SubGrp` G) <-> (G e. Grp /\ H e. Grp /\ H C_ G))

Syntax hints:  -. wn 2   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  dom cdm 3986  ` cfv 3998  Grpcgr 9311  SubGrpcsubg 9423

This theorem is referenced by:  subgres 9426  subgid 9429  issubgi 9431  subgabl 9432  ghsubgi 9446  ssga 9455  efghgrpilem 10073  hhssabli 10765  ghomfo 13634  ghomgsg 13636  cayleylem3 13643  rrisgrp 14698

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-subg 9424

Copyright terms: Public domain