Metamath Proof Explorer

Theorem symgfixf1

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a 1-1 function. (Contributed by AV, 4-Jan-2019)

Ref Expression
Hypotheses symgfixf.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
symgfixf.q ⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
symgfixf.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
symgfixf.h ⊢ 𝐻 = ( 𝑞 ∈ 𝑄 ↦ ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
Assertion symgfixf1 ( 𝐾 ∈ 𝑁 → 𝐻 : 𝑄 –1-1→ 𝑆 )

Proof

Step Hyp Ref Expression
1 symgfixf.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 symgfixf.q ⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
3 symgfixf.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
4 symgfixf.h ⊢ 𝐻 = ( 𝑞 ∈ 𝑄 ↦ ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
5 1 2 3 4 symgfixf ⊢ ( 𝐾 ∈ 𝑁 → 𝐻 : 𝑄 ⟶ 𝑆 )
6 4 fvtresfn ⊢ ( 𝑔 ∈ 𝑄 → ( 𝐻 ‘ 𝑔 ) = ( 𝑔 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
7 4 fvtresfn ⊢ ( 𝑝 ∈ 𝑄 → ( 𝐻 ‘ 𝑝 ) = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
8 6 7 eqeqan12d ⊢ ( ( 𝑔 ∈ 𝑄 ∧ 𝑝 ∈ 𝑄 ) → ( ( 𝐻 ‘ 𝑔 ) = ( 𝐻 ‘ 𝑝 ) ↔ ( 𝑔 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
9 8 adantl ⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝑔 ∈ 𝑄 ∧ 𝑝 ∈ 𝑄 ) ) → ( ( 𝐻 ‘ 𝑔 ) = ( 𝐻 ‘ 𝑝 ) ↔ ( 𝑔 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
10 1 2 symgfixelq ⊢ ( 𝑔 ∈ V → ( 𝑔 ∈ 𝑄 ↔ ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ) )
11 10 elv ⊢ ( 𝑔 ∈ 𝑄 ↔ ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) )
12 1 2 symgfixelq ⊢ ( 𝑝 ∈ V → ( 𝑝 ∈ 𝑄 ↔ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) )
13 12 elv ⊢ ( 𝑝 ∈ 𝑄 ↔ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) )
14 11 13 anbi12i ⊢ ( ( 𝑔 ∈ 𝑄 ∧ 𝑝 ∈ 𝑄 ) ↔ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) )
15 f1ofn ⊢ ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 → 𝑔 Fn 𝑁 )
16 15 adantr ⊢ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) → 𝑔 Fn 𝑁 )
17 f1ofn ⊢ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 → 𝑝 Fn 𝑁 )
18 17 adantr ⊢ ( ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) → 𝑝 Fn 𝑁 )
19 16 18 anim12i ⊢ ( ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) → ( 𝑔 Fn 𝑁 ∧ 𝑝 Fn 𝑁 ) )
20 difss ⊢ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁
21 19 20 jctir ⊢ ( ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑔 Fn 𝑁 ∧ 𝑝 Fn 𝑁 ) ∧ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) )
22 21 adantl ⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) → ( ( 𝑔 Fn 𝑁 ∧ 𝑝 Fn 𝑁 ) ∧ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) )
23 fvreseq ⊢ ( ( ( 𝑔 Fn 𝑁 ∧ 𝑝 Fn 𝑁 ) ∧ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) → ( ( 𝑔 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ↔ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) )
24 22 23 syl ⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) → ( ( 𝑔 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ↔ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) )
25 f1of ⊢ ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 → 𝑔 : 𝑁 ⟶ 𝑁 )
26 25 adantr ⊢ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) → 𝑔 : 𝑁 ⟶ 𝑁 )
27 f1of ⊢ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 → 𝑝 : 𝑁 ⟶ 𝑁 )
28 27 adantr ⊢ ( ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) → 𝑝 : 𝑁 ⟶ 𝑁 )
29 fdm ⊢ ( 𝑔 : 𝑁 ⟶ 𝑁 → dom 𝑔 = 𝑁 )
30 fdm ⊢ ( 𝑝 : 𝑁 ⟶ 𝑁 → dom 𝑝 = 𝑁 )
31 29 30 anim12i ⊢ ( ( 𝑔 : 𝑁 ⟶ 𝑁 ∧ 𝑝 : 𝑁 ⟶ 𝑁 ) → ( dom 𝑔 = 𝑁 ∧ dom 𝑝 = 𝑁 ) )
32 26 28 31 syl2an ⊢ ( ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) → ( dom 𝑔 = 𝑁 ∧ dom 𝑝 = 𝑁 ) )
33 eqtr3 ⊢ ( ( dom 𝑔 = 𝑁 ∧ dom 𝑝 = 𝑁 ) → dom 𝑔 = dom 𝑝 )
34 32 33 syl ⊢ ( ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) → dom 𝑔 = dom 𝑝 )
35 34 ad2antlr ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → dom 𝑔 = dom 𝑝 )
36 simpr ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) )
37 eqtr3 ⊢ ( ( ( 𝑔 ‘ 𝐾 ) = 𝐾 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) → ( 𝑔 ‘ 𝐾 ) = ( 𝑝 ‘ 𝐾 ) )
38 37 ad2ant2l ⊢ ( ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) → ( 𝑔 ‘ 𝐾 ) = ( 𝑝 ‘ 𝐾 ) )
39 38 ad2antlr ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → ( 𝑔 ‘ 𝐾 ) = ( 𝑝 ‘ 𝐾 ) )
40 fveq2 ⊢ ( 𝑖 = 𝐾 → ( 𝑔 ‘ 𝑖 ) = ( 𝑔 ‘ 𝐾 ) )
41 fveq2 ⊢ ( 𝑖 = 𝐾 → ( 𝑝 ‘ 𝑖 ) = ( 𝑝 ‘ 𝐾 ) )
42 40 41 eqeq12d ⊢ ( 𝑖 = 𝐾 → ( ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ↔ ( 𝑔 ‘ 𝐾 ) = ( 𝑝 ‘ 𝐾 ) ) )
43 42 ralunsn ⊢ ( 𝐾 ∈ 𝑁 → ( ∀ 𝑖 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ↔ ( ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ∧ ( 𝑔 ‘ 𝐾 ) = ( 𝑝 ‘ 𝐾 ) ) ) )
44 43 adantr ⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) → ( ∀ 𝑖 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ↔ ( ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ∧ ( 𝑔 ‘ 𝐾 ) = ( 𝑝 ‘ 𝐾 ) ) ) )
45 44 adantr ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → ( ∀ 𝑖 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ↔ ( ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ∧ ( 𝑔 ‘ 𝐾 ) = ( 𝑝 ‘ 𝐾 ) ) ) )
46 36 39 45 mpbir2and ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → ∀ 𝑖 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) )
47 f1odm ⊢ ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 → dom 𝑔 = 𝑁 )
48 47 adantr ⊢ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) → dom 𝑔 = 𝑁 )
49 48 adantr ⊢ ( ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) → dom 𝑔 = 𝑁 )
50 difsnid ⊢ ( 𝐾 ∈ 𝑁 → ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = 𝑁 )
51 50 eqcomd ⊢ ( 𝐾 ∈ 𝑁 → 𝑁 = ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
52 49 51 sylan9eqr ⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) → dom 𝑔 = ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
53 52 adantr ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → dom 𝑔 = ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
54 53 raleqdv ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → ( ∀ 𝑖 ∈ dom 𝑔 ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) )
55 46 54 mpbird ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → ∀ 𝑖 ∈ dom 𝑔 ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) )
56 f1ofun ⊢ ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 → Fun 𝑔 )
57 56 adantr ⊢ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) → Fun 𝑔 )
58 f1ofun ⊢ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 → Fun 𝑝 )
59 58 adantr ⊢ ( ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) → Fun 𝑝 )
60 57 59 anim12i ⊢ ( ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) → ( Fun 𝑔 ∧ Fun 𝑝 ) )
61 60 ad2antlr ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → ( Fun 𝑔 ∧ Fun 𝑝 ) )
62 eqfunfv ⊢ ( ( Fun 𝑔 ∧ Fun 𝑝 ) → ( 𝑔 = 𝑝 ↔ ( dom 𝑔 = dom 𝑝 ∧ ∀ 𝑖 ∈ dom 𝑔 ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) ) )
63 61 62 syl ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → ( 𝑔 = 𝑝 ↔ ( dom 𝑔 = dom 𝑝 ∧ ∀ 𝑖 ∈ dom 𝑔 ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) ) )
64 35 55 63 mpbir2and ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) ) → 𝑔 = 𝑝 )
65 64 ex ⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) → ( ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑔 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) → 𝑔 = 𝑝 ) )
66 24 65 sylbid ⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( ( 𝑔 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑔 ‘ 𝐾 ) = 𝐾 ) ∧ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) ) ) → ( ( 𝑔 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) → 𝑔 = 𝑝 ) )
67 14 66 sylan2b ⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝑔 ∈ 𝑄 ∧ 𝑝 ∈ 𝑄 ) ) → ( ( 𝑔 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) → 𝑔 = 𝑝 ) )
68 9 67 sylbid ⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝑔 ∈ 𝑄 ∧ 𝑝 ∈ 𝑄 ) ) → ( ( 𝐻 ‘ 𝑔 ) = ( 𝐻 ‘ 𝑝 ) → 𝑔 = 𝑝 ) )
69 68 ralrimivva ⊢ ( 𝐾 ∈ 𝑁 → ∀ 𝑔 ∈ 𝑄 ∀ 𝑝 ∈ 𝑄 ( ( 𝐻 ‘ 𝑔 ) = ( 𝐻 ‘ 𝑝 ) → 𝑔 = 𝑝 ) )
70 dff13 ⊢ ( 𝐻 : 𝑄 –1-1→ 𝑆 ↔ ( 𝐻 : 𝑄 ⟶ 𝑆 ∧ ∀ 𝑔 ∈ 𝑄 ∀ 𝑝 ∈ 𝑄 ( ( 𝐻 ‘ 𝑔 ) = ( 𝐻 ‘ 𝑝 ) → 𝑔 = 𝑝 ) ) )
71 5 69 70 sylanbrc ⊢ ( 𝐾 ∈ 𝑁 → 𝐻 : 𝑄 –1-1→ 𝑆 )