Theorem grpinvf 8075

Description: Mapping of the inverse function of a group.

Hypotheses

Ref	Expression
grpasscan1.1	⊢ X = ran G
grpasscan1.2	⊢ N = (inv ‘G)

Assertion

Ref	Expression
grpinvf	⊢ (G ∈ Grp → N:X–1-1-onto→X)

Proof of Theorem grpinvf

Step	Hyp	Ref	Expression
1		rnexg 3365	. . . . . . . . . 10 ⊢ (G ∈ Grp → ran G ∈ V)
2		grpasscan1.1	. . . . . . . . . 10 ⊢ X = ran G
3	1, 2	syl5eqel 1555	. . . . . . . . 9 ⊢ (G ∈ Grp → X ∈ V)
4		rabexg 2729	. . . . . . . . 9 ⊢ (X ∈ V → {z ∈ X∣(zGx) = (Id ‘G)} ∈ V)
5	3, 4	syl 10	. . . . . . . 8 ⊢ (G ∈ Grp → {z ∈ X∣(zGx) = (Id ‘G)} ∈ V)
6		uniexg 2877	. . . . . . . 8 ⊢ ({z ∈ X∣(zGx) = (Id ‘G)} ∈ V → ∪{z ∈ X∣(zGx) = (Id ‘G)} ∈ V)
7	5, 6	syl 10	. . . . . . 7 ⊢ (G ∈ Grp → ∪{z ∈ X∣(zGx) = (Id ‘G)} ∈ V)
8	7	adantr 391	. . . . . 6 ⊢ ((G ∈ Grp ⋀ x ∈ X) → ∪{z ∈ X∣(zGx) = (Id ‘G)} ∈ V)
9	8	r19.21aiva 1717	. . . . 5 ⊢ (G ∈ Grp → ∀x ∈ X ∪{z ∈ X∣(zGx) = (Id ‘G)} ∈ V)
10		eqid 1478	. . . . . 6 ⊢ {⟨x, y⟩∣(x ∈ X ⋀ y = ∪{z ∈ X∣(zGx) = (Id ‘G)})} = {⟨x, y⟩∣(x ∈ X ⋀ y = ∪{z ∈ X∣(zGx) = (Id ‘G)})}
11	10	fnopab2g 3622	. . . . 5 ⊢ (∀x ∈ X ∪{z ∈ X∣(zGx) = (Id ‘G)} ∈ V ↔ {⟨x, y⟩∣(x ∈ X ⋀ y = ∪{z ∈ X∣(zGx) = (Id ‘G)})} Fn X)
12	9, 11	sylib 198	. . . 4 ⊢ (G ∈ Grp → {⟨x, y⟩∣(x ∈ X ⋀ y = ∪{z ∈ X∣(zGx) = (Id ‘G)})} Fn X)
13		eqid 1478	. . . . . 6 ⊢ (Id ‘G) = (Id ‘G)
14		grpasscan1.2	. . . . . 6 ⊢ N = (inv ‘G)
15	2, 13, 14	grpinvfval 8062	. . . . 5 ⊢ (G ∈ Grp → N = {⟨x, y⟩∣(x ∈ X ⋀ y = ∪{z ∈ X∣(zGx) = (Id ‘G)})})
16		fneq1 3588	. . . . 5 ⊢ (N = {⟨x, y⟩∣(x ∈ X ⋀ y = ∪{z ∈ X∣(zGx) = (Id ‘G)})} → (N Fn X ↔ {⟨x, y⟩∣(x ∈ X ⋀ y = ∪{z ∈ X∣(zGx) = (Id ‘G)})} Fn X))
17	15, 16	syl 10	. . . 4 ⊢ (G ∈ Grp → (N Fn X ↔ {⟨x, y⟩∣(x ∈ X ⋀ y = ∪{z ∈ X∣(zGx) = (Id ‘G)})} Fn X))
18	12, 17	mpbird 196	. . 3 ⊢ (G ∈ Grp → N Fn X)
19		fnrnfv 3765	. . . . 5 ⊢ (N Fn X → ran N = {y∣∃x ∈ X y = (N ‘x)})
20	18, 19	syl 10	. . . 4 ⊢ (G ∈ Grp → ran N = {y∣∃x ∈ X y = (N ‘x)})
21		fveq2 3730	. . . . . . . . . 10 ⊢ (x = (N ‘y) → (N ‘x) = (N ‘(N ‘y)))
22	21	eqeq2d 1489	. . . . . . . . 9 ⊢ (x = (N ‘y) → (y = (N ‘x) ↔ y = (N ‘(N ‘y))))
23	22	rcla4ev 1880	. . . . . . . 8 ⊢ (((N ‘y) ∈ X ⋀ y = (N ‘(N ‘y))) → ∃x ∈ X y = (N ‘x))
24	2, 14	grpinvcl 8064	. . . . . . . 8 ⊢ ((G ∈ Grp ⋀ y ∈ X) → (N ‘y) ∈ X)
25	2, 14	grp2inv 8074	. . . . . . . . 9 ⊢ ((G ∈ Grp ⋀ y ∈ X) → (N ‘(N ‘y)) = y)
26	25	eqcomd 1483	. . . . . . . 8 ⊢ ((G ∈ Grp ⋀ y ∈ X) → y = (N ‘(N ‘y)))
27	23, 24, 26	sylanc 473	. . . . . . 7 ⊢ ((G ∈ Grp ⋀ y ∈ X) → ∃x ∈ X y = (N ‘x))
28	27	ex 373	. . . . . 6 ⊢ (G ∈ Grp → (y ∈ X → ∃x ∈ X y = (N ‘x)))
29		pm3.27 323	. . . . . . . . 9 ⊢ (((G ∈ Grp ⋀ x ∈ X) ⋀ y = (N ‘x)) → y = (N ‘x))
30	2, 14	grpinvcl 8064	. . . . . . . . . 10 ⊢ ((G ∈ Grp ⋀ x ∈ X) → (N ‘x) ∈ X)
31	30	adantr 391	. . . . . . . . 9 ⊢ (((G ∈ Grp ⋀ x ∈ X) ⋀ y = (N ‘x)) → (N ‘x) ∈ X)
32	29, 31	eqeltrd 1551	. . . . . . . 8 ⊢ (((G ∈ Grp ⋀ x ∈ X) ⋀ y = (N ‘x)) → y ∈ X)
33	32	exp31 378	. . . . . . 7 ⊢ (G ∈ Grp → (x ∈ X → (y = (N ‘x) → y ∈ X)))
34	33	r19.23adv 1749	. . . . . 6 ⊢ (G ∈ Grp → (∃x ∈ X y = (N ‘x) → y ∈ X))
35	28, 34	impbid 518	. . . . 5 ⊢ (G ∈ Grp → (y ∈ X ↔ ∃x ∈ X y = (N ‘x)))
36	35	abbi2dv 1581	. . . 4 ⊢ (G ∈ Grp → X = {y∣∃x ∈ X y = (N ‘x)})
37	20, 36	eqtr4d 1513	. . 3 ⊢ (G ∈ Grp → ran N = X)
38	2, 14	grp2inv 8074	. . . . . . . 8 ⊢ ((G ∈ Grp ⋀ x ∈ X) → (N ‘(N ‘x)) = x)
39	38, 25	eqeqan12d 1493	. . . . . . 7 ⊢ (((G ∈ Grp ⋀ x ∈ X) ⋀ (G ∈ Grp ⋀ y ∈ X)) → ((N ‘(N ‘x)) = (N ‘(N ‘y)) ↔ x = y))
40	39	anandis 514	. . . . . 6 ⊢ ((G ∈ Grp ⋀ (x ∈ X ⋀ y ∈ X)) → ((N ‘(N ‘x)) = (N ‘(N ‘y)) ↔ x = y))
41		fveq2 3730	. . . . . 6 ⊢ ((N ‘x) = (N ‘y) → (N ‘(N ‘x)) = (N ‘(N ‘y)))
42	40, 41	syl5bi 208	. . . . 5 ⊢ ((G ∈ Grp ⋀ (x ∈ X ⋀ y ∈ X)) → ((N ‘x) = (N ‘y) → x = y))
43	42	ex 373	. . . 4 ⊢ (G ∈ Grp → ((x ∈ X ⋀ y ∈ X) → ((N ‘x) = (N ‘y) → x = y)))
44	43	r19.21aivv 1723	. . 3 ⊢ (G ∈ Grp → ∀x ∈ X ∀y ∈ X ((N ‘x) = (N ‘y) → x = y))
45	18, 37, 44	3jca 821	. 2 ⊢ (G ∈ Grp → (N Fn X ⋀ ran N = X ⋀ ∀x ∈ X ∀y ∈ X ((N ‘x) = (N ‘y) → x = y)))
46		f1ofv 3883	. 2 ⊢ (N:X–1-1-onto→X ↔ (N Fn X ⋀ ran N = X ⋀ ∀x ∈ X ∀y ∈ X ((N ‘x) = (N ‘y) → x = y)))
47	45, 46	sylibr 200	1 ⊢ (G ∈ Grp → N:X–1-1-onto→X)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 777   = wceq 958   ∈ wcel 960  {cab 1466  ∀wral 1648  ∃wrex 1649  {crab 1651  Vcvv 1814  ∪cuni 2507  {copab 2671  ran crn 3177   Fn wfn 3183  –1-1-onto→wf1o 3187   ‘cfv 3188  (class class class)co 3969  Grpcgr 8030  Idcgi 8031  invcgn 8032

This theorem is referenced by:  invfval 8257

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-pow 2748  ax-pr 2785  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-id 2841  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-f1 3201  df-fo 3202  df-f1o 3203  df-fv 3204  df-opr 3971  df-grp 8034  df-gid 8035  df-ginv 8036

Copyright terms: Public domain