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 33778
Description: Lemma for subfacp1 33780. In subfacp1lem6 33779 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 13877 . . . . . . . 8 (1...(𝑁 + 1)) ∈ Fin
3 deranglem 33760 . . . . . . . 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 4040 . . . . . 6 𝐵𝐴
8 ssfi 9117 . . . . . 6 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)
95, 7, 8mp2an 690 . . . . 5 𝐵 ∈ Fin
109elexi 3464 . . . 4 𝐵 ∈ V
1110a1i 11 . . 3 (𝜑𝐵 ∈ V)
12 eqid 2736 . . . 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 6822 . . . . . . . . . . . 12 ( I ↾ 𝐾):𝐾1-1-onto𝐾
2120a1i 11 . . . . . . . . . . 11 (𝜑 → ( I ↾ 𝐾):𝐾1-1-onto𝐾)
2213, 14, 1, 15, 16, 17, 18, 19, 21subfacp1lem2a 33774 . . . . . . . . . 10 (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹𝑀) = 1))
2322simp1d 1142 . . . . . . . . 9 (𝜑𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
24 simpr 485 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → 𝑏𝐵)
25 fveq1 6841 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
2625eqeq1d 2738 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
27 fveq1 6841 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑏 → (𝑔𝑀) = (𝑏𝑀))
2827neeq1d 3003 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → ((𝑔𝑀) ≠ 1 ↔ (𝑏𝑀) ≠ 1))
2926, 28anbi12d 631 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3029, 6elrab2 3648 . . . . . . . . . . . . 13 (𝑏𝐵 ↔ (𝑏𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3124, 30sylib 217 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → (𝑏𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1)))
3231simpld 495 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → 𝑏𝐴)
33 vex 3449 . . . . . . . . . . . 12 𝑏 ∈ V
34 f1oeq1 6772 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
35 fveq1 6841 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
3635neeq1d 3003 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑏𝑦) ≠ 𝑦))
3736ralbidv 3174 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
3834, 37anbi12d 631 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦)))
3933, 38, 1elab2 3634 . . . . . . . . . . 11 (𝑏𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4032, 39sylib 217 . . . . . . . . . 10 ((𝜑𝑏𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦))
4140simpld 495 . . . . . . . . 9 ((𝜑𝑏𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
42 f1oco 6807 . . . . . . . . 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 683 . . . . . . . 8 ((𝜑𝑏𝐵) → (𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
44 f1of1 6783 . . . . . . . 8 ((𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
45 df-f1 6501 . . . . . . . . 9 ((𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ ((𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun (𝐹𝑏)))
4645simprbi 497 . . . . . . . 8 ((𝐹𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun (𝐹𝑏))
4743, 44, 463syl 18 . . . . . . 7 ((𝜑𝑏𝐵) → Fun (𝐹𝑏))
48 f1ofn 6785 . . . . . . . . . 10 ((𝐹𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
49 fnresdm 6620 . . . . . . . . . 10 ((𝐹𝑏) Fn (1...(𝑁 + 1)) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))) = (𝐹𝑏))
50 f1oeq1 6772 . . . . . . . . . 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 256 . . . . . . . 8 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
53 f1ofo 6791 . . . . . . . 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 11151 . . . . . . . . . 10 1 ∈ V
5655, 55f1osn 6824 . . . . . . . . 9 {⟨1, 1⟩}:{1}–1-1-onto→{1}
5743, 48syl 17 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
5815peano2nnd 12170 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ ℕ)
59 nnuz 12806 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
6058, 59eleqtrdi 2848 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
61 eluzfz1 13448 . . . . . . . . . . . . . 14 ((𝑁 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑁 + 1)))
6260, 61syl 17 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ (1...(𝑁 + 1)))
6362adantr 481 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → 1 ∈ (1...(𝑁 + 1)))
64 fnressn 7104 . . . . . . . . . . . 12 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹𝑏) ↾ {1}) = {⟨1, ((𝐹𝑏)‘1)⟩})
6557, 63, 64syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}) = {⟨1, ((𝐹𝑏)‘1)⟩})
66 f1of 6784 . . . . . . . . . . . . . . . 16 (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
6741, 66syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
6867, 63fvco3d 6941 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → ((𝐹𝑏)‘1) = (𝐹‘(𝑏‘1)))
6931simprd 496 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏𝑀) ≠ 1))
7069simpld 495 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝑏‘1) = 𝑀)
7170fveq2d 6846 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → (𝐹‘(𝑏‘1)) = (𝐹𝑀))
7222simp3d 1144 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑀) = 1)
7372adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → (𝐹𝑀) = 1)
7468, 71, 733eqtrd 2780 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → ((𝐹𝑏)‘1) = 1)
7574opeq2d 4837 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ⟨1, ((𝐹𝑏)‘1)⟩ = ⟨1, 1⟩)
7675sneqd 4598 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → {⟨1, ((𝐹𝑏)‘1)⟩} = {⟨1, 1⟩})
7765, 76eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}) = {⟨1, 1⟩})
7877f1oeq1d 6779 . . . . . . . . 9 ((𝜑𝑏𝐵) → (((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1} ↔ {⟨1, 1⟩}:{1}–1-1-onto→{1}))
7956, 78mpbiri 257 . . . . . . . 8 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1})
80 f1ofo 6791 . . . . . . . 8 (((𝐹𝑏) ↾ {1}):{1}–1-1-onto→{1} → ((𝐹𝑏) ↾ {1}):{1}–onto→{1})
8179, 80syl 17 . . . . . . 7 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ {1}):{1}–onto→{1})
82 resdif 6805 . . . . . . 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 1371 . . . . . 6 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
84 fzsplit 13467 . . . . . . . . . . 11 (1 ∈ (1...(𝑁 + 1)) → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
8562, 84syl 17 . . . . . . . . . 10 (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
86 1z 12533 . . . . . . . . . . . 12 1 ∈ ℤ
87 fzsn 13483 . . . . . . . . . . . 12 (1 ∈ ℤ → (1...1) = {1})
8886, 87ax-mp 5 . . . . . . . . . . 11 (1...1) = {1}
89 1p1e2 12278 . . . . . . . . . . . 12 (1 + 1) = 2
9089oveq1i 7367 . . . . . . . . . . 11 ((1 + 1)...(𝑁 + 1)) = (2...(𝑁 + 1))
9188, 90uneq12i 4121 . . . . . . . . . 10 ((1...1) ∪ ((1 + 1)...(𝑁 + 1))) = ({1} ∪ (2...(𝑁 + 1)))
9285, 91eqtr2di 2793 . . . . . . . . 9 (𝜑 → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
9362snssd 4769 . . . . . . . . . 10 (𝜑 → {1} ⊆ (1...(𝑁 + 1)))
94 incom 4161 . . . . . . . . . . 11 ({1} ∩ (2...(𝑁 + 1))) = ((2...(𝑁 + 1)) ∩ {1})
95 1lt2 12324 . . . . . . . . . . . . . 14 1 < 2
96 1re 11155 . . . . . . . . . . . . . . 15 1 ∈ ℝ
97 2re 12227 . . . . . . . . . . . . . . 15 2 ∈ ℝ
9896, 97ltnlei 11276 . . . . . . . . . . . . . 14 (1 < 2 ↔ ¬ 2 ≤ 1)
9995, 98mpbi 229 . . . . . . . . . . . . 13 ¬ 2 ≤ 1
100 elfzle1 13444 . . . . . . . . . . . . 13 (1 ∈ (2...(𝑁 + 1)) → 2 ≤ 1)
10199, 100mto 196 . . . . . . . . . . . 12 ¬ 1 ∈ (2...(𝑁 + 1))
102 disjsn 4672 . . . . . . . . . . . 12 (((2...(𝑁 + 1)) ∩ {1}) = ∅ ↔ ¬ 1 ∈ (2...(𝑁 + 1)))
103101, 102mpbir 230 . . . . . . . . . . 11 ((2...(𝑁 + 1)) ∩ {1}) = ∅
10494, 103eqtri 2764 . . . . . . . . . 10 ({1} ∩ (2...(𝑁 + 1))) = ∅
105 uneqdifeq 4450 . . . . . . . . . 10 (({1} ⊆ (1...(𝑁 + 1)) ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅) → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
10693, 104, 105sylancl 586 . . . . . . . . 9 (𝜑 → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
10792, 106mpbid 231 . . . . . . . 8 (𝜑 → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
108107adantr 481 . . . . . . 7 ((𝜑𝑏𝐵) → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
109 reseq2 5932 . . . . . . . . 9 (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → ((𝐹𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})) = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
110109f1oeq1d 6779 . . . . . . . 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 6773 . . . . . . . 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 6774 . . . . . . . 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 304 . . . . . . 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 481 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
117 fzp1ss 13492 . . . . . . . . . . 11 (1 ∈ ℤ → ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1)))
11886, 117ax-mp 5 . . . . . . . . . 10 ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
11990, 118eqsstrri 3979 . . . . . . . . 9 (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
120 simpr 485 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (2...(𝑁 + 1)))
121119, 120sselid 3942 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
122116, 121fvco3d 6941 . . . . . . 7 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (𝐹‘(𝑏𝑦)))
12313, 14, 1, 15, 16, 17, 18, 6, 19subfacp1lem4 33777 . . . . . . . . . . 11 (𝜑𝐹 = 𝐹)
124123fveq1d 6844 . . . . . . . . . 10 (𝜑 → (𝐹𝑦) = (𝐹𝑦))
125124ad2antrr 724 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) = (𝐹𝑦))
12669simprd 496 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → (𝑏𝑀) ≠ 1)
127126, 73neeqtrrd 3018 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (𝑏𝑀) ≠ (𝐹𝑀))
128127adantr 481 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑀) ≠ (𝐹𝑀))
129 fveq2 6842 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → (𝑏𝑦) = (𝑏𝑀))
130 fveq2 6842 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → (𝐹𝑦) = (𝐹𝑀))
131129, 130neeq12d 3005 . . . . . . . . . . . 12 (𝑦 = 𝑀 → ((𝑏𝑦) ≠ (𝐹𝑦) ↔ (𝑏𝑀) ≠ (𝐹𝑀)))
132128, 131syl5ibrcom 246 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑏𝑦) ≠ (𝐹𝑦)))
133119sseli 3940 . . . . . . . . . . . . . . 15 (𝑦 ∈ (2...(𝑁 + 1)) → 𝑦 ∈ (1...(𝑁 + 1)))
13440simprd 496 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏𝑦) ≠ 𝑦)
135134r19.21bi 3234 . . . . . . . . . . . . . . 15 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏𝑦) ≠ 𝑦)
136133, 135sylan2 593 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ≠ 𝑦)
137136adantrr 715 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑏𝑦) ≠ 𝑦)
13818eleq2i 2829 . . . . . . . . . . . . . . . 16 (𝑦𝐾𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}))
139 eldifsn 4747 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀))
140138, 139bitri 274 . . . . . . . . . . . . . . 15 (𝑦𝐾 ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀))
14113, 14, 1, 15, 16, 17, 18, 19, 21subfacp1lem2b 33775 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐾) → (𝐹𝑦) = (( I ↾ 𝐾)‘𝑦))
142 fvresi 7119 . . . . . . . . . . . . . . . . 17 (𝑦𝐾 → (( I ↾ 𝐾)‘𝑦) = 𝑦)
143142adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐾) → (( I ↾ 𝐾)‘𝑦) = 𝑦)
144141, 143eqtrd 2776 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐾) → (𝐹𝑦) = 𝑦)
145140, 144sylan2br 595 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
146145adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
147137, 146neeqtrrd 3018 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑏𝑦) ≠ (𝐹𝑦))
148147expr 457 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦𝑀 → (𝑏𝑦) ≠ (𝐹𝑦)))
149132, 148pm2.61dne 3031 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ≠ (𝐹𝑦))
150149necomd 2999 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (𝑏𝑦))
151125, 150eqnetrd 3011 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (𝑏𝑦))
15223adantr 481 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
153 ffvelcdm 7032 . . . . . . . . . . 11 ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏𝑦) ∈ (1...(𝑁 + 1)))
15467, 133, 153syl2an 596 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏𝑦) ∈ (1...(𝑁 + 1)))
155 f1ocnvfv 7224 . . . . . . . . . 10 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑏𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑏𝑦)) = 𝑦 → (𝐹𝑦) = (𝑏𝑦)))
156152, 154, 155syl2an2r 683 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹‘(𝑏𝑦)) = 𝑦 → (𝐹𝑦) = (𝑏𝑦)))
157156necon3d 2964 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑦) ≠ (𝑏𝑦) → (𝐹‘(𝑏𝑦)) ≠ 𝑦))
158151, 157mpd 15 . . . . . . 7 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘(𝑏𝑦)) ≠ 𝑦)
159122, 158eqnetrd 3011 . . . . . 6 (((𝜑𝑏𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) ≠ 𝑦)
160159ralrimiva 3143 . . . . 5 ((𝜑𝑏𝐵) → ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦)
161 f1of 6784 . . . . . . . . . . . 12 (( I ↾ 𝐾):𝐾1-1-onto𝐾 → ( I ↾ 𝐾):𝐾𝐾)
16220, 161ax-mp 5 . . . . . . . . . . 11 ( I ↾ 𝐾):𝐾𝐾
163 fzfi 13877 . . . . . . . . . . . . 13 (2...(𝑁 + 1)) ∈ Fin
164 difexg 5284 . . . . . . . . . . . . 13 ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V)
165163, 164ax-mp 5 . . . . . . . . . . . 12 ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V
16618, 165eqeltri 2834 . . . . . . . . . . 11 𝐾 ∈ V
167 fex 7176 . . . . . . . . . . 11 ((( I ↾ 𝐾):𝐾𝐾𝐾 ∈ V) → ( I ↾ 𝐾) ∈ V)
168162, 166, 167mp2an 690 . . . . . . . . . 10 ( I ↾ 𝐾) ∈ V
169 prex 5389 . . . . . . . . . 10 {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
170168, 169unex 7680 . . . . . . . . 9 (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
17119, 170eqeltri 2834 . . . . . . . 8 𝐹 ∈ V
172171, 33coex 7867 . . . . . . 7 (𝐹𝑏) ∈ V
173172resex 5985 . . . . . 6 ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ V
174 f1oeq1 6772 . . . . . . 7 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
175 fveq1 6841 . . . . . . . . . 10 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (𝑓𝑦) = (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
176 fvres 6861 . . . . . . . . . 10 (𝑦 ∈ (2...(𝑁 + 1)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹𝑏)‘𝑦))
177175, 176sylan9eq 2796 . . . . . . . . 9 ((𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑓𝑦) = ((𝐹𝑏)‘𝑦))
178177neeq1d 3003 . . . . . . . 8 ((𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝑓𝑦) ≠ 𝑦 ↔ ((𝐹𝑏)‘𝑦) ≠ 𝑦))
179178ralbidva 3172 . . . . . . 7 (𝑓 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦))
180174, 179anbi12d 631 . . . . . 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 3634 . . . . 5 (((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶 ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) ≠ 𝑦))
183115, 160, 182sylanbrc 583 . . . 4 ((𝜑𝑏𝐵) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶)
184 simpr 485 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → 𝑐𝐶)
185 vex 3449 . . . . . . . . . . . 12 𝑐 ∈ V
186 f1oeq1 6772 . . . . . . . . . . . . 13 (𝑓 = 𝑐 → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
187 fveq1 6841 . . . . . . . . . . . . . . 15 (𝑓 = 𝑐 → (𝑓𝑦) = (𝑐𝑦))
188187neeq1d 3003 . . . . . . . . . . . . . 14 (𝑓 = 𝑐 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑐𝑦) ≠ 𝑦))
189188ralbidv 3174 . . . . . . . . . . . . 13 (𝑓 = 𝑐 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
190186, 189anbi12d 631 . . . . . . . . . . . 12 (𝑓 = 𝑐 → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦)))
191185, 190, 181elab2 3634 . . . . . . . . . . 11 (𝑐𝐶 ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
192184, 191sylib 217 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦))
193192simpld 495 . . . . . . . . 9 ((𝜑𝑐𝐶) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
194 f1oun 6803 . . . . . . . . . 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 703 . . . . . . . . 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 587 . . . . . . . 8 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
197 f1oeq2 6773 . . . . . . . . . . 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 6774 . . . . . . . . . . 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 278 . . . . . . . . . 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 477 . . . . . . . 8 ((𝜑 ∧ ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1)))) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
202196, 201syldan 591 . . . . . . 7 ((𝜑𝑐𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
203 f1oco 6807 . . . . . . 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 683 . . . . . 6 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
205 f1of 6784 . . . . . . . . . 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 6940 . . . . . . . . 9 ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
208206, 207sylan 580 . . . . . . . 8 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
209124ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) = (𝐹𝑦))
210 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
21192ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
212210, 211eleqtrrd 2841 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))))
213 elun 4108 . . . . . . . . . . . 12 (𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
214212, 213sylib 217 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
215 nelne2 3042 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → 𝑀 ≠ 1)
21616, 101, 215sylancl 586 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ≠ 1)
217216adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐶) → 𝑀 ≠ 1)
21822simp2d 1143 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹‘1) = 𝑀)
219218adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐶) → (𝐹‘1) = 𝑀)
220 f1ofun 6786 . . . . . . . . . . . . . . . . . 18 (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
221196, 220syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐶) → Fun ({⟨1, 1⟩} ∪ 𝑐))
222 ssun1 4132 . . . . . . . . . . . . . . . . . 18 {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐)
22355snid 4622 . . . . . . . . . . . . . . . . . . 19 1 ∈ {1}
22455dmsnop 6168 . . . . . . . . . . . . . . . . . . 19 dom {⟨1, 1⟩} = {1}
225223, 224eleqtrri 2837 . . . . . . . . . . . . . . . . . 18 1 ∈ dom {⟨1, 1⟩}
226 funssfv 6863 . . . . . . . . . . . . . . . . . 18 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 1 ∈ dom {⟨1, 1⟩}) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
227222, 225, 226mp3an23 1453 . . . . . . . . . . . . . . . . 17 (Fun ({⟨1, 1⟩} ∪ 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
228221, 227syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
22955, 55fvsn 7127 . . . . . . . . . . . . . . . 16 ({⟨1, 1⟩}‘1) = 1
230228, 229eqtrdi 2792 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
231217, 219, 2303netr4d 3021 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐶) → (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1))
232 elsni 4603 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → 𝑦 = 1)
233232fveq2d 6846 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → (𝐹𝑦) = (𝐹‘1))
234232fveq2d 6846 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
235233, 234neeq12d 3005 . . . . . . . . . . . . . 14 (𝑦 ∈ {1} → ((𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1)))
236231, 235syl5ibrcom 246 . . . . . . . . . . . . 13 ((𝜑𝑐𝐶) → (𝑦 ∈ {1} → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
237236imp 407 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ {1}) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
238221adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
239 ssun2 4133 . . . . . . . . . . . . . . . 16 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐)
240239a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
241 f1odm 6788 . . . . . . . . . . . . . . . . . 18 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → dom 𝑐 = (2...(𝑁 + 1)))
242193, 241syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐶) → dom 𝑐 = (2...(𝑁 + 1)))
243242eleq2d 2823 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐶) → (𝑦 ∈ dom 𝑐𝑦 ∈ (2...(𝑁 + 1))))
244243biimpar 478 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ dom 𝑐)
245 funssfv 6863 . . . . . . . . . . . . . . 15 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑦 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
246238, 240, 244, 245syl3anc 1371 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
247 f1of 6784 . . . . . . . . . . . . . . . . . . . . 21 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
248193, 247syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐶) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
24916adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
250248, 249ffvelcdmd 7036 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐶) → (𝑐𝑀) ∈ (2...(𝑁 + 1)))
251 nelne2 3042 . . . . . . . . . . . . . . . . . . 19 (((𝑐𝑀) ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ 1)
252250, 101, 251sylancl 586 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐶) → (𝑐𝑀) ≠ 1)
253252adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ 1)
25472ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑀) = 1)
255253, 254neeqtrrd 3018 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑀) ≠ (𝐹𝑀))
256 fveq2 6842 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑀 → (𝑐𝑦) = (𝑐𝑀))
257256, 130neeq12d 3005 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑀 → ((𝑐𝑦) ≠ (𝐹𝑦) ↔ (𝑐𝑀) ≠ (𝐹𝑀)))
258255, 257syl5ibrcom 246 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑐𝑦) ≠ (𝐹𝑦)))
259192simprd 496 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐶) → ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐𝑦) ≠ 𝑦)
260259r19.21bi 3234 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑦) ≠ 𝑦)
261260adantrr 715 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑐𝑦) ≠ 𝑦)
262145adantlr 713 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝐹𝑦) = 𝑦)
263261, 262neeqtrrd 3018 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦𝑀)) → (𝑐𝑦) ≠ (𝐹𝑦))
264263expr 457 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦𝑀 → (𝑐𝑦) ≠ (𝐹𝑦)))
265258, 264pm2.61dne 3031 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐𝑦) ≠ (𝐹𝑦))
266246, 265eqnetrd 3011 . . . . . . . . . . . . 13 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ≠ (𝐹𝑦))
267266necomd 2999 . . . . . . . . . . . 12 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
268237, 267jaodan 956 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1)))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
269214, 268syldan 591 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
270209, 269eqnetrd 3011 . . . . . . . . 9 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
27123adantr 481 . . . . . . . . . . 11 ((𝜑𝑐𝐶) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
272206ffvelcdmda 7035 . . . . . . . . . . 11 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1)))
273 f1ocnvfv 7224 . . . . . . . . . . 11 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (𝐹𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
274271, 272, 273syl2an2r 683 . . . . . . . . . 10 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (𝐹𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
275274necon3d 2964 . . . . . . . . 9 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦))
276270, 275mpd 15 . . . . . . . 8 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦)
277208, 276eqnetrd 3011 . . . . . . 7 (((𝜑𝑐𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
278277ralrimiva 3143 . . . . . 6 ((𝜑𝑐𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
279 snex 5388 . . . . . . . . 9 {⟨1, 1⟩} ∈ V
280279, 185unex 7680 . . . . . . . 8 ({⟨1, 1⟩} ∪ 𝑐) ∈ V
281171, 280coex 7867 . . . . . . 7 (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ V
282 f1oeq1 6772 . . . . . . . 8 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
283 fveq1 6841 . . . . . . . . . 10 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓𝑦) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦))
284283neeq1d 3003 . . . . . . . . 9 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
285284ralbidv 3174 . . . . . . . 8 (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
286282, 285anbi12d 631 . . . . . . 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 3634 . . . . . 6 ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
288204, 278, 287sylanbrc 583 . . . . 5 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴)
28962adantr 481 . . . . . . . 8 ((𝜑𝑐𝐶) → 1 ∈ (1...(𝑁 + 1)))
290206, 289fvco3d 6941 . . . . . . 7 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
291230fveq2d 6846 . . . . . . 7 ((𝜑𝑐𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)) = (𝐹‘1))
292290, 291, 2193eqtrd 2780 . . . . . 6 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀)
293119, 16sselid 3942 . . . . . . . . . 10 (𝜑𝑀 ∈ (1...(𝑁 + 1)))
294293adantr 481 . . . . . . . . 9 ((𝜑𝑐𝐶) → 𝑀 ∈ (1...(𝑁 + 1)))
295206, 294fvco3d 6941 . . . . . . . 8 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
296239a1i 11 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
297249, 242eleqtrrd 2841 . . . . . . . . . 10 ((𝜑𝑐𝐶) → 𝑀 ∈ dom 𝑐)
298 funssfv 6863 . . . . . . . . . 10 ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑀 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐𝑀))
299221, 296, 297, 298syl3anc 1371 . . . . . . . . 9 ((𝜑𝑐𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐𝑀))
300299fveq2d 6846 . . . . . . . 8 ((𝜑𝑐𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)) = (𝐹‘(𝑐𝑀)))
301295, 300eqtrd 2776 . . . . . . 7 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(𝑐𝑀)))
302123fveq1d 6844 . . . . . . . . . . 11 (𝜑 → (𝐹‘1) = (𝐹‘1))
303302, 218eqtrd 2776 . . . . . . . . . 10 (𝜑 → (𝐹‘1) = 𝑀)
304303adantr 481 . . . . . . . . 9 ((𝜑𝑐𝐶) → (𝐹‘1) = 𝑀)
305 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑀𝑦 = 𝑀)
306256, 305neeq12d 3005 . . . . . . . . . . 11 (𝑦 = 𝑀 → ((𝑐𝑦) ≠ 𝑦 ↔ (𝑐𝑀) ≠ 𝑀))
307306, 259, 249rspcdva 3582 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (𝑐𝑀) ≠ 𝑀)
308307necomd 2999 . . . . . . . . 9 ((𝜑𝑐𝐶) → 𝑀 ≠ (𝑐𝑀))
309304, 308eqnetrd 3011 . . . . . . . 8 ((𝜑𝑐𝐶) → (𝐹‘1) ≠ (𝑐𝑀))
310119, 250sselid 3942 . . . . . . . . . 10 ((𝜑𝑐𝐶) → (𝑐𝑀) ∈ (1...(𝑁 + 1)))
311 f1ocnvfv 7224 . . . . . . . . . 10 ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑐𝑀) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑐𝑀)) = 1 → (𝐹‘1) = (𝑐𝑀)))
31223, 310, 311syl2an2r 683 . . . . . . . . 9 ((𝜑𝑐𝐶) → ((𝐹‘(𝑐𝑀)) = 1 → (𝐹‘1) = (𝑐𝑀)))
313312necon3d 2964 . . . . . . . 8 ((𝜑𝑐𝐶) → ((𝐹‘1) ≠ (𝑐𝑀) → (𝐹‘(𝑐𝑀)) ≠ 1))
314309, 313mpd 15 . . . . . . 7 ((𝜑𝑐𝐶) → (𝐹‘(𝑐𝑀)) ≠ 1)
315301, 314eqnetrd 3011 . . . . . 6 ((𝜑𝑐𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)
316292, 315jca 512 . . . . 5 ((𝜑𝑐𝐶) → (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
317 fveq1 6841 . . . . . . . 8 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘1) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1))
318317eqeq1d 2738 . . . . . . 7 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘1) = 𝑀 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀))
319 fveq1 6841 . . . . . . . 8 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔𝑀) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀))
320319neeq1d 3003 . . . . . . 7 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔𝑀) ≠ 1 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
321318, 320anbi12d 631 . . . . . 6 (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (((𝑔‘1) = 𝑀 ∧ (𝑔𝑀) ≠ 1) ↔ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
322321, 6elrab2 3648 . . . . 5 ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ∧ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
323288, 316, 322sylanbrc 583 . . . 4 ((𝜑𝑐𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵)
32423adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
325 f1of1 6783 . . . . . . 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 6784 . . . . . . . 8 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
328324, 327syl 17 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
32967adantrr 715 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
330328, 329fcod 6694 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
331206adantrl 714 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
332 cocan1 7237 . . . . . 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 1371 . . . . 5 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
334 coass 6217 . . . . . . 7 ((𝐹𝐹) ∘ 𝑏) = (𝐹 ∘ (𝐹𝑏))
335123coeq1d 5817 . . . . . . . . . . 11 (𝜑 → (𝐹𝐹) = (𝐹𝐹))
336 f1ococnv1 6813 . . . . . . . . . . . 12 (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
33723, 336syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
338335, 337eqtr3d 2778 . . . . . . . . . 10 (𝜑 → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
339338adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝐹) = ( I ↾ (1...(𝑁 + 1))))
340339coeq1d 5817 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝐹) ∘ 𝑏) = (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏))
341 fcoi2 6717 . . . . . . . . 9 (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
342329, 341syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
343340, 342eqtrd 2776 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝐹) ∘ 𝑏) = 𝑏)
344334, 343eqtr3id 2790 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹 ∘ (𝐹𝑏)) = 𝑏)
345344eqeq1d 2738 . . . . 5 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹 ∘ (𝐹𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))))
34674adantrr 715 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏)‘1) = 1)
347230adantrl 714 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
348346, 347eqtr4d 2779 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
349 fveq2 6842 . . . . . . . . . . . . 13 (𝑦 = 1 → ((𝐹𝑏)‘𝑦) = ((𝐹𝑏)‘1))
350 fveq2 6842 . . . . . . . . . . . . 13 (𝑦 = 1 → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
351349, 350eqeq12d 2752 . . . . . . . . . . . 12 (𝑦 = 1 → (((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1)))
35255, 351ralsn 4642 . . . . . . . . . . 11 (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
353348, 352sylibr 233 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
354353biantrurd 533 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))))
355 ralunb 4151 . . . . . . . . 9 (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
356354, 355bitr4di 288 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
357176adantl 482 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹𝑏)‘𝑦))
358357eqcomd 2742 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹𝑏)‘𝑦) = (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
359246adantlrl 718 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐𝑦))
360358, 359eqeq12d 2752 . . . . . . . . 9 (((𝜑 ∧ (𝑏𝐵𝑐𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
361360ralbidva 3172 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
36292adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
363362raleqdv 3313 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
364356, 361, 3633bitr3rd 309 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
36557adantrr 715 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝐹𝑏) Fn (1...(𝑁 + 1)))
366202adantrl 714 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
367 f1ofn 6785 . . . . . . . . 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 6982 . . . . . . . 8 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1))) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
370365, 368, 369syl2anc 584 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
371 fnssres 6624 . . . . . . . . 9 (((𝐹𝑏) Fn (1...(𝑁 + 1)) ∧ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
372365, 119, 371sylancl 586 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
373193adantrl 714 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
374 f1ofn 6785 . . . . . . . . 9 (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐 Fn (2...(𝑁 + 1)))
375373, 374syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → 𝑐 Fn (2...(𝑁 + 1)))
376 eqfnfv 6982 . . . . . . . 8 ((((𝐹𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)) ∧ 𝑐 Fn (2...(𝑁 + 1))) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
377372, 375, 376syl2anc 584 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐𝑦)))
378364, 370, 3773bitr4d 310 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐))
379 eqcom 2743 . . . . . 6 (((𝐹𝑏) ↾ (2...(𝑁 + 1))) = 𝑐𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1))))
380378, 379bitrdi 286 . . . . 5 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → ((𝐹𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1)))))
381333, 345, 3803bitr3d 308 . . . 4 ((𝜑 ∧ (𝑏𝐵𝑐𝐶)) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹𝑏) ↾ (2...(𝑁 + 1)))))
38212, 183, 323, 381f1o2d 7607 . . 3 (𝜑 → (𝑏𝐵 ↦ ((𝐹𝑏) ↾ (2...(𝑁 + 1)))):𝐵1-1-onto𝐶)
38311, 382hasheqf1od 14253 . 2 (𝜑 → (♯‘𝐵) = (♯‘𝐶))
38413, 14derangen2 33768 . . . . 5 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (𝑆‘(♯‘(2...(𝑁 + 1)))))
38513derangval 33761 . . . . . 6 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}))
386181fveq2i 6845 . . . . . 6 (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)})
387385, 386eqtr4di 2794 . . . . 5 ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘𝐶))
388384, 387eqtr3d 2778 . . . 4 ((2...(𝑁 + 1)) ∈ Fin → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶))
389163, 388ax-mp 5 . . 3 (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶)
39015, 59eleqtrdi 2848 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ‘1))
391 eluzp1p1 12791 . . . . . . . 8 (𝑁 ∈ (ℤ‘1) → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
392390, 391syl 17 . . . . . . 7 (𝜑 → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
393 df-2 12216 . . . . . . . 8 2 = (1 + 1)
394393fveq2i 6845 . . . . . . 7 (ℤ‘2) = (ℤ‘(1 + 1))
395392, 394eleqtrrdi 2849 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ (ℤ‘2))
396 hashfz 14327 . . . . . 6 ((𝑁 + 1) ∈ (ℤ‘2) → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
397395, 396syl 17 . . . . 5 (𝜑 → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
39858nncnd 12169 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ ℂ)
399 2cnd 12231 . . . . . 6 (𝜑 → 2 ∈ ℂ)
400 1cnd 11150 . . . . . 6 (𝜑 → 1 ∈ ℂ)
401398, 399, 400subsubd 11540 . . . . 5 (𝜑 → ((𝑁 + 1) − (2 − 1)) = (((𝑁 + 1) − 2) + 1))
402 2m1e1 12279 . . . . . . 7 (2 − 1) = 1
403402oveq2i 7368 . . . . . 6 ((𝑁 + 1) − (2 − 1)) = ((𝑁 + 1) − 1)
40415nncnd 12169 . . . . . . 7 (𝜑𝑁 ∈ ℂ)
405 ax-1cn 11109 . . . . . . 7 1 ∈ ℂ
406 pncan 11407 . . . . . . 7 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
407404, 405, 406sylancl 586 . . . . . 6 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
408403, 407eqtrid 2788 . . . . 5 (𝜑 → ((𝑁 + 1) − (2 − 1)) = 𝑁)
409397, 401, 4083eqtr2d 2782 . . . 4 (𝜑 → (♯‘(2...(𝑁 + 1))) = 𝑁)
410409fveq2d 6846 . . 3 (𝜑 → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (𝑆𝑁))
411389, 410eqtr3id 2790 . 2 (𝜑 → (♯‘𝐶) = (𝑆𝑁))
412383, 411eqtrd 2776 1 (𝜑 → (♯‘𝐵) = (𝑆𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  {cab 2713  wne 2943  wral 3064  {crab 3407  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  {csn 4586  {cpr 4588  cop 4592   class class class wbr 5105  cmpt 5188   I cid 5530  ccnv 5632  dom cdm 5633  cres 5635  ccom 5637  Fun wfun 6490   Fn wfn 6491  wf 6492  1-1wf1 6493  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  Fincfn 8883  cc 11049  1c1 11052   + caddc 11054   < clt 11189  cle 11190  cmin 11385  cn 12153  2c2 12208  0cn0 12413  cz 12499  cuz 12763  ...cfz 13424  chash 14230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-fz 13425  df-hash 14231
This theorem is referenced by:  subfacp1lem6  33779
  Copyright terms: Public domain W3C validator