Metamath Proof Explorer

Theorem grpoinvf

Description: Mapping of the inverse function of a group. (Contributed by NM, 29-Mar-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpasscan1.1 
|- X = ran G
grpasscan1.2 
|- N = ( inv ` G )
Assertion grpoinvf 
|- ( G e. GrpOp -> N : X -1-1-onto-> X )

Proof

Step Hyp Ref Expression
1 grpasscan1.1 
 |-  X = ran G
2 grpasscan1.2 
 |-  N = ( inv ` G )
3 riotaex 
 |-  ( iota_ y e. X ( y G x ) = ( GId ` G ) ) e. _V
4 eqid 
 |-  ( x e. X |-> ( iota_ y e. X ( y G x ) = ( GId ` G ) ) ) = ( x e. X |-> ( iota_ y e. X ( y G x ) = ( GId ` G ) ) )
5 3 4 fnmpti 
 |-  ( x e. X |-> ( iota_ y e. X ( y G x ) = ( GId ` G ) ) ) Fn X
6 eqid 
 |-  ( GId ` G ) = ( GId ` G )
7 1 6 2 grpoinvfval 
 |-  ( G e. GrpOp -> N = ( x e. X |-> ( iota_ y e. X ( y G x ) = ( GId ` G ) ) ) )
8 7 fneq1d 
 |-  ( G e. GrpOp -> ( N Fn X <-> ( x e. X |-> ( iota_ y e. X ( y G x ) = ( GId ` G ) ) ) Fn X ) )
9 5 8 mpbiri 
 |-  ( G e. GrpOp -> N Fn X )
10 fnrnfv 
 |-  ( N Fn X -> ran N = { y | E. x e. X y = ( N ` x ) } )
11 9 10 syl 
 |-  ( G e. GrpOp -> ran N = { y | E. x e. X y = ( N ` x ) } )
12 1 2 grpoinvcl 
 |-  ( ( G e. GrpOp /\ y e. X ) -> ( N ` y ) e. X )
13 1 2 grpo2inv 
 |-  ( ( G e. GrpOp /\ y e. X ) -> ( N ` ( N ` y ) ) = y )
14 13 eqcomd 
 |-  ( ( G e. GrpOp /\ y e. X ) -> y = ( N ` ( N ` y ) ) )
15 fveq2 
 |-  ( x = ( N ` y ) -> ( N ` x ) = ( N ` ( N ` y ) ) )
16 15 rspceeqv 
 |-  ( ( ( N ` y ) e. X /\ y = ( N ` ( N ` y ) ) ) -> E. x e. X y = ( N ` x ) )
17 12 14 16 syl2anc 
 |-  ( ( G e. GrpOp /\ y e. X ) -> E. x e. X y = ( N ` x ) )
18 17 ex 
 |-  ( G e. GrpOp -> ( y e. X -> E. x e. X y = ( N ` x ) ) )
19 simpr 
 |-  ( ( ( G e. GrpOp /\ x e. X ) /\ y = ( N ` x ) ) -> y = ( N ` x ) )
20 1 2 grpoinvcl 
 |-  ( ( G e. GrpOp /\ x e. X ) -> ( N ` x ) e. X )
21 20 adantr 
 |-  ( ( ( G e. GrpOp /\ x e. X ) /\ y = ( N ` x ) ) -> ( N ` x ) e. X )
22 19 21 eqeltrd 
 |-  ( ( ( G e. GrpOp /\ x e. X ) /\ y = ( N ` x ) ) -> y e. X )
23 22 rexlimdva2 
 |-  ( G e. GrpOp -> ( E. x e. X y = ( N ` x ) -> y e. X ) )
24 18 23 impbid 
 |-  ( G e. GrpOp -> ( y e. X <-> E. x e. X y = ( N ` x ) ) )
25 24 eqabdv 
 |-  ( G e. GrpOp -> X = { y | E. x e. X y = ( N ` x ) } )
26 11 25 eqtr4d 
 |-  ( G e. GrpOp -> ran N = X )
27 fveq2 
 |-  ( ( N ` x ) = ( N ` y ) -> ( N ` ( N ` x ) ) = ( N ` ( N ` y ) ) )
28 1 2 grpo2inv 
 |-  ( ( G e. GrpOp /\ x e. X ) -> ( N ` ( N ` x ) ) = x )
29 28 13 eqeqan12d 
 |-  ( ( ( G e. GrpOp /\ x e. X ) /\ ( G e. GrpOp /\ y e. X ) ) -> ( ( N ` ( N ` x ) ) = ( N ` ( N ` y ) ) <-> x = y ) )
30 29 anandis 
 |-  ( ( G e. GrpOp /\ ( x e. X /\ y e. X ) ) -> ( ( N ` ( N ` x ) ) = ( N ` ( N ` y ) ) <-> x = y ) )
31 27 30 imbitrid 
 |-  ( ( G e. GrpOp /\ ( x e. X /\ y e. X ) ) -> ( ( N ` x ) = ( N ` y ) -> x = y ) )
32 31 ralrimivva 
 |-  ( G e. GrpOp -> A. x e. X A. y e. X ( ( N ` x ) = ( N ` y ) -> x = y ) )
33 dff1o6 
 |-  ( N : X -1-1-onto-> X <-> ( N Fn X /\ ran N = X /\ A. x e. X A. y e. X ( ( N ` x ) = ( N ` y ) -> x = y ) ) )
34 9 26 32 33 syl3anbrc 
 |-  ( G e. GrpOp -> N : X -1-1-onto-> X )