| Step |
Hyp |
Ref |
Expression |
| 1 |
|
symgext.s |
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) ) |
| 2 |
|
symgext.e |
|- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) ) |
| 3 |
|
eqid |
|- ( SymGrp ` ( N \ { K } ) ) = ( SymGrp ` ( N \ { K } ) ) |
| 4 |
3 1
|
symgfv |
|- ( ( Z e. S /\ X e. ( N \ { K } ) ) -> ( Z ` X ) e. ( N \ { K } ) ) |
| 5 |
4
|
adantll |
|- ( ( ( K e. N /\ Z e. S ) /\ X e. ( N \ { K } ) ) -> ( Z ` X ) e. ( N \ { K } ) ) |
| 6 |
|
eldifsni |
|- ( ( Z ` X ) e. ( N \ { K } ) -> ( Z ` X ) =/= K ) |
| 7 |
1 2
|
symgextfv |
|- ( ( K e. N /\ Z e. S ) -> ( X e. ( N \ { K } ) -> ( E ` X ) = ( Z ` X ) ) ) |
| 8 |
7
|
imp |
|- ( ( ( K e. N /\ Z e. S ) /\ X e. ( N \ { K } ) ) -> ( E ` X ) = ( Z ` X ) ) |
| 9 |
8
|
neeq1d |
|- ( ( ( K e. N /\ Z e. S ) /\ X e. ( N \ { K } ) ) -> ( ( E ` X ) =/= K <-> ( Z ` X ) =/= K ) ) |
| 10 |
6 9
|
imbitrrid |
|- ( ( ( K e. N /\ Z e. S ) /\ X e. ( N \ { K } ) ) -> ( ( Z ` X ) e. ( N \ { K } ) -> ( E ` X ) =/= K ) ) |
| 11 |
5 10
|
mpd |
|- ( ( ( K e. N /\ Z e. S ) /\ X e. ( N \ { K } ) ) -> ( E ` X ) =/= K ) |
| 12 |
11
|
adantrr |
|- ( ( ( K e. N /\ Z e. S ) /\ ( X e. ( N \ { K } ) /\ Y e. { K } ) ) -> ( E ` X ) =/= K ) |
| 13 |
|
elsni |
|- ( Y e. { K } -> Y = K ) |
| 14 |
1 2
|
symgextfve |
|- ( K e. N -> ( Y = K -> ( E ` Y ) = K ) ) |
| 15 |
14
|
adantr |
|- ( ( K e. N /\ Z e. S ) -> ( Y = K -> ( E ` Y ) = K ) ) |
| 16 |
13 15
|
syl5com |
|- ( Y e. { K } -> ( ( K e. N /\ Z e. S ) -> ( E ` Y ) = K ) ) |
| 17 |
16
|
adantl |
|- ( ( X e. ( N \ { K } ) /\ Y e. { K } ) -> ( ( K e. N /\ Z e. S ) -> ( E ` Y ) = K ) ) |
| 18 |
17
|
impcom |
|- ( ( ( K e. N /\ Z e. S ) /\ ( X e. ( N \ { K } ) /\ Y e. { K } ) ) -> ( E ` Y ) = K ) |
| 19 |
12 18
|
neeqtrrd |
|- ( ( ( K e. N /\ Z e. S ) /\ ( X e. ( N \ { K } ) /\ Y e. { K } ) ) -> ( E ` X ) =/= ( E ` Y ) ) |
| 20 |
19
|
ex |
|- ( ( K e. N /\ Z e. S ) -> ( ( X e. ( N \ { K } ) /\ Y e. { K } ) -> ( E ` X ) =/= ( E ` Y ) ) ) |