Metamath Proof Explorer

Theorem symgextf1lem

Description: Lemma for symgextf1 . (Contributed by AV, 6-Jan-2019)

Ref Expression
Hypotheses symgext.s 
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
symgext.e 
|- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
Assertion symgextf1lem 
|- ( ( K e. N /\ Z e. S ) -> ( ( X e. ( N \ { K } ) /\ Y e. { K } ) -> ( E ` X ) =/= ( E ` Y ) ) )

Proof

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