Metamath Proof Explorer


Theorem subfacp1lem3

Description: Lemma for subfacp1 . In subfacp1lem6 we cut up the set of all derangements on 1 ... ( N + 1 ) first according to the value at 1 , and then by whether or not ( f( f1 ) ) = 1 . In this lemma, we show that the subset of all N + 1 derangements that satisfy this for fixed M = ( f1 ) is in bijection with N - 1 derangements, by simply dropping the x = 1 and x = M points from the function to get a derangement on K = ( 1 ... ( N - 1 ) ) \ { 1 , M } . (Contributed by Mario Carneiro, 23-Jan-2015)

Ref Expression
Hypotheses derang.d 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥1-1-onto𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
subfac.n 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
subfacp1lem.a 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓𝑦 ) ≠ 𝑦 ) }
subfacp1lem1.n ( 𝜑𝑁 ∈ ℕ )
subfacp1lem1.m ( 𝜑𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
subfacp1lem1.x 𝑀 ∈ V
subfacp1lem1.k 𝐾 = ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } )
subfacp1lem3.b 𝐵 = { 𝑔𝐴 ∣ ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔𝑀 ) = 1 ) }
subfacp1lem3.c 𝐶 = { 𝑓 ∣ ( 𝑓 : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑓𝑦 ) ≠ 𝑦 ) }
Assertion subfacp1lem3 ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 derang.d 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥1-1-onto𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
2 subfac.n 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3 subfacp1lem.a 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓𝑦 ) ≠ 𝑦 ) }
4 subfacp1lem1.n ( 𝜑𝑁 ∈ ℕ )
5 subfacp1lem1.m ( 𝜑𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
6 subfacp1lem1.x 𝑀 ∈ V
7 subfacp1lem1.k 𝐾 = ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } )
8 subfacp1lem3.b 𝐵 = { 𝑔𝐴 ∣ ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔𝑀 ) = 1 ) }
9 subfacp1lem3.c 𝐶 = { 𝑓 ∣ ( 𝑓 : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑓𝑦 ) ≠ 𝑦 ) }
10 fzfi ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin
11 deranglem ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin → { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓𝑦 ) ≠ 𝑦 ) } ∈ Fin )
12 10 11 ax-mp { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓𝑦 ) ≠ 𝑦 ) } ∈ Fin
13 3 12 eqeltri 𝐴 ∈ Fin
14 8 ssrab3 𝐵𝐴
15 ssfi ( ( 𝐴 ∈ Fin ∧ 𝐵𝐴 ) → 𝐵 ∈ Fin )
16 13 14 15 mp2an 𝐵 ∈ Fin
17 16 elexi 𝐵 ∈ V
18 17 a1i ( 𝜑𝐵 ∈ V )
19 eqid ( 𝑏𝐵 ↦ ( 𝑏𝐾 ) ) = ( 𝑏𝐵 ↦ ( 𝑏𝐾 ) )
20 simpr ( ( 𝜑𝑏𝐵 ) → 𝑏𝐵 )
21 fveq1 ( 𝑔 = 𝑏 → ( 𝑔 ‘ 1 ) = ( 𝑏 ‘ 1 ) )
22 21 eqeq1d ( 𝑔 = 𝑏 → ( ( 𝑔 ‘ 1 ) = 𝑀 ↔ ( 𝑏 ‘ 1 ) = 𝑀 ) )
23 fveq1 ( 𝑔 = 𝑏 → ( 𝑔𝑀 ) = ( 𝑏𝑀 ) )
24 23 eqeq1d ( 𝑔 = 𝑏 → ( ( 𝑔𝑀 ) = 1 ↔ ( 𝑏𝑀 ) = 1 ) )
25 22 24 anbi12d ( 𝑔 = 𝑏 → ( ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔𝑀 ) = 1 ) ↔ ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏𝑀 ) = 1 ) ) )
26 25 8 elrab2 ( 𝑏𝐵 ↔ ( 𝑏𝐴 ∧ ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏𝑀 ) = 1 ) ) )
27 20 26 sylib ( ( 𝜑𝑏𝐵 ) → ( 𝑏𝐴 ∧ ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏𝑀 ) = 1 ) ) )
28 27 simpld ( ( 𝜑𝑏𝐵 ) → 𝑏𝐴 )
29 vex 𝑏 ∈ V
30 f1oeq1 ( 𝑓 = 𝑏 → ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
31 fveq1 ( 𝑓 = 𝑏 → ( 𝑓𝑦 ) = ( 𝑏𝑦 ) )
32 31 neeq1d ( 𝑓 = 𝑏 → ( ( 𝑓𝑦 ) ≠ 𝑦 ↔ ( 𝑏𝑦 ) ≠ 𝑦 ) )
33 32 ralbidv ( 𝑓 = 𝑏 → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) ≠ 𝑦 ) )
34 30 33 anbi12d ( 𝑓 = 𝑏 → ( ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓𝑦 ) ≠ 𝑦 ) ↔ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) ≠ 𝑦 ) ) )
35 29 34 3 elab2 ( 𝑏𝐴 ↔ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) ≠ 𝑦 ) )
36 28 35 sylib ( ( 𝜑𝑏𝐵 ) → ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) ≠ 𝑦 ) )
37 36 simpld ( ( 𝜑𝑏𝐵 ) → 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
38 f1of1 ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) )
39 df-f1 ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) ∧ Fun 𝑏 ) )
40 39 simprbi ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) → Fun 𝑏 )
41 37 38 40 3syl ( ( 𝜑𝑏𝐵 ) → Fun 𝑏 )
42 f1ofn ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) )
43 37 42 syl ( ( 𝜑𝑏𝐵 ) → 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) )
44 fnresdm ( 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) = 𝑏 )
45 f1oeq1 ( ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) = 𝑏 → ( ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
46 43 44 45 3syl ( ( 𝜑𝑏𝐵 ) → ( ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
47 37 46 mpbird ( ( 𝜑𝑏𝐵 ) → ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
48 f1ofo ( ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –onto→ ( 1 ... ( 𝑁 + 1 ) ) )
49 47 48 syl ( ( 𝜑𝑏𝐵 ) → ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –onto→ ( 1 ... ( 𝑁 + 1 ) ) )
50 ssun2 { 1 , 𝑀 } ⊆ ( 𝐾 ∪ { 1 , 𝑀 } )
51 1 2 3 4 5 6 7 subfacp1lem1 ( 𝜑 → ( ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ ∧ ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) ∧ ( ♯ ‘ 𝐾 ) = ( 𝑁 − 1 ) ) )
52 51 simp2d ( 𝜑 → ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) )
53 50 52 sseqtrid ( 𝜑 → { 1 , 𝑀 } ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
54 53 adantr ( ( 𝜑𝑏𝐵 ) → { 1 , 𝑀 } ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
55 43 54 fnssresd ( ( 𝜑𝑏𝐵 ) → ( 𝑏 ↾ { 1 , 𝑀 } ) Fn { 1 , 𝑀 } )
56 27 simprd ( ( 𝜑𝑏𝐵 ) → ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏𝑀 ) = 1 ) )
57 56 simpld ( ( 𝜑𝑏𝐵 ) → ( 𝑏 ‘ 1 ) = 𝑀 )
58 6 prid2 𝑀 ∈ { 1 , 𝑀 }
59 57 58 eqeltrdi ( ( 𝜑𝑏𝐵 ) → ( 𝑏 ‘ 1 ) ∈ { 1 , 𝑀 } )
60 56 simprd ( ( 𝜑𝑏𝐵 ) → ( 𝑏𝑀 ) = 1 )
61 1ex 1 ∈ V
62 61 prid1 1 ∈ { 1 , 𝑀 }
63 60 62 eqeltrdi ( ( 𝜑𝑏𝐵 ) → ( 𝑏𝑀 ) ∈ { 1 , 𝑀 } )
64 fveq2 ( 𝑥 = 1 → ( 𝑏𝑥 ) = ( 𝑏 ‘ 1 ) )
65 64 eleq1d ( 𝑥 = 1 → ( ( 𝑏𝑥 ) ∈ { 1 , 𝑀 } ↔ ( 𝑏 ‘ 1 ) ∈ { 1 , 𝑀 } ) )
66 fveq2 ( 𝑥 = 𝑀 → ( 𝑏𝑥 ) = ( 𝑏𝑀 ) )
67 66 eleq1d ( 𝑥 = 𝑀 → ( ( 𝑏𝑥 ) ∈ { 1 , 𝑀 } ↔ ( 𝑏𝑀 ) ∈ { 1 , 𝑀 } ) )
68 61 6 65 67 ralpr ( ∀ 𝑥 ∈ { 1 , 𝑀 } ( 𝑏𝑥 ) ∈ { 1 , 𝑀 } ↔ ( ( 𝑏 ‘ 1 ) ∈ { 1 , 𝑀 } ∧ ( 𝑏𝑀 ) ∈ { 1 , 𝑀 } ) )
69 59 63 68 sylanbrc ( ( 𝜑𝑏𝐵 ) → ∀ 𝑥 ∈ { 1 , 𝑀 } ( 𝑏𝑥 ) ∈ { 1 , 𝑀 } )
70 fvres ( 𝑥 ∈ { 1 , 𝑀 } → ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑥 ) = ( 𝑏𝑥 ) )
71 70 eleq1d ( 𝑥 ∈ { 1 , 𝑀 } → ( ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑥 ) ∈ { 1 , 𝑀 } ↔ ( 𝑏𝑥 ) ∈ { 1 , 𝑀 } ) )
72 71 ralbiia ( ∀ 𝑥 ∈ { 1 , 𝑀 } ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑥 ) ∈ { 1 , 𝑀 } ↔ ∀ 𝑥 ∈ { 1 , 𝑀 } ( 𝑏𝑥 ) ∈ { 1 , 𝑀 } )
73 69 72 sylibr ( ( 𝜑𝑏𝐵 ) → ∀ 𝑥 ∈ { 1 , 𝑀 } ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑥 ) ∈ { 1 , 𝑀 } )
74 ffnfv ( ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } ⟶ { 1 , 𝑀 } ↔ ( ( 𝑏 ↾ { 1 , 𝑀 } ) Fn { 1 , 𝑀 } ∧ ∀ 𝑥 ∈ { 1 , 𝑀 } ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑥 ) ∈ { 1 , 𝑀 } ) )
75 55 73 74 sylanbrc ( ( 𝜑𝑏𝐵 ) → ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } ⟶ { 1 , 𝑀 } )
76 fveqeq2 ( 𝑦 = 𝑀 → ( ( 𝑏𝑦 ) = 1 ↔ ( 𝑏𝑀 ) = 1 ) )
77 76 rspcev ( ( 𝑀 ∈ { 1 , 𝑀 } ∧ ( 𝑏𝑀 ) = 1 ) → ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 1 )
78 58 60 77 sylancr ( ( 𝜑𝑏𝐵 ) → ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 1 )
79 fveqeq2 ( 𝑦 = 1 → ( ( 𝑏𝑦 ) = 𝑀 ↔ ( 𝑏 ‘ 1 ) = 𝑀 ) )
80 79 rspcev ( ( 1 ∈ { 1 , 𝑀 } ∧ ( 𝑏 ‘ 1 ) = 𝑀 ) → ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 𝑀 )
81 62 57 80 sylancr ( ( 𝜑𝑏𝐵 ) → ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 𝑀 )
82 eqeq2 ( 𝑥 = 1 → ( ( 𝑏𝑦 ) = 𝑥 ↔ ( 𝑏𝑦 ) = 1 ) )
83 82 rexbidv ( 𝑥 = 1 → ( ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 𝑥 ↔ ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 1 ) )
84 eqeq2 ( 𝑥 = 𝑀 → ( ( 𝑏𝑦 ) = 𝑥 ↔ ( 𝑏𝑦 ) = 𝑀 ) )
85 84 rexbidv ( 𝑥 = 𝑀 → ( ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 𝑥 ↔ ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 𝑀 ) )
86 61 6 83 85 ralpr ( ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 𝑥 ↔ ( ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 1 ∧ ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 𝑀 ) )
87 78 81 86 sylanbrc ( ( 𝜑𝑏𝐵 ) → ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 𝑥 )
88 eqcom ( 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) ↔ ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) = 𝑥 )
89 fvres ( 𝑦 ∈ { 1 , 𝑀 } → ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) = ( 𝑏𝑦 ) )
90 89 eqeq1d ( 𝑦 ∈ { 1 , 𝑀 } → ( ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) = 𝑥 ↔ ( 𝑏𝑦 ) = 𝑥 ) )
91 88 90 syl5bb ( 𝑦 ∈ { 1 , 𝑀 } → ( 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) ↔ ( 𝑏𝑦 ) = 𝑥 ) )
92 91 rexbiia ( ∃ 𝑦 ∈ { 1 , 𝑀 } 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 𝑥 )
93 92 ralbii ( ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = 𝑥 )
94 87 93 sylibr ( ( 𝜑𝑏𝐵 ) → ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) )
95 dffo3 ( ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } –onto→ { 1 , 𝑀 } ↔ ( ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } ⟶ { 1 , 𝑀 } ∧ ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) ) )
96 75 94 95 sylanbrc ( ( 𝜑𝑏𝐵 ) → ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } –onto→ { 1 , 𝑀 } )
97 resdif ( ( Fun 𝑏 ∧ ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } –onto→ { 1 , 𝑀 } ) → ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) )
98 41 49 96 97 syl3anc ( ( 𝜑𝑏𝐵 ) → ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) )
99 uncom ( { 1 , 𝑀 } ∪ 𝐾 ) = ( 𝐾 ∪ { 1 , 𝑀 } )
100 99 52 eqtrid ( 𝜑 → ( { 1 , 𝑀 } ∪ 𝐾 ) = ( 1 ... ( 𝑁 + 1 ) ) )
101 incom ( { 1 , 𝑀 } ∩ 𝐾 ) = ( 𝐾 ∩ { 1 , 𝑀 } )
102 51 simp1d ( 𝜑 → ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ )
103 101 102 eqtrid ( 𝜑 → ( { 1 , 𝑀 } ∩ 𝐾 ) = ∅ )
104 uneqdifeq ( ( { 1 , 𝑀 } ⊆ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( { 1 , 𝑀 } ∩ 𝐾 ) = ∅ ) → ( ( { 1 , 𝑀 } ∪ 𝐾 ) = ( 1 ... ( 𝑁 + 1 ) ) ↔ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 ) )
105 53 103 104 syl2anc ( 𝜑 → ( ( { 1 , 𝑀 } ∪ 𝐾 ) = ( 1 ... ( 𝑁 + 1 ) ) ↔ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 ) )
106 100 105 mpbid ( 𝜑 → ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 )
107 106 adantr ( ( 𝜑𝑏𝐵 ) → ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 )
108 reseq2 ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 → ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) = ( 𝑏𝐾 ) )
109 108 f1oeq1d ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 → ( ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ↔ ( 𝑏𝐾 ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) )
110 f1oeq2 ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 → ( ( 𝑏𝐾 ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ↔ ( 𝑏𝐾 ) : 𝐾1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) )
111 f1oeq3 ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 → ( ( 𝑏𝐾 ) : 𝐾1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ↔ ( 𝑏𝐾 ) : 𝐾1-1-onto𝐾 ) )
112 109 110 111 3bitrd ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 → ( ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ↔ ( 𝑏𝐾 ) : 𝐾1-1-onto𝐾 ) )
113 107 112 syl ( ( 𝜑𝑏𝐵 ) → ( ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ↔ ( 𝑏𝐾 ) : 𝐾1-1-onto𝐾 ) )
114 98 113 mpbid ( ( 𝜑𝑏𝐵 ) → ( 𝑏𝐾 ) : 𝐾1-1-onto𝐾 )
115 ssun1 𝐾 ⊆ ( 𝐾 ∪ { 1 , 𝑀 } )
116 115 52 sseqtrid ( 𝜑𝐾 ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
117 116 adantr ( ( 𝜑𝑏𝐵 ) → 𝐾 ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
118 36 simprd ( ( 𝜑𝑏𝐵 ) → ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) ≠ 𝑦 )
119 ssralv ( 𝐾 ⊆ ( 1 ... ( 𝑁 + 1 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) ≠ 𝑦 → ∀ 𝑦𝐾 ( 𝑏𝑦 ) ≠ 𝑦 ) )
120 117 118 119 sylc ( ( 𝜑𝑏𝐵 ) → ∀ 𝑦𝐾 ( 𝑏𝑦 ) ≠ 𝑦 )
121 29 resex ( 𝑏𝐾 ) ∈ V
122 f1oeq1 ( 𝑓 = ( 𝑏𝐾 ) → ( 𝑓 : 𝐾1-1-onto𝐾 ↔ ( 𝑏𝐾 ) : 𝐾1-1-onto𝐾 ) )
123 fveq1 ( 𝑓 = ( 𝑏𝐾 ) → ( 𝑓𝑦 ) = ( ( 𝑏𝐾 ) ‘ 𝑦 ) )
124 fvres ( 𝑦𝐾 → ( ( 𝑏𝐾 ) ‘ 𝑦 ) = ( 𝑏𝑦 ) )
125 123 124 sylan9eq ( ( 𝑓 = ( 𝑏𝐾 ) ∧ 𝑦𝐾 ) → ( 𝑓𝑦 ) = ( 𝑏𝑦 ) )
126 125 neeq1d ( ( 𝑓 = ( 𝑏𝐾 ) ∧ 𝑦𝐾 ) → ( ( 𝑓𝑦 ) ≠ 𝑦 ↔ ( 𝑏𝑦 ) ≠ 𝑦 ) )
127 126 ralbidva ( 𝑓 = ( 𝑏𝐾 ) → ( ∀ 𝑦𝐾 ( 𝑓𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦𝐾 ( 𝑏𝑦 ) ≠ 𝑦 ) )
128 122 127 anbi12d ( 𝑓 = ( 𝑏𝐾 ) → ( ( 𝑓 : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑓𝑦 ) ≠ 𝑦 ) ↔ ( ( 𝑏𝐾 ) : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑏𝑦 ) ≠ 𝑦 ) ) )
129 121 128 9 elab2 ( ( 𝑏𝐾 ) ∈ 𝐶 ↔ ( ( 𝑏𝐾 ) : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑏𝑦 ) ≠ 𝑦 ) )
130 114 120 129 sylanbrc ( ( 𝜑𝑏𝐵 ) → ( 𝑏𝐾 ) ∈ 𝐶 )
131 4 adantr ( ( 𝜑𝑐𝐶 ) → 𝑁 ∈ ℕ )
132 5 adantr ( ( 𝜑𝑐𝐶 ) → 𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
133 eqid ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } )
134 simpr ( ( 𝜑𝑐𝐶 ) → 𝑐𝐶 )
135 vex 𝑐 ∈ V
136 f1oeq1 ( 𝑓 = 𝑐 → ( 𝑓 : 𝐾1-1-onto𝐾𝑐 : 𝐾1-1-onto𝐾 ) )
137 fveq1 ( 𝑓 = 𝑐 → ( 𝑓𝑦 ) = ( 𝑐𝑦 ) )
138 137 neeq1d ( 𝑓 = 𝑐 → ( ( 𝑓𝑦 ) ≠ 𝑦 ↔ ( 𝑐𝑦 ) ≠ 𝑦 ) )
139 138 ralbidv ( 𝑓 = 𝑐 → ( ∀ 𝑦𝐾 ( 𝑓𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦𝐾 ( 𝑐𝑦 ) ≠ 𝑦 ) )
140 136 139 anbi12d ( 𝑓 = 𝑐 → ( ( 𝑓 : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑓𝑦 ) ≠ 𝑦 ) ↔ ( 𝑐 : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑐𝑦 ) ≠ 𝑦 ) ) )
141 135 140 9 elab2 ( 𝑐𝐶 ↔ ( 𝑐 : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑐𝑦 ) ≠ 𝑦 ) )
142 134 141 sylib ( ( 𝜑𝑐𝐶 ) → ( 𝑐 : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑐𝑦 ) ≠ 𝑦 ) )
143 142 simpld ( ( 𝜑𝑐𝐶 ) → 𝑐 : 𝐾1-1-onto𝐾 )
144 1 2 3 131 132 6 7 133 143 subfacp1lem2a ( ( 𝜑𝑐𝐶 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 ) )
145 144 simp1d ( ( 𝜑𝑐𝐶 ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
146 1 2 3 131 132 6 7 133 143 subfacp1lem2b ( ( ( 𝜑𝑐𝐶 ) ∧ 𝑦𝐾 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) = ( 𝑐𝑦 ) )
147 142 simprd ( ( 𝜑𝑐𝐶 ) → ∀ 𝑦𝐾 ( 𝑐𝑦 ) ≠ 𝑦 )
148 147 r19.21bi ( ( ( 𝜑𝑐𝐶 ) ∧ 𝑦𝐾 ) → ( 𝑐𝑦 ) ≠ 𝑦 )
149 146 148 eqnetrd ( ( ( 𝜑𝑐𝐶 ) ∧ 𝑦𝐾 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 )
150 149 ralrimiva ( ( 𝜑𝑐𝐶 ) → ∀ 𝑦𝐾 ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 )
151 144 simp2d ( ( 𝜑𝑐𝐶 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 )
152 elfzuz ( 𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) → 𝑀 ∈ ( ℤ ‘ 2 ) )
153 eluz2b3 ( 𝑀 ∈ ( ℤ ‘ 2 ) ↔ ( 𝑀 ∈ ℕ ∧ 𝑀 ≠ 1 ) )
154 153 simprbi ( 𝑀 ∈ ( ℤ ‘ 2 ) → 𝑀 ≠ 1 )
155 5 152 154 3syl ( 𝜑𝑀 ≠ 1 )
156 155 adantr ( ( 𝜑𝑐𝐶 ) → 𝑀 ≠ 1 )
157 151 156 eqnetrd ( ( 𝜑𝑐𝐶 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) ≠ 1 )
158 144 simp3d ( ( 𝜑𝑐𝐶 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 )
159 156 necomd ( ( 𝜑𝑐𝐶 ) → 1 ≠ 𝑀 )
160 158 159 eqnetrd ( ( 𝜑𝑐𝐶 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) ≠ 𝑀 )
161 fveq2 ( 𝑦 = 1 → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) )
162 id ( 𝑦 = 1 → 𝑦 = 1 )
163 161 162 neeq12d ( 𝑦 = 1 → ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) ≠ 1 ) )
164 fveq2 ( 𝑦 = 𝑀 → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) )
165 id ( 𝑦 = 𝑀𝑦 = 𝑀 )
166 164 165 neeq12d ( 𝑦 = 𝑀 → ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) ≠ 𝑀 ) )
167 61 6 163 166 ralpr ( ∀ 𝑦 ∈ { 1 , 𝑀 } ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ↔ ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) ≠ 1 ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) ≠ 𝑀 ) )
168 157 160 167 sylanbrc ( ( 𝜑𝑐𝐶 ) → ∀ 𝑦 ∈ { 1 , 𝑀 } ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 )
169 ralunb ( ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ↔ ( ∀ 𝑦𝐾 ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ∧ ∀ 𝑦 ∈ { 1 , 𝑀 } ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) )
170 150 168 169 sylanbrc ( ( 𝜑𝑐𝐶 ) → ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 )
171 52 adantr ( ( 𝜑𝑐𝐶 ) → ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) )
172 171 raleqdv ( ( 𝜑𝑐𝐶 ) → ( ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) )
173 170 172 mpbid ( ( 𝜑𝑐𝐶 ) → ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 )
174 prex { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ∈ V
175 135 174 unex ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ V
176 f1oeq1 ( 𝑓 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
177 fveq1 ( 𝑓 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( 𝑓𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) )
178 177 neeq1d ( 𝑓 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ( 𝑓𝑦 ) ≠ 𝑦 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) )
179 178 ralbidv ( 𝑓 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) )
180 176 179 anbi12d ( 𝑓 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓𝑦 ) ≠ 𝑦 ) ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) ) )
181 175 180 3 elab2 ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ 𝐴 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) )
182 145 173 181 sylanbrc ( ( 𝜑𝑐𝐶 ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ 𝐴 )
183 151 158 jca ( ( 𝜑𝑐𝐶 ) → ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 ) )
184 fveq1 ( 𝑔 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( 𝑔 ‘ 1 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) )
185 184 eqeq1d ( 𝑔 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ( 𝑔 ‘ 1 ) = 𝑀 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 ) )
186 fveq1 ( 𝑔 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( 𝑔𝑀 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) )
187 186 eqeq1d ( 𝑔 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ( 𝑔𝑀 ) = 1 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 ) )
188 185 187 anbi12d ( 𝑔 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔𝑀 ) = 1 ) ↔ ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 ) ) )
189 188 8 elrab2 ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ 𝐵 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ 𝐴 ∧ ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 ) ) )
190 182 183 189 sylanbrc ( ( 𝜑𝑐𝐶 ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ 𝐵 )
191 57 adantrr ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝑏 ‘ 1 ) = 𝑀 )
192 151 adantrl ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 )
193 191 192 eqtr4d ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝑏 ‘ 1 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) )
194 60 adantrr ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝑏𝑀 ) = 1 )
195 158 adantrl ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 )
196 194 195 eqtr4d ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝑏𝑀 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) )
197 fveq2 ( 𝑦 = 1 → ( 𝑏𝑦 ) = ( 𝑏 ‘ 1 ) )
198 197 161 eqeq12d ( 𝑦 = 1 → ( ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( 𝑏 ‘ 1 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) ) )
199 fveq2 ( 𝑦 = 𝑀 → ( 𝑏𝑦 ) = ( 𝑏𝑀 ) )
200 199 164 eqeq12d ( 𝑦 = 𝑀 → ( ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( 𝑏𝑀 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) ) )
201 61 6 198 200 ralpr ( ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( ( 𝑏 ‘ 1 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) ∧ ( 𝑏𝑀 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) ) )
202 193 196 201 sylanbrc ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) )
203 202 biantrud ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( ∀ 𝑦𝐾 ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( ∀ 𝑦𝐾 ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) ) )
204 ralunb ( ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( ∀ 𝑦𝐾 ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) )
205 203 204 bitr4di ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( ∀ 𝑦𝐾 ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) )
206 146 eqeq2d ( ( ( 𝜑𝑐𝐶 ) ∧ 𝑦𝐾 ) → ( ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
207 206 ralbidva ( ( 𝜑𝑐𝐶 ) → ( ∀ 𝑦𝐾 ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦𝐾 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
208 207 adantrl ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( ∀ 𝑦𝐾 ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦𝐾 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
209 52 adantr ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) )
210 209 raleqdv ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) )
211 205 208 210 3bitr3rd ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦𝐾 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
212 124 eqeq2d ( 𝑦𝐾 → ( ( 𝑐𝑦 ) = ( ( 𝑏𝐾 ) ‘ 𝑦 ) ↔ ( 𝑐𝑦 ) = ( 𝑏𝑦 ) ) )
213 eqcom ( ( 𝑐𝑦 ) = ( 𝑏𝑦 ) ↔ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) )
214 212 213 bitrdi ( 𝑦𝐾 → ( ( 𝑐𝑦 ) = ( ( 𝑏𝐾 ) ‘ 𝑦 ) ↔ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
215 214 ralbiia ( ∀ 𝑦𝐾 ( 𝑐𝑦 ) = ( ( 𝑏𝐾 ) ‘ 𝑦 ) ↔ ∀ 𝑦𝐾 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) )
216 211 215 bitr4di ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦𝐾 ( 𝑐𝑦 ) = ( ( 𝑏𝐾 ) ‘ 𝑦 ) ) )
217 43 adantrr ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) )
218 145 adantrl ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
219 f1ofn ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) Fn ( 1 ... ( 𝑁 + 1 ) ) )
220 218 219 syl ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) Fn ( 1 ... ( 𝑁 + 1 ) ) )
221 eqfnfv ( ( 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) Fn ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑏 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) )
222 217 220 221 syl2anc ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝑏 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) )
223 143 adantrl ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → 𝑐 : 𝐾1-1-onto𝐾 )
224 f1ofn ( 𝑐 : 𝐾1-1-onto𝐾𝑐 Fn 𝐾 )
225 223 224 syl ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → 𝑐 Fn 𝐾 )
226 116 adantr ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → 𝐾 ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
227 217 226 fnssresd ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝑏𝐾 ) Fn 𝐾 )
228 eqfnfv ( ( 𝑐 Fn 𝐾 ∧ ( 𝑏𝐾 ) Fn 𝐾 ) → ( 𝑐 = ( 𝑏𝐾 ) ↔ ∀ 𝑦𝐾 ( 𝑐𝑦 ) = ( ( 𝑏𝐾 ) ‘ 𝑦 ) ) )
229 225 227 228 syl2anc ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝑐 = ( 𝑏𝐾 ) ↔ ∀ 𝑦𝐾 ( 𝑐𝑦 ) = ( ( 𝑏𝐾 ) ‘ 𝑦 ) ) )
230 216 222 229 3bitr4d ( ( 𝜑 ∧ ( 𝑏𝐵𝑐𝐶 ) ) → ( 𝑏 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ↔ 𝑐 = ( 𝑏𝐾 ) ) )
231 19 130 190 230 f1o2d ( 𝜑 → ( 𝑏𝐵 ↦ ( 𝑏𝐾 ) ) : 𝐵1-1-onto𝐶 )
232 18 231 hasheqf1od ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐶 ) )
233 9 fveq2i ( ♯ ‘ 𝐶 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑓𝑦 ) ≠ 𝑦 ) } )
234 fzfi ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin
235 diffi ( ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin → ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∈ Fin )
236 234 235 ax-mp ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∈ Fin
237 7 236 eqeltri 𝐾 ∈ Fin
238 1 derangval ( 𝐾 ∈ Fin → ( 𝐷𝐾 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
239 237 238 ax-mp ( 𝐷𝐾 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝐾1-1-onto𝐾 ∧ ∀ 𝑦𝐾 ( 𝑓𝑦 ) ≠ 𝑦 ) } )
240 1 2 derangen2 ( 𝐾 ∈ Fin → ( 𝐷𝐾 ) = ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) ) )
241 237 240 ax-mp ( 𝐷𝐾 ) = ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) )
242 233 239 241 3eqtr2ri ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) ) = ( ♯ ‘ 𝐶 )
243 51 simp3d ( 𝜑 → ( ♯ ‘ 𝐾 ) = ( 𝑁 − 1 ) )
244 243 fveq2d ( 𝜑 → ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) )
245 242 244 eqtr3id ( 𝜑 → ( ♯ ‘ 𝐶 ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) )
246 232 245 eqtrd ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) )