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 = ( Base ` G )
	grpinvinv.n	|- N = ( invg ` G )
	grpinv11.g	|- ( ph -> G e. Grp )
Assertion	grpinvf1o	|- ( ph -> N : B -1-1-onto-> B )

Proof

Step	Hyp	Ref	Expression
1		grpinvinv.b	|- B = ( Base ` G )
2		grpinvinv.n	|- N = ( invg ` G )
3		grpinv11.g	|- ( ph -> G e. Grp )
4	1 2	grpinvf	|- ( G e. Grp -> N : B --> B )
5	3 4	syl	|- ( ph -> N : B --> B )
6	5	ffnd	|- ( ph -> N Fn B )
7	1 2	grpinvcnv	|- ( G e. Grp -> `' N = N )
8	3 7	syl	|- ( ph -> `' N = N )
9	8	fneq1d	|- ( ph -> ( `' N Fn B <-> N Fn B ) )
10	6 9	mpbird	|- ( ph -> `' N Fn B )
11		dff1o4	|- ( N : B -1-1-onto-> B <-> ( N Fn B /\ `' N Fn B ) )
12	6 10 11	sylanbrc	|- ( ph -> N : B -1-1-onto-> B )