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

Theorem subfacp1lem5 32329
Description: Lemma for subfacp1 32331. In subfacp1lem6 32330 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 13330 . . . . . . . . 9 (1...(𝑁 + 1)) ∈ Fin
3 deranglem 32311 . . . . . . . . 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 2909 . . . . . . 7 𝐴 ∈ Fin
6 subfacp1lem5.b . . . . . . . 8 𝐵 = {𝑔𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1)}
7 ssrab2 4055 . . . . . . . 8 {𝑔𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1)} ⊆ 𝐴
86, 7eqsstri 4000 . . . . . . 7 𝐵𝐴
9 ssfi 8727 . . . . . . 7 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)
105, 8, 9mp2an 688 . . . . . 6 𝐵 ∈ Fin
1110elexi 3514 . . . . 5 𝐵 ∈ V
1211a1i 11 . . . 4 (𝜑𝐵 ∈ V)
13 subfacp1lem5.c . . . . . . 7 𝐶 = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}
14 fzfi 13330 . . . . . . . 8 (2...(𝑁 + 1)) ∈ Fin
15 deranglem 32311 . . . . . . . 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 2909 . . . . . 6 𝐶 ∈ Fin
1817elexi 3514 . . . . 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 6646 . . . . . . . . . . . . . 14 ( I ↾ 𝐾):𝐾1-1-onto𝐾
2827a1i 11 . . . . . . . . . . . . 13 (𝜑 → ( I ↾ 𝐾):𝐾1-1-onto𝐾)
2920, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2a 32325 . . . . . . . . . . . 12 (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹𝑀) = 1))
3029simp1d 1134 . . . . . . . . . . 11 (𝜑𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
3130adantr 481 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
32 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → 𝑏𝐵)
33 fveq1 6663 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
3433eqeq1d 2823 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
35 fveq1 6663 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑏 → (𝑔𝑀) = (𝑏𝑀))
3635neeq1d 3075 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑏 → ((𝑔𝑀) ≠ 1 ↔ (𝑏𝑀) ≠ 1))
3734, 36anbi12d 630 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3837, 6elrab2 3682 . . . . . . . . . . . . . 14 (𝑏𝐵 ↔ (𝑏𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3932, 38sylib 219 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (𝑏𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
4039simpld 495 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → 𝑏𝐴)
41 vex 3498 . . . . . . . . . . . . 13 𝑏 ∈ V
42 f1oeq1 6598 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
43 fveq1 6663 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
4443neeq1d 3075 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑏𝑦) ≠ 𝑦))
4544ralbidv 3197 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4642, 45anbi12d 630 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦)))
4741, 46, 1elab2 3669 . . . . . . . . . . . 12 (𝑏𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4840, 47sylib 219 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4948simpld 495 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
50 f1oco 6631 . . . . . . . . . 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 584 . . . . . . . . 9 ((𝜑𝑏𝐵) → (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
52 f1of1 6608 . . . . . . . . 9 ((𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
53 df-f1 6354 . . . . . . . . . 10 ((𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ ((𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun (𝐹𝑏)))
5453simprbi 497 . . . . . . . . 9 ((𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun (𝐹𝑏))
5551, 52, 543syl 18 . . . . . . . 8 ((𝜑𝑏𝐵) → Fun (𝐹𝑏))
56 f1ofn 6610 . . . . . . . . . . 11 ((𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
57 fnresdm 6460 . . . . . . . . . . 11 ((𝐹𝑏) Fn (1...(𝑁 + 1)) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))) = (𝐹𝑏))
58 f1oeq1 6598 . . . . . . . . . . 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 258 . . . . . . . . 9 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
61 f1ofo 6616 . . . . . . . . 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 10626 . . . . . . . . . . 11 1 ∈ V
6463, 63f1osn 6648 . . . . . . . . . 10 {⟨1, 1⟩}:{1}–1-1-onto→{1}
6551, 56syl 17 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
6622peano2nnd 11644 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ ℕ)
67 nnuz 12270 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
6866, 67eleqtrdi 2923 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
69 eluzfz1 12904 . . . . . . . . . . . . . . 15 ((𝑁 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑁 + 1)))
7068, 69syl 17 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ (1...(𝑁 + 1)))
7170adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → 1 ∈ (1...(𝑁 + 1)))
72 fnressn 6913 . . . . . . . . . . . . 13 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏) ↾ {1}) = {⟨1, ((𝐹𝑏)‘1)⟩})
7365, 71, 72syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}) = {⟨1, ((𝐹𝑏)‘1)⟩})
74 f1of 6609 . . . . . . . . . . . . . . . . 17 (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
7549, 74syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
76 fvco3 6754 . . . . . . . . . . . . . . . 16 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏)‘1) = (𝐹‘(𝑏‘1)))
7775, 71, 76syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → ((𝐹𝑏)‘1) = (𝐹‘(𝑏‘1)))
7839simprd 496 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1))
7978simpld 495 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → (𝑏‘1) = 𝑀)
8079fveq2d 6668 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝐹‘(𝑏‘1)) = (𝐹𝑀))
8129simp3d 1136 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝑀) = 1)
8281adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝐹𝑀) = 1)
8377, 80, 823eqtrd 2860 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → ((𝐹𝑏)‘1) = 1)
8483opeq2d 4804 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → ⟨1, ((𝐹𝑏)‘1)⟩ = ⟨1, 1⟩)
8584sneqd 4571 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → {⟨1, ((𝐹𝑏)‘1)⟩} = {⟨1, 1⟩})
8673, 85eqtrd 2856 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}) = {⟨1, 1⟩})
87 f1oeq1 6598 . . . . . . . . . . 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 259 . . . . . . . . 9 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1})
90 f1ofo 6616 . . . . . . . . 9 (((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1} → ((𝐹𝑏) ↾ {1}):{1}–onto→{1})
9189, 90syl 17 . . . . . . . 8 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}):{1}–onto→{1})
92 resdif 6629 . . . . . . . 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 1363 . . . . . . 7 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
94 fzsplit 12923 . . . . . . . . . . . 12 (1 ∈ (1...(𝑁 + 1)) → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
9570, 94syl 17 . . . . . . . . . . 11 (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
96 1z 12001 . . . . . . . . . . . . 13 1 ∈ ℤ
97 fzsn 12939 . . . . . . . . . . . . 13 (1 ∈ ℤ → (1...1) = {1})
9896, 97ax-mp 5 . . . . . . . . . . . 12 (1...1) = {1}
99 1p1e2 11751 . . . . . . . . . . . . 13 (1 + 1) = 2
10099oveq1i 7155 . . . . . . . . . . . 12 ((1 + 1)...(𝑁 + 1)) = (2...(𝑁 + 1))
10198, 100uneq12i 4136 . . . . . . . . . . 11 ((1...1) ∪ ((1 + 1)...(𝑁 + 1))) = ({1} ∪ (2...(𝑁 + 1)))
10295, 101syl6req 2873 . . . . . . . . . 10 (𝜑 → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
10370snssd 4736 . . . . . . . . . . 11 (𝜑 → {1} ⊆ (1...(𝑁 + 1)))
104 incom 4177 . . . . . . . . . . . 12 ({1} ∩ (2...(𝑁 + 1))) = ((2...(𝑁 + 1)) ∩ {1})
105 1lt2 11797 . . . . . . . . . . . . . . 15 1 < 2
106 1re 10630 . . . . . . . . . . . . . . . 16 1 ∈ ℝ
107 2re 11700 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
108106, 107ltnlei 10750 . . . . . . . . . . . . . . 15 (1 < 2 ↔ ¬ 2 ≤ 1)
109105, 108mpbi 231 . . . . . . . . . . . . . 14 ¬ 2 ≤ 1
110 elfzle1 12900 . . . . . . . . . . . . . 14 (1 ∈ (2...(𝑁 + 1)) → 2 ≤ 1)
111109, 110mto 198 . . . . . . . . . . . . 13 ¬ 1 ∈ (2...(𝑁 + 1))
112 disjsn 4641 . . . . . . . . . . . . 13 (((2...(𝑁 + 1)) ∩ {1}) = ∅ ↔ ¬ 1 ∈ (2...(𝑁 + 1)))
113111, 112mpbir 232 . . . . . . . . . . . 12 ((2...(𝑁 + 1)) ∩ {1}) = ∅
114104, 113eqtri 2844 . . . . . . . . . . 11 ({1} ∩ (2...(𝑁 + 1))) = ∅
115 uneqdifeq 4436 . . . . . . . . . . 11 (({1} ⊆ (1...(𝑁 + 1)) ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅) → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
116103, 114, 115sylancl 586 . . . . . . . . . 10 (𝜑 → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
117102, 116mpbid 233 . . . . . . . . 9 (𝜑 → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
118117adantr 481 . . . . . . . 8 ((𝜑𝑏𝐵) → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
119 reseq2 5842 . . . . . . . . . 10 (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})) = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
120 f1oeq1 6598 . . . . . . . . . 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 6599 . . . . . . . . 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 6600 . . . . . . . . 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 306 . . . . . . . 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 233 . . . . . 6 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
12775adantr 481 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
128 fzp1ss 12948 . . . . . . . . . . . 12 (1 ∈ ℤ → ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1)))
12996, 128ax-mp 5 . . . . . . . . . . 11 ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
130100, 129eqsstrri 4001 . . . . . . . . . 10 (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
131 simpr 485 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (2...(𝑁 + 1)))
132130, 131sseldi 3964 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
133 fvco3 6754 . . . . . . . . 9 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (𝐹‘(𝑏𝑦)))
134127, 132, 133syl2anc 584 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (𝐹‘(𝑏𝑦)))
13520, 21, 1, 22, 23, 24, 25, 6, 26subfacp1lem4 32328 . . . . . . . . . . . 12 (𝜑𝐹 = 𝐹)
136135fveq1d 6666 . . . . . . . . . . 11 (𝜑 → (𝐹𝑦) = (𝐹𝑦))
137136ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) = (𝐹𝑦))
13878simprd 496 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝑏𝑀) ≠ 1)
139138, 82neeqtrrd 3090 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → (𝑏𝑀) ≠ (𝐹𝑀))
140139adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑀) ≠ (𝐹𝑀))
141 fveq2 6664 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → (𝑏𝑦) = (𝑏𝑀))
142 fveq2 6664 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → (𝐹𝑦) = (𝐹𝑀))
143141, 142neeq12d 3077 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → ((𝑏𝑦) ≠ (𝐹𝑦) ↔ (𝑏𝑀) ≠ (𝐹𝑀)))
144140, 143syl5ibrcom 248 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑏𝑦) ≠ (𝐹𝑦)))
145130sseli 3962 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (2...(𝑁 + 1)) → 𝑦 ∈ (1...(𝑁 + 1)))
14648simprd 496 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦)
147146r19.21bi 3208 . . . . . . . . . . . . . . . 16 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏𝑦) ≠ 𝑦)
148145, 147sylan2 592 . . . . . . . . . . . . . . 15 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ≠ 𝑦)
149148adantrr 713 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑏𝑦) ≠ 𝑦)
15025eleq2i 2904 . . . . . . . . . . . . . . . . 17 (𝑦𝐾𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}))
151 eldifsn 4713 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀))
152150, 151bitri 276 . . . . . . . . . . . . . . . 16 (𝑦𝐾 ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀))
15320, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2b 32326 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐾) → (𝐹𝑦) = (( I ↾ 𝐾)‘𝑦))
154 fvresi 6928 . . . . . . . . . . . . . . . . . 18 (𝑦𝐾 → (( I ↾ 𝐾)‘𝑦) = 𝑦)
155154adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐾) → (( I ↾ 𝐾)‘𝑦) = 𝑦)
156153, 155eqtrd 2856 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐾) → (𝐹𝑦) = 𝑦)
157152, 156sylan2br 594 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
158157adantlr 711 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
159149, 158neeqtrrd 3090 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑏𝑦) ≠ (𝐹𝑦))
160159expr 457 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦𝑀 → (𝑏𝑦) ≠ (𝐹𝑦)))
161144, 160pm2.61dne 3103 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ≠ (𝐹𝑦))
162161necomd 3071 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (𝑏𝑦))
163137, 162eqnetrd 3083 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (𝑏𝑦))
16431adantr 481 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
165 ffvelrn 6842 . . . . . . . . . . . 12 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏𝑦) ∈ (1...(𝑁 + 1)))
16675, 145, 165syl2an 595 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ∈ (1...(𝑁 + 1)))
167 f1ocnvfv 7026 . . . . . . . . . . 11 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑏𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑏𝑦)) = 𝑦 → (𝐹𝑦) = (𝑏𝑦)))
168164, 166, 167syl2anc 584 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹‘(𝑏𝑦)) = 𝑦 → (𝐹𝑦) = (𝑏𝑦)))
169168necon3d 3037 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑦) ≠ (𝑏𝑦) → (𝐹‘(𝑏𝑦)) ≠ 𝑦))
170163, 169mpd 15 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘(𝑏𝑦)) ≠ 𝑦)
171134, 170eqnetrd 3083 . . . . . . 7 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) ≠ 𝑦)
172171ralrimiva 3182 . . . . . 6 ((𝜑𝑏𝐵) → ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦)
173 f1of 6609 . . . . . . . . . . . . 13 (( I ↾ 𝐾):𝐾1-1-onto𝐾 → ( I ↾ 𝐾):𝐾𝐾)
17427, 173ax-mp 5 . . . . . . . . . . . 12 ( I ↾ 𝐾):𝐾𝐾
175 difexg 5223 . . . . . . . . . . . . . 14 ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V)
17614, 175ax-mp 5 . . . . . . . . . . . . 13 ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V
17725, 176eqeltri 2909 . . . . . . . . . . . 12 𝐾 ∈ V
178 fex 6981 . . . . . . . . . . . 12 ((( I ↾ 𝐾):𝐾𝐾𝐾 ∈ V) → ( I ↾ 𝐾) ∈ V)
179174, 177, 178mp2an 688 . . . . . . . . . . 11 ( I ↾ 𝐾) ∈ V
180 prex 5324 . . . . . . . . . . 11 {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
181179, 180unex 7457 . . . . . . . . . 10 (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
18226, 181eqeltri 2909 . . . . . . . . 9 𝐹 ∈ V
183182, 41coex 7623 . . . . . . . 8 (𝐹𝑏) ∈ V
184183resex 5893 . . . . . . 7 ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ V
185 f1oeq1 6598 . . . . . . . 8 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
186 fveq1 6663 . . . . . . . . . . 11 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (𝑓𝑦) = (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
187 fvres 6683 . . . . . . . . . . 11 (𝑦 ∈ (2...(𝑁 + 1)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹𝑏)‘𝑦))
188186, 187sylan9eq 2876 . . . . . . . . . 10 ((𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑓𝑦) = ((𝐹𝑏)‘𝑦))
189188neeq1d 3075 . . . . . . . . 9 ((𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝑓𝑦) ≠ 𝑦 ↔ ((𝐹𝑏)‘𝑦) ≠ 𝑦))
190189ralbidva 3196 . . . . . . . 8 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦))
191185, 190anbi12d 630 . . . . . . 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 3669 . . . . . 6 (((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶 ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦))
193126, 172, 192sylanbrc 583 . . . . 5 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶)
194193ex 413 . . . 4 (𝜑 → (𝑏𝐵 → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶))
19530adantr 481 . . . . . . . 8 ((𝜑𝑐𝐶) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
196 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑐𝐶) → 𝑐𝐶)
197 vex 3498 . . . . . . . . . . . . 13 𝑐 ∈ V
198 f1oeq1 6598 . . . . . . . . . . . . . 14 (𝑓 = 𝑐 → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
199 fveq1 6663 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑐 → (𝑓𝑦) = (𝑐𝑦))
200199neeq1d 3075 . . . . . . . . . . . . . . 15 (𝑓 = 𝑐 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑐𝑦) ≠ 𝑦))
201200ralbidv 3197 . . . . . . . . . . . . . 14 (𝑓 = 𝑐 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
202198, 201anbi12d 630 . . . . . . . . . . . . 13 (𝑓 = 𝑐 → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦)))
203197, 202, 13elab2 3669 . . . . . . . . . . . 12 (𝑐𝐶 ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
204196, 203sylib 219 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
205204simpld 495 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
206 f1oun 6628 . . . . . . . . . . 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 701 . . . . . . . . . 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 587 . . . . . . . . 9 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
209 f1oeq2 6599 . . . . . . . . . . . 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 6600 . . . . . . . . . . . 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 280 . . . . . . . . . . 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 477 . . . . . . . . 9 ((𝜑 ∧ ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1)))) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
214208, 213syldan 591 . . . . . . . 8 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
215 f1oco 6631 . . . . . . . 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 584 . . . . . . 7 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
217 f1of 6609 . . . . . . . . . . 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 6754 . . . . . . . . . 10 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
220218, 219sylan 580 . . . . . . . . 9 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
221136ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) = (𝐹𝑦))
222 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
223102ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
224222, 223eleqtrrd 2916 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))))
225 elun 4124 . . . . . . . . . . . . 13 (𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
226224, 225sylib 219 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
227 nelne2 3115 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → 𝑀 ≠ 1)
22823, 111, 227sylancl 586 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ≠ 1)
229228adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → 𝑀 ≠ 1)
23029simp2d 1135 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹‘1) = 𝑀)
231230adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → (𝐹‘1) = 𝑀)
232 f1ofun 6611 . . . . . . . . . . . . . . . . . . 19 (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
233208, 232syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐶) → Fun ({⟨1, 1⟩} ∪ 𝑐))
234 ssun1 4147 . . . . . . . . . . . . . . . . . . 19 {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐)
23563snid 4593 . . . . . . . . . . . . . . . . . . . 20 1 ∈ {1}
23663dmsnop 6067 . . . . . . . . . . . . . . . . . . . 20 dom {⟨1, 1⟩} = {1}
237235, 236eleqtrri 2912 . . . . . . . . . . . . . . . . . . 19 1 ∈ dom {⟨1, 1⟩}
238 funssfv 6685 . . . . . . . . . . . . . . . . . . 19 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 1 ∈ dom {⟨1, 1⟩}) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
239234, 237, 238mp3an23 1444 . . . . . . . . . . . . . . . . . 18 (Fun ({⟨1, 1⟩} ∪ 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
240233, 239syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
24163, 63fvsn 6936 . . . . . . . . . . . . . . . . 17 ({⟨1, 1⟩}‘1) = 1
242240, 241syl6eq 2872 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
243229, 231, 2423netr4d 3093 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐶) → (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1))
244 elsni 4576 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {1} → 𝑦 = 1)
245244fveq2d 6668 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (𝐹𝑦) = (𝐹‘1))
246244fveq2d 6668 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
247245, 246neeq12d 3077 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → ((𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1)))
248243, 247syl5ibrcom 248 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐶) → (𝑦 ∈ {1} → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
249248imp 407 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ {1}) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
250233adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
251 ssun2 4148 . . . . . . . . . . . . . . . . 17 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐)
252251a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
253 f1odm 6613 . . . . . . . . . . . . . . . . . . 19 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → dom 𝑐 = (2...(𝑁 + 1)))
254205, 253syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐶) → dom 𝑐 = (2...(𝑁 + 1)))
255254eleq2d 2898 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐶) → (𝑦 ∈ dom 𝑐𝑦 ∈ (2...(𝑁 + 1))))
256255biimpar 478 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ dom 𝑐)
257 funssfv 6685 . . . . . . . . . . . . . . . 16 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑦 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
258250, 252, 256, 257syl3anc 1363 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
259 f1of 6609 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
260205, 259syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐶) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
26123adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
262260, 261ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐶) → (𝑐𝑀) ∈ (2...(𝑁 + 1)))
263 nelne2 3115 . . . . . . . . . . . . . . . . . . . 20 (((𝑐𝑀) ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ 1)
264262, 111, 263sylancl 586 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐶) → (𝑐𝑀) ≠ 1)
265264adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ 1)
26681ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑀) = 1)
267265, 266neeqtrrd 3090 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ (𝐹𝑀))
268 fveq2 6664 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑀 → (𝑐𝑦) = (𝑐𝑀))
269268, 142neeq12d 3077 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑀 → ((𝑐𝑦) ≠ (𝐹𝑦) ↔ (𝑐𝑀) ≠ (𝐹𝑀)))
270267, 269syl5ibrcom 248 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑐𝑦) ≠ (𝐹𝑦)))
271204simprd 496 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐶) → ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦)
272271r19.21bi 3208 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑦) ≠ 𝑦)
273272adantrr 713 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑐𝑦) ≠ 𝑦)
274157adantlr 711 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
275273, 274neeqtrrd 3090 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑐𝑦) ≠ (𝐹𝑦))
276275expr 457 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦𝑀 → (𝑐𝑦) ≠ (𝐹𝑦)))
277270, 276pm2.61dne 3103 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑦) ≠ (𝐹𝑦))
278258, 277eqnetrd 3083 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ≠ (𝐹𝑦))
279278necomd 3071 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
280249, 279jaodan 951 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1)))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
281226, 280syldan 591 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
282221, 281eqnetrd 3083 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
283195adantr 481 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
284218ffvelrnda 6844 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1)))
285 f1ocnvfv 7026 . . . . . . . . . . . 12 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (𝐹𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
286283, 284, 285syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (𝐹𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
287286necon3d 3037 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦))
288282, 287mpd 15 . . . . . . . . 9 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦)
289220, 288eqnetrd 3083 . . . . . . . 8 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
290289ralrimiva 3182 . . . . . . 7 ((𝜑𝑐𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
291 snex 5323 . . . . . . . . . 10 {⟨1, 1⟩} ∈ V
292291, 197unex 7457 . . . . . . . . 9 ({⟨1, 1⟩} ∪ 𝑐) ∈ V
293182, 292coex 7623 . . . . . . . 8 (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ V
294 f1oeq1 6598 . . . . . . . . 9 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
295 fveq1 6663 . . . . . . . . . . 11 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓𝑦) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦))
296295neeq1d 3075 . . . . . . . . . 10 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
297296ralbidv 3197 . . . . . . . . 9 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
298294, 297anbi12d 630 . . . . . . . 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 3669 . . . . . . 7 ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
300216, 290, 299sylanbrc 583 . . . . . 6 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴)
30170adantr 481 . . . . . . . . 9 ((𝜑𝑐𝐶) → 1 ∈ (1...(𝑁 + 1)))
302 fvco3 6754 . . . . . . . . 9 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
303218, 301, 302syl2anc 584 . . . . . . . 8 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
304242fveq2d 6668 . . . . . . . 8 ((𝜑𝑐𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)) = (𝐹‘1))
305303, 304, 2313eqtrd 2860 . . . . . . 7 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀)
306130, 23sseldi 3964 . . . . . . . . . . 11 (𝜑𝑀 ∈ (1...(𝑁 + 1)))
307306adantr 481 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑀 ∈ (1...(𝑁 + 1)))
308 fvco3 6754 . . . . . . . . . 10 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑀 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
309218, 307, 308syl2anc 584 . . . . . . . . 9 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
310251a1i 11 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
311261, 254eleqtrrd 2916 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → 𝑀 ∈ dom 𝑐)
312 funssfv 6685 . . . . . . . . . . 11 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑀 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐𝑀))
313233, 310, 311, 312syl3anc 1363 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐𝑀))
314313fveq2d 6668 . . . . . . . . 9 ((𝜑𝑐𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)) = (𝐹‘(𝑐𝑀)))
315309, 314eqtrd 2856 . . . . . . . 8 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(𝑐𝑀)))
316135fveq1d 6666 . . . . . . . . . . . 12 (𝜑 → (𝐹‘1) = (𝐹‘1))
317316, 230eqtrd 2856 . . . . . . . . . . 11 (𝜑 → (𝐹‘1) = 𝑀)
318317adantr 481 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (𝐹‘1) = 𝑀)
319 id 22 . . . . . . . . . . . . . 14 (𝑦 = 𝑀𝑦 = 𝑀)
320268, 319neeq12d 3077 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → ((𝑐𝑦) ≠ 𝑦 ↔ (𝑐𝑀) ≠ 𝑀))
321320rspcv 3617 . . . . . . . . . . . 12 (𝑀 ∈ (2...(𝑁 + 1)) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦 → (𝑐𝑀) ≠ 𝑀))
322261, 271, 321sylc 65 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → (𝑐𝑀) ≠ 𝑀)
323322necomd 3071 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑀 ≠ (𝑐𝑀))
324318, 323eqnetrd 3083 . . . . . . . . 9 ((𝜑𝑐𝐶) → (𝐹‘1) ≠ (𝑐𝑀))
325130, 262sseldi 3964 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → (𝑐𝑀) ∈ (1...(𝑁 + 1)))
326 f1ocnvfv 7026 . . . . . . . . . . 11 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑐𝑀) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑐𝑀)) = 1 → (𝐹‘1) = (𝑐𝑀)))
327195, 325, 326syl2anc 584 . . . . . . . . . 10 ((𝜑𝑐𝐶) → ((𝐹‘(𝑐𝑀)) = 1 → (𝐹‘1) = (𝑐𝑀)))
328327necon3d 3037 . . . . . . . . 9 ((𝜑𝑐𝐶) → ((𝐹‘1) ≠ (𝑐𝑀) → (𝐹‘(𝑐𝑀)) ≠ 1))
329324, 328mpd 15 . . . . . . . 8 ((𝜑𝑐𝐶) → (𝐹‘(𝑐𝑀)) ≠ 1)
330315, 329eqnetrd 3083 . . . . . . 7 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)
331305, 330jca 512 . . . . . 6 ((𝜑𝑐𝐶) → (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
332 fveq1 6663 . . . . . . . . 9 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘1) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1))
333332eqeq1d 2823 . . . . . . . 8 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘1) = 𝑀 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀))
334 fveq1 6663 . . . . . . . . 9 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔𝑀) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀))
335334neeq1d 3075 . . . . . . . 8 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔𝑀) ≠ 1 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
336333, 335anbi12d 630 . . . . . . 7 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1) ↔ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
337336, 6elrab2 3682 . . . . . 6 ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ∧ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
338300, 331, 337sylanbrc 583 . . . . 5 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵)
339338ex 413 . . . 4 (𝜑 → (𝑐𝐶 → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵))
34030adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
341 f1of1 6608 . . . . . . . 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 6609 . . . . . . . . 9 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
344340, 343syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
34575adantrr 713 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
346 fco 6525 . . . . . . . 8 ((𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) → (𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
347344, 345, 346syl2anc 584 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
348218adantrl 712 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
349 cocan1 7038 . . . . . . 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 1363 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
351 coass 6112 . . . . . . . 8 ((𝐹𝐹) ∘ 𝑏) = (𝐹 ∘ (𝐹𝑏))
352135coeq1d 5726 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐹) = (𝐹𝐹))
353 f1ococnv1 6637 . . . . . . . . . . . . 13 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
35430, 353syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
355352, 354eqtr3d 2858 . . . . . . . . . . 11 (𝜑 → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
356355adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
357356coeq1d 5726 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝐹) ∘ 𝑏) = (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏))
358 fcoi2 6547 . . . . . . . . . 10 (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
359345, 358syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
360357, 359eqtrd 2856 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝐹) ∘ 𝑏) = 𝑏)
361351, 360syl5eqr 2870 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹 ∘ (𝐹𝑏)) = 𝑏)
362361eqeq1d 2823 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))))
36383adantrr 713 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏)‘1) = 1)
364242adantrl 712 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
365363, 364eqtr4d 2859 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
366 fveq2 6664 . . . . . . . . . . . . . 14 (𝑦 = 1 → ((𝐹𝑏)‘𝑦) = ((𝐹𝑏)‘1))
367 fveq2 6664 . . . . . . . . . . . . . 14 (𝑦 = 1 → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
368366, 367eqeq12d 2837 . . . . . . . . . . . . 13 (𝑦 = 1 → (((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1)))
36963, 368ralsn 4613 . . . . . . . . . . . 12 (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
370365, 369sylibr 235 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
371370biantrurd 533 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))))
372 ralunb 4166 . . . . . . . . . 10 (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
373371, 372syl6bbr 290 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
374187adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹𝑏)‘𝑦))
375374eqcomd 2827 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
376258adantlrl 716 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
377375, 376eqeq12d 2837 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
378377ralbidva 3196 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
379102adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
380379raleqdv 3416 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
381373, 378, 3803bitr3rd 311 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
38265adantrr 713 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
383214adantrl 712 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
384 f1ofn 6610 . . . . . . . . . 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 6795 . . . . . . . . 9 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1))) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
387382, 385, 386syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
388 fnssres 6464 . . . . . . . . . 10 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
389382, 130, 388sylancl 586 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
390205adantrl 712 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
391 f1ofn 6610 . . . . . . . . . 10 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐 Fn (2...(𝑁 + 1)))
392390, 391syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑐 Fn (2...(𝑁 + 1)))
393 eqfnfv 6795 . . . . . . . . 9 ((((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)) ∧ 𝑐 Fn (2...(𝑁 + 1))) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
394389, 392, 393syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
395381, 387, 3943bitr4d 312 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐))
396 eqcom 2828 . . . . . . 7 (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
397395, 396syl6bb 288 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1)))))
398350, 362, 3973bitr3d 310 . . . . 5 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1)))))
399398ex 413 . . . 4 (𝜑 → ((𝑏𝐵𝑐𝐶) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))))
40012, 19, 194, 339, 399en3d 8535 . . 3 (𝜑𝐵𝐶)
401 hashen 13697 . . . 4 ((𝐵 ∈ Fin ∧ 𝐶 ∈ Fin) → ((♯‘𝐵) = (♯‘𝐶) ↔ 𝐵𝐶))
40210, 17, 401mp2an 688 . . 3 ((♯‘𝐵) = (♯‘𝐶) ↔ 𝐵𝐶)
403400, 402sylibr 235 . 2 (𝜑 → (♯‘𝐵) = (♯‘𝐶))
40420, 21derangen2 32319 . . . . 5 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (𝑆‘(♯‘(2...(𝑁 + 1)))))
40520derangval 32312 . . . . . 6 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}))
40613fveq2i 6667 . . . . . 6 (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)})
407405, 406syl6eqr 2874 . . . . 5 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘𝐶))
408404, 407eqtr3d 2858 . . . 4 ((2...(𝑁 + 1)) ∈ Fin → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶))
40914, 408ax-mp 5 . . 3 (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶)
41022, 67eleqtrdi 2923 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ‘1))
411 eluzp1p1 12259 . . . . . . . 8 (𝑁 ∈ (ℤ‘1) → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
412410, 411syl 17 . . . . . . 7 (𝜑 → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
413 df-2 11689 . . . . . . . 8 2 = (1 + 1)
414413fveq2i 6667 . . . . . . 7 (ℤ‘2) = (ℤ‘(1 + 1))
415412, 414eleqtrrdi 2924 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ (ℤ‘2))
416 hashfz 13778 . . . . . 6 ((𝑁 + 1) ∈ (ℤ‘2) → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
417415, 416syl 17 . . . . 5 (𝜑 → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
41866nncnd 11643 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ ℂ)
419 2cnd 11704 . . . . . 6 (𝜑 → 2 ∈ ℂ)
420 1cnd 10625 . . . . . 6 (𝜑 → 1 ∈ ℂ)
421418, 419, 420subsubd 11014 . . . . 5 (𝜑 → ((𝑁 + 1) − (2 − 1)) = (((𝑁 + 1) − 2) + 1))
422 2m1e1 11752 . . . . . . 7 (2 − 1) = 1
423422oveq2i 7156 . . . . . 6 ((𝑁 + 1) − (2 − 1)) = ((𝑁 + 1) − 1)
42422nncnd 11643 . . . . . . 7 (𝜑𝑁 ∈ ℂ)
425 ax-1cn 10584 . . . . . . 7 1 ∈ ℂ
426 pncan 10881 . . . . . . 7 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
427424, 425, 426sylancl 586 . . . . . 6 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
428423, 427syl5eq 2868 . . . . 5 (𝜑 → ((𝑁 + 1) − (2 − 1)) = 𝑁)
429417, 421, 4283eqtr2d 2862 . . . 4 (𝜑 → (♯‘(2...(𝑁 + 1))) = 𝑁)
430429fveq2d 6668 . . 3 (𝜑 → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (𝑆𝑁))
431409, 430syl5eqr 2870 . 2 (𝜑 → (♯‘𝐶) = (𝑆𝑁))
432403, 431eqtrd 2856 1 (𝜑 → (♯‘𝐵) = (𝑆𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105  {cab 2799  wne 3016  wral 3138  {crab 3142  Vcvv 3495  cdif 3932  cun 3933  cin 3934  wss 3935  c0 4290  {csn 4559  {cpr 4561  cop 4565   class class class wbr 5058  cmpt 5138   I cid 5453  ccnv 5548  dom cdm 5549  cres 5551  ccom 5553  Fun wfun 6343   Fn wfn 6344  wf 6345  1-1wf1 6346  ontowfo 6347  1-1-ontowf1o 6348  cfv 6349  (class class class)co 7145  cen 8495  Fincfn 8498  cc 10524  1c1 10527   + caddc 10529   < clt 10664  cle 10665  cmin 10859  cn 11627  2c2 11681  0cn0 11886  cz 11970  cuz 12232  ...cfz 12882  chash 13680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-2o 8094  df-oadd 8097  df-er 8279  df-map 8398  df-pm 8399  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-dju 9319  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-2 11689  df-n0 11887  df-xnn0 11957  df-z 11971  df-uz 12233  df-fz 12883  df-hash 13681
This theorem is referenced by:  subfacp1lem6  32330
  Copyright terms: Public domain W3C validator