Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  subfacp1lem5 Structured version   Visualization version   GIF version

Theorem subfacp1lem5 31292
 Description: Lemma for subfacp1 31294. In subfacp1lem6 31293 we cut up the set of all derangements on 1...(𝑁 + 1) first according to the value at 1, and then by whether or not (𝑓‘(𝑓‘1)) = 1. In this lemma, we show that the subset of all 𝑁 + 1 derangements with (𝑓‘(𝑓‘1)) ≠ 1 for fixed 𝑀 = (𝑓‘1) is in bijection with derangements of 2...(𝑁 + 1), because pre-composing with the function 𝐹 swaps 1 and 𝑀 and turns the function into a bijection with (𝑓‘1) = 1 and (𝑓‘𝑥) ≠ 𝑥 for all other 𝑥, so dropping the point at 1 yields a derangement on the 𝑁 remaining points. (Contributed by Mario Carneiro, 23-Jan-2015.)
Hypotheses
Ref Expression
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
Ref Expression
subfacp1lem5 (𝜑 → (#‘𝐵) = (𝑆𝑁))
Distinct variable groups:   𝑓,𝑔,𝑛,𝑥,𝑦,𝐴   𝑓,𝐹,𝑔,𝑥,𝑦   𝑓,𝑁,𝑔,𝑛,𝑥,𝑦   𝐵,𝑓,𝑔,𝑥,𝑦   𝑥,𝐶,𝑦   𝜑,𝑥,𝑦   𝐷,𝑛   𝑓,𝐾,𝑛,𝑥,𝑦   𝑓,𝑀,𝑔,𝑥,𝑦   𝑆,𝑛,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑓,𝑔,𝑛)   𝐵(𝑛)   𝐶(𝑓,𝑔,𝑛)   𝐷(𝑥,𝑦,𝑓,𝑔)   𝑆(𝑓,𝑔)   𝐹(𝑛)   𝐾(𝑔)   𝑀(𝑛)

Proof of Theorem subfacp1lem5
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 subfacp1lem.a . . . . . . . 8 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}
2 fzfi 12811 . . . . . . . . 9 (1...(𝑁 + 1)) ∈ Fin
3 deranglem 31274 . . . . . . . . 9 ((1...(𝑁 + 1)) ∈ Fin → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ∈ Fin)
42, 3ax-mp 5 . . . . . . . 8 {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ∈ Fin
51, 4eqeltri 2726 . . . . . . 7 𝐴 ∈ Fin
6 subfacp1lem5.b . . . . . . . 8 𝐵 = {𝑔𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1)}
7 ssrab2 3720 . . . . . . . 8 {𝑔𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1)} ⊆ 𝐴
86, 7eqsstri 3668 . . . . . . 7 𝐵𝐴
9 ssfi 8221 . . . . . . 7 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)
105, 8, 9mp2an 708 . . . . . 6 𝐵 ∈ Fin
1110elexi 3244 . . . . 5 𝐵 ∈ V
1211a1i 11 . . . 4 (𝜑𝐵 ∈ V)
13 subfacp1lem5.c . . . . . . 7 𝐶 = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}
14 fzfi 12811 . . . . . . . 8 (2...(𝑁 + 1)) ∈ Fin
15 deranglem 31274 . . . . . . . 8 ((2...(𝑁 + 1)) ∈ Fin → {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ∈ Fin)
1614, 15ax-mp 5 . . . . . . 7 {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ∈ Fin
1713, 16eqeltri 2726 . . . . . 6 𝐶 ∈ Fin
1817elexi 3244 . . . . 5 𝐶 ∈ V
1918a1i 11 . . . 4 (𝜑𝐶 ∈ V)
20 derang.d . . . . . . . . . . . . 13 𝐷 = (𝑥 ∈ Fin ↦ (#‘{𝑓 ∣ (𝑓:𝑥1-1-onto𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) ≠ 𝑦)}))
21 subfac.n . . . . . . . . . . . . 13 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))
22 subfacp1lem1.n . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
23 subfacp1lem1.m . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (2...(𝑁 + 1)))
24 subfacp1lem1.x . . . . . . . . . . . . 13 𝑀 ∈ V
25 subfacp1lem1.k . . . . . . . . . . . . 13 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})
26 subfacp1lem5.f . . . . . . . . . . . . 13 𝐹 = (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})
27 f1oi 6212 . . . . . . . . . . . . . 14 ( I ↾ 𝐾):𝐾1-1-onto𝐾
2827a1i 11 . . . . . . . . . . . . 13 (𝜑 → ( I ↾ 𝐾):𝐾1-1-onto𝐾)
2920, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2a 31288 . . . . . . . . . . . 12 (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹𝑀) = 1))
3029simp1d 1093 . . . . . . . . . . 11 (𝜑𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
3130adantr 480 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
32 simpr 476 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → 𝑏𝐵)
33 fveq1 6228 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
3433eqeq1d 2653 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
35 fveq1 6228 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑏 → (𝑔𝑀) = (𝑏𝑀))
3635neeq1d 2882 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑏 → ((𝑔𝑀) ≠ 1 ↔ (𝑏𝑀) ≠ 1))
3734, 36anbi12d 747 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3837, 6elrab2 3399 . . . . . . . . . . . . . 14 (𝑏𝐵 ↔ (𝑏𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3932, 38sylib 208 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (𝑏𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
4039simpld 474 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → 𝑏𝐴)
41 vex 3234 . . . . . . . . . . . . 13 𝑏 ∈ V
42 f1oeq1 6165 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
43 fveq1 6228 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
4443neeq1d 2882 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑏𝑦) ≠ 𝑦))
4544ralbidv 3015 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4642, 45anbi12d 747 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦)))
4741, 46, 1elab2 3386 . . . . . . . . . . . 12 (𝑏𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4840, 47sylib 208 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4948simpld 474 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
50 f1oco 6197 . . . . . . . . . 10 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) → (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
5131, 49, 50syl2anc 694 . . . . . . . . 9 ((𝜑𝑏𝐵) → (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
52 f1of1 6174 . . . . . . . . 9 ((𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
53 df-f1 5931 . . . . . . . . . 10 ((𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ ((𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun (𝐹𝑏)))
5453simprbi 479 . . . . . . . . 9 ((𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun (𝐹𝑏))
5551, 52, 543syl 18 . . . . . . . 8 ((𝜑𝑏𝐵) → Fun (𝐹𝑏))
56 f1ofn 6176 . . . . . . . . . . 11 ((𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
57 fnresdm 6038 . . . . . . . . . . 11 ((𝐹𝑏) Fn (1...(𝑁 + 1)) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))) = (𝐹𝑏))
58 f1oeq1 6165 . . . . . . . . . . 11 (((𝐹𝑏) ↾ (1...(𝑁 + 1))) = (𝐹𝑏) → (((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
5951, 56, 57, 584syl 19 . . . . . . . . . 10 ((𝜑𝑏𝐵) → (((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
6051, 59mpbird 247 . . . . . . . . 9 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
61 f1ofo 6182 . . . . . . . . 9 (((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
6260, 61syl 17 . . . . . . . 8 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
63 1ex 10073 . . . . . . . . . . 11 1 ∈ V
6463, 63f1osn 6214 . . . . . . . . . 10 {⟨1, 1⟩}:{1}–1-1-onto→{1}
6551, 56syl 17 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
6622peano2nnd 11075 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ ℕ)
67 nnuz 11761 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
6866, 67syl6eleq 2740 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
69 eluzfz1 12386 . . . . . . . . . . . . . . 15 ((𝑁 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑁 + 1)))
7068, 69syl 17 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ (1...(𝑁 + 1)))
7170adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → 1 ∈ (1...(𝑁 + 1)))
72 fnressn 6465 . . . . . . . . . . . . 13 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏) ↾ {1}) = {⟨1, ((𝐹𝑏)‘1)⟩})
7365, 71, 72syl2anc 694 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}) = {⟨1, ((𝐹𝑏)‘1)⟩})
74 f1of 6175 . . . . . . . . . . . . . . . . 17 (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
7549, 74syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
76 fvco3 6314 . . . . . . . . . . . . . . . 16 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏)‘1) = (𝐹‘(𝑏‘1)))
7775, 71, 76syl2anc 694 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → ((𝐹𝑏)‘1) = (𝐹‘(𝑏‘1)))
7839simprd 478 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1))
7978simpld 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → (𝑏‘1) = 𝑀)
8079fveq2d 6233 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝐹‘(𝑏‘1)) = (𝐹𝑀))
8129simp3d 1095 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝑀) = 1)
8281adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝐹𝑀) = 1)
8377, 80, 823eqtrd 2689 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → ((𝐹𝑏)‘1) = 1)
8483opeq2d 4440 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → ⟨1, ((𝐹𝑏)‘1)⟩ = ⟨1, 1⟩)
8584sneqd 4222 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → {⟨1, ((𝐹𝑏)‘1)⟩} = {⟨1, 1⟩})
8673, 85eqtrd 2685 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}) = {⟨1, 1⟩})
87 f1oeq1 6165 . . . . . . . . . . 11 (((𝐹𝑏) ↾ {1}) = {⟨1, 1⟩} → (((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1} ↔ {⟨1, 1⟩}:{1}–1-1-onto→{1}))
8886, 87syl 17 . . . . . . . . . 10 ((𝜑𝑏𝐵) → (((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1} ↔ {⟨1, 1⟩}:{1}–1-1-onto→{1}))
8964, 88mpbiri 248 . . . . . . . . 9 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1})
90 f1ofo 6182 . . . . . . . . 9 (((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1} → ((𝐹𝑏) ↾ {1}):{1}–onto→{1})
9189, 90syl 17 . . . . . . . 8 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}):{1}–onto→{1})
92 resdif 6195 . . . . . . . 8 ((Fun (𝐹𝑏) ∧ ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)) ∧ ((𝐹𝑏) ↾ {1}):{1}–onto→{1}) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
9355, 62, 91, 92syl3anc 1366 . . . . . . 7 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
94 fzsplit 12405 . . . . . . . . . . . 12 (1 ∈ (1...(𝑁 + 1)) → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
9570, 94syl 17 . . . . . . . . . . 11 (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
96 1z 11445 . . . . . . . . . . . . 13 1 ∈ ℤ
97 fzsn 12421 . . . . . . . . . . . . 13 (1 ∈ ℤ → (1...1) = {1})
9896, 97ax-mp 5 . . . . . . . . . . . 12 (1...1) = {1}
99 1p1e2 11172 . . . . . . . . . . . . 13 (1 + 1) = 2
10099oveq1i 6700 . . . . . . . . . . . 12 ((1 + 1)...(𝑁 + 1)) = (2...(𝑁 + 1))
10198, 100uneq12i 3798 . . . . . . . . . . 11 ((1...1) ∪ ((1 + 1)...(𝑁 + 1))) = ({1} ∪ (2...(𝑁 + 1)))
10295, 101syl6req 2702 . . . . . . . . . 10 (𝜑 → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
10370snssd 4372 . . . . . . . . . . 11 (𝜑 → {1} ⊆ (1...(𝑁 + 1)))
104 incom 3838 . . . . . . . . . . . 12 ({1} ∩ (2...(𝑁 + 1))) = ((2...(𝑁 + 1)) ∩ {1})
105 1lt2 11232 . . . . . . . . . . . . . . 15 1 < 2
106 1re 10077 . . . . . . . . . . . . . . . 16 1 ∈ ℝ
107 2re 11128 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
108106, 107ltnlei 10196 . . . . . . . . . . . . . . 15 (1 < 2 ↔ ¬ 2 ≤ 1)
109105, 108mpbi 220 . . . . . . . . . . . . . 14 ¬ 2 ≤ 1
110 elfzle1 12382 . . . . . . . . . . . . . 14 (1 ∈ (2...(𝑁 + 1)) → 2 ≤ 1)
111109, 110mto 188 . . . . . . . . . . . . 13 ¬ 1 ∈ (2...(𝑁 + 1))
112 disjsn 4278 . . . . . . . . . . . . 13 (((2...(𝑁 + 1)) ∩ {1}) = ∅ ↔ ¬ 1 ∈ (2...(𝑁 + 1)))
113111, 112mpbir 221 . . . . . . . . . . . 12 ((2...(𝑁 + 1)) ∩ {1}) = ∅
114104, 113eqtri 2673 . . . . . . . . . . 11 ({1} ∩ (2...(𝑁 + 1))) = ∅
115 uneqdifeq 4090 . . . . . . . . . . 11 (({1} ⊆ (1...(𝑁 + 1)) ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅) → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
116103, 114, 115sylancl 695 . . . . . . . . . 10 (𝜑 → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
117102, 116mpbid 222 . . . . . . . . 9 (𝜑 → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
118117adantr 480 . . . . . . . 8 ((𝜑𝑏𝐵) → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
119 reseq2 5423 . . . . . . . . . 10 (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})) = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
120 f1oeq1 6165 . . . . . . . . . 10 (((𝐹𝑏) ↾ ((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})))
121119, 120syl 17 . . . . . . . . 9 (((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 6166 . . . . . . . . 9 (((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 6167 . . . . . . . . 9 (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
124121, 122, 1233bitrd 294 . . . . . . . 8 (((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))))
125118, 124syl 17 . . . . . . 7 ((𝜑𝑏𝐵) → (((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
12693, 125mpbid 222 . . . . . 6 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
12775adantr 480 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
128 fzp1ss 12430 . . . . . . . . . . . 12 (1 ∈ ℤ → ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1)))
12996, 128ax-mp 5 . . . . . . . . . . 11 ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
130100, 129eqsstr3i 3669 . . . . . . . . . 10 (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
131 simpr 476 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (2...(𝑁 + 1)))
132130, 131sseldi 3634 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
133 fvco3 6314 . . . . . . . . 9 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (𝐹‘(𝑏𝑦)))
134127, 132, 133syl2anc 694 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (𝐹‘(𝑏𝑦)))
13520, 21, 1, 22, 23, 24, 25, 6, 26subfacp1lem4 31291 . . . . . . . . . . . 12 (𝜑𝐹 = 𝐹)
136135fveq1d 6231 . . . . . . . . . . 11 (𝜑 → (𝐹𝑦) = (𝐹𝑦))
137136ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) = (𝐹𝑦))
13878simprd 478 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝑏𝑀) ≠ 1)
139138, 82neeqtrrd 2897 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → (𝑏𝑀) ≠ (𝐹𝑀))
140139adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑀) ≠ (𝐹𝑀))
141 fveq2 6229 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → (𝑏𝑦) = (𝑏𝑀))
142 fveq2 6229 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → (𝐹𝑦) = (𝐹𝑀))
143141, 142neeq12d 2884 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → ((𝑏𝑦) ≠ (𝐹𝑦) ↔ (𝑏𝑀) ≠ (𝐹𝑀)))
144140, 143syl5ibrcom 237 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑏𝑦) ≠ (𝐹𝑦)))
145130sseli 3632 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (2...(𝑁 + 1)) → 𝑦 ∈ (1...(𝑁 + 1)))
14648simprd 478 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦)
147146r19.21bi 2961 . . . . . . . . . . . . . . . 16 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏𝑦) ≠ 𝑦)
148145, 147sylan2 490 . . . . . . . . . . . . . . 15 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ≠ 𝑦)
149148adantrr 753 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑏𝑦) ≠ 𝑦)
15025eleq2i 2722 . . . . . . . . . . . . . . . . 17 (𝑦𝐾𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}))
151 eldifsn 4350 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀))
152150, 151bitri 264 . . . . . . . . . . . . . . . 16 (𝑦𝐾 ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀))
15320, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2b 31289 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐾) → (𝐹𝑦) = (( I ↾ 𝐾)‘𝑦))
154 fvresi 6480 . . . . . . . . . . . . . . . . . 18 (𝑦𝐾 → (( I ↾ 𝐾)‘𝑦) = 𝑦)
155154adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐾) → (( I ↾ 𝐾)‘𝑦) = 𝑦)
156153, 155eqtrd 2685 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐾) → (𝐹𝑦) = 𝑦)
157152, 156sylan2br 492 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
158157adantlr 751 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
159149, 158neeqtrrd 2897 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑏𝑦) ≠ (𝐹𝑦))
160159expr 642 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦𝑀 → (𝑏𝑦) ≠ (𝐹𝑦)))
161144, 160pm2.61dne 2909 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ≠ (𝐹𝑦))
162161necomd 2878 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (𝑏𝑦))
163137, 162eqnetrd 2890 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (𝑏𝑦))
16431adantr 480 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
165 ffvelrn 6397 . . . . . . . . . . . 12 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏𝑦) ∈ (1...(𝑁 + 1)))
16675, 145, 165syl2an 493 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ∈ (1...(𝑁 + 1)))
167 f1ocnvfv 6574 . . . . . . . . . . 11 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑏𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑏𝑦)) = 𝑦 → (𝐹𝑦) = (𝑏𝑦)))
168164, 166, 167syl2anc 694 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹‘(𝑏𝑦)) = 𝑦 → (𝐹𝑦) = (𝑏𝑦)))
169168necon3d 2844 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑦) ≠ (𝑏𝑦) → (𝐹‘(𝑏𝑦)) ≠ 𝑦))
170163, 169mpd 15 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘(𝑏𝑦)) ≠ 𝑦)
171134, 170eqnetrd 2890 . . . . . . 7 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) ≠ 𝑦)
172171ralrimiva 2995 . . . . . 6 ((𝜑𝑏𝐵) → ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦)
173 f1of 6175 . . . . . . . . . . . . 13 (( I ↾ 𝐾):𝐾1-1-onto𝐾 → ( I ↾ 𝐾):𝐾𝐾)
17427, 173ax-mp 5 . . . . . . . . . . . 12 ( I ↾ 𝐾):𝐾𝐾
175 difexg 4841 . . . . . . . . . . . . . 14 ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V)
17614, 175ax-mp 5 . . . . . . . . . . . . 13 ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V
17725, 176eqeltri 2726 . . . . . . . . . . . 12 𝐾 ∈ V
178 fex 6530 . . . . . . . . . . . 12 ((( I ↾ 𝐾):𝐾𝐾𝐾 ∈ V) → ( I ↾ 𝐾) ∈ V)
179174, 177, 178mp2an 708 . . . . . . . . . . 11 ( I ↾ 𝐾) ∈ V
180 prex 4939 . . . . . . . . . . 11 {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
181179, 180unex 6998 . . . . . . . . . 10 (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
18226, 181eqeltri 2726 . . . . . . . . 9 𝐹 ∈ V
183182, 41coex 7160 . . . . . . . 8 (𝐹𝑏) ∈ V
184183resex 5478 . . . . . . 7 ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ V
185 f1oeq1 6165 . . . . . . . 8 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
186 fveq1 6228 . . . . . . . . . . 11 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (𝑓𝑦) = (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
187 fvres 6245 . . . . . . . . . . 11 (𝑦 ∈ (2...(𝑁 + 1)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹𝑏)‘𝑦))
188186, 187sylan9eq 2705 . . . . . . . . . 10 ((𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑓𝑦) = ((𝐹𝑏)‘𝑦))
189188neeq1d 2882 . . . . . . . . 9 ((𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝑓𝑦) ≠ 𝑦 ↔ ((𝐹𝑏)‘𝑦) ≠ 𝑦))
190189ralbidva 3014 . . . . . . . 8 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦))
191185, 190anbi12d 747 . . . . . . 7 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦)))
192184, 191, 13elab2 3386 . . . . . 6 (((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶 ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦))
193126, 172, 192sylanbrc 699 . . . . 5 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶)
194193ex 449 . . . 4 (𝜑 → (𝑏𝐵 → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶))
19530adantr 480 . . . . . . . 8 ((𝜑𝑐𝐶) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
196 simpr 476 . . . . . . . . . . . 12 ((𝜑𝑐𝐶) → 𝑐𝐶)
197 vex 3234 . . . . . . . . . . . . 13 𝑐 ∈ V
198 f1oeq1 6165 . . . . . . . . . . . . . 14 (𝑓 = 𝑐 → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
199 fveq1 6228 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑐 → (𝑓𝑦) = (𝑐𝑦))
200199neeq1d 2882 . . . . . . . . . . . . . . 15 (𝑓 = 𝑐 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑐𝑦) ≠ 𝑦))
201200ralbidv 3015 . . . . . . . . . . . . . 14 (𝑓 = 𝑐 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
202198, 201anbi12d 747 . . . . . . . . . . . . 13 (𝑓 = 𝑐 → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦)))
203197, 202, 13elab2 3386 . . . . . . . . . . . 12 (𝑐𝐶 ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
204196, 203sylib 208 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
205204simpld 474 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
206 f1oun 6194 . . . . . . . . . . 11 ((({⟨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))))
207114, 114, 206mpanr12 721 . . . . . . . . . 10 (({⟨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))))
20864, 205, 207sylancr 696 . . . . . . . . 9 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
209 f1oeq2 6166 . . . . . . . . . . . 12 (({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 6167 . . . . . . . . . . . 12 (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) → (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
211209, 210bitrd 268 . . . . . . . . . . 11 (({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))))
212102, 211syl 17 . . . . . . . . . 10 (𝜑 → (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
213212biimpa 500 . . . . . . . . 9 ((𝜑 ∧ ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1)))) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
214208, 213syldan 486 . . . . . . . 8 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
215 f1oco 6197 . . . . . . . 8 ((𝐹:(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)))
216195, 214, 215syl2anc 694 . . . . . . 7 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
217 f1of 6175 . . . . . . . . . . 11 (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
218214, 217syl 17 . . . . . . . . . 10 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
219 fvco3 6314 . . . . . . . . . 10 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
220218, 219sylan 487 . . . . . . . . 9 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
221136ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) = (𝐹𝑦))
222 simpr 476 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
223102ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
224222, 223eleqtrrd 2733 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))))
225 elun 3786 . . . . . . . . . . . . 13 (𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
226224, 225sylib 208 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
227 nelne2 2920 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → 𝑀 ≠ 1)
22823, 111, 227sylancl 695 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ≠ 1)
229228adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → 𝑀 ≠ 1)
23029simp2d 1094 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹‘1) = 𝑀)
231230adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → (𝐹‘1) = 𝑀)
232 f1ofun 6177 . . . . . . . . . . . . . . . . . . 19 (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
233208, 232syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐶) → Fun ({⟨1, 1⟩} ∪ 𝑐))
234 ssun1 3809 . . . . . . . . . . . . . . . . . . 19 {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐)
23563snid 4241 . . . . . . . . . . . . . . . . . . . 20 1 ∈ {1}
23663dmsnop 5645 . . . . . . . . . . . . . . . . . . . 20 dom {⟨1, 1⟩} = {1}
237235, 236eleqtrri 2729 . . . . . . . . . . . . . . . . . . 19 1 ∈ dom {⟨1, 1⟩}
238 funssfv 6247 . . . . . . . . . . . . . . . . . . 19 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 1 ∈ dom {⟨1, 1⟩}) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
239234, 237, 238mp3an23 1456 . . . . . . . . . . . . . . . . . 18 (Fun ({⟨1, 1⟩} ∪ 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
240233, 239syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
24163, 63fvsn 6487 . . . . . . . . . . . . . . . . 17 ({⟨1, 1⟩}‘1) = 1
242240, 241syl6eq 2701 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
243229, 231, 2423netr4d 2900 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐶) → (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1))
244 elsni 4227 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {1} → 𝑦 = 1)
245244fveq2d 6233 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (𝐹𝑦) = (𝐹‘1))
246244fveq2d 6233 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
247245, 246neeq12d 2884 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → ((𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1)))
248243, 247syl5ibrcom 237 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐶) → (𝑦 ∈ {1} → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
249248imp 444 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ {1}) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
250233adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
251 ssun2 3810 . . . . . . . . . . . . . . . . 17 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐)
252251a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
253 f1odm 6179 . . . . . . . . . . . . . . . . . . 19 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → dom 𝑐 = (2...(𝑁 + 1)))
254205, 253syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐶) → dom 𝑐 = (2...(𝑁 + 1)))
255254eleq2d 2716 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐶) → (𝑦 ∈ dom 𝑐𝑦 ∈ (2...(𝑁 + 1))))
256255biimpar 501 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ dom 𝑐)
257 funssfv 6247 . . . . . . . . . . . . . . . 16 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑦 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
258250, 252, 256, 257syl3anc 1366 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
259 f1of 6175 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
260205, 259syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐶) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
26123adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
262260, 261ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐶) → (𝑐𝑀) ∈ (2...(𝑁 + 1)))
263 nelne2 2920 . . . . . . . . . . . . . . . . . . . 20 (((𝑐𝑀) ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ 1)
264262, 111, 263sylancl 695 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐶) → (𝑐𝑀) ≠ 1)
265264adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ 1)
26681ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑀) = 1)
267265, 266neeqtrrd 2897 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ (𝐹𝑀))
268 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑀 → (𝑐𝑦) = (𝑐𝑀))
269268, 142neeq12d 2884 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑀 → ((𝑐𝑦) ≠ (𝐹𝑦) ↔ (𝑐𝑀) ≠ (𝐹𝑀)))
270267, 269syl5ibrcom 237 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑐𝑦) ≠ (𝐹𝑦)))
271204simprd 478 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐶) → ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦)
272271r19.21bi 2961 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑦) ≠ 𝑦)
273272adantrr 753 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑐𝑦) ≠ 𝑦)
274157adantlr 751 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
275273, 274neeqtrrd 2897 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑐𝑦) ≠ (𝐹𝑦))
276275expr 642 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦𝑀 → (𝑐𝑦) ≠ (𝐹𝑦)))
277270, 276pm2.61dne 2909 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑦) ≠ (𝐹𝑦))
278258, 277eqnetrd 2890 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ≠ (𝐹𝑦))
279278necomd 2878 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
280249, 279jaodan 843 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1)))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
281226, 280syldan 486 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
282221, 281eqnetrd 2890 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
283195adantr 480 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
284218ffvelrnda 6399 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1)))
285 f1ocnvfv 6574 . . . . . . . . . . . 12 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (𝐹𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
286283, 284, 285syl2anc 694 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (𝐹𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
287286necon3d 2844 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦))
288282, 287mpd 15 . . . . . . . . 9 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦)
289220, 288eqnetrd 2890 . . . . . . . 8 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
290289ralrimiva 2995 . . . . . . 7 ((𝜑𝑐𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
291 snex 4938 . . . . . . . . . 10 {⟨1, 1⟩} ∈ V
292291, 197unex 6998 . . . . . . . . 9 ({⟨1, 1⟩} ∪ 𝑐) ∈ V
293182, 292coex 7160 . . . . . . . 8 (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ V
294 f1oeq1 6165 . . . . . . . . 9 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
295 fveq1 6228 . . . . . . . . . . 11 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓𝑦) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦))
296295neeq1d 2882 . . . . . . . . . 10 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
297296ralbidv 3015 . . . . . . . . 9 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
298294, 297anbi12d 747 . . . . . . . 8 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)))
299293, 298, 1elab2 3386 . . . . . . 7 ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
300216, 290, 299sylanbrc 699 . . . . . 6 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴)
30170adantr 480 . . . . . . . . 9 ((𝜑𝑐𝐶) → 1 ∈ (1...(𝑁 + 1)))
302 fvco3 6314 . . . . . . . . 9 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
303218, 301, 302syl2anc 694 . . . . . . . 8 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
304242fveq2d 6233 . . . . . . . 8 ((𝜑𝑐𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)) = (𝐹‘1))
305303, 304, 2313eqtrd 2689 . . . . . . 7 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀)
306130, 23sseldi 3634 . . . . . . . . . . 11 (𝜑𝑀 ∈ (1...(𝑁 + 1)))
307306adantr 480 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑀 ∈ (1...(𝑁 + 1)))
308 fvco3 6314 . . . . . . . . . 10 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑀 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
309218, 307, 308syl2anc 694 . . . . . . . . 9 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
310251a1i 11 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
311261, 254eleqtrrd 2733 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → 𝑀 ∈ dom 𝑐)
312 funssfv 6247 . . . . . . . . . . 11 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑀 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐𝑀))
313233, 310, 311, 312syl3anc 1366 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐𝑀))
314313fveq2d 6233 . . . . . . . . 9 ((𝜑𝑐𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)) = (𝐹‘(𝑐𝑀)))
315309, 314eqtrd 2685 . . . . . . . 8 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(𝑐𝑀)))
316135fveq1d 6231 . . . . . . . . . . . 12 (𝜑 → (𝐹‘1) = (𝐹‘1))
317316, 230eqtrd 2685 . . . . . . . . . . 11 (𝜑 → (𝐹‘1) = 𝑀)
318317adantr 480 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (𝐹‘1) = 𝑀)
319 id 22 . . . . . . . . . . . . . 14 (𝑦 = 𝑀𝑦 = 𝑀)
320268, 319neeq12d 2884 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → ((𝑐𝑦) ≠ 𝑦 ↔ (𝑐𝑀) ≠ 𝑀))
321320rspcv 3336 . . . . . . . . . . . 12 (𝑀 ∈ (2...(𝑁 + 1)) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦 → (𝑐𝑀) ≠ 𝑀))
322261, 271, 321sylc 65 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → (𝑐𝑀) ≠ 𝑀)
323322necomd 2878 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑀 ≠ (𝑐𝑀))
324318, 323eqnetrd 2890 . . . . . . . . 9 ((𝜑𝑐𝐶) → (𝐹‘1) ≠ (𝑐𝑀))
325130, 262sseldi 3634 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → (𝑐𝑀) ∈ (1...(𝑁 + 1)))
326 f1ocnvfv 6574 . . . . . . . . . . 11 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑐𝑀) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑐𝑀)) = 1 → (𝐹‘1) = (𝑐𝑀)))
327195, 325, 326syl2anc 694 . . . . . . . . . 10 ((𝜑𝑐𝐶) → ((𝐹‘(𝑐𝑀)) = 1 → (𝐹‘1) = (𝑐𝑀)))
328327necon3d 2844 . . . . . . . . 9 ((𝜑𝑐𝐶) → ((𝐹‘1) ≠ (𝑐𝑀) → (𝐹‘(𝑐𝑀)) ≠ 1))
329324, 328mpd 15 . . . . . . . 8 ((𝜑𝑐𝐶) → (𝐹‘(𝑐𝑀)) ≠ 1)
330315, 329eqnetrd 2890 . . . . . . 7 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)
331305, 330jca 553 . . . . . 6 ((𝜑𝑐𝐶) → (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
332 fveq1 6228 . . . . . . . . 9 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘1) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1))
333332eqeq1d 2653 . . . . . . . 8 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘1) = 𝑀 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀))
334 fveq1 6228 . . . . . . . . 9 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔𝑀) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀))
335334neeq1d 2882 . . . . . . . 8 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔𝑀) ≠ 1 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
336333, 335anbi12d 747 . . . . . . 7 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1) ↔ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
337336, 6elrab2 3399 . . . . . 6 ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ∧ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
338300, 331, 337sylanbrc 699 . . . . 5 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵)
339338ex 449 . . . 4 (𝜑 → (𝑐𝐶 → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵))
34030adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
341 f1of1 6174 . . . . . . . 8 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
342340, 341syl 17 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
343 f1of 6175 . . . . . . . . 9 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
344340, 343syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
34575adantrr 753 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
346 fco 6096 . . . . . . . 8 ((𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) → (𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
347344, 345, 346syl2anc 694 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
348218adantrl 752 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
349 cocan1 6586 . . . . . . 7 ((𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ∧ (𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
350342, 347, 348, 349syl3anc 1366 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
351 coass 5692 . . . . . . . 8 ((𝐹𝐹) ∘ 𝑏) = (𝐹 ∘ (𝐹𝑏))
352135coeq1d 5316 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐹) = (𝐹𝐹))
353 f1ococnv1 6203 . . . . . . . . . . . . 13 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
35430, 353syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
355352, 354eqtr3d 2687 . . . . . . . . . . 11 (𝜑 → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
356355adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
357356coeq1d 5316 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝐹) ∘ 𝑏) = (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏))
358 fcoi2 6117 . . . . . . . . . 10 (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
359345, 358syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
360357, 359eqtrd 2685 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝐹) ∘ 𝑏) = 𝑏)
361351, 360syl5eqr 2699 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹 ∘ (𝐹𝑏)) = 𝑏)
362361eqeq1d 2653 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))))
36383adantrr 753 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏)‘1) = 1)
364242adantrl 752 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
365363, 364eqtr4d 2688 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
366 fveq2 6229 . . . . . . . . . . . . . 14 (𝑦 = 1 → ((𝐹𝑏)‘𝑦) = ((𝐹𝑏)‘1))
367 fveq2 6229 . . . . . . . . . . . . . 14 (𝑦 = 1 → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
368366, 367eqeq12d 2666 . . . . . . . . . . . . 13 (𝑦 = 1 → (((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1)))
36963, 368ralsn 4254 . . . . . . . . . . . 12 (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
370365, 369sylibr 224 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
371370biantrurd 528 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))))
372 ralunb 3827 . . . . . . . . . 10 (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
373371, 372syl6bbr 278 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
374187adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹𝑏)‘𝑦))
375374eqcomd 2657 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
376258adantlrl 756 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
377375, 376eqeq12d 2666 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
378377ralbidva 3014 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
379102adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
380379raleqdv 3174 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
381373, 378, 3803bitr3rd 299 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
38265adantrr 753 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
383214adantrl 752 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
384 f1ofn 6176 . . . . . . . . . 10 (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
385383, 384syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
386 eqfnfv 6351 . . . . . . . . 9 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1))) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
387382, 385, 386syl2anc 694 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
388 fnssres 6042 . . . . . . . . . 10 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
389382, 130, 388sylancl 695 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
390205adantrl 752 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
391 f1ofn 6176 . . . . . . . . . 10 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐 Fn (2...(𝑁 + 1)))
392390, 391syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑐 Fn (2...(𝑁 + 1)))
393 eqfnfv 6351 . . . . . . . . 9 ((((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)) ∧ 𝑐 Fn (2...(𝑁 + 1))) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
394389, 392, 393syl2anc 694 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
395381, 387, 3943bitr4d 300 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐))
396 eqcom 2658 . . . . . . 7 (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
397395, 396syl6bb 276 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1)))))
398350, 362, 3973bitr3d 298 . . . . 5 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1)))))
399398ex 449 . . . 4 (𝜑 → ((𝑏𝐵𝑐𝐶) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))))
40012, 19, 194, 339, 399en3d 8034 . . 3 (𝜑𝐵𝐶)
401 hashen 13175 . . . 4 ((𝐵 ∈ Fin ∧ 𝐶 ∈ Fin) → ((#‘𝐵) = (#‘𝐶) ↔ 𝐵𝐶))
40210, 17, 401mp2an 708 . . 3 ((#‘𝐵) = (#‘𝐶) ↔ 𝐵𝐶)
403400, 402sylibr 224 . 2 (𝜑 → (#‘𝐵) = (#‘𝐶))
40420, 21derangen2 31282 . . . . 5 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (𝑆‘(#‘(2...(𝑁 + 1)))))
40520derangval 31275 . . . . . 6 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (#‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}))
40613fveq2i 6232 . . . . . 6 (#‘𝐶) = (#‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)})
407405, 406syl6eqr 2703 . . . . 5 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (#‘𝐶))
408404, 407eqtr3d 2687 . . . 4 ((2...(𝑁 + 1)) ∈ Fin → (𝑆‘(#‘(2...(𝑁 + 1)))) = (#‘𝐶))
40914, 408ax-mp 5 . . 3 (𝑆‘(#‘(2...(𝑁 + 1)))) = (#‘𝐶)
41022, 67syl6eleq 2740 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ‘1))
411 eluzp1p1 11751 . . . . . . . 8 (𝑁 ∈ (ℤ‘1) → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
412410, 411syl 17 . . . . . . 7 (𝜑 → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
413 df-2 11117 . . . . . . . 8 2 = (1 + 1)
414413fveq2i 6232 . . . . . . 7 (ℤ‘2) = (ℤ‘(1 + 1))
415412, 414syl6eleqr 2741 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ (ℤ‘2))
416 hashfz 13252 . . . . . 6 ((𝑁 + 1) ∈ (ℤ‘2) → (#‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
417415, 416syl 17 . . . . 5 (𝜑 → (#‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
41866nncnd 11074 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ ℂ)
419 2cnd 11131 . . . . . 6 (𝜑 → 2 ∈ ℂ)
420 1cnd 10094 . . . . . 6 (𝜑 → 1 ∈ ℂ)
421418, 419, 420subsubd 10458 . . . . 5 (𝜑 → ((𝑁 + 1) − (2 − 1)) = (((𝑁 + 1) − 2) + 1))
422 2m1e1 11173 . . . . . . 7 (2 − 1) = 1
423422oveq2i 6701 . . . . . 6 ((𝑁 + 1) − (2 − 1)) = ((𝑁 + 1) − 1)
42422nncnd 11074 . . . . . . 7 (𝜑𝑁 ∈ ℂ)
425 ax-1cn 10032 . . . . . . 7 1 ∈ ℂ
426 pncan 10325 . . . . . . 7 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
427424, 425, 426sylancl 695 . . . . . 6 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
428423, 427syl5eq 2697 . . . . 5 (𝜑 → ((𝑁 + 1) − (2 − 1)) = 𝑁)
429417, 421, 4283eqtr2d 2691 . . . 4 (𝜑 → (#‘(2...(𝑁 + 1))) = 𝑁)
430429fveq2d 6233 . . 3 (𝜑 → (𝑆‘(#‘(2...(𝑁 + 1)))) = (𝑆𝑁))
431409, 430syl5eqr 2699 . 2 (𝜑 → (#‘𝐶) = (𝑆𝑁))
432403, 431eqtrd 2685 1 (𝜑 → (#‘𝐵) = (𝑆𝑁))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   = wceq 1523   ∈ wcel 2030  {cab 2637   ≠ wne 2823  ∀wral 2941  {crab 2945  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  {csn 4210  {cpr 4212  ⟨cop 4216   class class class wbr 4685   ↦ cmpt 4762   I cid 5052  ◡ccnv 5142  dom cdm 5143   ↾ cres 5145   ∘ ccom 5147  Fun wfun 5920   Fn wfn 5921  ⟶wf 5922  –1-1→wf1 5923  –onto→wfo 5924  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690   ≈ cen 7994  Fincfn 7997  ℂcc 9972  1c1 9975   + caddc 9977   < clt 10112   ≤ cle 10113   − cmin 10304  ℕcn 11058  2c2 11108  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ...cfz 12364  #chash 13157 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-fz 12365  df-hash 13158 This theorem is referenced by:  subfacp1lem6  31293
 Copyright terms: Public domain W3C validator