Metamath Proof Explorer


Theorem elsymgbas

Description: Two ways of saying a function is a 1-1-onto mapping of A to itself. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 28-Jan-2015)

Ref Expression
Hypotheses symgbas.1
|- G = ( SymGrp ` A )
symgbas.2
|- B = ( Base ` G )
Assertion elsymgbas
|- ( A e. V -> ( F e. B <-> F : A -1-1-onto-> A ) )

Proof

Step Hyp Ref Expression
1 symgbas.1
 |-  G = ( SymGrp ` A )
2 symgbas.2
 |-  B = ( Base ` G )
3 elex
 |-  ( F e. B -> F e. _V )
4 3 a1i
 |-  ( A e. V -> ( F e. B -> F e. _V ) )
5 f1of
 |-  ( F : A -1-1-onto-> A -> F : A --> A )
6 fex
 |-  ( ( F : A --> A /\ A e. V ) -> F e. _V )
7 6 expcom
 |-  ( A e. V -> ( F : A --> A -> F e. _V ) )
8 5 7 syl5
 |-  ( A e. V -> ( F : A -1-1-onto-> A -> F e. _V ) )
9 1 2 elsymgbas2
 |-  ( F e. _V -> ( F e. B <-> F : A -1-1-onto-> A ) )
10 9 a1i
 |-  ( A e. V -> ( F e. _V -> ( F e. B <-> F : A -1-1-onto-> A ) ) )
11 4 8 10 pm5.21ndd
 |-  ( A e. V -> ( F e. B <-> F : A -1-1-onto-> A ) )