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