Theorem grpsn 8273

Description: The group operation for the singleton group.

Hypothesis

Ref	Expression
grpsn.1	⊢ A ∈ V

Assertion

Ref	Expression
grpsn	⊢ {<.<.A, A>., A>.} ∈ Grp

Proof of Theorem grpsn

Step	Hyp	Ref	Expression
1		snex 2826	. 2 ⊢ {A} ∈ V
2		opex 2858	. . . . 5 ⊢ <.A, A>. ∈ V
3		grpsn.1	. . . . 5 ⊢ A ∈ 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} × {A}) = {<.A, A>.}
8		feq2 3728	. . . 4 ⊢ (({A} × {A}) = {<.A, A>.} → ({<.<.A, A>., A>.}:({A} × {A})–→{A} ↔ {<.<.A, A>., A>.}:{<.A, A>.}–→{A}))
9	7, 8	ax-mp 7	. . 3 ⊢ ({<.<.A, A>., A>.}:({A} × {A})–→{A} ↔ {<.<.A, A>., A>.}:{<.A, A>.}–→{A})
10	6, 9	mpbir 188	. 2 ⊢ {<.<.A, A>., A>.}:({A} × {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 ∈ {A} ↔ x = A)
34		elsn 2479	. . 3 ⊢ (y ∈ {A} ↔ y = A)
35		elsn 2479	. . 3 ⊢ (z ∈ {A} ↔ z = A)
36	32, 33, 34, 35	syl3anb 875	. 2 ⊢ ((x ∈ {A} ⋀ y ∈ {A} ⋀ z ∈ {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 ∈ {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 ∈ {A} → (A{<.<.A, A>., A>.}x) = x)
42	37	a1i 8	. 2 ⊢ (x ∈ {A} → A ∈ {A})
43	38, 16	syl6eq 1566	. . 3 ⊢ (x = A → (A{<.<.A, A>., A>.}x) = A)
44	33, 43	sylbi 197	. 2 ⊢ (x ∈ {A} → (A{<.<.A, A>., A>.}x) = A)
45	1, 10, 36, 37, 41, 42, 44	isgrpi 8255	1 ⊢ {<.<.A, A>., A>.} ∈ Grp

Syntax hints:   ↔ wb 144   ⋀ wa 221   ⋀ w3a 781   = wceq 992   ∈ wcel 994  Vcvv 1857  {csn 2467  <.cop 2469   × 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