grpinvf1o - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > grpinvf1o		GIF version

Theorem grpinvf1o 13828

Description: The group inverse is a one-to-one onto function. (Contributed by NM, 22-Oct-2014.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)

**Hypotheses**
Ref	Expression
grpinvinv.b	⊢ 𝐵 = (Base‘𝐺)
grpinvinv.n	⊢ 𝑁 = (inv_g‘𝐺)
grpinv11.g	⊢ (𝜑 → 𝐺 ∈ Grp)

**Assertion**
Ref	Expression
grpinvf1o	⊢ (𝜑 → 𝑁:𝐵–1-1-onto→𝐵)

**Proof of Theorem grpinvf1o**
Step	Hyp	Ref	Expression
1		grpinv11.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ Grp)
2		grpinvinv.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐺)
3		grpinvinv.n	. . . . 5 ⊢ 𝑁 = (inv_g‘𝐺)
4	2, 3	grpinvf 13805	. . . 4 ⊢ (𝐺 ∈ Grp → 𝑁:𝐵⟶𝐵)
5	1, 4	syl 14	. . 3 ⊢ (𝜑 → 𝑁:𝐵⟶𝐵)
6	5	ffnd 5514	. 2 ⊢ (𝜑 → 𝑁 Fn 𝐵)
7	2, 3	grpinvcnv 13826	. . . . 5 ⊢ (𝐺 ∈ Grp → ^◡𝑁 = 𝑁)
8	1, 7	syl 14	. . . 4 ⊢ (𝜑 → ^◡𝑁 = 𝑁)
9	8	fneq1d 5451	. . 3 ⊢ (𝜑 → (^◡𝑁 Fn 𝐵 ↔ 𝑁 Fn 𝐵))
10	6, 9	mpbird 167	. 2 ⊢ (𝜑 → ^◡𝑁 Fn 𝐵)
11		dff1o4 5627	. 2 ⊢ (𝑁:𝐵–1-1-onto→𝐵 ↔ (𝑁 Fn 𝐵 ∧ ^◡𝑁 Fn 𝐵))
12	6, 10, 11	sylanbrc 417	1 ⊢ (𝜑 → 𝑁:𝐵–1-1-onto→𝐵)

Colors of variables: wff set class

Syntax hints: → wi 4 = wceq 1398 ∈ wcel 2205 ^◡ccnv 4753 Fn wfn 5352 ⟶wf 5353 –1-1-onto→wf1o 5356 ‘cfv 5357 Basecbs 13299 Grpcgrp 13758 inv_gcminusg 13759

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4230 ax-sep 4233 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-cnex 8234 ax-resscn 8235 ax-1re 8237 ax-addrcl 8240

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ral 2527 df-rex 2528 df-reu 2529 df-rmo 2530 df-rab 2531 df-v 2817 df-sbc 3046 df-csb 3142 df-un 3218 df-in 3220 df-ss 3227 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-id 4419 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-riota 6011 df-ov 6061 df-inn 9258 df-2 9316 df-ndx 13302 df-slot 13303 df-base 13305 df-plusg 13390 df-0g 13558 df-mgm 13622 df-sgrp 13668 df-mnd 13681 df-grp 13761 df-minusg 13762

This theorem is referenced by: psrnegcl 14967 psrlinv 14968

W3C validator