Metamath Proof Explorer


Theorem symg2hash

Description: The symmetric group on a (proper) pair has cardinality 2 . (Contributed by AV, 9-Dec-2018)

Ref Expression
Hypotheses symg1bas.1
|- G = ( SymGrp ` A )
symg1bas.2
|- B = ( Base ` G )
symg2bas.0
|- A = { I , J }
Assertion symg2hash
|- ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` B ) = 2 )

Proof

Step Hyp Ref Expression
1 symg1bas.1
 |-  G = ( SymGrp ` A )
2 symg1bas.2
 |-  B = ( Base ` G )
3 symg2bas.0
 |-  A = { I , J }
4 prfi
 |-  { I , J } e. Fin
5 3 4 eqeltri
 |-  A e. Fin
6 1 2 symghash
 |-  ( A e. Fin -> ( # ` B ) = ( ! ` ( # ` A ) ) )
7 5 6 ax-mp
 |-  ( # ` B ) = ( ! ` ( # ` A ) )
8 3 fveq2i
 |-  ( # ` A ) = ( # ` { I , J } )
9 elex
 |-  ( I e. V -> I e. _V )
10 elex
 |-  ( J e. W -> J e. _V )
11 id
 |-  ( I =/= J -> I =/= J )
12 9 10 11 3anim123i
 |-  ( ( I e. V /\ J e. W /\ I =/= J ) -> ( I e. _V /\ J e. _V /\ I =/= J ) )
13 hashprb
 |-  ( ( I e. _V /\ J e. _V /\ I =/= J ) <-> ( # ` { I , J } ) = 2 )
14 12 13 sylib
 |-  ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` { I , J } ) = 2 )
15 8 14 syl5eq
 |-  ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` A ) = 2 )
16 15 fveq2d
 |-  ( ( I e. V /\ J e. W /\ I =/= J ) -> ( ! ` ( # ` A ) ) = ( ! ` 2 ) )
17 fac2
 |-  ( ! ` 2 ) = 2
18 16 17 eqtrdi
 |-  ( ( I e. V /\ J e. W /\ I =/= J ) -> ( ! ` ( # ` A ) ) = 2 )
19 7 18 syl5eq
 |-  ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` B ) = 2 )