Step | Hyp | Ref
| Expression |
1 | | symgext.s |
. . 3
⊢ 𝑆 =
(Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) |
2 | | symgext.e |
. . 3
⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) |
3 | 1, 2 | symgextf 18656 |
. 2
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁⟶𝑁) |
4 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(SymGrp‘(𝑁
∖ {𝐾})) =
(SymGrp‘(𝑁 ∖
{𝐾})) |
5 | 4, 1 | symgbasf1o 18614 |
. . . . . . . . . 10
⊢ (𝑍 ∈ 𝑆 → 𝑍:(𝑁 ∖ {𝐾})–1-1-onto→(𝑁 ∖ {𝐾})) |
6 | | f1ofo 6619 |
. . . . . . . . . 10
⊢ (𝑍:(𝑁 ∖ {𝐾})–1-1-onto→(𝑁 ∖ {𝐾}) → 𝑍:(𝑁 ∖ {𝐾})–onto→(𝑁 ∖ {𝐾})) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝑍 ∈ 𝑆 → 𝑍:(𝑁 ∖ {𝐾})–onto→(𝑁 ∖ {𝐾})) |
8 | 7 | adantl 485 |
. . . . . . . 8
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝑍:(𝑁 ∖ {𝐾})–onto→(𝑁 ∖ {𝐾})) |
9 | | dffo3 6872 |
. . . . . . . 8
⊢ (𝑍:(𝑁 ∖ {𝐾})–onto→(𝑁 ∖ {𝐾}) ↔ (𝑍:(𝑁 ∖ {𝐾})⟶(𝑁 ∖ {𝐾}) ∧ ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝑍‘𝑖))) |
10 | 8, 9 | sylib 221 |
. . . . . . 7
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (𝑍:(𝑁 ∖ {𝐾})⟶(𝑁 ∖ {𝐾}) ∧ ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝑍‘𝑖))) |
11 | 10 | simprd 499 |
. . . . . 6
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝑍‘𝑖)) |
12 | 1, 2 | symgextfv 18657 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (𝑖 ∈ (𝑁 ∖ {𝐾}) → (𝐸‘𝑖) = (𝑍‘𝑖))) |
13 | 12 | imp 410 |
. . . . . . . . 9
⊢ (((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) ∧ 𝑖 ∈ (𝑁 ∖ {𝐾})) → (𝐸‘𝑖) = (𝑍‘𝑖)) |
14 | 13 | eqeq2d 2749 |
. . . . . . . 8
⊢ (((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) ∧ 𝑖 ∈ (𝑁 ∖ {𝐾})) → (𝑘 = (𝐸‘𝑖) ↔ 𝑘 = (𝑍‘𝑖))) |
15 | 14 | rexbidva 3205 |
. . . . . . 7
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖) ↔ ∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝑍‘𝑖))) |
16 | 15 | ralbidv 3109 |
. . . . . 6
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖) ↔ ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝑍‘𝑖))) |
17 | 11, 16 | mpbird 260 |
. . . . 5
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖)) |
18 | | difssd 4021 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑁 ∖ {𝐾}) → (𝑁 ∖ {𝐾}) ⊆ 𝑁) |
19 | | ssrexv 3942 |
. . . . . . 7
⊢ ((𝑁 ∖ {𝐾}) ⊆ 𝑁 → (∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖) → ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖))) |
20 | 18, 19 | syl 17 |
. . . . . 6
⊢ (𝑘 ∈ (𝑁 ∖ {𝐾}) → (∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖) → ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖))) |
21 | 20 | ralimia 3073 |
. . . . 5
⊢
(∀𝑘 ∈
(𝑁 ∖ {𝐾})∃𝑖 ∈ (𝑁 ∖ {𝐾})𝑘 = (𝐸‘𝑖) → ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖)) |
22 | 17, 21 | syl 17 |
. . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖)) |
23 | | simpl 486 |
. . . . 5
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐾 ∈ 𝑁) |
24 | 1, 2 | symgextfve 18658 |
. . . . . . . 8
⊢ (𝐾 ∈ 𝑁 → (𝑖 = 𝐾 → (𝐸‘𝑖) = 𝐾)) |
25 | 24 | adantr 484 |
. . . . . . 7
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (𝑖 = 𝐾 → (𝐸‘𝑖) = 𝐾)) |
26 | 25 | imp 410 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) ∧ 𝑖 = 𝐾) → (𝐸‘𝑖) = 𝐾) |
27 | 26 | eqcomd 2744 |
. . . . 5
⊢ (((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) ∧ 𝑖 = 𝐾) → 𝐾 = (𝐸‘𝑖)) |
28 | 23, 27 | rspcedeq2vd 3531 |
. . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∃𝑖 ∈ 𝑁 𝐾 = (𝐸‘𝑖)) |
29 | | eqeq1 2742 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑘 = (𝐸‘𝑖) ↔ 𝐾 = (𝐸‘𝑖))) |
30 | 29 | rexbidv 3206 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ↔ ∃𝑖 ∈ 𝑁 𝐾 = (𝐸‘𝑖))) |
31 | 30 | ralunsn 4779 |
. . . . 5
⊢ (𝐾 ∈ 𝑁 → (∀𝑘 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ↔ (∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ∧ ∃𝑖 ∈ 𝑁 𝐾 = (𝐸‘𝑖)))) |
32 | 31 | adantr 484 |
. . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (∀𝑘 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ↔ (∀𝑘 ∈ (𝑁 ∖ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ∧ ∃𝑖 ∈ 𝑁 𝐾 = (𝐸‘𝑖)))) |
33 | 22, 28, 32 | mpbir2and 713 |
. . 3
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∀𝑘 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖)) |
34 | | difsnid 4695 |
. . . . . 6
⊢ (𝐾 ∈ 𝑁 → ((𝑁 ∖ {𝐾}) ∪ {𝐾}) = 𝑁) |
35 | 34 | eqcomd 2744 |
. . . . 5
⊢ (𝐾 ∈ 𝑁 → 𝑁 = ((𝑁 ∖ {𝐾}) ∪ {𝐾})) |
36 | 35 | raleqdv 3315 |
. . . 4
⊢ (𝐾 ∈ 𝑁 → (∀𝑘 ∈ 𝑁 ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ↔ ∀𝑘 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖))) |
37 | 36 | adantr 484 |
. . 3
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → (∀𝑘 ∈ 𝑁 ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖) ↔ ∀𝑘 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾})∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖))) |
38 | 33, 37 | mpbird 260 |
. 2
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ∀𝑘 ∈ 𝑁 ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖)) |
39 | | dffo3 6872 |
. 2
⊢ (𝐸:𝑁–onto→𝑁 ↔ (𝐸:𝑁⟶𝑁 ∧ ∀𝑘 ∈ 𝑁 ∃𝑖 ∈ 𝑁 𝑘 = (𝐸‘𝑖))) |
40 | 3, 38, 39 | sylanbrc 586 |
1
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁–onto→𝑁) |