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