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 30226
Description: Lemma for subfacp1 30228. In subfacp1lem6 30227 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 12588 . . . . . . . . 9 (1...(𝑁 + 1)) ∈ Fin
3 deranglem 30208 . . . . . . . . 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 2683 . . . . . . 7 𝐴 ∈ Fin
6 subfacp1lem5.b . . . . . . . 8 𝐵 = {𝑔𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1)}
7 ssrab2 3649 . . . . . . . 8 {𝑔𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1)} ⊆ 𝐴
86, 7eqsstri 3597 . . . . . . 7 𝐵𝐴
9 ssfi 8042 . . . . . . 7 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)
105, 8, 9mp2an 703 . . . . . 6 𝐵 ∈ Fin
1110elexi 3185 . . . . 5 𝐵 ∈ V
1211a1i 11 . . . 4 (𝜑𝐵 ∈ V)
13 subfacp1lem5.c . . . . . . 7 𝐶 = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}
14 fzfi 12588 . . . . . . . 8 (2...(𝑁 + 1)) ∈ Fin
15 deranglem 30208 . . . . . . . 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 2683 . . . . . 6 𝐶 ∈ Fin
1817elexi 3185 . . . . 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 6071 . . . . . . . . . . . . . 14 ( I ↾ 𝐾):𝐾1-1-onto𝐾
2827a1i 11 . . . . . . . . . . . . 13 (𝜑 → ( I ↾ 𝐾):𝐾1-1-onto𝐾)
2920, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2a 30222 . . . . . . . . . . . 12 (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹𝑀) = 1))
3029simp1d 1065 . . . . . . . . . . 11 (𝜑𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
3130adantr 479 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
32 simpr 475 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → 𝑏𝐵)
33 fveq1 6087 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
3433eqeq1d 2611 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
35 fveq1 6087 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑏 → (𝑔𝑀) = (𝑏𝑀))
3635neeq1d 2840 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑏 → ((𝑔𝑀) ≠ 1 ↔ (𝑏𝑀) ≠ 1))
3734, 36anbi12d 742 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3837, 6elrab2 3332 . . . . . . . . . . . . . 14 (𝑏𝐵 ↔ (𝑏𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3932, 38sylib 206 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (𝑏𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
4039simpld 473 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → 𝑏𝐴)
41 vex 3175 . . . . . . . . . . . . 13 𝑏 ∈ V
42 f1oeq1 6025 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
43 fveq1 6087 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
4443neeq1d 2840 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑏𝑦) ≠ 𝑦))
4544ralbidv 2968 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4642, 45anbi12d 742 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦)))
4741, 46, 1elab2 3322 . . . . . . . . . . . 12 (𝑏𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4840, 47sylib 206 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4948simpld 473 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
50 f1oco 6057 . . . . . . . . . 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 690 . . . . . . . . 9 ((𝜑𝑏𝐵) → (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
52 f1of1 6034 . . . . . . . . 9 ((𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
53 df-f1 5795 . . . . . . . . . 10 ((𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ ((𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun (𝐹𝑏)))
5453simprbi 478 . . . . . . . . 9 ((𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun (𝐹𝑏))
5551, 52, 543syl 18 . . . . . . . 8 ((𝜑𝑏𝐵) → Fun (𝐹𝑏))
56 f1ofn 6036 . . . . . . . . . . 11 ((𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
57 fnresdm 5900 . . . . . . . . . . 11 ((𝐹𝑏) Fn (1...(𝑁 + 1)) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))) = (𝐹𝑏))
58 f1oeq1 6025 . . . . . . . . . . 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 245 . . . . . . . . 9 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
61 f1ofo 6042 . . . . . . . . 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 9891 . . . . . . . . . . 11 1 ∈ V
6463, 63f1osn 6073 . . . . . . . . . 10 {⟨1, 1⟩}:{1}–1-1-onto→{1}
6551, 56syl 17 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
6622peano2nnd 10884 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ ℕ)
67 nnuz 11555 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
6866, 67syl6eleq 2697 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
69 eluzfz1 12174 . . . . . . . . . . . . . . 15 ((𝑁 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑁 + 1)))
7068, 69syl 17 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ (1...(𝑁 + 1)))
7170adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → 1 ∈ (1...(𝑁 + 1)))
72 fnressn 6308 . . . . . . . . . . . . 13 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏) ↾ {1}) = {⟨1, ((𝐹𝑏)‘1)⟩})
7365, 71, 72syl2anc 690 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}) = {⟨1, ((𝐹𝑏)‘1)⟩})
74 f1of 6035 . . . . . . . . . . . . . . . . 17 (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
7549, 74syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
76 fvco3 6170 . . . . . . . . . . . . . . . 16 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏)‘1) = (𝐹‘(𝑏‘1)))
7775, 71, 76syl2anc 690 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → ((𝐹𝑏)‘1) = (𝐹‘(𝑏‘1)))
7839simprd 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1))
7978simpld 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → (𝑏‘1) = 𝑀)
8079fveq2d 6092 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝐹‘(𝑏‘1)) = (𝐹𝑀))
8129simp3d 1067 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝑀) = 1)
8281adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝐹𝑀) = 1)
8377, 80, 823eqtrd 2647 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → ((𝐹𝑏)‘1) = 1)
8483opeq2d 4341 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → ⟨1, ((𝐹𝑏)‘1)⟩ = ⟨1, 1⟩)
8584sneqd 4136 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → {⟨1, ((𝐹𝑏)‘1)⟩} = {⟨1, 1⟩})
8673, 85eqtrd 2643 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}) = {⟨1, 1⟩})
87 f1oeq1 6025 . . . . . . . . . . 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 246 . . . . . . . . 9 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1})
90 f1ofo 6042 . . . . . . . . 9 (((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1} → ((𝐹𝑏) ↾ {1}):{1}–onto→{1})
9189, 90syl 17 . . . . . . . 8 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}):{1}–onto→{1})
92 resdif 6055 . . . . . . . 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 1317 . . . . . . 7 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
94 fzsplit 12193 . . . . . . . . . . . 12 (1 ∈ (1...(𝑁 + 1)) → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
9570, 94syl 17 . . . . . . . . . . 11 (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
96 1z 11240 . . . . . . . . . . . . 13 1 ∈ ℤ
97 fzsn 12209 . . . . . . . . . . . . 13 (1 ∈ ℤ → (1...1) = {1})
9896, 97ax-mp 5 . . . . . . . . . . . 12 (1...1) = {1}
99 1p1e2 10981 . . . . . . . . . . . . 13 (1 + 1) = 2
10099oveq1i 6537 . . . . . . . . . . . 12 ((1 + 1)...(𝑁 + 1)) = (2...(𝑁 + 1))
10198, 100uneq12i 3726 . . . . . . . . . . 11 ((1...1) ∪ ((1 + 1)...(𝑁 + 1))) = ({1} ∪ (2...(𝑁 + 1)))
10295, 101syl6req 2660 . . . . . . . . . 10 (𝜑 → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
10370snssd 4280 . . . . . . . . . . 11 (𝜑 → {1} ⊆ (1...(𝑁 + 1)))
104 incom 3766 . . . . . . . . . . . 12 ({1} ∩ (2...(𝑁 + 1))) = ((2...(𝑁 + 1)) ∩ {1})
105 1lt2 11041 . . . . . . . . . . . . . . 15 1 < 2
106 1re 9895 . . . . . . . . . . . . . . . 16 1 ∈ ℝ
107 2re 10937 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
108106, 107ltnlei 10009 . . . . . . . . . . . . . . 15 (1 < 2 ↔ ¬ 2 ≤ 1)
109105, 108mpbi 218 . . . . . . . . . . . . . 14 ¬ 2 ≤ 1
110 elfzle1 12170 . . . . . . . . . . . . . 14 (1 ∈ (2...(𝑁 + 1)) → 2 ≤ 1)
111109, 110mto 186 . . . . . . . . . . . . 13 ¬ 1 ∈ (2...(𝑁 + 1))
112 disjsn 4191 . . . . . . . . . . . . 13 (((2...(𝑁 + 1)) ∩ {1}) = ∅ ↔ ¬ 1 ∈ (2...(𝑁 + 1)))
113111, 112mpbir 219 . . . . . . . . . . . 12 ((2...(𝑁 + 1)) ∩ {1}) = ∅
114104, 113eqtri 2631 . . . . . . . . . . 11 ({1} ∩ (2...(𝑁 + 1))) = ∅
115 uneqdifeq 4008 . . . . . . . . . . 11 (({1} ⊆ (1...(𝑁 + 1)) ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅) → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
116103, 114, 115sylancl 692 . . . . . . . . . 10 (𝜑 → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
117102, 116mpbid 220 . . . . . . . . 9 (𝜑 → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
118117adantr 479 . . . . . . . 8 ((𝜑𝑏𝐵) → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
119 reseq2 5299 . . . . . . . . . 10 (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})) = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
120 f1oeq1 6025 . . . . . . . . . 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 6026 . . . . . . . . 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 6027 . . . . . . . . 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 292 . . . . . . . 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 220 . . . . . 6 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
12775adantr 479 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
128 fzp1ss 12217 . . . . . . . . . . . 12 (1 ∈ ℤ → ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1)))
12996, 128ax-mp 5 . . . . . . . . . . 11 ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
130100, 129eqsstr3i 3598 . . . . . . . . . 10 (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
131 simpr 475 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (2...(𝑁 + 1)))
132130, 131sseldi 3565 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
133 fvco3 6170 . . . . . . . . 9 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (𝐹‘(𝑏𝑦)))
134127, 132, 133syl2anc 690 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (𝐹‘(𝑏𝑦)))
13520, 21, 1, 22, 23, 24, 25, 6, 26subfacp1lem4 30225 . . . . . . . . . . . 12 (𝜑𝐹 = 𝐹)
136135fveq1d 6090 . . . . . . . . . . 11 (𝜑 → (𝐹𝑦) = (𝐹𝑦))
137136ad2antrr 757 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) = (𝐹𝑦))
13878simprd 477 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝑏𝑀) ≠ 1)
139138, 82neeqtrrd 2855 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → (𝑏𝑀) ≠ (𝐹𝑀))
140139adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑀) ≠ (𝐹𝑀))
141 fveq2 6088 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → (𝑏𝑦) = (𝑏𝑀))
142 fveq2 6088 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → (𝐹𝑦) = (𝐹𝑀))
143141, 142neeq12d 2842 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → ((𝑏𝑦) ≠ (𝐹𝑦) ↔ (𝑏𝑀) ≠ (𝐹𝑀)))
144140, 143syl5ibrcom 235 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑏𝑦) ≠ (𝐹𝑦)))
145130sseli 3563 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (2...(𝑁 + 1)) → 𝑦 ∈ (1...(𝑁 + 1)))
14648simprd 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦)
147146r19.21bi 2915 . . . . . . . . . . . . . . . 16 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏𝑦) ≠ 𝑦)
148145, 147sylan2 489 . . . . . . . . . . . . . . 15 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ≠ 𝑦)
149148adantrr 748 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑏𝑦) ≠ 𝑦)
15025eleq2i 2679 . . . . . . . . . . . . . . . . 17 (𝑦𝐾𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}))
151 eldifsn 4259 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀))
152150, 151bitri 262 . . . . . . . . . . . . . . . 16 (𝑦𝐾 ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀))
15320, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2b 30223 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐾) → (𝐹𝑦) = (( I ↾ 𝐾)‘𝑦))
154 fvresi 6322 . . . . . . . . . . . . . . . . . 18 (𝑦𝐾 → (( I ↾ 𝐾)‘𝑦) = 𝑦)
155154adantl 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐾) → (( I ↾ 𝐾)‘𝑦) = 𝑦)
156153, 155eqtrd 2643 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐾) → (𝐹𝑦) = 𝑦)
157152, 156sylan2br 491 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
158157adantlr 746 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
159149, 158neeqtrrd 2855 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑏𝑦) ≠ (𝐹𝑦))
160159expr 640 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦𝑀 → (𝑏𝑦) ≠ (𝐹𝑦)))
161144, 160pm2.61dne 2867 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ≠ (𝐹𝑦))
162161necomd 2836 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (𝑏𝑦))
163137, 162eqnetrd 2848 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (𝑏𝑦))
16431adantr 479 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
165 ffvelrn 6250 . . . . . . . . . . . 12 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏𝑦) ∈ (1...(𝑁 + 1)))
16675, 145, 165syl2an 492 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ∈ (1...(𝑁 + 1)))
167 f1ocnvfv 6412 . . . . . . . . . . 11 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑏𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑏𝑦)) = 𝑦 → (𝐹𝑦) = (𝑏𝑦)))
168164, 166, 167syl2anc 690 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹‘(𝑏𝑦)) = 𝑦 → (𝐹𝑦) = (𝑏𝑦)))
169168necon3d 2802 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑦) ≠ (𝑏𝑦) → (𝐹‘(𝑏𝑦)) ≠ 𝑦))
170163, 169mpd 15 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘(𝑏𝑦)) ≠ 𝑦)
171134, 170eqnetrd 2848 . . . . . . 7 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) ≠ 𝑦)
172171ralrimiva 2948 . . . . . 6 ((𝜑𝑏𝐵) → ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦)
173 f1of 6035 . . . . . . . . . . . . 13 (( I ↾ 𝐾):𝐾1-1-onto𝐾 → ( I ↾ 𝐾):𝐾𝐾)
17427, 173ax-mp 5 . . . . . . . . . . . 12 ( I ↾ 𝐾):𝐾𝐾
175 difexg 4730 . . . . . . . . . . . . . 14 ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V)
17614, 175ax-mp 5 . . . . . . . . . . . . 13 ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V
17725, 176eqeltri 2683 . . . . . . . . . . . 12 𝐾 ∈ V
178 fex 6372 . . . . . . . . . . . 12 ((( I ↾ 𝐾):𝐾𝐾𝐾 ∈ V) → ( I ↾ 𝐾) ∈ V)
179174, 177, 178mp2an 703 . . . . . . . . . . 11 ( I ↾ 𝐾) ∈ V
180 prex 4831 . . . . . . . . . . 11 {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
181179, 180unex 6831 . . . . . . . . . 10 (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
18226, 181eqeltri 2683 . . . . . . . . 9 𝐹 ∈ V
183182, 41coex 6988 . . . . . . . 8 (𝐹𝑏) ∈ V
184183resex 5350 . . . . . . 7 ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ V
185 f1oeq1 6025 . . . . . . . 8 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
186 fveq1 6087 . . . . . . . . . . 11 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (𝑓𝑦) = (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
187 fvres 6102 . . . . . . . . . . 11 (𝑦 ∈ (2...(𝑁 + 1)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹𝑏)‘𝑦))
188186, 187sylan9eq 2663 . . . . . . . . . 10 ((𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑓𝑦) = ((𝐹𝑏)‘𝑦))
189188neeq1d 2840 . . . . . . . . 9 ((𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝑓𝑦) ≠ 𝑦 ↔ ((𝐹𝑏)‘𝑦) ≠ 𝑦))
190189ralbidva 2967 . . . . . . . 8 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦))
191185, 190anbi12d 742 . . . . . . 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 3322 . . . . . 6 (((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶 ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦))
193126, 172, 192sylanbrc 694 . . . . 5 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶)
194193ex 448 . . . 4 (𝜑 → (𝑏𝐵 → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶))
19530adantr 479 . . . . . . . 8 ((𝜑𝑐𝐶) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
196 simpr 475 . . . . . . . . . . . 12 ((𝜑𝑐𝐶) → 𝑐𝐶)
197 vex 3175 . . . . . . . . . . . . 13 𝑐 ∈ V
198 f1oeq1 6025 . . . . . . . . . . . . . 14 (𝑓 = 𝑐 → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
199 fveq1 6087 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑐 → (𝑓𝑦) = (𝑐𝑦))
200199neeq1d 2840 . . . . . . . . . . . . . . 15 (𝑓 = 𝑐 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑐𝑦) ≠ 𝑦))
201200ralbidv 2968 . . . . . . . . . . . . . 14 (𝑓 = 𝑐 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
202198, 201anbi12d 742 . . . . . . . . . . . . 13 (𝑓 = 𝑐 → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦)))
203197, 202, 13elab2 3322 . . . . . . . . . . . 12 (𝑐𝐶 ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
204196, 203sylib 206 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
205204simpld 473 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
206 f1oun 6054 . . . . . . . . . . 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 716 . . . . . . . . . 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 693 . . . . . . . . 9 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
209 f1oeq2 6026 . . . . . . . . . . . 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 6027 . . . . . . . . . . . 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 266 . . . . . . . . . . 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 499 . . . . . . . . 9 ((𝜑 ∧ ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1)))) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
214208, 213syldan 485 . . . . . . . 8 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
215 f1oco 6057 . . . . . . . 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 690 . . . . . . 7 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
217 f1of 6035 . . . . . . . . . . 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 6170 . . . . . . . . . 10 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
220218, 219sylan 486 . . . . . . . . 9 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
221136ad2antrr 757 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) = (𝐹𝑦))
222 simpr 475 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
223102ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
224222, 223eleqtrrd 2690 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))))
225 elun 3714 . . . . . . . . . . . . 13 (𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
226224, 225sylib 206 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
227 nelne2 2878 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → 𝑀 ≠ 1)
22823, 111, 227sylancl 692 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ≠ 1)
229228adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → 𝑀 ≠ 1)
23029simp2d 1066 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹‘1) = 𝑀)
231230adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → (𝐹‘1) = 𝑀)
232 f1ofun 6037 . . . . . . . . . . . . . . . . . . 19 (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
233208, 232syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐶) → Fun ({⟨1, 1⟩} ∪ 𝑐))
234 ssun1 3737 . . . . . . . . . . . . . . . . . . 19 {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐)
23563snid 4154 . . . . . . . . . . . . . . . . . . . 20 1 ∈ {1}
23663dmsnop 5513 . . . . . . . . . . . . . . . . . . . 20 dom {⟨1, 1⟩} = {1}
237235, 236eleqtrri 2686 . . . . . . . . . . . . . . . . . . 19 1 ∈ dom {⟨1, 1⟩}
238 funssfv 6104 . . . . . . . . . . . . . . . . . . 19 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 1 ∈ dom {⟨1, 1⟩}) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
239234, 237, 238mp3an23 1407 . . . . . . . . . . . . . . . . . 18 (Fun ({⟨1, 1⟩} ∪ 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
240233, 239syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
24163, 63fvsn 6329 . . . . . . . . . . . . . . . . 17 ({⟨1, 1⟩}‘1) = 1
242240, 241syl6eq 2659 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
243229, 231, 2423netr4d 2858 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐶) → (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1))
244 elsni 4141 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {1} → 𝑦 = 1)
245244fveq2d 6092 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (𝐹𝑦) = (𝐹‘1))
246244fveq2d 6092 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
247245, 246neeq12d 2842 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → ((𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1)))
248243, 247syl5ibrcom 235 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐶) → (𝑦 ∈ {1} → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
249248imp 443 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ {1}) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
250233adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
251 ssun2 3738 . . . . . . . . . . . . . . . . 17 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐)
252251a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
253 f1odm 6039 . . . . . . . . . . . . . . . . . . 19 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → dom 𝑐 = (2...(𝑁 + 1)))
254205, 253syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐶) → dom 𝑐 = (2...(𝑁 + 1)))
255254eleq2d 2672 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐶) → (𝑦 ∈ dom 𝑐𝑦 ∈ (2...(𝑁 + 1))))
256255biimpar 500 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ dom 𝑐)
257 funssfv 6104 . . . . . . . . . . . . . . . 16 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑦 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
258250, 252, 256, 257syl3anc 1317 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
259 f1of 6035 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
260205, 259syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐶) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
26123adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
262260, 261ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐶) → (𝑐𝑀) ∈ (2...(𝑁 + 1)))
263 nelne2 2878 . . . . . . . . . . . . . . . . . . . 20 (((𝑐𝑀) ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ 1)
264262, 111, 263sylancl 692 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐶) → (𝑐𝑀) ≠ 1)
265264adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ 1)
26681ad2antrr 757 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑀) = 1)
267265, 266neeqtrrd 2855 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ (𝐹𝑀))
268 fveq2 6088 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑀 → (𝑐𝑦) = (𝑐𝑀))
269268, 142neeq12d 2842 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑀 → ((𝑐𝑦) ≠ (𝐹𝑦) ↔ (𝑐𝑀) ≠ (𝐹𝑀)))
270267, 269syl5ibrcom 235 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑐𝑦) ≠ (𝐹𝑦)))
271204simprd 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐶) → ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦)
272271r19.21bi 2915 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑦) ≠ 𝑦)
273272adantrr 748 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑐𝑦) ≠ 𝑦)
274157adantlr 746 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
275273, 274neeqtrrd 2855 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑐𝑦) ≠ (𝐹𝑦))
276275expr 640 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦𝑀 → (𝑐𝑦) ≠ (𝐹𝑦)))
277270, 276pm2.61dne 2867 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑦) ≠ (𝐹𝑦))
278258, 277eqnetrd 2848 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ≠ (𝐹𝑦))
279278necomd 2836 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
280249, 279jaodan 821 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1)))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
281226, 280syldan 485 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
282221, 281eqnetrd 2848 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
283195adantr 479 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
284218ffvelrnda 6252 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1)))
285 f1ocnvfv 6412 . . . . . . . . . . . 12 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (𝐹𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
286283, 284, 285syl2anc 690 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (𝐹𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
287286necon3d 2802 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦))
288282, 287mpd 15 . . . . . . . . 9 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦)
289220, 288eqnetrd 2848 . . . . . . . 8 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
290289ralrimiva 2948 . . . . . . 7 ((𝜑𝑐𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
291 snex 4830 . . . . . . . . . 10 {⟨1, 1⟩} ∈ V
292291, 197unex 6831 . . . . . . . . 9 ({⟨1, 1⟩} ∪ 𝑐) ∈ V
293182, 292coex 6988 . . . . . . . 8 (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ V
294 f1oeq1 6025 . . . . . . . . 9 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
295 fveq1 6087 . . . . . . . . . . 11 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓𝑦) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦))
296295neeq1d 2840 . . . . . . . . . 10 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
297296ralbidv 2968 . . . . . . . . 9 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
298294, 297anbi12d 742 . . . . . . . 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 3322 . . . . . . 7 ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
300216, 290, 299sylanbrc 694 . . . . . 6 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴)
30170adantr 479 . . . . . . . . 9 ((𝜑𝑐𝐶) → 1 ∈ (1...(𝑁 + 1)))
302 fvco3 6170 . . . . . . . . 9 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
303218, 301, 302syl2anc 690 . . . . . . . 8 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
304242fveq2d 6092 . . . . . . . 8 ((𝜑𝑐𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)) = (𝐹‘1))
305303, 304, 2313eqtrd 2647 . . . . . . 7 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀)
306130, 23sseldi 3565 . . . . . . . . . . 11 (𝜑𝑀 ∈ (1...(𝑁 + 1)))
307306adantr 479 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑀 ∈ (1...(𝑁 + 1)))
308 fvco3 6170 . . . . . . . . . 10 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑀 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
309218, 307, 308syl2anc 690 . . . . . . . . 9 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
310251a1i 11 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
311261, 254eleqtrrd 2690 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → 𝑀 ∈ dom 𝑐)
312 funssfv 6104 . . . . . . . . . . 11 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑀 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐𝑀))
313233, 310, 311, 312syl3anc 1317 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐𝑀))
314313fveq2d 6092 . . . . . . . . 9 ((𝜑𝑐𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)) = (𝐹‘(𝑐𝑀)))
315309, 314eqtrd 2643 . . . . . . . 8 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(𝑐𝑀)))
316135fveq1d 6090 . . . . . . . . . . . 12 (𝜑 → (𝐹‘1) = (𝐹‘1))
317316, 230eqtrd 2643 . . . . . . . . . . 11 (𝜑 → (𝐹‘1) = 𝑀)
318317adantr 479 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (𝐹‘1) = 𝑀)
319 id 22 . . . . . . . . . . . . . 14 (𝑦 = 𝑀𝑦 = 𝑀)
320268, 319neeq12d 2842 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → ((𝑐𝑦) ≠ 𝑦 ↔ (𝑐𝑀) ≠ 𝑀))
321320rspcv 3277 . . . . . . . . . . . 12 (𝑀 ∈ (2...(𝑁 + 1)) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦 → (𝑐𝑀) ≠ 𝑀))
322261, 271, 321sylc 62 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → (𝑐𝑀) ≠ 𝑀)
323322necomd 2836 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑀 ≠ (𝑐𝑀))
324318, 323eqnetrd 2848 . . . . . . . . 9 ((𝜑𝑐𝐶) → (𝐹‘1) ≠ (𝑐𝑀))
325130, 262sseldi 3565 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → (𝑐𝑀) ∈ (1...(𝑁 + 1)))
326 f1ocnvfv 6412 . . . . . . . . . . 11 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑐𝑀) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑐𝑀)) = 1 → (𝐹‘1) = (𝑐𝑀)))
327195, 325, 326syl2anc 690 . . . . . . . . . 10 ((𝜑𝑐𝐶) → ((𝐹‘(𝑐𝑀)) = 1 → (𝐹‘1) = (𝑐𝑀)))
328327necon3d 2802 . . . . . . . . 9 ((𝜑𝑐𝐶) → ((𝐹‘1) ≠ (𝑐𝑀) → (𝐹‘(𝑐𝑀)) ≠ 1))
329324, 328mpd 15 . . . . . . . 8 ((𝜑𝑐𝐶) → (𝐹‘(𝑐𝑀)) ≠ 1)
330315, 329eqnetrd 2848 . . . . . . 7 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)
331305, 330jca 552 . . . . . 6 ((𝜑𝑐𝐶) → (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
332 fveq1 6087 . . . . . . . . 9 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘1) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1))
333332eqeq1d 2611 . . . . . . . 8 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘1) = 𝑀 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀))
334 fveq1 6087 . . . . . . . . 9 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔𝑀) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀))
335334neeq1d 2840 . . . . . . . 8 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔𝑀) ≠ 1 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
336333, 335anbi12d 742 . . . . . . 7 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1) ↔ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
337336, 6elrab2 3332 . . . . . 6 ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ∧ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
338300, 331, 337sylanbrc 694 . . . . 5 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵)
339338ex 448 . . . 4 (𝜑 → (𝑐𝐶 → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵))
34030adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
341 f1of1 6034 . . . . . . . 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 6035 . . . . . . . . 9 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
344340, 343syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
34575adantrr 748 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
346 fco 5957 . . . . . . . 8 ((𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) → (𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
347344, 345, 346syl2anc 690 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
348218adantrl 747 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
349 cocan1 6424 . . . . . . 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 1317 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
351 coass 5557 . . . . . . . 8 ((𝐹𝐹) ∘ 𝑏) = (𝐹 ∘ (𝐹𝑏))
352135coeq1d 5193 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐹) = (𝐹𝐹))
353 f1ococnv1 6063 . . . . . . . . . . . . 13 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
35430, 353syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
355352, 354eqtr3d 2645 . . . . . . . . . . 11 (𝜑 → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
356355adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
357356coeq1d 5193 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝐹) ∘ 𝑏) = (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏))
358 fcoi2 5977 . . . . . . . . . 10 (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
359345, 358syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
360357, 359eqtrd 2643 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝐹) ∘ 𝑏) = 𝑏)
361351, 360syl5eqr 2657 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹 ∘ (𝐹𝑏)) = 𝑏)
362361eqeq1d 2611 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))))
36383adantrr 748 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏)‘1) = 1)
364242adantrl 747 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
365363, 364eqtr4d 2646 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
366 fveq2 6088 . . . . . . . . . . . . . 14 (𝑦 = 1 → ((𝐹𝑏)‘𝑦) = ((𝐹𝑏)‘1))
367 fveq2 6088 . . . . . . . . . . . . . 14 (𝑦 = 1 → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
368366, 367eqeq12d 2624 . . . . . . . . . . . . 13 (𝑦 = 1 → (((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1)))
36963, 368ralsn 4168 . . . . . . . . . . . 12 (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
370365, 369sylibr 222 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
371370biantrurd 527 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))))
372 ralunb 3755 . . . . . . . . . 10 (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
373371, 372syl6bbr 276 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
374187adantl 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹𝑏)‘𝑦))
375374eqcomd 2615 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
376258adantlrl 751 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
377375, 376eqeq12d 2624 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
378377ralbidva 2967 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
379102adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
380379raleqdv 3120 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
381373, 378, 3803bitr3rd 297 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
38265adantrr 748 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
383214adantrl 747 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
384 f1ofn 6036 . . . . . . . . . 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 6204 . . . . . . . . 9 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1))) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
387382, 385, 386syl2anc 690 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
388 fnssres 5904 . . . . . . . . . 10 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
389382, 130, 388sylancl 692 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
390205adantrl 747 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
391 f1ofn 6036 . . . . . . . . . 10 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐 Fn (2...(𝑁 + 1)))
392390, 391syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑐 Fn (2...(𝑁 + 1)))
393 eqfnfv 6204 . . . . . . . . 9 ((((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)) ∧ 𝑐 Fn (2...(𝑁 + 1))) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
394389, 392, 393syl2anc 690 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
395381, 387, 3943bitr4d 298 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐))
396 eqcom 2616 . . . . . . 7 (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
397395, 396syl6bb 274 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1)))))
398350, 362, 3973bitr3d 296 . . . . 5 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1)))))
399398ex 448 . . . 4 (𝜑 → ((𝑏𝐵𝑐𝐶) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))))
40012, 19, 194, 339, 399en3d 7855 . . 3 (𝜑𝐵𝐶)
401 hashen 12949 . . . 4 ((𝐵 ∈ Fin ∧ 𝐶 ∈ Fin) → ((#‘𝐵) = (#‘𝐶) ↔ 𝐵𝐶))
40210, 17, 401mp2an 703 . . 3 ((#‘𝐵) = (#‘𝐶) ↔ 𝐵𝐶)
403400, 402sylibr 222 . 2 (𝜑 → (#‘𝐵) = (#‘𝐶))
40420, 21derangen2 30216 . . . . 5 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (𝑆‘(#‘(2...(𝑁 + 1)))))
40520derangval 30209 . . . . . 6 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (#‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}))
40613fveq2i 6091 . . . . . 6 (#‘𝐶) = (#‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)})
407405, 406syl6eqr 2661 . . . . 5 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (#‘𝐶))
408404, 407eqtr3d 2645 . . . 4 ((2...(𝑁 + 1)) ∈ Fin → (𝑆‘(#‘(2...(𝑁 + 1)))) = (#‘𝐶))
40914, 408ax-mp 5 . . 3 (𝑆‘(#‘(2...(𝑁 + 1)))) = (#‘𝐶)
41022, 67syl6eleq 2697 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ‘1))
411 eluzp1p1 11545 . . . . . . . 8 (𝑁 ∈ (ℤ‘1) → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
412410, 411syl 17 . . . . . . 7 (𝜑 → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
413 df-2 10926 . . . . . . . 8 2 = (1 + 1)
414413fveq2i 6091 . . . . . . 7 (ℤ‘2) = (ℤ‘(1 + 1))
415412, 414syl6eleqr 2698 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ (ℤ‘2))
416 hashfz 13026 . . . . . 6 ((𝑁 + 1) ∈ (ℤ‘2) → (#‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
417415, 416syl 17 . . . . 5 (𝜑 → (#‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
41866nncnd 10883 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ ℂ)
419 2cnd 10940 . . . . . 6 (𝜑 → 2 ∈ ℂ)
420 1cnd 9912 . . . . . 6 (𝜑 → 1 ∈ ℂ)
421418, 419, 420subsubd 10271 . . . . 5 (𝜑 → ((𝑁 + 1) − (2 − 1)) = (((𝑁 + 1) − 2) + 1))
422 2m1e1 10982 . . . . . . 7 (2 − 1) = 1
423422oveq2i 6538 . . . . . 6 ((𝑁 + 1) − (2 − 1)) = ((𝑁 + 1) − 1)
42422nncnd 10883 . . . . . . 7 (𝜑𝑁 ∈ ℂ)
425 ax-1cn 9850 . . . . . . 7 1 ∈ ℂ
426 pncan 10138 . . . . . . 7 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
427424, 425, 426sylancl 692 . . . . . 6 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
428423, 427syl5eq 2655 . . . . 5 (𝜑 → ((𝑁 + 1) − (2 − 1)) = 𝑁)
429417, 421, 4283eqtr2d 2649 . . . 4 (𝜑 → (#‘(2...(𝑁 + 1))) = 𝑁)
430429fveq2d 6092 . . 3 (𝜑 → (𝑆‘(#‘(2...(𝑁 + 1)))) = (𝑆𝑁))
431409, 430syl5eqr 2657 . 2 (𝜑 → (#‘𝐶) = (𝑆𝑁))
432403, 431eqtrd 2643 1 (𝜑 → (#‘𝐵) = (𝑆𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wcel 1976  {cab 2595  wne 2779  wral 2895  {crab 2899  Vcvv 3172  cdif 3536  cun 3537  cin 3538  wss 3539  c0 3873  {csn 4124  {cpr 4126  cop 4130   class class class wbr 4577  cmpt 4637   I cid 4938  ccnv 5027  dom cdm 5028  cres 5030  ccom 5032  Fun wfun 5784   Fn wfn 5785  wf 5786  1-1wf1 5787  ontowfo 5788  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  cen 7815  Fincfn 7818  cc 9790  1c1 9793   + caddc 9795   < clt 9930  cle 9931  cmin 10117  cn 10867  2c2 10917  0cn0 11139  cz 11210  cuz 11519  ...cfz 12152  #chash 12934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-2 10926  df-n0 11140  df-z 11211  df-uz 11520  df-fz 12153  df-hash 12935
This theorem is referenced by:  subfacp1lem6  30227
  Copyright terms: Public domain W3C validator