Metamath Proof Explorer


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 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𝑁 )