Metamath Proof Explorer

Theorem pmtrdifellem4

Description: Lemma 4 for pmtrdifel . (Contributed by AV, 28-Jan-2019)

Ref Expression
Hypotheses pmtrdifel.t 
|- T = ran ( pmTrsp ` ( N \ { K } ) )
pmtrdifel.r 
|- R = ran ( pmTrsp ` N )
pmtrdifel.0 
|- S = ( ( pmTrsp ` N ) ` dom ( Q \ _I ) )
Assertion pmtrdifellem4 
|- ( ( Q e. T /\ K e. N ) -> ( S ` K ) = K )

Proof

Step Hyp Ref Expression
1 pmtrdifel.t 
 |-  T = ran ( pmTrsp ` ( N \ { K } ) )
2 pmtrdifel.r 
 |-  R = ran ( pmTrsp ` N )
3 pmtrdifel.0 
 |-  S = ( ( pmTrsp ` N ) ` dom ( Q \ _I ) )
4 1 2 3 pmtrdifellem1 
 |-  ( Q e. T -> S e. R )
5 eqid 
 |-  ( pmTrsp ` N ) = ( pmTrsp ` N )
6 eqid 
 |-  dom ( S \ _I ) = dom ( S \ _I )
7 5 2 6 pmtrffv 
 |-  ( ( S e. R /\ K e. N ) -> ( S ` K ) = if ( K e. dom ( S \ _I ) , U. ( dom ( S \ _I ) \ { K } ) , K ) )
8 4 7 sylan 
 |-  ( ( Q e. T /\ K e. N ) -> ( S ` K ) = if ( K e. dom ( S \ _I ) , U. ( dom ( S \ _I ) \ { K } ) , K ) )
9 eqid 
 |-  ( SymGrp ` ( N \ { K } ) ) = ( SymGrp ` ( N \ { K } ) )
10 eqid 
 |-  ( Base ` ( SymGrp ` ( N \ { K } ) ) ) = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
11 1 9 10 symgtrf 
 |-  T C_ ( Base ` ( SymGrp ` ( N \ { K } ) ) )
12 11 sseli 
 |-  ( Q e. T -> Q e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) )
13 9 10 symgbasf 
 |-  ( Q e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) -> Q : ( N \ { K } ) --> ( N \ { K } ) )
14 ffn 
 |-  ( Q : ( N \ { K } ) --> ( N \ { K } ) -> Q Fn ( N \ { K } ) )
15 fndifnfp 
 |-  ( Q Fn ( N \ { K } ) -> dom ( Q \ _I ) = { x e. ( N \ { K } ) | ( Q ` x ) =/= x } )
16 ssrab2 
 |-  { x e. ( N \ { K } ) | ( Q ` x ) =/= x } C_ ( N \ { K } )
17 ssel2 
 |-  ( ( { x e. ( N \ { K } ) | ( Q ` x ) =/= x } C_ ( N \ { K } ) /\ K e. { x e. ( N \ { K } ) | ( Q ` x ) =/= x } ) -> K e. ( N \ { K } ) )
18 eldif 
 |-  ( K e. ( N \ { K } ) <-> ( K e. N /\ -. K e. { K } ) )
19 elsng 
 |-  ( K e. N -> ( K e. { K } <-> K = K ) )
20 19 notbid 
 |-  ( K e. N -> ( -. K e. { K } <-> -. K = K ) )
21 eqid 
 |-  K = K
22 21 pm2.24i 
 |-  ( -. K = K -> -. K e. N )
23 20 22 syl6bi 
 |-  ( K e. N -> ( -. K e. { K } -> -. K e. N ) )
24 23 imp 
 |-  ( ( K e. N /\ -. K e. { K } ) -> -. K e. N )
25 18 24 sylbi 
 |-  ( K e. ( N \ { K } ) -> -. K e. N )
26 17 25 syl 
 |-  ( ( { x e. ( N \ { K } ) | ( Q ` x ) =/= x } C_ ( N \ { K } ) /\ K e. { x e. ( N \ { K } ) | ( Q ` x ) =/= x } ) -> -. K e. N )
27 16 26 mpan 
 |-  ( K e. { x e. ( N \ { K } ) | ( Q ` x ) =/= x } -> -. K e. N )
28 27 con2i 
 |-  ( K e. N -> -. K e. { x e. ( N \ { K } ) | ( Q ` x ) =/= x } )
29 eleq2 
 |-  ( dom ( Q \ _I ) = { x e. ( N \ { K } ) | ( Q ` x ) =/= x } -> ( K e. dom ( Q \ _I ) <-> K e. { x e. ( N \ { K } ) | ( Q ` x ) =/= x } ) )
30 29 notbid 
 |-  ( dom ( Q \ _I ) = { x e. ( N \ { K } ) | ( Q ` x ) =/= x } -> ( -. K e. dom ( Q \ _I ) <-> -. K e. { x e. ( N \ { K } ) | ( Q ` x ) =/= x } ) )
31 28 30 syl5ibr 
 |-  ( dom ( Q \ _I ) = { x e. ( N \ { K } ) | ( Q ` x ) =/= x } -> ( K e. N -> -. K e. dom ( Q \ _I ) ) )
32 14 15 31 3syl 
 |-  ( Q : ( N \ { K } ) --> ( N \ { K } ) -> ( K e. N -> -. K e. dom ( Q \ _I ) ) )
33 12 13 32 3syl 
 |-  ( Q e. T -> ( K e. N -> -. K e. dom ( Q \ _I ) ) )
34 33 imp 
 |-  ( ( Q e. T /\ K e. N ) -> -. K e. dom ( Q \ _I ) )
35 1 2 3 pmtrdifellem2 
 |-  ( Q e. T -> dom ( S \ _I ) = dom ( Q \ _I ) )
36 35 eleq2d 
 |-  ( Q e. T -> ( K e. dom ( S \ _I ) <-> K e. dom ( Q \ _I ) ) )
37 36 adantr 
 |-  ( ( Q e. T /\ K e. N ) -> ( K e. dom ( S \ _I ) <-> K e. dom ( Q \ _I ) ) )
38 34 37 mtbird 
 |-  ( ( Q e. T /\ K e. N ) -> -. K e. dom ( S \ _I ) )
39 38 iffalsed 
 |-  ( ( Q e. T /\ K e. N ) -> if ( K e. dom ( S \ _I ) , U. ( dom ( S \ _I ) \ { K } ) , K ) = K )
40 8 39 eqtrd 
 |-  ( ( Q e. T /\ K e. N ) -> ( S ` K ) = K )