This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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