| 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
|
eqtrid |
|- ( ( 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
|
eqtrid |
|- ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` B ) = 2 ) |