Theorem symgextfo

Description: The extension of a permutation, fixing the additional element, is an onto function. (Contributed by AV, 7-Jan-2019)

	Ref	Expression
Hypotheses	symgext.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
	symgext.e	⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
Assertion	symgextfo	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 –onto→ 𝑁 )

Proof

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	rspcedeqvd	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ∃ 𝑖 ∈ 𝑁 𝐾 = ( 𝐸 ‘ 𝑖 ) )
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→ 𝑁 )