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