Metamath Proof Explorer

Theorem subfacp1lem5

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 with ( f( f1 ) ) =/= 1 for fixed M = ( f1 ) is in bijection with derangements of 2 ... ( N + 1 ) , because pre-composing with the function F swaps 1 and M and turns the function into a bijection with ( f1 ) = 1 and ( fx ) =/= x for all other x , so dropping the point at 1 yields a derangement on the N remaining points. (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 ) ) ∖ { 𝑀 } )
subfacp1lem5.b ⊢ 𝐵 = { 𝑔 ∈ 𝐴 ∣ ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔 ‘ 𝑀 ) ≠ 1 ) }
subfacp1lem5.f ⊢ 𝐹 = ( ( I ↾ 𝐾 ) ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } )
subfacp1lem5.c ⊢ 𝐶 = { 𝑓 ∣ ( 𝑓 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) }
Assertion subfacp1lem5 ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑆 ‘ 𝑁 ) )

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 subfacp1lem5.b ⊢ 𝐵 = { 𝑔 ∈ 𝐴 ∣ ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔 ‘ 𝑀 ) ≠ 1 ) }
9 subfacp1lem5.f ⊢ 𝐹 = ( ( I ↾ 𝐾 ) ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } )
10 subfacp1lem5.c ⊢ 𝐶 = { 𝑓 ∣ ( 𝑓 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) }
11 fzfi ⊢ ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin
12 deranglem ⊢ ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin → { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ∈ Fin )
13 11 12 ax-mp ⊢ { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ∈ Fin
14 3 13 eqeltri ⊢ 𝐴 ∈ Fin
15 8 ssrab3 ⊢ 𝐵 ⊆ 𝐴
16 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )
17 14 15 16 mp2an ⊢ 𝐵 ∈ Fin
18 17 elexi ⊢ 𝐵 ∈ V
19 18 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
20 eqid ⊢ ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ) = ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) )
21 f1oi ⊢ ( I ↾ 𝐾 ) : 𝐾 –1-1-onto→ 𝐾
22 21 a1i ⊢ ( 𝜑 → ( I ↾ 𝐾 ) : 𝐾 –1-1-onto→ 𝐾 )
23 1 2 3 4 5 6 7 9 22 subfacp1lem2a ⊢ ( 𝜑 → ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝐹 ‘ 1 ) = 𝑀 ∧ ( 𝐹 ‘ 𝑀 ) = 1 ) )
24 23 simp1d ⊢ ( 𝜑 → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
26 fveq1 ⊢ ( 𝑔 = 𝑏 → ( 𝑔 ‘ 1 ) = ( 𝑏 ‘ 1 ) )
27 26 eqeq1d ⊢ ( 𝑔 = 𝑏 → ( ( 𝑔 ‘ 1 ) = 𝑀 ↔ ( 𝑏 ‘ 1 ) = 𝑀 ) )
28 fveq1 ⊢ ( 𝑔 = 𝑏 → ( 𝑔 ‘ 𝑀 ) = ( 𝑏 ‘ 𝑀 ) )
29 28 neeq1d ⊢ ( 𝑔 = 𝑏 → ( ( 𝑔 ‘ 𝑀 ) ≠ 1 ↔ ( 𝑏 ‘ 𝑀 ) ≠ 1 ) )
30 27 29 anbi12d ⊢ ( 𝑔 = 𝑏 → ( ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔 ‘ 𝑀 ) ≠ 1 ) ↔ ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏 ‘ 𝑀 ) ≠ 1 ) ) )
31 30 8 elrab2 ⊢ ( 𝑏 ∈ 𝐵 ↔ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏 ‘ 𝑀 ) ≠ 1 ) ) )
32 25 31 sylib ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏 ‘ 𝑀 ) ≠ 1 ) ) )
33 32 simpld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐴 )
34 vex ⊢ 𝑏 ∈ V
35 f1oeq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
36 fveq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) )
37 36 neeq1d ⊢ ( 𝑓 = 𝑏 → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
38 37 ralbidv ⊢ ( 𝑓 = 𝑏 → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
39 35 38 anbi12d ⊢ ( 𝑓 = 𝑏 → ( ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ↔ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) ) )
40 34 39 3 elab2 ⊢ ( 𝑏 ∈ 𝐴 ↔ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
41 33 40 sylib ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
42 41 simpld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
43 f1oco ⊢ ( ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
44 24 42 43 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
45 f1of1 ⊢ ( ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) )
46 df-f1 ⊢ ( ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) ∧ Fun ◡ ( 𝐹 ∘ 𝑏 ) ) )
47 46 simprbi ⊢ ( ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) → Fun ◡ ( 𝐹 ∘ 𝑏 ) )
48 44 45 47 3syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Fun ◡ ( 𝐹 ∘ 𝑏 ) )
49 f1ofn ⊢ ( ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝐹 ∘ 𝑏 ) Fn ( 1 ... ( 𝑁 + 1 ) ) )
50 fnresdm ⊢ ( ( 𝐹 ∘ 𝑏 ) Fn ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝐹 ∘ 𝑏 ) ↾ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝐹 ∘ 𝑏 ) )
51 f1oeq1 ⊢ ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝐹 ∘ 𝑏 ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
52 44 49 50 51 4syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
53 44 52 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
54 f1ofo ⊢ ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝐹 ∘ 𝑏 ) ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –onto→ ( 1 ... ( 𝑁 + 1 ) ) )
55 53 54 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –onto→ ( 1 ... ( 𝑁 + 1 ) ) )
56 1ex ⊢ 1 ∈ V
57 56 56 f1osn ⊢ { ⟨ 1 , 1 ⟩ } : { 1 } –1-1-onto→ { 1 }
58 44 49 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ∘ 𝑏 ) Fn ( 1 ... ( 𝑁 + 1 ) ) )
59 4 peano2nnd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
60 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
61 59 60 eleqtrdi ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
62 eluzfz1 ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
63 61 62 syl ⊢ ( 𝜑 → 1 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 1 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
65 fnressn ⊢ ( ( ( 𝐹 ∘ 𝑏 ) Fn ( 1 ... ( 𝑁 + 1 ) ) ∧ 1 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ∘ 𝑏 ) ↾ { 1 } ) = { ⟨ 1 , ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) ⟩ } )
66 58 64 65 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ↾ { 1 } ) = { ⟨ 1 , ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) ⟩ } )
67 f1of ⊢ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
68 42 67 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
69 68 64 fvco3d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) = ( 𝐹 ‘ ( 𝑏 ‘ 1 ) ) )
70 32 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏 ‘ 𝑀 ) ≠ 1 ) )
71 70 simpld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 1 ) = 𝑀 )
72 71 fveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑏 ‘ 1 ) ) = ( 𝐹 ‘ 𝑀 ) )
73 23 simp3d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = 1 )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑀 ) = 1 )
75 69 72 74 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) = 1 )
76 75 opeq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ⟨ 1 , ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) ⟩ = ⟨ 1 , 1 ⟩ )
77 76 sneqd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → { ⟨ 1 , ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) ⟩ } = { ⟨ 1 , 1 ⟩ } )
78 66 77 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ↾ { 1 } ) = { ⟨ 1 , 1 ⟩ } )
79 f1oeq1 ⊢ ( ( ( 𝐹 ∘ 𝑏 ) ↾ { 1 } ) = { ⟨ 1 , 1 ⟩ } → ( ( ( 𝐹 ∘ 𝑏 ) ↾ { 1 } ) : { 1 } –1-1-onto→ { 1 } ↔ { ⟨ 1 , 1 ⟩ } : { 1 } –1-1-onto→ { 1 } ) )
80 78 79 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ { 1 } ) : { 1 } –1-1-onto→ { 1 } ↔ { ⟨ 1 , 1 ⟩ } : { 1 } –1-1-onto→ { 1 } ) )
81 57 80 mpbiri ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ↾ { 1 } ) : { 1 } –1-1-onto→ { 1 } )
82 f1ofo ⊢ ( ( ( 𝐹 ∘ 𝑏 ) ↾ { 1 } ) : { 1 } –1-1-onto→ { 1 } → ( ( 𝐹 ∘ 𝑏 ) ↾ { 1 } ) : { 1 } –onto→ { 1 } )
83 81 82 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ↾ { 1 } ) : { 1 } –onto→ { 1 } )
84 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 } ) )
85 48 55 83 84 syl3anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) )
86 fzsplit ⊢ ( 1 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( 1 ... ( 𝑁 + 1 ) ) = ( ( 1 ... 1 ) ∪ ( ( 1 + 1 ) ... ( 𝑁 + 1 ) ) ) )
87 63 86 syl ⊢ ( 𝜑 → ( 1 ... ( 𝑁 + 1 ) ) = ( ( 1 ... 1 ) ∪ ( ( 1 + 1 ) ... ( 𝑁 + 1 ) ) ) )
88 1z ⊢ 1 ∈ ℤ
89 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
90 88 89 ax-mp ⊢ ( 1 ... 1 ) = { 1 }
91 1p1e2 ⊢ ( 1 + 1 ) = 2
92 91 oveq1i ⊢ ( ( 1 + 1 ) ... ( 𝑁 + 1 ) ) = ( 2 ... ( 𝑁 + 1 ) )
93 90 92 uneq12i ⊢ ( ( 1 ... 1 ) ∪ ( ( 1 + 1 ) ... ( 𝑁 + 1 ) ) ) = ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) )
94 87 93 eqtr2di ⊢ ( 𝜑 → ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
95 63 snssd ⊢ ( 𝜑 → { 1 } ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
96 incom ⊢ ( { 1 } ∩ ( 2 ... ( 𝑁 + 1 ) ) ) = ( ( 2 ... ( 𝑁 + 1 ) ) ∩ { 1 } )
97 1lt2 ⊢ 1 < 2
98 1re ⊢ 1 ∈ ℝ
99 2re ⊢ 2 ∈ ℝ
100 98 99 ltnlei ⊢ ( 1 < 2 ↔ ¬ 2 ≤ 1 )
101 97 100 mpbi ⊢ ¬ 2 ≤ 1
102 elfzle1 ⊢ ( 1 ∈ ( 2 ... ( 𝑁 + 1 ) ) → 2 ≤ 1 )
103 101 102 mto ⊢ ¬ 1 ∈ ( 2 ... ( 𝑁 + 1 ) )
104 disjsn ⊢ ( ( ( 2 ... ( 𝑁 + 1 ) ) ∩ { 1 } ) = ∅ ↔ ¬ 1 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
105 103 104 mpbir ⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∩ { 1 } ) = ∅
106 96 105 eqtri ⊢ ( { 1 } ∩ ( 2 ... ( 𝑁 + 1 ) ) ) = ∅
107 uneqdifeq ⊢ ( ( { 1 } ⊆ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( { 1 } ∩ ( 2 ... ( 𝑁 + 1 ) ) ) = ∅ ) → ( ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) = ( 1 ... ( 𝑁 + 1 ) ) ↔ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) = ( 2 ... ( 𝑁 + 1 ) ) ) )
108 95 106 107 sylancl ⊢ ( 𝜑 → ( ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) = ( 1 ... ( 𝑁 + 1 ) ) ↔ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) = ( 2 ... ( 𝑁 + 1 ) ) ) )
109 94 108 mpbid ⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) = ( 2 ... ( 𝑁 + 1 ) ) )
110 109 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) = ( 2 ... ( 𝑁 + 1 ) ) )
111 reseq2 ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) = ( 2 ... ( 𝑁 + 1 ) ) → ( ( 𝐹 ∘ 𝑏 ) ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ) = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) )
112 f1oeq1 ⊢ ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ) = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ↔ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ) )
113 111 112 syl ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) = ( 2 ... ( 𝑁 + 1 ) ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ↔ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ) )
114 f1oeq2 ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) = ( 2 ... ( 𝑁 + 1 ) ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ↔ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ) )
115 f1oeq3 ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) = ( 2 ... ( 𝑁 + 1 ) ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ↔ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ) )
116 113 114 115 3bitrd ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) = ( 2 ... ( 𝑁 + 1 ) ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ↔ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ) )
117 110 116 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 } ) ↔ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ) )
118 85 117 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) )
119 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
120 fzp1ss ⊢ ( 1 ∈ ℤ → ( ( 1 + 1 ) ... ( 𝑁 + 1 ) ) ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
121 88 120 ax-mp ⊢ ( ( 1 + 1 ) ... ( 𝑁 + 1 ) ) ⊆ ( 1 ... ( 𝑁 + 1 ) )
122 92 121 eqsstrri ⊢ ( 2 ... ( 𝑁 + 1 ) ) ⊆ ( 1 ... ( 𝑁 + 1 ) )
123 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
124 122 123 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
125 119 124 fvco3d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑏 ‘ 𝑦 ) ) )
126 1 2 3 4 5 6 7 8 9 subfacp1lem4 ⊢ ( 𝜑 → ◡ 𝐹 = 𝐹 )
127 126 fveq1d ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
128 127 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ◡ 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
129 70 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝑀 ) ≠ 1 )
130 129 74 neeqtrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝑀 ) ≠ ( 𝐹 ‘ 𝑀 ) )
131 130 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑏 ‘ 𝑀 ) ≠ ( 𝐹 ‘ 𝑀 ) )
132 fveq2 ⊢ ( 𝑦 = 𝑀 → ( 𝑏 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑀 ) )
133 fveq2 ⊢ ( 𝑦 = 𝑀 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑀 ) )
134 132 133 neeq12d ⊢ ( 𝑦 = 𝑀 → ( ( 𝑏 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑀 ) ≠ ( 𝐹 ‘ 𝑀 ) ) )
135 131 134 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑦 = 𝑀 → ( 𝑏 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
136 122 sseli ⊢ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) → 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
137 41 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 )
138 137 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 )
139 136 138 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 )
140 139 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ≠ 𝑀 ) ) → ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 )
141 7 eleq2i ⊢ ( 𝑦 ∈ 𝐾 ↔ 𝑦 ∈ ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) )
142 eldifsn ⊢ ( 𝑦 ∈ ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ↔ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ≠ 𝑀 ) )
143 141 142 bitri ⊢ ( 𝑦 ∈ 𝐾 ↔ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ≠ 𝑀 ) )
144 1 2 3 4 5 6 7 9 22 subfacp1lem2b ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑦 ) = ( ( I ↾ 𝐾 ) ‘ 𝑦 ) )
145 fvresi ⊢ ( 𝑦 ∈ 𝐾 → ( ( I ↾ 𝐾 ) ‘ 𝑦 ) = 𝑦 )
146 145 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( ( I ↾ 𝐾 ) ‘ 𝑦 ) = 𝑦 )
147 144 146 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑦 ) = 𝑦 )
148 143 147 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ≠ 𝑀 ) ) → ( 𝐹 ‘ 𝑦 ) = 𝑦 )
149 148 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ≠ 𝑀 ) ) → ( 𝐹 ‘ 𝑦 ) = 𝑦 )
150 140 149 neeqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ≠ 𝑀 ) ) → ( 𝑏 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) )
151 150 expr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑦 ≠ 𝑀 → ( 𝑏 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
152 135 151 pm2.61dne ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑏 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) )
153 152 necomd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑦 ) ≠ ( 𝑏 ‘ 𝑦 ) )
154 128 153 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ≠ ( 𝑏 ‘ 𝑦 ) )
155 24 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
156 ffvelrn ⊢ ( ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑏 ‘ 𝑦 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
157 68 136 156 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑏 ‘ 𝑦 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
158 f1ocnvfv ⊢ ( ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ‘ ( 𝑏 ‘ 𝑦 ) ) = 𝑦 → ( ◡ 𝐹 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ) )
159 155 157 158 syl2an2r ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ‘ ( 𝑏 ‘ 𝑦 ) ) = 𝑦 → ( ◡ 𝐹 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ) )
160 159 necon3d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( ◡ 𝐹 ‘ 𝑦 ) ≠ ( 𝑏 ‘ 𝑦 ) → ( 𝐹 ‘ ( 𝑏 ‘ 𝑦 ) ) ≠ 𝑦 ) )
161 154 160 mpd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ ( 𝑏 ‘ 𝑦 ) ) ≠ 𝑦 )
162 125 161 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) ≠ 𝑦 )
163 162 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) ≠ 𝑦 )
164 f1of ⊢ ( ( I ↾ 𝐾 ) : 𝐾 –1-1-onto→ 𝐾 → ( I ↾ 𝐾 ) : 𝐾 ⟶ 𝐾 )
165 21 164 ax-mp ⊢ ( I ↾ 𝐾 ) : 𝐾 ⟶ 𝐾
166 fzfi ⊢ ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin
167 difexg ⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin → ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∈ V )
168 166 167 ax-mp ⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∈ V
169 7 168 eqeltri ⊢ 𝐾 ∈ V
170 fex ⊢ ( ( ( I ↾ 𝐾 ) : 𝐾 ⟶ 𝐾 ∧ 𝐾 ∈ V ) → ( I ↾ 𝐾 ) ∈ V )
171 165 169 170 mp2an ⊢ ( I ↾ 𝐾 ) ∈ V
172 prex ⊢ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ∈ V
173 171 172 unex ⊢ ( ( I ↾ 𝐾 ) ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ V
174 9 173 eqeltri ⊢ 𝐹 ∈ V
175 174 34 coex ⊢ ( 𝐹 ∘ 𝑏 ) ∈ V
176 175 resex ⊢ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ∈ V
177 f1oeq1 ⊢ ( 𝑓 = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑓 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ↔ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ) )
178 fveq1 ⊢ ( 𝑓 = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑓 ‘ 𝑦 ) = ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ‘ 𝑦 ) )
179 fvres ⊢ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) )
180 178 179 sylan9eq ⊢ ( ( 𝑓 = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) )
181 180 neeq1d ⊢ ( ( 𝑓 = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) ≠ 𝑦 ) )
182 181 ralbidva ⊢ ( 𝑓 = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) ≠ 𝑦 ) )
183 177 182 anbi12d ⊢ ( 𝑓 = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑓 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ↔ ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) ≠ 𝑦 ) ) )
184 176 183 10 elab2 ⊢ ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ∈ 𝐶 ↔ ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) ≠ 𝑦 ) )
185 118 163 184 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ∈ 𝐶 )
186 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ∈ 𝐶 )
187 vex ⊢ 𝑐 ∈ V
188 f1oeq1 ⊢ ( 𝑓 = 𝑐 → ( 𝑓 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ↔ 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ) )
189 fveq1 ⊢ ( 𝑓 = 𝑐 → ( 𝑓 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) )
190 189 neeq1d ⊢ ( 𝑓 = 𝑐 → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ) )
191 190 ralbidv ⊢ ( 𝑓 = 𝑐 → ( ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ) )
192 188 191 anbi12d ⊢ ( 𝑓 = 𝑐 → ( ( 𝑓 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ↔ ( 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ) ) )
193 187 192 10 elab2 ⊢ ( 𝑐 ∈ 𝐶 ↔ ( 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ) )
194 186 193 sylib ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ) )
195 194 simpld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) )
196 f1oun ⊢ ( ( ( { ⟨ 1 , 1 ⟩ } : { 1 } –1-1-onto→ { 1 } ∧ 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ) ∧ ( ( { 1 } ∩ ( 2 ... ( 𝑁 + 1 ) ) ) = ∅ ∧ ( { 1 } ∩ ( 2 ... ( 𝑁 + 1 ) ) ) = ∅ ) ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) –1-1-onto→ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) )
197 106 106 196 mpanr12 ⊢ ( ( { ⟨ 1 , 1 ⟩ } : { 1 } –1-1-onto→ { 1 } ∧ 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) –1-1-onto→ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) )
198 57 195 197 sylancr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) –1-1-onto→ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) )
199 f1oeq2 ⊢ ( ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) = ( 1 ... ( 𝑁 + 1 ) ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) –1-1-onto→ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) ↔ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) ) )
200 f1oeq3 ⊢ ( ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) = ( 1 ... ( 𝑁 + 1 ) ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) ↔ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
201 199 200 bitrd ⊢ ( ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) = ( 1 ... ( 𝑁 + 1 ) ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) –1-1-onto→ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) ↔ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
202 94 201 syl ⊢ ( 𝜑 → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) –1-1-onto→ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) ↔ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
203 202 biimpa ⊢ ( ( 𝜑 ∧ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) –1-1-onto→ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
204 198 203 syldan ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
205 f1oco ⊢ ( ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
206 24 204 205 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
207 f1of ⊢ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
208 204 207 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
209 fvco3 ⊢ ( ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑦 ) = ( 𝐹 ‘ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) )
210 208 209 sylan ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑦 ) = ( 𝐹 ‘ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) )
211 127 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ◡ 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
212 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
213 94 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
214 212 213 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑦 ∈ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) )
215 elun ⊢ ( 𝑦 ∈ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) ↔ ( 𝑦 ∈ { 1 } ∨ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) )
216 214 215 sylib ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑦 ∈ { 1 } ∨ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) )
217 nelne2 ⊢ ( ( 𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ ¬ 1 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → 𝑀 ≠ 1 )
218 5 103 217 sylancl ⊢ ( 𝜑 → 𝑀 ≠ 1 )
219 218 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑀 ≠ 1 )
220 23 simp2d ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = 𝑀 )
221 220 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝐹 ‘ 1 ) = 𝑀 )
222 f1ofun ⊢ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) –1-1-onto→ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) → Fun ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) )
223 198 222 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → Fun ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) )
224 ssun1 ⊢ { ⟨ 1 , 1 ⟩ } ⊆ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 )
225 56 snid ⊢ 1 ∈ { 1 }
226 56 dmsnop ⊢ dom { ⟨ 1 , 1 ⟩ } = { 1 }
227 225 226 eleqtrri ⊢ 1 ∈ dom { ⟨ 1 , 1 ⟩ }
228 funssfv ⊢ ( ( Fun ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ∧ { ⟨ 1 , 1 ⟩ } ⊆ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ∧ 1 ∈ dom { ⟨ 1 , 1 ⟩ } ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ } ‘ 1 ) )
229 224 227 228 mp3an23 ⊢ ( Fun ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ } ‘ 1 ) )
230 223 229 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ } ‘ 1 ) )
231 56 56 fvsn ⊢ ( { ⟨ 1 , 1 ⟩ } ‘ 1 ) = 1
232 230 231 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) = 1 )
233 219 221 232 3netr4d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝐹 ‘ 1 ) ≠ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) )
234 elsni ⊢ ( 𝑦 ∈ { 1 } → 𝑦 = 1 )
235 234 fveq2d ⊢ ( 𝑦 ∈ { 1 } → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 1 ) )
236 234 fveq2d ⊢ ( 𝑦 ∈ { 1 } → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) )
237 235 236 neeq12d ⊢ ( 𝑦 ∈ { 1 } → ( ( 𝐹 ‘ 𝑦 ) ≠ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ↔ ( 𝐹 ‘ 1 ) ≠ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) ) )
238 233 237 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑦 ∈ { 1 } → ( 𝐹 ‘ 𝑦 ) ≠ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) )
239 238 imp ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ { 1 } ) → ( 𝐹 ‘ 𝑦 ) ≠ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) )
240 223 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → Fun ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) )
241 ssun2 ⊢ 𝑐 ⊆ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 )
242 241 a1i ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → 𝑐 ⊆ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) )
243 f1odm ⊢ ( 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) → dom 𝑐 = ( 2 ... ( 𝑁 + 1 ) ) )
244 195 243 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → dom 𝑐 = ( 2 ... ( 𝑁 + 1 ) ) )
245 244 eleq2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑦 ∈ dom 𝑐 ↔ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) )
246 245 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → 𝑦 ∈ dom 𝑐 )
247 funssfv ⊢ ( ( Fun ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ∧ 𝑐 ⊆ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ∧ 𝑦 ∈ dom 𝑐 ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) )
248 240 242 246 247 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) )
249 f1of ⊢ ( 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) → 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) ⟶ ( 2 ... ( 𝑁 + 1 ) ) )
250 195 249 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) ⟶ ( 2 ... ( 𝑁 + 1 ) ) )
251 5 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
252 250 251 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 ‘ 𝑀 ) ∈ ( 2 ... ( 𝑁 + 1 ) ) )
253 nelne2 ⊢ ( ( ( 𝑐 ‘ 𝑀 ) ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ ¬ 1 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑐 ‘ 𝑀 ) ≠ 1 )
254 252 103 253 sylancl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 ‘ 𝑀 ) ≠ 1 )
255 254 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑐 ‘ 𝑀 ) ≠ 1 )
256 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑀 ) = 1 )
257 255 256 neeqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑐 ‘ 𝑀 ) ≠ ( 𝐹 ‘ 𝑀 ) )
258 fveq2 ⊢ ( 𝑦 = 𝑀 → ( 𝑐 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑀 ) )
259 258 133 neeq12d ⊢ ( 𝑦 = 𝑀 → ( ( 𝑐 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑐 ‘ 𝑀 ) ≠ ( 𝐹 ‘ 𝑀 ) ) )
260 257 259 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑦 = 𝑀 → ( 𝑐 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
261 194 simprd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 )
262 261 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 )
263 262 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ≠ 𝑀 ) ) → ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 )
264 148 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ≠ 𝑀 ) ) → ( 𝐹 ‘ 𝑦 ) = 𝑦 )
265 263 264 neeqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ≠ 𝑀 ) ) → ( 𝑐 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) )
266 265 expr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑦 ≠ 𝑀 → ( 𝑐 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
267 260 266 pm2.61dne ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝑐 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) )
268 248 267 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑦 ) )
269 268 necomd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑦 ) ≠ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) )
270 239 269 jaodan ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑦 ∈ { 1 } ∨ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) ) → ( 𝐹 ‘ 𝑦 ) ≠ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) )
271 216 270 syldan ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑦 ) ≠ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) )
272 211 271 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ≠ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) )
273 24 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
274 208 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
275 f1ocnvfv ⊢ ( ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ‘ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) = 𝑦 → ( ◡ 𝐹 ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) )
276 273 274 275 syl2an2r ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ‘ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) = 𝑦 → ( ◡ 𝐹 ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) )
277 276 necon3d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ◡ 𝐹 ‘ 𝑦 ) ≠ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) → ( 𝐹 ‘ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) ≠ 𝑦 ) )
278 272 277 mpd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) ≠ 𝑦 )
279 210 278 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑦 ) ≠ 𝑦 )
280 279 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑦 ) ≠ 𝑦 )
281 snex ⊢ { ⟨ 1 , 1 ⟩ } ∈ V
282 281 187 unex ⊢ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ∈ V
283 174 282 coex ⊢ ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ∈ V
284 f1oeq1 ⊢ ( 𝑓 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) → ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
285 fveq1 ⊢ ( 𝑓 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑦 ) )
286 285 neeq1d ⊢ ( 𝑓 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑦 ) ≠ 𝑦 ) )
287 286 ralbidv ⊢ ( 𝑓 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑦 ) ≠ 𝑦 ) )
288 284 287 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 ⟩ } ∪ 𝑐 ) ) ‘ 𝑦 ) ≠ 𝑦 ) ) )
289 283 288 3 elab2 ⊢ ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ∈ 𝐴 ↔ ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑦 ) ≠ 𝑦 ) )
290 206 280 289 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ∈ 𝐴 )
291 63 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 1 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
292 208 291 fvco3d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 1 ) = ( 𝐹 ‘ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) ) )
293 232 fveq2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝐹 ‘ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) ) = ( 𝐹 ‘ 1 ) )
294 292 293 221 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 1 ) = 𝑀 )
295 122 5 sseldi ⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
296 295 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑀 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
297 208 296 fvco3d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑀 ) = ( 𝐹 ‘ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑀 ) ) )
298 241 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ⊆ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) )
299 251 244 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑀 ∈ dom 𝑐 )
300 funssfv ⊢ ( ( Fun ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ∧ 𝑐 ⊆ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ∧ 𝑀 ∈ dom 𝑐 ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑀 ) = ( 𝑐 ‘ 𝑀 ) )
301 223 298 299 300 syl3anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑀 ) = ( 𝑐 ‘ 𝑀 ) )
302 301 fveq2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝐹 ‘ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑀 ) ) = ( 𝐹 ‘ ( 𝑐 ‘ 𝑀 ) ) )
303 297 302 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑀 ) = ( 𝐹 ‘ ( 𝑐 ‘ 𝑀 ) ) )
304 126 fveq1d ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
305 304 220 eqtrd ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 1 ) = 𝑀 )
306 305 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ◡ 𝐹 ‘ 1 ) = 𝑀 )
307 id ⊢ ( 𝑦 = 𝑀 → 𝑦 = 𝑀 )
308 258 307 neeq12d ⊢ ( 𝑦 = 𝑀 → ( ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ↔ ( 𝑐 ‘ 𝑀 ) ≠ 𝑀 ) )
309 308 261 251 rspcdva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 ‘ 𝑀 ) ≠ 𝑀 )
310 309 necomd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑀 ≠ ( 𝑐 ‘ 𝑀 ) )
311 306 310 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ◡ 𝐹 ‘ 1 ) ≠ ( 𝑐 ‘ 𝑀 ) )
312 122 252 sseldi ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 ‘ 𝑀 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
313 f1ocnvfv ⊢ ( ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝑐 ‘ 𝑀 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ‘ ( 𝑐 ‘ 𝑀 ) ) = 1 → ( ◡ 𝐹 ‘ 1 ) = ( 𝑐 ‘ 𝑀 ) ) )
314 24 312 313 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝐹 ‘ ( 𝑐 ‘ 𝑀 ) ) = 1 → ( ◡ 𝐹 ‘ 1 ) = ( 𝑐 ‘ 𝑀 ) ) )
315 314 necon3d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( ◡ 𝐹 ‘ 1 ) ≠ ( 𝑐 ‘ 𝑀 ) → ( 𝐹 ‘ ( 𝑐 ‘ 𝑀 ) ) ≠ 1 ) )
316 311 315 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝐹 ‘ ( 𝑐 ‘ 𝑀 ) ) ≠ 1 )
317 303 316 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑀 ) ≠ 1 )
318 294 317 jca ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 1 ) = 𝑀 ∧ ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑀 ) ≠ 1 ) )
319 fveq1 ⊢ ( 𝑔 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) → ( 𝑔 ‘ 1 ) = ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 1 ) )
320 319 eqeq1d ⊢ ( 𝑔 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) → ( ( 𝑔 ‘ 1 ) = 𝑀 ↔ ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 1 ) = 𝑀 ) )
321 fveq1 ⊢ ( 𝑔 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) → ( 𝑔 ‘ 𝑀 ) = ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑀 ) )
322 321 neeq1d ⊢ ( 𝑔 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) → ( ( 𝑔 ‘ 𝑀 ) ≠ 1 ↔ ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑀 ) ≠ 1 ) )
323 320 322 anbi12d ⊢ ( 𝑔 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) → ( ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔 ‘ 𝑀 ) ≠ 1 ) ↔ ( ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 1 ) = 𝑀 ∧ ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑀 ) ≠ 1 ) ) )
324 323 8 elrab2 ⊢ ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ∈ 𝐵 ↔ ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ∈ 𝐴 ∧ ( ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 1 ) = 𝑀 ∧ ( ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ‘ 𝑀 ) ≠ 1 ) ) )
325 290 318 324 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ∈ 𝐵 )
326 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
327 f1of1 ⊢ ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) )
328 326 327 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) )
329 f1of ⊢ ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
330 326 329 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
331 68 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
332 330 331 fcod ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
333 208 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
334 cocan1 ⊢ ( ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝐹 ∘ 𝑏 ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ∘ ( 𝐹 ∘ 𝑏 ) ) = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ↔ ( 𝐹 ∘ 𝑏 ) = ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) )
335 328 332 333 334 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐹 ∘ ( 𝐹 ∘ 𝑏 ) ) = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ↔ ( 𝐹 ∘ 𝑏 ) = ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) )
336 coass ⊢ ( ( 𝐹 ∘ 𝐹 ) ∘ 𝑏 ) = ( 𝐹 ∘ ( 𝐹 ∘ 𝑏 ) )
337 126 coeq1d ⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐹 ) = ( 𝐹 ∘ 𝐹 ) )
338 f1ococnv1 ⊢ ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( 1 ... ( 𝑁 + 1 ) ) ) )
339 24 338 syl ⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( 1 ... ( 𝑁 + 1 ) ) ) )
340 337 339 eqtr3d ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐹 ) = ( I ↾ ( 1 ... ( 𝑁 + 1 ) ) ) )
341 340 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝐹 ∘ 𝐹 ) = ( I ↾ ( 1 ... ( 𝑁 + 1 ) ) ) )
342 341 coeq1d ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐹 ∘ 𝐹 ) ∘ 𝑏 ) = ( ( I ↾ ( 1 ... ( 𝑁 + 1 ) ) ) ∘ 𝑏 ) )
343 fcoi2 ⊢ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) → ( ( I ↾ ( 1 ... ( 𝑁 + 1 ) ) ) ∘ 𝑏 ) = 𝑏 )
344 331 343 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( I ↾ ( 1 ... ( 𝑁 + 1 ) ) ) ∘ 𝑏 ) = 𝑏 )
345 342 344 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐹 ∘ 𝐹 ) ∘ 𝑏 ) = 𝑏 )
346 336 345 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝐹 ∘ ( 𝐹 ∘ 𝑏 ) ) = 𝑏 )
347 346 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐹 ∘ ( 𝐹 ∘ 𝑏 ) ) = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ↔ 𝑏 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ) )
348 75 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) = 1 )
349 232 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) = 1 )
350 348 349 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) )
351 fveq2 ⊢ ( 𝑦 = 1 → ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) )
352 fveq2 ⊢ ( 𝑦 = 1 → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) )
353 351 352 eqeq12d ⊢ ( 𝑦 = 1 → ( ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ↔ ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) ) )
354 56 353 ralsn ⊢ ( ∀ 𝑦 ∈ { 1 } ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ↔ ( ( 𝐹 ∘ 𝑏 ) ‘ 1 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 1 ) )
355 350 354 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ∀ 𝑦 ∈ { 1 } ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) )
356 355 biantrurd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ { 1 } ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) ) )
357 ralunb ⊢ ( ∀ 𝑦 ∈ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ { 1 } ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) )
358 356 357 bitr4di ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) )
359 179 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) )
360 359 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ‘ 𝑦 ) )
361 248 adantlrl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) )
362 360 361 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ↔ ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) )
363 362 ralbidva ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) )
364 94 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
365 364 raleqdv ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( { 1 } ∪ ( 2 ... ( 𝑁 + 1 ) ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) )
366 358 363 365 3bitr3rd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) )
367 58 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝐹 ∘ 𝑏 ) Fn ( 1 ... ( 𝑁 + 1 ) ) )
368 204 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
369 f1ofn ⊢ ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) Fn ( 1 ... ( 𝑁 + 1 ) ) )
370 368 369 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) Fn ( 1 ... ( 𝑁 + 1 ) ) )
371 eqfnfv ⊢ ( ( ( 𝐹 ∘ 𝑏 ) Fn ( 1 ... ( 𝑁 + 1 ) ) ∧ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) Fn ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ∘ 𝑏 ) = ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) )
372 367 370 371 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐹 ∘ 𝑏 ) = ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝐹 ∘ 𝑏 ) ‘ 𝑦 ) = ( ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ‘ 𝑦 ) ) )
373 fnssres ⊢ ( ( ( 𝐹 ∘ 𝑏 ) Fn ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 2 ... ( 𝑁 + 1 ) ) ⊆ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) Fn ( 2 ... ( 𝑁 + 1 ) ) )
374 367 122 373 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) Fn ( 2 ... ( 𝑁 + 1 ) ) )
375 195 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) )
376 f1ofn ⊢ ( 𝑐 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) → 𝑐 Fn ( 2 ... ( 𝑁 + 1 ) ) )
377 375 376 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑐 Fn ( 2 ... ( 𝑁 + 1 ) ) )
378 eqfnfv ⊢ ( ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) Fn ( 2 ... ( 𝑁 + 1 ) ) ∧ 𝑐 Fn ( 2 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) = 𝑐 ↔ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) )
379 374 377 378 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) = 𝑐 ↔ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) )
380 366 372 379 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐹 ∘ 𝑏 ) = ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ↔ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) = 𝑐 ) )
381 eqcom ⊢ ( ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) = 𝑐 ↔ 𝑐 = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) )
382 380 381 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐹 ∘ 𝑏 ) = ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ↔ 𝑐 = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ) )
383 335 347 382 3bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 = ( 𝐹 ∘ ( { ⟨ 1 , 1 ⟩ } ∪ 𝑐 ) ) ↔ 𝑐 = ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ) )
384 20 185 325 383 f1o2d ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐹 ∘ 𝑏 ) ↾ ( 2 ... ( 𝑁 + 1 ) ) ) ) : 𝐵 –1-1-onto→ 𝐶 )
385 19 384 hasheqf1od ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐶 ) )
386 1 2 derangen2 ⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin → ( 𝐷 ‘ ( 2 ... ( 𝑁 + 1 ) ) ) = ( 𝑆 ‘ ( ♯ ‘ ( 2 ... ( 𝑁 + 1 ) ) ) ) )
387 1 derangval ⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin → ( 𝐷 ‘ ( 2 ... ( 𝑁 + 1 ) ) ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
388 10 fveq2i ⊢ ( ♯ ‘ 𝐶 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ( 2 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 2 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 2 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } )
389 387 388 eqtr4di ⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin → ( 𝐷 ‘ ( 2 ... ( 𝑁 + 1 ) ) ) = ( ♯ ‘ 𝐶 ) )
390 386 389 eqtr3d ⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin → ( 𝑆 ‘ ( ♯ ‘ ( 2 ... ( 𝑁 + 1 ) ) ) ) = ( ♯ ‘ 𝐶 ) )
391 166 390 ax-mp ⊢ ( 𝑆 ‘ ( ♯ ‘ ( 2 ... ( 𝑁 + 1 ) ) ) ) = ( ♯ ‘ 𝐶 )
392 4 60 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
393 eluzp1p1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
394 392 393 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
395 df-2 ⊢ 2 = ( 1 + 1 )
396 395 fveq2i ⊢ ( ℤ≥ ‘ 2 ) = ( ℤ≥ ‘ ( 1 + 1 ) )
397 394 396 eleqtrrdi ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
398 hashfz ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ( ♯ ‘ ( 2 ... ( 𝑁 + 1 ) ) ) = ( ( ( 𝑁 + 1 ) − 2 ) + 1 ) )
399 397 398 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 2 ... ( 𝑁 + 1 ) ) ) = ( ( ( 𝑁 + 1 ) − 2 ) + 1 ) )
400 59 nncnd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℂ )
401 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
402 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
403 400 401 402 subsubd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − ( 2 − 1 ) ) = ( ( ( 𝑁 + 1 ) − 2 ) + 1 ) )
404 2m1e1 ⊢ ( 2 − 1 ) = 1
405 404 oveq2i ⊢ ( ( 𝑁 + 1 ) − ( 2 − 1 ) ) = ( ( 𝑁 + 1 ) − 1 )
406 4 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
407 ax-1cn ⊢ 1 ∈ ℂ
408 pncan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
409 406 407 408 sylancl ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
410 405 409 syl5eq ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − ( 2 − 1 ) ) = 𝑁 )
411 399 403 410 3eqtr2d ⊢ ( 𝜑 → ( ♯ ‘ ( 2 ... ( 𝑁 + 1 ) ) ) = 𝑁 )
412 411 fveq2d ⊢ ( 𝜑 → ( 𝑆 ‘ ( ♯ ‘ ( 2 ... ( 𝑁 + 1 ) ) ) ) = ( 𝑆 ‘ 𝑁 ) )
413 391 412 eqtr3id ⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) = ( 𝑆 ‘ 𝑁 ) )
414 385 413 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑆 ‘ 𝑁 ) )