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 33818
Description: Lemma for subfacp1 33820. In subfacp1lem6 33819 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 . . . . . . 7 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}
2 fzfi 13884 . . . . . . . 8 (1...(𝑁 + 1)) ∈ Fin
3 deranglem 33800 . . . . . . . 8 ((1...(𝑁 + 1)) ∈ Fin → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ∈ Fin)
42, 3ax-mp 5 . . . . . . 7 {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ∈ Fin
51, 4eqeltri 2834 . . . . . 6 𝐴 ∈ Fin
6 subfacp1lem5.b . . . . . . 7 𝐵 = {𝑔𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1)}
76ssrab3 4045 . . . . . 6 𝐵𝐴
8 ssfi 9124 . . . . . 6 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)
95, 7, 8mp2an 691 . . . . 5 𝐵 ∈ Fin
109elexi 3467 . . . 4 𝐵 ∈ V
1110a1i 11 . . 3 (𝜑𝐵 ∈ V)
12 eqid 2737 . . . 4 (𝑏𝐵 ↦ ((𝐹𝑏) ↾ (2...(𝑁 + 1)))) = (𝑏𝐵 ↦ ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
13 derang.d . . . . . . . . . . 11 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥1-1-onto𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) ≠ 𝑦)}))
14 subfac.n . . . . . . . . . . 11 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))
15 subfacp1lem1.n . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
16 subfacp1lem1.m . . . . . . . . . . 11 (𝜑𝑀 ∈ (2...(𝑁 + 1)))
17 subfacp1lem1.x . . . . . . . . . . 11 𝑀 ∈ V
18 subfacp1lem1.k . . . . . . . . . . 11 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})
19 subfacp1lem5.f . . . . . . . . . . 11 𝐹 = (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})
20 f1oi 6827 . . . . . . . . . . . 12 ( I ↾ 𝐾):𝐾1-1-onto𝐾
2120a1i 11 . . . . . . . . . . 11 (𝜑 → ( I ↾ 𝐾):𝐾1-1-onto𝐾)
2213, 14, 1, 15, 16, 17, 18, 19, 21subfacp1lem2a 33814 . . . . . . . . . 10 (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹𝑀) = 1))
2322simp1d 1143 . . . . . . . . 9 (𝜑𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
24 simpr 486 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → 𝑏𝐵)
25 fveq1 6846 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
2625eqeq1d 2739 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
27 fveq1 6846 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑏 → (𝑔𝑀) = (𝑏𝑀))
2827neeq1d 3004 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → ((𝑔𝑀) ≠ 1 ↔ (𝑏𝑀) ≠ 1))
2926, 28anbi12d 632 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3029, 6elrab2 3653 . . . . . . . . . . . . 13 (𝑏𝐵 ↔ (𝑏𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3124, 30sylib 217 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → (𝑏𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3231simpld 496 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → 𝑏𝐴)
33 vex 3452 . . . . . . . . . . . 12 𝑏 ∈ V
34 f1oeq1 6777 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
35 fveq1 6846 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
3635neeq1d 3004 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑏𝑦) ≠ 𝑦))
3736ralbidv 3175 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
3834, 37anbi12d 632 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦)))
3933, 38, 1elab2 3639 . . . . . . . . . . 11 (𝑏𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4032, 39sylib 217 . . . . . . . . . 10 ((𝜑𝑏𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4140simpld 496 . . . . . . . . 9 ((𝜑𝑏𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
42 f1oco 6812 . . . . . . . . 9 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) → (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
4323, 41, 42syl2an2r 684 . . . . . . . 8 ((𝜑𝑏𝐵) → (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
44 f1of1 6788 . . . . . . . 8 ((𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
45 df-f1 6506 . . . . . . . . 9 ((𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ ((𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun (𝐹𝑏)))
4645simprbi 498 . . . . . . . 8 ((𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun (𝐹𝑏))
4743, 44, 463syl 18 . . . . . . 7 ((𝜑𝑏𝐵) → Fun (𝐹𝑏))
48 f1ofn 6790 . . . . . . . . . 10 ((𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
49 fnresdm 6625 . . . . . . . . . 10 ((𝐹𝑏) Fn (1...(𝑁 + 1)) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))) = (𝐹𝑏))
50 f1oeq1 6777 . . . . . . . . . 10 (((𝐹𝑏) ↾ (1...(𝑁 + 1))) = (𝐹𝑏) → (((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
5143, 48, 49, 504syl 19 . . . . . . . . 9 ((𝜑𝑏𝐵) → (((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
5243, 51mpbird 257 . . . . . . . 8 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
53 f1ofo 6796 . . . . . . . 8 (((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
5452, 53syl 17 . . . . . . 7 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
55 1ex 11158 . . . . . . . . . 10 1 ∈ V
5655, 55f1osn 6829 . . . . . . . . 9 {⟨1, 1⟩}:{1}–1-1-onto→{1}
5743, 48syl 17 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
5815peano2nnd 12177 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ ℕ)
59 nnuz 12813 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
6058, 59eleqtrdi 2848 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
61 eluzfz1 13455 . . . . . . . . . . . . . 14 ((𝑁 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑁 + 1)))
6260, 61syl 17 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ (1...(𝑁 + 1)))
6362adantr 482 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → 1 ∈ (1...(𝑁 + 1)))
64 fnressn 7109 . . . . . . . . . . . 12 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏) ↾ {1}) = {⟨1, ((𝐹𝑏)‘1)⟩})
6557, 63, 64syl2anc 585 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}) = {⟨1, ((𝐹𝑏)‘1)⟩})
66 f1of 6789 . . . . . . . . . . . . . . . 16 (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
6741, 66syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
6867, 63fvco3d 6946 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → ((𝐹𝑏)‘1) = (𝐹‘(𝑏‘1)))
6931simprd 497 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1))
7069simpld 496 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝑏‘1) = 𝑀)
7170fveq2d 6851 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → (𝐹‘(𝑏‘1)) = (𝐹𝑀))
7222simp3d 1145 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑀) = 1)
7372adantr 482 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → (𝐹𝑀) = 1)
7468, 71, 733eqtrd 2781 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → ((𝐹𝑏)‘1) = 1)
7574opeq2d 4842 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ⟨1, ((𝐹𝑏)‘1)⟩ = ⟨1, 1⟩)
7675sneqd 4603 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → {⟨1, ((𝐹𝑏)‘1)⟩} = {⟨1, 1⟩})
7765, 76eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}) = {⟨1, 1⟩})
7877f1oeq1d 6784 . . . . . . . . 9 ((𝜑𝑏𝐵) → (((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1} ↔ {⟨1, 1⟩}:{1}–1-1-onto→{1}))
7956, 78mpbiri 258 . . . . . . . 8 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1})
80 f1ofo 6796 . . . . . . . 8 (((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1} → ((𝐹𝑏) ↾ {1}):{1}–onto→{1})
8179, 80syl 17 . . . . . . 7 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}):{1}–onto→{1})
82 resdif 6810 . . . . . . 7 ((Fun (𝐹𝑏) ∧ ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)) ∧ ((𝐹𝑏) ↾ {1}):{1}–onto→{1}) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
8347, 54, 81, 82syl3anc 1372 . . . . . 6 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
84 fzsplit 13474 . . . . . . . . . . 11 (1 ∈ (1...(𝑁 + 1)) → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
8562, 84syl 17 . . . . . . . . . 10 (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
86 1z 12540 . . . . . . . . . . . 12 1 ∈ ℤ
87 fzsn 13490 . . . . . . . . . . . 12 (1 ∈ ℤ → (1...1) = {1})
8886, 87ax-mp 5 . . . . . . . . . . 11 (1...1) = {1}
89 1p1e2 12285 . . . . . . . . . . . 12 (1 + 1) = 2
9089oveq1i 7372 . . . . . . . . . . 11 ((1 + 1)...(𝑁 + 1)) = (2...(𝑁 + 1))
9188, 90uneq12i 4126 . . . . . . . . . 10 ((1...1) ∪ ((1 + 1)...(𝑁 + 1))) = ({1} ∪ (2...(𝑁 + 1)))
9285, 91eqtr2di 2794 . . . . . . . . 9 (𝜑 → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
9362snssd 4774 . . . . . . . . . 10 (𝜑 → {1} ⊆ (1...(𝑁 + 1)))
94 incom 4166 . . . . . . . . . . 11 ({1} ∩ (2...(𝑁 + 1))) = ((2...(𝑁 + 1)) ∩ {1})
95 1lt2 12331 . . . . . . . . . . . . . 14 1 < 2
96 1re 11162 . . . . . . . . . . . . . . 15 1 ∈ ℝ
97 2re 12234 . . . . . . . . . . . . . . 15 2 ∈ ℝ
9896, 97ltnlei 11283 . . . . . . . . . . . . . 14 (1 < 2 ↔ ¬ 2 ≤ 1)
9995, 98mpbi 229 . . . . . . . . . . . . 13 ¬ 2 ≤ 1
100 elfzle1 13451 . . . . . . . . . . . . 13 (1 ∈ (2...(𝑁 + 1)) → 2 ≤ 1)
10199, 100mto 196 . . . . . . . . . . . 12 ¬ 1 ∈ (2...(𝑁 + 1))
102 disjsn 4677 . . . . . . . . . . . 12 (((2...(𝑁 + 1)) ∩ {1}) = ∅ ↔ ¬ 1 ∈ (2...(𝑁 + 1)))
103101, 102mpbir 230 . . . . . . . . . . 11 ((2...(𝑁 + 1)) ∩ {1}) = ∅
10494, 103eqtri 2765 . . . . . . . . . 10 ({1} ∩ (2...(𝑁 + 1))) = ∅
105 uneqdifeq 4455 . . . . . . . . . 10 (({1} ⊆ (1...(𝑁 + 1)) ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅) → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
10693, 104, 105sylancl 587 . . . . . . . . 9 (𝜑 → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
10792, 106mpbid 231 . . . . . . . 8 (𝜑 → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
108107adantr 482 . . . . . . 7 ((𝜑𝑏𝐵) → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
109 reseq2 5937 . . . . . . . . 9 (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})) = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
110109f1oeq1d 6784 . . . . . . . 8 (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → (((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1})))
111 f1oeq2 6778 . . . . . . . 8 (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→((1...(𝑁 + 1)) ∖ {1})))
112 f1oeq3 6779 . . . . . . . 8 (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
113110, 111, 1123bitrd 305 . . . . . . 7 (((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))))
114108, 113syl 17 . . . . . 6 ((𝜑𝑏𝐵) → (((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
11583, 114mpbid 231 . . . . 5 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
11667adantr 482 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
117 fzp1ss 13499 . . . . . . . . . . 11 (1 ∈ ℤ → ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1)))
11886, 117ax-mp 5 . . . . . . . . . 10 ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
11990, 118eqsstrri 3984 . . . . . . . . 9 (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
120 simpr 486 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (2...(𝑁 + 1)))
121119, 120sselid 3947 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
122116, 121fvco3d 6946 . . . . . . 7 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (𝐹‘(𝑏𝑦)))
12313, 14, 1, 15, 16, 17, 18, 6, 19subfacp1lem4 33817 . . . . . . . . . . 11 (𝜑𝐹 = 𝐹)
124123fveq1d 6849 . . . . . . . . . 10 (𝜑 → (𝐹𝑦) = (𝐹𝑦))
125124ad2antrr 725 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) = (𝐹𝑦))
12669simprd 497 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → (𝑏𝑀) ≠ 1)
127126, 73neeqtrrd 3019 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (𝑏𝑀) ≠ (𝐹𝑀))
128127adantr 482 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑀) ≠ (𝐹𝑀))
129 fveq2 6847 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → (𝑏𝑦) = (𝑏𝑀))
130 fveq2 6847 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → (𝐹𝑦) = (𝐹𝑀))
131129, 130neeq12d 3006 . . . . . . . . . . . 12 (𝑦 = 𝑀 → ((𝑏𝑦) ≠ (𝐹𝑦) ↔ (𝑏𝑀) ≠ (𝐹𝑀)))
132128, 131syl5ibrcom 247 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑏𝑦) ≠ (𝐹𝑦)))
133119sseli 3945 . . . . . . . . . . . . . . 15 (𝑦 ∈ (2...(𝑁 + 1)) → 𝑦 ∈ (1...(𝑁 + 1)))
13440simprd 497 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦)
135134r19.21bi 3237 . . . . . . . . . . . . . . 15 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏𝑦) ≠ 𝑦)
136133, 135sylan2 594 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ≠ 𝑦)
137136adantrr 716 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑏𝑦) ≠ 𝑦)
13818eleq2i 2830 . . . . . . . . . . . . . . . 16 (𝑦𝐾𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}))
139 eldifsn 4752 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀))
140138, 139bitri 275 . . . . . . . . . . . . . . 15 (𝑦𝐾 ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀))
14113, 14, 1, 15, 16, 17, 18, 19, 21subfacp1lem2b 33815 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐾) → (𝐹𝑦) = (( I ↾ 𝐾)‘𝑦))
142 fvresi 7124 . . . . . . . . . . . . . . . . 17 (𝑦𝐾 → (( I ↾ 𝐾)‘𝑦) = 𝑦)
143142adantl 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐾) → (( I ↾ 𝐾)‘𝑦) = 𝑦)
144141, 143eqtrd 2777 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐾) → (𝐹𝑦) = 𝑦)
145140, 144sylan2br 596 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
146145adantlr 714 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
147137, 146neeqtrrd 3019 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑏𝑦) ≠ (𝐹𝑦))
148147expr 458 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦𝑀 → (𝑏𝑦) ≠ (𝐹𝑦)))
149132, 148pm2.61dne 3032 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ≠ (𝐹𝑦))
150149necomd 3000 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (𝑏𝑦))
151125, 150eqnetrd 3012 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (𝑏𝑦))
15223adantr 482 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
153 ffvelcdm 7037 . . . . . . . . . . 11 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏𝑦) ∈ (1...(𝑁 + 1)))
15467, 133, 153syl2an 597 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ∈ (1...(𝑁 + 1)))
155 f1ocnvfv 7229 . . . . . . . . . 10 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑏𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑏𝑦)) = 𝑦 → (𝐹𝑦) = (𝑏𝑦)))
156152, 154, 155syl2an2r 684 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹‘(𝑏𝑦)) = 𝑦 → (𝐹𝑦) = (𝑏𝑦)))
157156necon3d 2965 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑦) ≠ (𝑏𝑦) → (𝐹‘(𝑏𝑦)) ≠ 𝑦))
158151, 157mpd 15 . . . . . . 7 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘(𝑏𝑦)) ≠ 𝑦)
159122, 158eqnetrd 3012 . . . . . 6 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) ≠ 𝑦)
160159ralrimiva 3144 . . . . 5 ((𝜑𝑏𝐵) → ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦)
161 f1of 6789 . . . . . . . . . . . 12 (( I ↾ 𝐾):𝐾1-1-onto𝐾 → ( I ↾ 𝐾):𝐾𝐾)
16220, 161ax-mp 5 . . . . . . . . . . 11 ( I ↾ 𝐾):𝐾𝐾
163 fzfi 13884 . . . . . . . . . . . . 13 (2...(𝑁 + 1)) ∈ Fin
164 difexg 5289 . . . . . . . . . . . . 13 ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V)
165163, 164ax-mp 5 . . . . . . . . . . . 12 ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V
16618, 165eqeltri 2834 . . . . . . . . . . 11 𝐾 ∈ V
167 fex 7181 . . . . . . . . . . 11 ((( I ↾ 𝐾):𝐾𝐾𝐾 ∈ V) → ( I ↾ 𝐾) ∈ V)
168162, 166, 167mp2an 691 . . . . . . . . . 10 ( I ↾ 𝐾) ∈ V
169 prex 5394 . . . . . . . . . 10 {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
170168, 169unex 7685 . . . . . . . . 9 (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
17119, 170eqeltri 2834 . . . . . . . 8 𝐹 ∈ V
172171, 33coex 7872 . . . . . . 7 (𝐹𝑏) ∈ V
173172resex 5990 . . . . . 6 ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ V
174 f1oeq1 6777 . . . . . . 7 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
175 fveq1 6846 . . . . . . . . . 10 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (𝑓𝑦) = (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
176 fvres 6866 . . . . . . . . . 10 (𝑦 ∈ (2...(𝑁 + 1)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹𝑏)‘𝑦))
177175, 176sylan9eq 2797 . . . . . . . . 9 ((𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑓𝑦) = ((𝐹𝑏)‘𝑦))
178177neeq1d 3004 . . . . . . . 8 ((𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝑓𝑦) ≠ 𝑦 ↔ ((𝐹𝑏)‘𝑦) ≠ 𝑦))
179178ralbidva 3173 . . . . . . 7 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦))
180174, 179anbi12d 632 . . . . . 6 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦)))
181 subfacp1lem5.c . . . . . 6 𝐶 = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}
182173, 180, 181elab2 3639 . . . . 5 (((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶 ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦))
183115, 160, 182sylanbrc 584 . . . 4 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶)
184 simpr 486 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → 𝑐𝐶)
185 vex 3452 . . . . . . . . . . . 12 𝑐 ∈ V
186 f1oeq1 6777 . . . . . . . . . . . . 13 (𝑓 = 𝑐 → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
187 fveq1 6846 . . . . . . . . . . . . . . 15 (𝑓 = 𝑐 → (𝑓𝑦) = (𝑐𝑦))
188187neeq1d 3004 . . . . . . . . . . . . . 14 (𝑓 = 𝑐 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑐𝑦) ≠ 𝑦))
189188ralbidv 3175 . . . . . . . . . . . . 13 (𝑓 = 𝑐 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
190186, 189anbi12d 632 . . . . . . . . . . . 12 (𝑓 = 𝑐 → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦)))
191185, 190, 181elab2 3639 . . . . . . . . . . 11 (𝑐𝐶 ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
192184, 191sylib 217 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
193192simpld 496 . . . . . . . . 9 ((𝜑𝑐𝐶) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
194 f1oun 6808 . . . . . . . . . 10 ((({⟨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))))
195104, 104, 194mpanr12 704 . . . . . . . . 9 (({⟨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))))
19656, 193, 195sylancr 588 . . . . . . . 8 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
197 f1oeq2 6778 . . . . . . . . . . 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} ∪ (2...(𝑁 + 1)))))
198 f1oeq3 6779 . . . . . . . . . . 11 (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) → (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
199197, 198bitrd 279 . . . . . . . . . 10 (({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))))
20092, 199syl 17 . . . . . . . . 9 (𝜑 → (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
201200biimpa 478 . . . . . . . 8 ((𝜑 ∧ ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1)))) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
202196, 201syldan 592 . . . . . . 7 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
203 f1oco 6812 . . . . . . 7 ((𝐹:(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)))
20423, 202, 203syl2an2r 684 . . . . . 6 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
205 f1of 6789 . . . . . . . . . 10 (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
206202, 205syl 17 . . . . . . . . 9 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
207 fvco3 6945 . . . . . . . . 9 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
208206, 207sylan 581 . . . . . . . 8 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
209124ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) = (𝐹𝑦))
210 simpr 486 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
21192ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
212210, 211eleqtrrd 2841 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))))
213 elun 4113 . . . . . . . . . . . 12 (𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
214212, 213sylib 217 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
215 nelne2 3043 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → 𝑀 ≠ 1)
21616, 101, 215sylancl 587 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ≠ 1)
217216adantr 482 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐶) → 𝑀 ≠ 1)
21822simp2d 1144 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹‘1) = 𝑀)
219218adantr 482 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐶) → (𝐹‘1) = 𝑀)
220 f1ofun 6791 . . . . . . . . . . . . . . . . . 18 (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
221196, 220syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐶) → Fun ({⟨1, 1⟩} ∪ 𝑐))
222 ssun1 4137 . . . . . . . . . . . . . . . . . 18 {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐)
22355snid 4627 . . . . . . . . . . . . . . . . . . 19 1 ∈ {1}
22455dmsnop 6173 . . . . . . . . . . . . . . . . . . 19 dom {⟨1, 1⟩} = {1}
225223, 224eleqtrri 2837 . . . . . . . . . . . . . . . . . 18 1 ∈ dom {⟨1, 1⟩}
226 funssfv 6868 . . . . . . . . . . . . . . . . . 18 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 1 ∈ dom {⟨1, 1⟩}) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
227222, 225, 226mp3an23 1454 . . . . . . . . . . . . . . . . 17 (Fun ({⟨1, 1⟩} ∪ 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
228221, 227syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
22955, 55fvsn 7132 . . . . . . . . . . . . . . . 16 ({⟨1, 1⟩}‘1) = 1
230228, 229eqtrdi 2793 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
231217, 219, 2303netr4d 3022 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐶) → (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1))
232 elsni 4608 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → 𝑦 = 1)
233232fveq2d 6851 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → (𝐹𝑦) = (𝐹‘1))
234232fveq2d 6851 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
235233, 234neeq12d 3006 . . . . . . . . . . . . . 14 (𝑦 ∈ {1} → ((𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1)))
236231, 235syl5ibrcom 247 . . . . . . . . . . . . 13 ((𝜑𝑐𝐶) → (𝑦 ∈ {1} → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
237236imp 408 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ {1}) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
238221adantr 482 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
239 ssun2 4138 . . . . . . . . . . . . . . . 16 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐)
240239a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
241 f1odm 6793 . . . . . . . . . . . . . . . . . 18 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → dom 𝑐 = (2...(𝑁 + 1)))
242193, 241syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐶) → dom 𝑐 = (2...(𝑁 + 1)))
243242eleq2d 2824 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → (𝑦 ∈ dom 𝑐𝑦 ∈ (2...(𝑁 + 1))))
244243biimpar 479 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ dom 𝑐)
245 funssfv 6868 . . . . . . . . . . . . . . 15 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑦 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
246238, 240, 244, 245syl3anc 1372 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
247 f1of 6789 . . . . . . . . . . . . . . . . . . . . 21 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
248193, 247syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐶) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
24916adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
250248, 249ffvelcdmd 7041 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐶) → (𝑐𝑀) ∈ (2...(𝑁 + 1)))
251 nelne2 3043 . . . . . . . . . . . . . . . . . . 19 (((𝑐𝑀) ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ 1)
252250, 101, 251sylancl 587 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐶) → (𝑐𝑀) ≠ 1)
253252adantr 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ 1)
25472ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑀) = 1)
255253, 254neeqtrrd 3019 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ (𝐹𝑀))
256 fveq2 6847 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑀 → (𝑐𝑦) = (𝑐𝑀))
257256, 130neeq12d 3006 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑀 → ((𝑐𝑦) ≠ (𝐹𝑦) ↔ (𝑐𝑀) ≠ (𝐹𝑀)))
258255, 257syl5ibrcom 247 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑐𝑦) ≠ (𝐹𝑦)))
259192simprd 497 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐶) → ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦)
260259r19.21bi 3237 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑦) ≠ 𝑦)
261260adantrr 716 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑐𝑦) ≠ 𝑦)
262145adantlr 714 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
263261, 262neeqtrrd 3019 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑐𝑦) ≠ (𝐹𝑦))
264263expr 458 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦𝑀 → (𝑐𝑦) ≠ (𝐹𝑦)))
265258, 264pm2.61dne 3032 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑦) ≠ (𝐹𝑦))
266246, 265eqnetrd 3012 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ≠ (𝐹𝑦))
267266necomd 3000 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
268237, 267jaodan 957 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1)))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
269214, 268syldan 592 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
270209, 269eqnetrd 3012 . . . . . . . . 9 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
27123adantr 482 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
272206ffvelcdmda 7040 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1)))
273 f1ocnvfv 7229 . . . . . . . . . . 11 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (𝐹𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
274271, 272, 273syl2an2r 684 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (𝐹𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
275274necon3d 2965 . . . . . . . . 9 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦))
276270, 275mpd 15 . . . . . . . 8 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦)
277208, 276eqnetrd 3012 . . . . . . 7 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
278277ralrimiva 3144 . . . . . 6 ((𝜑𝑐𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
279 snex 5393 . . . . . . . . 9 {⟨1, 1⟩} ∈ V
280279, 185unex 7685 . . . . . . . 8 ({⟨1, 1⟩} ∪ 𝑐) ∈ V
281171, 280coex 7872 . . . . . . 7 (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ V
282 f1oeq1 6777 . . . . . . . 8 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
283 fveq1 6846 . . . . . . . . . 10 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓𝑦) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦))
284283neeq1d 3004 . . . . . . . . 9 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
285284ralbidv 3175 . . . . . . . 8 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
286282, 285anbi12d 632 . . . . . . 7 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)))
287281, 286, 1elab2 3639 . . . . . 6 ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
288204, 278, 287sylanbrc 584 . . . . 5 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴)
28962adantr 482 . . . . . . . 8 ((𝜑𝑐𝐶) → 1 ∈ (1...(𝑁 + 1)))
290206, 289fvco3d 6946 . . . . . . 7 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
291230fveq2d 6851 . . . . . . 7 ((𝜑𝑐𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)) = (𝐹‘1))
292290, 291, 2193eqtrd 2781 . . . . . 6 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀)
293119, 16sselid 3947 . . . . . . . . . 10 (𝜑𝑀 ∈ (1...(𝑁 + 1)))
294293adantr 482 . . . . . . . . 9 ((𝜑𝑐𝐶) → 𝑀 ∈ (1...(𝑁 + 1)))
295206, 294fvco3d 6946 . . . . . . . 8 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
296239a1i 11 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
297249, 242eleqtrrd 2841 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑀 ∈ dom 𝑐)
298 funssfv 6868 . . . . . . . . . 10 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑀 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐𝑀))
299221, 296, 297, 298syl3anc 1372 . . . . . . . . 9 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐𝑀))
300299fveq2d 6851 . . . . . . . 8 ((𝜑𝑐𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)) = (𝐹‘(𝑐𝑀)))
301295, 300eqtrd 2777 . . . . . . 7 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(𝑐𝑀)))
302123fveq1d 6849 . . . . . . . . . . 11 (𝜑 → (𝐹‘1) = (𝐹‘1))
303302, 218eqtrd 2777 . . . . . . . . . 10 (𝜑 → (𝐹‘1) = 𝑀)
304303adantr 482 . . . . . . . . 9 ((𝜑𝑐𝐶) → (𝐹‘1) = 𝑀)
305 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑀𝑦 = 𝑀)
306256, 305neeq12d 3006 . . . . . . . . . . 11 (𝑦 = 𝑀 → ((𝑐𝑦) ≠ 𝑦 ↔ (𝑐𝑀) ≠ 𝑀))
307306, 259, 249rspcdva 3585 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (𝑐𝑀) ≠ 𝑀)
308307necomd 3000 . . . . . . . . 9 ((𝜑𝑐𝐶) → 𝑀 ≠ (𝑐𝑀))
309304, 308eqnetrd 3012 . . . . . . . 8 ((𝜑𝑐𝐶) → (𝐹‘1) ≠ (𝑐𝑀))
310119, 250sselid 3947 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (𝑐𝑀) ∈ (1...(𝑁 + 1)))
311 f1ocnvfv 7229 . . . . . . . . . 10 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑐𝑀) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑐𝑀)) = 1 → (𝐹‘1) = (𝑐𝑀)))
31223, 310, 311syl2an2r 684 . . . . . . . . 9 ((𝜑𝑐𝐶) → ((𝐹‘(𝑐𝑀)) = 1 → (𝐹‘1) = (𝑐𝑀)))
313312necon3d 2965 . . . . . . . 8 ((𝜑𝑐𝐶) → ((𝐹‘1) ≠ (𝑐𝑀) → (𝐹‘(𝑐𝑀)) ≠ 1))
314309, 313mpd 15 . . . . . . 7 ((𝜑𝑐𝐶) → (𝐹‘(𝑐𝑀)) ≠ 1)
315301, 314eqnetrd 3012 . . . . . 6 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)
316292, 315jca 513 . . . . 5 ((𝜑𝑐𝐶) → (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
317 fveq1 6846 . . . . . . . 8 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘1) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1))
318317eqeq1d 2739 . . . . . . 7 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘1) = 𝑀 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀))
319 fveq1 6846 . . . . . . . 8 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔𝑀) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀))
320319neeq1d 3004 . . . . . . 7 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔𝑀) ≠ 1 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
321318, 320anbi12d 632 . . . . . 6 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1) ↔ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
322321, 6elrab2 3653 . . . . 5 ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ∧ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
323288, 316, 322sylanbrc 584 . . . 4 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵)
32423adantr 482 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
325 f1of1 6788 . . . . . . 7 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
326324, 325syl 17 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
327 f1of 6789 . . . . . . . 8 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
328324, 327syl 17 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
32967adantrr 716 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
330328, 329fcod 6699 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
331206adantrl 715 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
332 cocan1 7242 . . . . . 6 ((𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ∧ (𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
333326, 330, 331, 332syl3anc 1372 . . . . 5 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
334 coass 6222 . . . . . . 7 ((𝐹𝐹) ∘ 𝑏) = (𝐹 ∘ (𝐹𝑏))
335123coeq1d 5822 . . . . . . . . . . 11 (𝜑 → (𝐹𝐹) = (𝐹𝐹))
336 f1ococnv1 6818 . . . . . . . . . . . 12 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
33723, 336syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
338335, 337eqtr3d 2779 . . . . . . . . . 10 (𝜑 → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
339338adantr 482 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
340339coeq1d 5822 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝐹) ∘ 𝑏) = (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏))
341 fcoi2 6722 . . . . . . . . 9 (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
342329, 341syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
343340, 342eqtrd 2777 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝐹) ∘ 𝑏) = 𝑏)
344334, 343eqtr3id 2791 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹 ∘ (𝐹𝑏)) = 𝑏)
345344eqeq1d 2739 . . . . 5 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))))
34674adantrr 716 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏)‘1) = 1)
347230adantrl 715 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
348346, 347eqtr4d 2780 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
349 fveq2 6847 . . . . . . . . . . . . 13 (𝑦 = 1 → ((𝐹𝑏)‘𝑦) = ((𝐹𝑏)‘1))
350 fveq2 6847 . . . . . . . . . . . . 13 (𝑦 = 1 → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
351349, 350eqeq12d 2753 . . . . . . . . . . . 12 (𝑦 = 1 → (((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1)))
35255, 351ralsn 4647 . . . . . . . . . . 11 (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
353348, 352sylibr 233 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
354353biantrurd 534 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))))
355 ralunb 4156 . . . . . . . . 9 (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
356354, 355bitr4di 289 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
357176adantl 483 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹𝑏)‘𝑦))
358357eqcomd 2743 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
359246adantlrl 719 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
360358, 359eqeq12d 2753 . . . . . . . . 9 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
361360ralbidva 3173 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
36292adantr 482 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
363362raleqdv 3316 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
364356, 361, 3633bitr3rd 310 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
36557adantrr 716 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
366202adantrl 715 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
367 f1ofn 6790 . . . . . . . . 9 (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
368366, 367syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
369 eqfnfv 6987 . . . . . . . 8 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1))) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
370365, 368, 369syl2anc 585 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
371 fnssres 6629 . . . . . . . . 9 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
372365, 119, 371sylancl 587 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
373193adantrl 715 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
374 f1ofn 6790 . . . . . . . . 9 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐 Fn (2...(𝑁 + 1)))
375373, 374syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑐 Fn (2...(𝑁 + 1)))
376 eqfnfv 6987 . . . . . . . 8 ((((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)) ∧ 𝑐 Fn (2...(𝑁 + 1))) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
377372, 375, 376syl2anc 585 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
378364, 370, 3773bitr4d 311 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐))
379 eqcom 2744 . . . . . 6 (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
380378, 379bitrdi 287 . . . . 5 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1)))))
381333, 345, 3803bitr3d 309 . . . 4 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1)))))
38212, 183, 323, 381f1o2d 7612 . . 3 (𝜑 → (𝑏𝐵 ↦ ((𝐹𝑏) ↾ (2...(𝑁 + 1)))):𝐵1-1-onto𝐶)
38311, 382hasheqf1od 14260 . 2 (𝜑 → (♯‘𝐵) = (♯‘𝐶))
38413, 14derangen2 33808 . . . . 5 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (𝑆‘(♯‘(2...(𝑁 + 1)))))
38513derangval 33801 . . . . . 6 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}))
386181fveq2i 6850 . . . . . 6 (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)})
387385, 386eqtr4di 2795 . . . . 5 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘𝐶))
388384, 387eqtr3d 2779 . . . 4 ((2...(𝑁 + 1)) ∈ Fin → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶))
389163, 388ax-mp 5 . . 3 (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶)
39015, 59eleqtrdi 2848 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ‘1))
391 eluzp1p1 12798 . . . . . . . 8 (𝑁 ∈ (ℤ‘1) → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
392390, 391syl 17 . . . . . . 7 (𝜑 → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
393 df-2 12223 . . . . . . . 8 2 = (1 + 1)
394393fveq2i 6850 . . . . . . 7 (ℤ‘2) = (ℤ‘(1 + 1))
395392, 394eleqtrrdi 2849 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ (ℤ‘2))
396 hashfz 14334 . . . . . 6 ((𝑁 + 1) ∈ (ℤ‘2) → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
397395, 396syl 17 . . . . 5 (𝜑 → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
39858nncnd 12176 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ ℂ)
399 2cnd 12238 . . . . . 6 (𝜑 → 2 ∈ ℂ)
400 1cnd 11157 . . . . . 6 (𝜑 → 1 ∈ ℂ)
401398, 399, 400subsubd 11547 . . . . 5 (𝜑 → ((𝑁 + 1) − (2 − 1)) = (((𝑁 + 1) − 2) + 1))
402 2m1e1 12286 . . . . . . 7 (2 − 1) = 1
403402oveq2i 7373 . . . . . 6 ((𝑁 + 1) − (2 − 1)) = ((𝑁 + 1) − 1)
40415nncnd 12176 . . . . . . 7 (𝜑𝑁 ∈ ℂ)
405 ax-1cn 11116 . . . . . . 7 1 ∈ ℂ
406 pncan 11414 . . . . . . 7 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
407404, 405, 406sylancl 587 . . . . . 6 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
408403, 407eqtrid 2789 . . . . 5 (𝜑 → ((𝑁 + 1) − (2 − 1)) = 𝑁)
409397, 401, 4083eqtr2d 2783 . . . 4 (𝜑 → (♯‘(2...(𝑁 + 1))) = 𝑁)
410409fveq2d 6851 . . 3 (𝜑 → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (𝑆𝑁))
411389, 410eqtr3id 2791 . 2 (𝜑 → (♯‘𝐶) = (𝑆𝑁))
412383, 411eqtrd 2777 1 (𝜑 → (♯‘𝐵) = (𝑆𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846   = wceq 1542  wcel 2107  {cab 2714  wne 2944  wral 3065  {crab 3410  Vcvv 3448  cdif 3912  cun 3913  cin 3914  wss 3915  c0 4287  {csn 4591  {cpr 4593  cop 4597   class class class wbr 5110  cmpt 5193   I cid 5535  ccnv 5637  dom cdm 5638  cres 5640  ccom 5642  Fun wfun 6495   Fn wfn 6496  wf 6497  1-1wf1 6498  ontowfo 6499  1-1-ontowf1o 6500  cfv 6501  (class class class)co 7362  Fincfn 8890  cc 11056  1c1 11059   + caddc 11061   < clt 11196  cle 11197  cmin 11392  cn 12160  2c2 12215  0cn0 12420  cz 12506  cuz 12770  ...cfz 13431  chash 14237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-n0 12421  df-xnn0 12493  df-z 12507  df-uz 12771  df-fz 13432  df-hash 14238
This theorem is referenced by:  subfacp1lem6  33819
  Copyright terms: Public domain W3C validator