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

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