Metamath Proof Explorer

Theorem symgfix2

Description: If a permutation does not move a certain element of a set to a second element, there is a third element which is moved to the second element. (Contributed by AV, 2-Jan-2019)

Ref Expression
Hypothesis symgfix2.p 
|- P = ( Base ` ( SymGrp ` N ) )
Assertion symgfix2 
|- ( L e. N -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) )

Proof

Step Hyp Ref Expression
1 symgfix2.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 eldif 
 |-  ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) <-> ( Q e. P /\ -. Q e. { q e. P | ( q ` K ) = L } ) )
3 ianor 
 |-  ( -. ( Q e. P /\ ( Q ` K ) = L ) <-> ( -. Q e. P \/ -. ( Q ` K ) = L ) )
4 fveq1 
 |-  ( q = Q -> ( q ` K ) = ( Q ` K ) )
5 4 eqeq1d 
 |-  ( q = Q -> ( ( q ` K ) = L <-> ( Q ` K ) = L ) )
6 5 elrab 
 |-  ( Q e. { q e. P | ( q ` K ) = L } <-> ( Q e. P /\ ( Q ` K ) = L ) )
7 3 6 xchnxbir 
 |-  ( -. Q e. { q e. P | ( q ` K ) = L } <-> ( -. Q e. P \/ -. ( Q ` K ) = L ) )
8 7 anbi2i 
 |-  ( ( Q e. P /\ -. Q e. { q e. P | ( q ` K ) = L } ) <-> ( Q e. P /\ ( -. Q e. P \/ -. ( Q ` K ) = L ) ) )
9 2 8 bitri 
 |-  ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) <-> ( Q e. P /\ ( -. Q e. P \/ -. ( Q ` K ) = L ) ) )
10 pm2.21 
 |-  ( -. Q e. P -> ( Q e. P -> ( L e. N -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) ) )
11 1 symgmov2 
 |-  ( Q e. P -> A. l e. N E. k e. N ( Q ` k ) = l )
12 eqeq2 
 |-  ( l = L -> ( ( Q ` k ) = l <-> ( Q ` k ) = L ) )
13 12 rexbidv 
 |-  ( l = L -> ( E. k e. N ( Q ` k ) = l <-> E. k e. N ( Q ` k ) = L ) )
14 13 rspcva 
 |-  ( ( L e. N /\ A. l e. N E. k e. N ( Q ` k ) = l ) -> E. k e. N ( Q ` k ) = L )
15 eqeq2 
 |-  ( L = ( Q ` k ) -> ( ( Q ` K ) = L <-> ( Q ` K ) = ( Q ` k ) ) )
16 15 eqcoms 
 |-  ( ( Q ` k ) = L -> ( ( Q ` K ) = L <-> ( Q ` K ) = ( Q ` k ) ) )
17 16 notbid 
 |-  ( ( Q ` k ) = L -> ( -. ( Q ` K ) = L <-> -. ( Q ` K ) = ( Q ` k ) ) )
18 fveq2 
 |-  ( K = k -> ( Q ` K ) = ( Q ` k ) )
19 18 eqcoms 
 |-  ( k = K -> ( Q ` K ) = ( Q ` k ) )
20 19 necon3bi 
 |-  ( -. ( Q ` K ) = ( Q ` k ) -> k =/= K )
21 17 20 syl6bi 
 |-  ( ( Q ` k ) = L -> ( -. ( Q ` K ) = L -> k =/= K ) )
22 21 com12 
 |-  ( -. ( Q ` K ) = L -> ( ( Q ` k ) = L -> k =/= K ) )
23 22 pm4.71rd 
 |-  ( -. ( Q ` K ) = L -> ( ( Q ` k ) = L <-> ( k =/= K /\ ( Q ` k ) = L ) ) )
24 23 rexbidv 
 |-  ( -. ( Q ` K ) = L -> ( E. k e. N ( Q ` k ) = L <-> E. k e. N ( k =/= K /\ ( Q ` k ) = L ) ) )
25 rexdifsn 
 |-  ( E. k e. ( N \ { K } ) ( Q ` k ) = L <-> E. k e. N ( k =/= K /\ ( Q ` k ) = L ) )
26 24 25 bitr4di 
 |-  ( -. ( Q ` K ) = L -> ( E. k e. N ( Q ` k ) = L <-> E. k e. ( N \ { K } ) ( Q ` k ) = L ) )
27 14 26 syl5ibcom 
 |-  ( ( L e. N /\ A. l e. N E. k e. N ( Q ` k ) = l ) -> ( -. ( Q ` K ) = L -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) )
28 27 ex 
 |-  ( L e. N -> ( A. l e. N E. k e. N ( Q ` k ) = l -> ( -. ( Q ` K ) = L -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) ) )
29 28 com13 
 |-  ( -. ( Q ` K ) = L -> ( A. l e. N E. k e. N ( Q ` k ) = l -> ( L e. N -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) ) )
30 11 29 syl5 
 |-  ( -. ( Q ` K ) = L -> ( Q e. P -> ( L e. N -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) ) )
31 10 30 jaoi 
 |-  ( ( -. Q e. P \/ -. ( Q ` K ) = L ) -> ( Q e. P -> ( L e. N -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) ) )
32 31 com13 
 |-  ( L e. N -> ( Q e. P -> ( ( -. Q e. P \/ -. ( Q ` K ) = L ) -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) ) )
33 32 impd 
 |-  ( L e. N -> ( ( Q e. P /\ ( -. Q e. P \/ -. ( Q ` K ) = L ) ) -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) )
34 9 33 syl5bi 
 |-  ( L e. N -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) )