This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝐵 )