Proof of Theorem symgfixelsi
| Step | Hyp | Ref
| Expression |
| 1 | | symgfixf.p |
. . . . 5
⊢ 𝑃 =
(Base‘(SymGrp‘𝑁)) |
| 2 | | symgfixf.q |
. . . . 5
⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} |
| 3 | 1, 2 | symgfixelq 19451 |
. . . 4
⊢ (𝐹 ∈ 𝑄 → (𝐹 ∈ 𝑄 ↔ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾))) |
| 4 | | f1of1 6847 |
. . . . . . . . . 10
⊢ (𝐹:𝑁–1-1-onto→𝑁 → 𝐹:𝑁–1-1→𝑁) |
| 5 | 4 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → 𝐹:𝑁–1-1→𝑁) |
| 6 | | difssd 4137 |
. . . . . . . . 9
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → (𝑁 ∖ {𝐾}) ⊆ 𝑁) |
| 7 | | f1ores 6862 |
. . . . . . . . 9
⊢ ((𝐹:𝑁–1-1→𝑁 ∧ (𝑁 ∖ {𝐾}) ⊆ 𝑁) → (𝐹 ↾ (𝑁 ∖ {𝐾})):(𝑁 ∖ {𝐾})–1-1-onto→(𝐹 “ (𝑁 ∖ {𝐾}))) |
| 8 | 5, 6, 7 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → (𝐹 ↾ (𝑁 ∖ {𝐾})):(𝑁 ∖ {𝐾})–1-1-onto→(𝐹 “ (𝑁 ∖ {𝐾}))) |
| 9 | | symgfixf.d |
. . . . . . . . . . 11
⊢ 𝐷 = (𝑁 ∖ {𝐾}) |
| 10 | 9 | reseq2i 5994 |
. . . . . . . . . 10
⊢ (𝐹 ↾ 𝐷) = (𝐹 ↾ (𝑁 ∖ {𝐾})) |
| 11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → (𝐹 ↾ 𝐷) = (𝐹 ↾ (𝑁 ∖ {𝐾}))) |
| 12 | 9 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → 𝐷 = (𝑁 ∖ {𝐾})) |
| 13 | | f1ofo 6855 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑁–1-1-onto→𝑁 → 𝐹:𝑁–onto→𝑁) |
| 14 | | foima 6825 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝑁–onto→𝑁 → (𝐹 “ 𝑁) = 𝑁) |
| 15 | 14 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑁–onto→𝑁 → 𝑁 = (𝐹 “ 𝑁)) |
| 16 | 13, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑁–1-1-onto→𝑁 → 𝑁 = (𝐹 “ 𝑁)) |
| 17 | 16 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → 𝑁 = (𝐹 “ 𝑁)) |
| 18 | | sneq 4636 |
. . . . . . . . . . . . . 14
⊢ (𝐾 = (𝐹‘𝐾) → {𝐾} = {(𝐹‘𝐾)}) |
| 19 | 18 | eqcoms 2745 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝐾) = 𝐾 → {𝐾} = {(𝐹‘𝐾)}) |
| 20 | 19 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → {𝐾} = {(𝐹‘𝐾)}) |
| 21 | | f1ofn 6849 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝑁–1-1-onto→𝑁 → 𝐹 Fn 𝑁) |
| 22 | 21 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → 𝐹 Fn 𝑁) |
| 23 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → 𝐾 ∈ 𝑁) |
| 24 | | fnsnfv 6988 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝑁 ∧ 𝐾 ∈ 𝑁) → {(𝐹‘𝐾)} = (𝐹 “ {𝐾})) |
| 25 | 22, 23, 24 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → {(𝐹‘𝐾)} = (𝐹 “ {𝐾})) |
| 26 | 20, 25 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → {𝐾} = (𝐹 “ {𝐾})) |
| 27 | 17, 26 | difeq12d 4127 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → (𝑁 ∖ {𝐾}) = ((𝐹 “ 𝑁) ∖ (𝐹 “ {𝐾}))) |
| 28 | | dff1o2 6853 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑁–1-1-onto→𝑁 ↔ (𝐹 Fn 𝑁 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝑁)) |
| 29 | 28 | simp2bi 1147 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑁–1-1-onto→𝑁 → Fun ◡𝐹) |
| 30 | 29 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → Fun ◡𝐹) |
| 31 | | imadif 6650 |
. . . . . . . . . . 11
⊢ (Fun
◡𝐹 → (𝐹 “ (𝑁 ∖ {𝐾})) = ((𝐹 “ 𝑁) ∖ (𝐹 “ {𝐾}))) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → (𝐹 “ (𝑁 ∖ {𝐾})) = ((𝐹 “ 𝑁) ∖ (𝐹 “ {𝐾}))) |
| 33 | 27, 12, 32 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → 𝐷 = (𝐹 “ (𝑁 ∖ {𝐾}))) |
| 34 | 11, 12, 33 | f1oeq123d 6842 |
. . . . . . . 8
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → ((𝐹 ↾ 𝐷):𝐷–1-1-onto→𝐷 ↔ (𝐹 ↾ (𝑁 ∖ {𝐾})):(𝑁 ∖ {𝐾})–1-1-onto→(𝐹 “ (𝑁 ∖ {𝐾})))) |
| 35 | 8, 34 | mpbird 257 |
. . . . . . 7
⊢ ((𝐾 ∈ 𝑁 ∧ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)) → (𝐹 ↾ 𝐷):𝐷–1-1-onto→𝐷) |
| 36 | 35 | ancoms 458 |
. . . . . 6
⊢ (((𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾) ∧ 𝐾 ∈ 𝑁) → (𝐹 ↾ 𝐷):𝐷–1-1-onto→𝐷) |
| 37 | | symgfixf.s |
. . . . . . 7
⊢ 𝑆 =
(Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) |
| 38 | 1, 2, 37, 9 | symgfixels 19452 |
. . . . . 6
⊢ (𝐹 ∈ 𝑄 → ((𝐹 ↾ 𝐷) ∈ 𝑆 ↔ (𝐹 ↾ 𝐷):𝐷–1-1-onto→𝐷)) |
| 39 | 36, 38 | imbitrrid 246 |
. . . . 5
⊢ (𝐹 ∈ 𝑄 → (((𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾) ∧ 𝐾 ∈ 𝑁) → (𝐹 ↾ 𝐷) ∈ 𝑆)) |
| 40 | 39 | expd 415 |
. . . 4
⊢ (𝐹 ∈ 𝑄 → ((𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾) → (𝐾 ∈ 𝑁 → (𝐹 ↾ 𝐷) ∈ 𝑆))) |
| 41 | 3, 40 | sylbid 240 |
. . 3
⊢ (𝐹 ∈ 𝑄 → (𝐹 ∈ 𝑄 → (𝐾 ∈ 𝑁 → (𝐹 ↾ 𝐷) ∈ 𝑆))) |
| 42 | 41 | pm2.43i 52 |
. 2
⊢ (𝐹 ∈ 𝑄 → (𝐾 ∈ 𝑁 → (𝐹 ↾ 𝐷) ∈ 𝑆)) |
| 43 | 42 | impcom 407 |
1
⊢ ((𝐾 ∈ 𝑁 ∧ 𝐹 ∈ 𝑄) → (𝐹 ↾ 𝐷) ∈ 𝑆) |