Theorem cayleythlem 10409

Description: Lemma for cayleyth 10410.

Hypotheses

Ref	Expression
cayleythlem.1	|- Q = {<.<.x, x>., x>.}
cayleythlem.2	|- X = ran if(G e. Grp, G, Q)
cayleythlem.3	|- H = (SymGrp` X)
cayleythlem.4	|- F = {<.g, j>. | (g e. X /\ j = {<.a, b>. | (a e. X /\ b = (gif(G e. Grp, G, Q)a))})}
cayleythlem.5	|- Y = ran F
cayleythlem.6	|- S = (H |` (Y X. Y))

Assertion

Ref	Expression
cayleythlem	|- (G e. Grp -> E.fE.h e. (SubGrp` (SymGrp` ran G))f e. (G GrpIso h))

Distinct variable groups:   f,F,h   G,a,b,g,j   f,G,h   f,H,h   Q,a,b,g,j   Q,f,h   S,h   X,a,b,g,j

Proof of Theorem cayleythlem

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . . . 6 |- (G = if(G e. Grp, G, Q) -> (G GrpIso h) = (if(G e. Grp, G, Q) GrpIso h))
2	1	eleq2d 1541	. . . . 5 |- (G = if(G e. Grp, G, Q) -> (f e. (G GrpIso h) <-> f e. (if(G e. Grp, G, Q) GrpIso h)))
3	2	rexbidv 1664	. . . 4 |- (G = if(G e. Grp, G, Q) -> (E.h e. (SubGrp` H)f e. (G GrpIso h) <-> E.h e. (SubGrp` H)f e. (if(G e. Grp, G, Q) GrpIso h)))
4	3	exbidv 1279	. . 3 |- (G = if(G e. Grp, G, Q) -> (E.fE.h e. (SubGrp` H)f e. (G GrpIso h) <-> E.fE.h e. (SubGrp` H)f e. (if(G e. Grp, G, Q) GrpIso h)))
5		cayleythlem.1	. . . . . . . 8 |- Q = {<.<.x, x>., x>.}
6		visset 1813	. . . . . . . . 9 |- x e. V
7	6	grpsn 8120	. . . . . . . 8 |- {<.<.x, x>., x>.} e. Grp
8	5, 7	eqeltr 1544	. . . . . . 7 |- Q e. Grp
9	8	elimel 2394	. . . . . 6 |- if(G e. Grp, G, Q) e. Grp
10		cayleythlem.2	. . . . . 6 |- X = ran if(G e. Grp, G, Q)
11		cayleythlem.3	. . . . . 6 |- H = (SymGrp` X)
12		cayleythlem.4	. . . . . 6 |- F = {<.g, j>. | (g e. X /\ j = {<.a, b>. | (a e. X /\ b = (gif(G e. Grp, G, Q)a))})}
13		cayleythlem.5	. . . . . 6 |- Y = ran F
14		cayleythlem.6	. . . . . 6 |- S = (H |` (Y X. Y))
15	9, 10, 11, 12, 13, 14	cayleyi 10408	. . . . 5 |- (S e. (SubGrp` H) /\ F e. (if(G e. Grp, G, Q) GrpIso S))
16		opreq2 3969	. . . . . . 7 |- (h = S -> (if(G e. Grp, G, Q) GrpIso h) = (if(G e. Grp, G, Q) GrpIso S))
17	16	eleq2d 1541	. . . . . 6 |- (h = S -> (F e. (if(G e. Grp, G, Q) GrpIso h) <-> F e. (if(G e. Grp, G, Q) GrpIso S)))
18	17	rcla4ev 1877	. . . . 5 |- ((S e. (SubGrp` H) /\ F e. (if(G e. Grp, G, Q) GrpIso S)) -> E.h e. (SubGrp` H)F e. (if(G e. Grp, G, Q) GrpIso h))
19	15, 18	ax-mp 7	. . . 4 |- E.h e. (SubGrp` H)F e. (if(G e. Grp, G, Q) GrpIso h)
20		rnexg 3359	. . . . . . . 8 |- (if(G e. Grp, G, Q) e. Grp -> ran if(G e. Grp, G, Q) e. V)
21	9, 20	ax-mp 7	. . . . . . 7 |- ran if(G e. Grp, G, Q) e. V
22	10, 21	eqeltr 1544	. . . . . 6 |- X e. V
23	22, 12	fopabex2 3612	. . . . 5 |- F e. V
24		eleq1 1534	. . . . . 6 |- (f = F -> (f e. (if(G e. Grp, G, Q) GrpIso h) <-> F e. (if(G e. Grp, G, Q) GrpIso h)))
25	24	rexbidv 1664	. . . . 5 |- (f = F -> (E.h e. (SubGrp` H)f e. (if(G e. Grp, G, Q) GrpIso h) <-> E.h e. (SubGrp` H)F e. (if(G e. Grp, G, Q) GrpIso h)))
26	23, 25	cla4ev 1869	. . . 4 |- (E.h e. (SubGrp` H)F e. (if(G e. Grp, G, Q) GrpIso h) -> E.fE.h e. (SubGrp` H)f e. (if(G e. Grp, G, Q) GrpIso h))
27	19, 26	ax-mp 7	. . 3 |- E.fE.h e. (SubGrp` H)f e. (if(G e. Grp, G, Q) GrpIso h)
28	4, 27	dedth 2383	. 2 |- (G e. Grp -> E.fE.h e. (SubGrp` H)f e. (G GrpIso h))
29		iftrue 2366	. . . . . . . . 9 |- (G e. Grp -> if(G e. Grp, G, Q) = G)
30	29	rneqd 3341	. . . . . . . 8 |- (G e. Grp -> ran if(G e. Grp, G, Q) = ran G)
31	30, 10	syl5eq 1519	. . . . . . 7 |- (G e. Grp -> X = ran G)
32	31	fveq2d 3728	. . . . . 6 |- (G e. Grp -> (SymGrp` X) = (SymGrp` ran G))
33	32, 11	syl5eq 1519	. . . . 5 |- (G e. Grp -> H = (SymGrp` ran G))
34	33	fveq2d 3728	. . . 4 |- (G e. Grp -> (SubGrp` H) = (SubGrp` (SymGrp` ran G)))
35	34	rexeq1d 1790	. . 3 |- (G e. Grp -> (E.h e. (SubGrp` H)f e. (G GrpIso h) <-> E.h e. (SubGrp` (SymGrp` ran G))f e. (G GrpIso h)))
36	35	exbidv 1279	. 2 |- (G e. Grp -> (E.fE.h e. (SubGrp` H)f e. (G GrpIso h) <-> E.fE.h e. (SubGrp` (SymGrp` ran G))f e. (G GrpIso h)))
37	28, 36	mpbid 195	1 |- (G e. Grp -> E.fE.h e. (SubGrp` (SymGrp` ran G))f e. (G GrpIso h))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956   e. wcel 958  E.wex 980  E.wrex 1646  Vcvv 1811  ifcif 2361  {csn 2409  <.cop 2411  {copab 2666   X. cxp 3168  ran crn 3171   |` cres 3172  ` cfv 3182  (class class class)co 3963  Grpcgr 8029  SubGrpcsubg 8110   GrpIso cgiso 10375  SymGrpcsymgrp 10395

This theorem is referenced by:  cayleyth 10410

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-reu 1651  df-rab 1652  df-v 1812  df-sbc 1942  df-csb 2002  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-if 2362  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-id 2835  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-f 3194  df-f1 3195  df-fo 3196  df-f1o 3197  df-fv 3198  df-opr 3965  df-oprab 3966  df-1st 4079  df-2nd 4080  df-grp 8033  df-gid 8034  df-ginv 8035  df-subg 8111  df-ghom 10376  df-giso 10377  df-symgrp 10396

Copyright terms: Public domain