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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpinvinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
	grpinv11.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
Assertion	grpinvf1o	⊢ ( 𝜑 → 𝑁 : 𝐵 –1-1-onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		grpinvinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpinvinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
3		grpinv11.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4	1 2	grpinvf	⊢ ( 𝐺 ∈ Grp → 𝑁 : 𝐵 ⟶ 𝐵 )
5	3 4	syl	⊢ ( 𝜑 → 𝑁 : 𝐵 ⟶ 𝐵 )
6	5	ffnd	⊢ ( 𝜑 → 𝑁 Fn 𝐵 )
7	1 2	grpinvcnv	⊢ ( 𝐺 ∈ Grp → ◡ 𝑁 = 𝑁 )
8	3 7	syl	⊢ ( 𝜑 → ◡ 𝑁 = 𝑁 )
9	8	fneq1d	⊢ ( 𝜑 → ( ◡ 𝑁 Fn 𝐵 ↔ 𝑁 Fn 𝐵 ) )
10	6 9	mpbird	⊢ ( 𝜑 → ◡ 𝑁 Fn 𝐵 )
11		dff1o4	⊢ ( 𝑁 : 𝐵 –1-1-onto→ 𝐵 ↔ ( 𝑁 Fn 𝐵 ∧ ◡ 𝑁 Fn 𝐵 ) )
12	6 10 11	sylanbrc	⊢ ( 𝜑 → 𝑁 : 𝐵 –1-1-onto→ 𝐵 )