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

Metamath Proof Explorer

Theorem symgfixelq

Description: A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019)

Ref Expression
Hypotheses symgfixf.p 
|- P = ( Base ` ( SymGrp ` N ) )
symgfixf.q 
|- Q = { q e. P | ( q ` K ) = K }
Assertion symgfixelq 
|- ( F e. V -> ( F e. Q <-> ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) )

Proof

Step Hyp Ref Expression
1 symgfixf.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 symgfixf.q 
 |-  Q = { q e. P | ( q ` K ) = K }
3 fveq1 
 |-  ( f = F -> ( f ` K ) = ( F ` K ) )
4 3 eqeq1d 
 |-  ( f = F -> ( ( f ` K ) = K <-> ( F ` K ) = K ) )
5 fveq1 
 |-  ( q = f -> ( q ` K ) = ( f ` K ) )
6 5 eqeq1d 
 |-  ( q = f -> ( ( q ` K ) = K <-> ( f ` K ) = K ) )
7 6 cbvrabv 
 |-  { q e. P | ( q ` K ) = K } = { f e. P | ( f ` K ) = K }
8 2 7 eqtri 
 |-  Q = { f e. P | ( f ` K ) = K }
9 4 8 elrab2 
 |-  ( F e. Q <-> ( F e. P /\ ( F ` K ) = K ) )
10 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
11 10 1 elsymgbas2 
 |-  ( F e. V -> ( F e. P <-> F : N -1-1-onto-> N ) )
12 11 anbi1d 
 |-  ( F e. V -> ( ( F e. P /\ ( F ` K ) = K ) <-> ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) )
13 9 12 bitrid 
 |-  ( F e. V -> ( F e. Q <-> ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) )