Theorem symgfixelq

Description: A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019)

	Ref	Expression
Hypotheses	symgfixf.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	symgfixf.q	⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
Assertion	symgfixelq	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝑄 ↔ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		symgfixf.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		symgfixf.q	⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
3		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝐾 ) = ( 𝐹 ‘ 𝐾 ) )
4	3	eqeq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝐾 ) = 𝐾 ↔ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) )
5		fveq1	⊢ ( 𝑞 = 𝑓 → ( 𝑞 ‘ 𝐾 ) = ( 𝑓 ‘ 𝐾 ) )
6	5	eqeq1d	⊢ ( 𝑞 = 𝑓 → ( ( 𝑞 ‘ 𝐾 ) = 𝐾 ↔ ( 𝑓 ‘ 𝐾 ) = 𝐾 ) )
7	6	cbvrabv	⊢ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } = { 𝑓 ∈ 𝑃 ∣ ( 𝑓 ‘ 𝐾 ) = 𝐾 }
8	2 7	eqtri	⊢ 𝑄 = { 𝑓 ∈ 𝑃 ∣ ( 𝑓 ‘ 𝐾 ) = 𝐾 }
9	4 8	elrab2	⊢ ( 𝐹 ∈ 𝑄 ↔ ( 𝐹 ∈ 𝑃 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) )
10		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
11	10 1	elsymgbas2	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝑃 ↔ 𝐹 : 𝑁 –1-1-onto→ 𝑁 ) )
12	11	anbi1d	⊢ ( 𝐹 ∈ 𝑉 → ( ( 𝐹 ∈ 𝑃 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ↔ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) )
13	9 12	bitrid	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝑄 ↔ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) )