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	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
Assertion	symgfix2	⊢ ( 𝐿 ∈ 𝑁 → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		symgfix2.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		eldif	⊢ ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ↔ ( 𝑄 ∈ 𝑃 ∧ ¬ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) )
3		ianor	⊢ ( ¬ ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ↔ ( ¬ 𝑄 ∈ 𝑃 ∨ ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
4		fveq1	⊢ ( 𝑞 = 𝑄 → ( 𝑞 ‘ 𝐾 ) = ( 𝑄 ‘ 𝐾 ) )
5	4	eqeq1d	⊢ ( 𝑞 = 𝑄 → ( ( 𝑞 ‘ 𝐾 ) = 𝐿 ↔ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
6	5	elrab	⊢ ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ↔ ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
7	3 6	xchnxbir	⊢ ( ¬ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ↔ ( ¬ 𝑄 ∈ 𝑃 ∨ ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
8	7	anbi2i	⊢ ( ( 𝑄 ∈ 𝑃 ∧ ¬ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ↔ ( 𝑄 ∈ 𝑃 ∧ ( ¬ 𝑄 ∈ 𝑃 ∨ ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ) )
9	2 8	bitri	⊢ ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ↔ ( 𝑄 ∈ 𝑃 ∧ ( ¬ 𝑄 ∈ 𝑃 ∨ ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ) )
10		pm2.21	⊢ ( ¬ 𝑄 ∈ 𝑃 → ( 𝑄 ∈ 𝑃 → ( 𝐿 ∈ 𝑁 → ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) ) )
11	1	symgmov2	⊢ ( 𝑄 ∈ 𝑃 → ∀ 𝑙 ∈ 𝑁 ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝑙 )
12		eqeq2	⊢ ( 𝑙 = 𝐿 → ( ( 𝑄 ‘ 𝑘 ) = 𝑙 ↔ ( 𝑄 ‘ 𝑘 ) = 𝐿 ) )
13	12	rexbidv	⊢ ( 𝑙 = 𝐿 → ( ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝑙 ↔ ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝐿 ) )
14	13	rspcva	⊢ ( ( 𝐿 ∈ 𝑁 ∧ ∀ 𝑙 ∈ 𝑁 ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝑙 ) → ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝐿 )
15		eqeq2	⊢ ( 𝐿 = ( 𝑄 ‘ 𝑘 ) → ( ( 𝑄 ‘ 𝐾 ) = 𝐿 ↔ ( 𝑄 ‘ 𝐾 ) = ( 𝑄 ‘ 𝑘 ) ) )
16	15	eqcoms	⊢ ( ( 𝑄 ‘ 𝑘 ) = 𝐿 → ( ( 𝑄 ‘ 𝐾 ) = 𝐿 ↔ ( 𝑄 ‘ 𝐾 ) = ( 𝑄 ‘ 𝑘 ) ) )
17	16	notbid	⊢ ( ( 𝑄 ‘ 𝑘 ) = 𝐿 → ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ↔ ¬ ( 𝑄 ‘ 𝐾 ) = ( 𝑄 ‘ 𝑘 ) ) )
18		fveq2	⊢ ( 𝐾 = 𝑘 → ( 𝑄 ‘ 𝐾 ) = ( 𝑄 ‘ 𝑘 ) )
19	18	eqcoms	⊢ ( 𝑘 = 𝐾 → ( 𝑄 ‘ 𝐾 ) = ( 𝑄 ‘ 𝑘 ) )
20	19	necon3bi	⊢ ( ¬ ( 𝑄 ‘ 𝐾 ) = ( 𝑄 ‘ 𝑘 ) → 𝑘 ≠ 𝐾 )
21	17 20	syl6bi	⊢ ( ( 𝑄 ‘ 𝑘 ) = 𝐿 → ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 → 𝑘 ≠ 𝐾 ) )
22	21	com12	⊢ ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 → ( ( 𝑄 ‘ 𝑘 ) = 𝐿 → 𝑘 ≠ 𝐾 ) )
23	22	pm4.71rd	⊢ ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 → ( ( 𝑄 ‘ 𝑘 ) = 𝐿 ↔ ( 𝑘 ≠ 𝐾 ∧ ( 𝑄 ‘ 𝑘 ) = 𝐿 ) ) )
24	23	rexbidv	⊢ ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 → ( ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝐿 ↔ ∃ 𝑘 ∈ 𝑁 ( 𝑘 ≠ 𝐾 ∧ ( 𝑄 ‘ 𝑘 ) = 𝐿 ) ) )
25		rexdifsn	⊢ ( ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ↔ ∃ 𝑘 ∈ 𝑁 ( 𝑘 ≠ 𝐾 ∧ ( 𝑄 ‘ 𝑘 ) = 𝐿 ) )
26	24 25	bitr4di	⊢ ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 → ( ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝐿 ↔ ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) )
27	14 26	syl5ibcom	⊢ ( ( 𝐿 ∈ 𝑁 ∧ ∀ 𝑙 ∈ 𝑁 ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝑙 ) → ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 → ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) )
28	27	ex	⊢ ( 𝐿 ∈ 𝑁 → ( ∀ 𝑙 ∈ 𝑁 ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝑙 → ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 → ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) ) )
29	28	com13	⊢ ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 → ( ∀ 𝑙 ∈ 𝑁 ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝑙 → ( 𝐿 ∈ 𝑁 → ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) ) )
30	11 29	syl5	⊢ ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 → ( 𝑄 ∈ 𝑃 → ( 𝐿 ∈ 𝑁 → ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) ) )
31	10 30	jaoi	⊢ ( ( ¬ 𝑄 ∈ 𝑃 ∨ ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) → ( 𝑄 ∈ 𝑃 → ( 𝐿 ∈ 𝑁 → ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) ) )
32	31	com13	⊢ ( 𝐿 ∈ 𝑁 → ( 𝑄 ∈ 𝑃 → ( ( ¬ 𝑄 ∈ 𝑃 ∨ ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) → ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) ) )
33	32	impd	⊢ ( 𝐿 ∈ 𝑁 → ( ( 𝑄 ∈ 𝑃 ∧ ( ¬ 𝑄 ∈ 𝑃 ∨ ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ) → ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) )
34	9 33	syl5bi	⊢ ( 𝐿 ∈ 𝑁 → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → ∃ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑘 ) = 𝐿 ) )