Step |
Hyp |
Ref |
Expression |
1 |
|
symgfixf.p |
⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) ) |
2 |
|
symgfixf.q |
⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } |
3 |
|
symgfixf.s |
⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) |
4 |
|
symgfixf.h |
⊢ 𝐻 = ( 𝑞 ∈ 𝑄 ↦ ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) |
5 |
1 2 3 4
|
symgfixf1 |
⊢ ( 𝐾 ∈ 𝑁 → 𝐻 : 𝑄 –1-1→ 𝑆 ) |
6 |
5
|
adantl |
⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐻 : 𝑄 –1-1→ 𝑆 ) |
7 |
1 2 3 4
|
symgfixfo |
⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐻 : 𝑄 –onto→ 𝑆 ) |
8 |
|
df-f1o |
⊢ ( 𝐻 : 𝑄 –1-1-onto→ 𝑆 ↔ ( 𝐻 : 𝑄 –1-1→ 𝑆 ∧ 𝐻 : 𝑄 –onto→ 𝑆 ) ) |
9 |
6 7 8
|
sylanbrc |
⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐻 : 𝑄 –1-1-onto→ 𝑆 ) |