This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) )