Theorem grpinvf1o

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)

	Ref	Expression
Hypotheses	grpinvinv.b	$$⊢B={\mathrm{Base}}_G$$
	grpinvinv.n	$$⊢N={inv}_g\left(G\right)$$
	grpinv11.g	$$⊢\phi \to G\in \mathrm{Grp}$$
Assertion	grpinvf1o	$$⊢\phi \to N:B\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		grpinvinv.b	$$⊢B={\mathrm{Base}}_G$$
2		grpinvinv.n	$$⊢N={inv}_g\left(G\right)$$
3		grpinv11.g	$$⊢\phi \to G\in \mathrm{Grp}$$
4	1 2	grpinvf	$$⊢G\in \mathrm{Grp}\to N:B⟶B$$
5	3 4	syl	$$⊢\phi \to N:B⟶B$$
6	5	ffnd	$$⊢\phi \to NFnB$$
7	1 2	grpinvcnv	$$⊢G\in \mathrm{Grp}\to N^{-1}=N$$
8	3 7	syl	$$⊢\phi \to N^{-1}=N$$
9	8	fneq1d	$$⊢\phi \to \left(N^{-1}FnB\leftrightarrow NFnB\right)$$
10	6 9	mpbird	$$⊢\phi \to N^{-1}FnB$$
11		dff1o4	$$⊢N:B\underset{1-1\; onto}{⟶}B\leftrightarrow \left(NFnB\wedge N^{-1}FnB\right)$$
12	6 10 11	sylanbrc	$$⊢\phi \to N:B\underset{1-1\; onto}{⟶}B$$