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