Step |
Hyp |
Ref |
Expression |
1 |
|
symgext.s |
⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) |
2 |
|
symgext.e |
⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) ) |
3 |
1 2
|
symgextf |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 ⟶ 𝑁 ) |
4 |
|
eqid |
⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) |
5 |
4 1
|
symgbasf1o |
⊢ ( 𝑍 ∈ 𝑆 → 𝑍 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) ) |
6 |
|
f1ofo |
⊢ ( 𝑍 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) → 𝑍 : ( 𝑁 ∖ { 𝐾 } ) –onto→ ( 𝑁 ∖ { 𝐾 } ) ) |
7 |
5 6
|
syl |
⊢ ( 𝑍 ∈ 𝑆 → 𝑍 : ( 𝑁 ∖ { 𝐾 } ) –onto→ ( 𝑁 ∖ { 𝐾 } ) ) |
8 |
7
|
adantl |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝑍 : ( 𝑁 ∖ { 𝐾 } ) –onto→ ( 𝑁 ∖ { 𝐾 } ) ) |
9 |
|
dffo3 |
⊢ ( 𝑍 : ( 𝑁 ∖ { 𝐾 } ) –onto→ ( 𝑁 ∖ { 𝐾 } ) ↔ ( 𝑍 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) ∧ ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝑍 ‘ 𝑖 ) ) ) |
10 |
8 9
|
sylib |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑍 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) ∧ ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝑍 ‘ 𝑖 ) ) ) |
11 |
10
|
simprd |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝑍 ‘ 𝑖 ) ) |
12 |
1 2
|
symgextfv |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐸 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) ) |
13 |
12
|
imp |
⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝐸 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) |
14 |
13
|
eqeq2d |
⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑘 = ( 𝐸 ‘ 𝑖 ) ↔ 𝑘 = ( 𝑍 ‘ 𝑖 ) ) ) |
15 |
14
|
rexbidva |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝐸 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝑍 ‘ 𝑖 ) ) ) |
16 |
15
|
ralbidv |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝐸 ‘ 𝑖 ) ↔ ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝑍 ‘ 𝑖 ) ) ) |
17 |
11 16
|
mpbird |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝐸 ‘ 𝑖 ) ) |
18 |
|
difssd |
⊢ ( 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) |
19 |
|
ssrexv |
⊢ ( ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 → ( ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝐸 ‘ 𝑖 ) → ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ) ) |
20 |
18 19
|
syl |
⊢ ( 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝐸 ‘ 𝑖 ) → ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ) ) |
21 |
20
|
ralimia |
⊢ ( ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) 𝑘 = ( 𝐸 ‘ 𝑖 ) → ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ) |
22 |
17 21
|
syl |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ) |
23 |
|
simpl |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐾 ∈ 𝑁 ) |
24 |
1 2
|
symgextfve |
⊢ ( 𝐾 ∈ 𝑁 → ( 𝑖 = 𝐾 → ( 𝐸 ‘ 𝑖 ) = 𝐾 ) ) |
25 |
24
|
adantr |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑖 = 𝐾 → ( 𝐸 ‘ 𝑖 ) = 𝐾 ) ) |
26 |
25
|
imp |
⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑖 = 𝐾 ) → ( 𝐸 ‘ 𝑖 ) = 𝐾 ) |
27 |
26
|
eqcomd |
⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑖 = 𝐾 ) → 𝐾 = ( 𝐸 ‘ 𝑖 ) ) |
28 |
23 27
|
rspcedeq2vd |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ∃ 𝑖 ∈ 𝑁 𝐾 = ( 𝐸 ‘ 𝑖 ) ) |
29 |
|
eqeq1 |
⊢ ( 𝑘 = 𝐾 → ( 𝑘 = ( 𝐸 ‘ 𝑖 ) ↔ 𝐾 = ( 𝐸 ‘ 𝑖 ) ) ) |
30 |
29
|
rexbidv |
⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ 𝑁 𝐾 = ( 𝐸 ‘ 𝑖 ) ) ) |
31 |
30
|
ralunsn |
⊢ ( 𝐾 ∈ 𝑁 → ( ∀ 𝑘 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ↔ ( ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ∧ ∃ 𝑖 ∈ 𝑁 𝐾 = ( 𝐸 ‘ 𝑖 ) ) ) ) |
32 |
31
|
adantr |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( ∀ 𝑘 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ↔ ( ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ∧ ∃ 𝑖 ∈ 𝑁 𝐾 = ( 𝐸 ‘ 𝑖 ) ) ) ) |
33 |
22 28 32
|
mpbir2and |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ∀ 𝑘 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ) |
34 |
|
difsnid |
⊢ ( 𝐾 ∈ 𝑁 → ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = 𝑁 ) |
35 |
34
|
eqcomd |
⊢ ( 𝐾 ∈ 𝑁 → 𝑁 = ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) |
36 |
35
|
raleqdv |
⊢ ( 𝐾 ∈ 𝑁 → ( ∀ 𝑘 ∈ 𝑁 ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ↔ ∀ 𝑘 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ) ) |
37 |
36
|
adantr |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( ∀ 𝑘 ∈ 𝑁 ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ↔ ∀ 𝑘 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ) ) |
38 |
33 37
|
mpbird |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ∀ 𝑘 ∈ 𝑁 ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ) |
39 |
|
dffo3 |
⊢ ( 𝐸 : 𝑁 –onto→ 𝑁 ↔ ( 𝐸 : 𝑁 ⟶ 𝑁 ∧ ∀ 𝑘 ∈ 𝑁 ∃ 𝑖 ∈ 𝑁 𝑘 = ( 𝐸 ‘ 𝑖 ) ) ) |
40 |
3 38 39
|
sylanbrc |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 –onto→ 𝑁 ) |