Theorem grpsn 8273

Description: The group operation for the singleton group.

Hypothesis

Ref	Expression
grpsn.1	|- A e. V

Assertion

Ref	Expression
grpsn	|- {<.<.A, A>., A>.} e. Grp

Proof of Theorem grpsn

Step	Hyp	Ref	Expression
1		snex 2826	. 2 |- {A} e. V
2		opex 2858	. . . . 5 |- <.A, A>. e. V
3		grpsn.1	. . . . 5 |- A e. V
4	2, 3	f1osn 3830	. . . 4 |- {<.<.A, A>., A>.}:{<.A, A>.}-1-1-onto->{A}
5		f1of 3797	. . . 4 |- ({<.<.A, A>., A>.}:{<.A, A>.}-1-1-onto->{A} -> {<.<.A, A>., A>.}:{<.A, A>.}-->{A})
6	4, 5	ax-mp 7	. . 3 |- {<.<.A, A>., A>.}:{<.A, A>.}-->{A}
7	3, 3	xpsn 3949	. . . 4 |- ({A} X. {A}) = {<.A, A>.}
8		feq2 3728	. . . 4 |- (({A} X. {A}) = {<.A, A>.} -> ({<.<.A, A>., A>.}:({A} X. {A})-->{A} <-> {<.<.A, A>., A>.}:{<.A, A>.}-->{A}))
9	7, 8	ax-mp 7	. . 3 |- ({<.<.A, A>., A>.}:({A} X. {A})-->{A} <-> {<.<.A, A>., A>.}:{<.A, A>.}-->{A})
10	6, 9	mpbir 188	. 2 |- {<.<.A, A>., A>.}:({A} X. {A})-->{A}
11		opreq2 4027	. . . . . 6 |- (z = A -> ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}A))
12		opreq1 4026	. . . . . . . . 9 |- (x = A -> (x{<.<.A, A>., A>.}y) = (A{<.<.A, A>., A>.}y))
13		opreq2 4027	. . . . . . . . . 10 |- (y = A -> (A{<.<.A, A>., A>.}y) = (A{<.<.A, A>., A>.}A))
14		df-opr 4023	. . . . . . . . . . 11 |- (A{<.<.A, A>., A>.}A) = ({<.<.A, A>., A>.}` <.A, A>.)
15	2, 3	fvsn 3906	. . . . . . . . . . 11 |- ({<.<.A, A>., A>.}` <.A, A>.) = A
16	14, 15	eqtri 1538	. . . . . . . . . 10 |- (A{<.<.A, A>., A>.}A) = A
17	13, 16	syl6eq 1566	. . . . . . . . 9 |- (y = A -> (A{<.<.A, A>., A>.}y) = A)
18	12, 17	sylan9eq 1570	. . . . . . . 8 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) = A)
19	18	opreq1d 4033	. . . . . . 7 |- ((x = A /\ y = A) -> ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}A) = (A{<.<.A, A>., A>.}A))
20	19, 16	syl6eq 1566	. . . . . 6 |- ((x = A /\ y = A) -> ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}A) = A)
21	11, 20	sylan9eqr 1572	. . . . 5 |- (((x = A /\ y = A) /\ z = A) -> ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = A)
22	21	3impa 834	. . . 4 |- ((x = A /\ y = A /\ z = A) -> ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = A)
23		opreq1 4026	. . . . . 6 |- (x = A -> (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = (A{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)))
24		opreq1 4026	. . . . . . . . 9 |- (y = A -> (y{<.<.A, A>., A>.}z) = (A{<.<.A, A>., A>.}z))
25		opreq2 4027	. . . . . . . . . 10 |- (z = A -> (A{<.<.A, A>., A>.}z) = (A{<.<.A, A>., A>.}A))
26	25, 16	syl6eq 1566	. . . . . . . . 9 |- (z = A -> (A{<.<.A, A>., A>.}z) = A)
27	24, 26	sylan9eq 1570	. . . . . . . 8 |- ((y = A /\ z = A) -> (y{<.<.A, A>., A>.}z) = A)
28	27	opreq2d 4034	. . . . . . 7 |- ((y = A /\ z = A) -> (A{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = (A{<.<.A, A>., A>.}A))
29	28, 16	syl6eq 1566	. . . . . 6 |- ((y = A /\ z = A) -> (A{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = A)
30	23, 29	sylan9eq 1570	. . . . 5 |- ((x = A /\ (y = A /\ z = A)) -> (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = A)
31	30	3impb 835	. . . 4 |- ((x = A /\ y = A /\ z = A) -> (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = A)
32	22, 31	eqtr4d 1553	. . 3 |- ((x = A /\ y = A /\ z = A) -> ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)))
33		elsn 2479	. . 3 |- (x e. {A} <-> x = A)
34		elsn 2479	. . 3 |- (y e. {A} <-> y = A)
35		elsn 2479	. . 3 |- (z e. {A} <-> z = A)
36	32, 33, 34, 35	syl3anb 875	. 2 |- ((x e. {A} /\ y e. {A} /\ z e. {A}) -> ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)))
37	3	snid 2496	. 2 |- A e. {A}
38		opreq2 4027	. . . 4 |- (x = A -> (A{<.<.A, A>., A>.}x) = (A{<.<.A, A>., A>.}A))
39		id 59	. . . 4 |- (x = A -> x = A)
40	16, 38, 39	3eqtr4a 1575	. . 3 |- (x = A -> (A{<.<.A, A>., A>.}x) = x)
41	33, 40	sylbi 197	. 2 |- (x e. {A} -> (A{<.<.A, A>., A>.}x) = x)
42	37	a1i 8	. 2 |- (x e. {A} -> A e. {A})
43	38, 16	syl6eq 1566	. . 3 |- (x = A -> (A{<.<.A, A>., A>.}x) = A)
44	33, 43	sylbi 197	. 2 |- (x e. {A} -> (A{<.<.A, A>., A>.}x) = A)
45	1, 10, 36, 37, 41, 42, 44	isgrpi 8255	1 |- {<.<.A, A>., A>.} e. Grp

Syntax hints:   <-> wb 144   /\ wa 221   /\ w3a 781   = wceq 992   e. wcel 994  Vcvv 1857  {csn 2467  <.cop 2469   X. cxp 3249  -->wf 3259  -1-1-onto->wf1o 3262  ` cfv 3263  (class class class)co 4021  Grpcgr 8244

This theorem is referenced by:  grpidval 8275  ablsn 8366  ghomsn 10673  ghomgrplem 10674  cayleythlem 10698  zrdivrng 10969

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-reu 1697  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-id 2913  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-opr 4023  df-grp 8249

Copyright terms: Public domain