| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | symgext.s | . . 3
⊢ 𝑆 =
(Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) | 
| 2 |  | symgext.e | . . 3
⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) | 
| 3 | 1, 2 | symgextf 19435 | . 2
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁⟶𝑁) | 
| 4 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(SymGrp‘(𝑁
∖ {𝐾})) =
(SymGrp‘(𝑁 ∖
{𝐾})) | 
| 5 | 4, 1 | symgbasf1o 19392 | . . . . . . . . . 10
⊢ (𝑍 ∈ 𝑆 → 𝑍:(𝑁 ∖ {𝐾})–1-1-onto→(𝑁 ∖ {𝐾})) | 
| 6 |  | f1ofo 6855 | . . . . . . . . . 10
⊢ (𝑍:(𝑁 ∖ {𝐾})–1-1-onto→(𝑁 ∖ {𝐾}) → 𝑍:(𝑁 ∖ {𝐾})–onto→(𝑁 ∖ {𝐾})) | 
| 7 | 5, 6 | syl 17 | . . . . . . . . 9
⊢ (𝑍 ∈ 𝑆 → 𝑍:(𝑁 ∖ {𝐾})–onto→(𝑁 ∖ {𝐾})) | 
| 8 | 7 | adantl 481 | . . . . . . . 8
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝑍:(𝑁 ∖ {𝐾})–onto→(𝑁 ∖ {𝐾})) | 
| 9 |  | dffo3 7122 | . . . . . . . 8
⊢ (𝑍:(𝑁 ∖ {𝐾})–onto→(𝑁 ∖ {𝐾}) ↔ (𝑍:(𝑁 ∖ {𝐾})⟶(𝑁 ∖ {𝐾}) ∧ ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝑍‘𝑖))) | 
| 10 | 8, 9 | sylib 218 | . . . . . . 7
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (𝑍:(𝑁 ∖ {𝐾})⟶(𝑁 ∖ {𝐾}) ∧ ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝑍‘𝑖))) | 
| 11 | 10 | simprd 495 | . . . . . 6
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝑍‘𝑖)) | 
| 12 | 1, 2 | symgextfv 19436 | . . . . . . . . . 10
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (𝑖 ∈ (𝑁 ∖ {𝐾}) → (𝐸‘𝑖) = (𝑍‘𝑖))) | 
| 13 | 12 | imp 406 | . . . . . . . . 9
⊢ (((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) ∧ 𝑖 ∈ (𝑁 ∖ {𝐾})) → (𝐸‘𝑖) = (𝑍‘𝑖)) | 
| 14 | 13 | eqeq2d 2748 | . . . . . . . 8
⊢ (((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) ∧ 𝑖 ∈ (𝑁 ∖ {𝐾})) → (𝑘 = (𝐸‘𝑖) ↔ 𝑘 = (𝑍‘𝑖))) | 
| 15 | 14 | rexbidva 3177 | . . . . . . 7
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖) ↔ ∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝑍‘𝑖))) | 
| 16 | 15 | ralbidv 3178 | . . . . . 6
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖) ↔ ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝑍‘𝑖))) | 
| 17 | 11, 16 | mpbird 257 | . . . . 5
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖)) | 
| 18 |  | difssd 4137 | . . . . . . 7
⊢ (𝑘 ∈ (𝑁 ∖ {𝐾}) → (𝑁 ∖ {𝐾}) ⊆ 𝑁) | 
| 19 |  | ssrexv 4053 | . . . . . . 7
⊢ ((𝑁 ∖ {𝐾}) ⊆ 𝑁 → (∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖) → ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖))) | 
| 20 | 18, 19 | syl 17 | . . . . . 6
⊢ (𝑘 ∈ (𝑁 ∖ {𝐾}) → (∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖) → ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖))) | 
| 21 | 20 | ralimia 3080 | . . . . 5
⊢
(∀𝑘 ∈
(𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖) → ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖)) | 
| 22 | 17, 21 | syl 17 | . . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖)) | 
| 23 |  | simpl 482 | . . . . 5
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐾 ∈ 𝑁) | 
| 24 | 1, 2 | symgextfve 19437 | . . . . . . . 8
⊢ (𝐾 ∈ 𝑁 → (𝑖 = 𝐾 → (𝐸‘𝑖) = 𝐾)) | 
| 25 | 24 | adantr 480 | . . . . . . 7
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (𝑖 = 𝐾 → (𝐸‘𝑖) = 𝐾)) | 
| 26 | 25 | imp 406 | . . . . . 6
⊢ (((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) ∧ 𝑖 = 𝐾) → (𝐸‘𝑖) = 𝐾) | 
| 27 | 26 | eqcomd 2743 | . . . . 5
⊢ (((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) ∧ 𝑖 = 𝐾) → 𝐾 = (𝐸‘𝑖)) | 
| 28 | 23, 27 | rspcedeq2vd 3630 | . . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∃𝑖 ∈ 𝑁 𝐾 = (𝐸‘𝑖)) | 
| 29 |  | eqeq1 2741 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑘 = (𝐸‘𝑖) ↔ 𝐾 = (𝐸‘𝑖))) | 
| 30 | 29 | rexbidv 3179 | . . . . . 6
⊢ (𝑘 = 𝐾 → (∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ↔ ∃𝑖 ∈ 𝑁 𝐾 = (𝐸‘𝑖))) | 
| 31 | 30 | ralunsn 4894 | . . . . 5
⊢ (𝐾 ∈ 𝑁 → (∀𝑘 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ↔ (∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ∧ ∃𝑖 ∈ 𝑁 𝐾 = (𝐸‘𝑖)))) | 
| 32 | 31 | adantr 480 | . . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (∀𝑘 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ↔ (∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ∧ ∃𝑖 ∈ 𝑁 𝐾 = (𝐸‘𝑖)))) | 
| 33 | 22, 28, 32 | mpbir2and 713 | . . 3
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∀𝑘 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖)) | 
| 34 |  | difsnid 4810 | . . . . . 6
⊢ (𝐾 ∈ 𝑁 → ((𝑁 ∖ {𝐾}) ∪ {𝐾}) = 𝑁) | 
| 35 | 34 | eqcomd 2743 | . . . . 5
⊢ (𝐾 ∈ 𝑁 → 𝑁 = ((𝑁 ∖ {𝐾}) ∪ {𝐾})) | 
| 36 | 35 | raleqdv 3326 | . . . 4
⊢ (𝐾 ∈ 𝑁 → (∀𝑘 ∈ 𝑁 ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ↔ ∀𝑘 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖))) | 
| 37 | 36 | adantr 480 | . . 3
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (∀𝑘 ∈ 𝑁 ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ↔ ∀𝑘 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖))) | 
| 38 | 33, 37 | mpbird 257 | . 2
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∀𝑘 ∈ 𝑁 ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖)) | 
| 39 |  | dffo3 7122 | . 2
⊢ (𝐸:𝑁–onto→𝑁 ↔ (𝐸:𝑁⟶𝑁 ∧ ∀𝑘 ∈ 𝑁 ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖))) | 
| 40 | 3, 38, 39 | sylanbrc 583 | 1
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁–onto→𝑁) |