subfacp1lem5 - Mathbox for Mario Carneiro

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

Theorem subfacp1lem5 31708

Description: Lemma for subfacp1 31710. In subfacp1lem6 31709 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	⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(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.

Step	Hyp	Ref	Expression
1		subfacp1lem.a	. . . . . . . 8 ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}
2		fzfi 13073	. . . . . . . . 9 ⊢ (1...(𝑁 + 1)) ∈ Fin
3		deranglem 31690	. . . . . . . . 9 ⊢ ((1...(𝑁 + 1)) ∈ Fin → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
4	2, 3	ax-mp 5	. . . . . . . 8 ⊢ {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin
5	1, 4	eqeltri 2902	. . . . . . 7 ⊢ 𝐴 ∈ Fin
6		subfacp1lem5.b	. . . . . . . 8 ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1)}
7		ssrab2 3914	. . . . . . . 8 ⊢ {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1)} ⊆ 𝐴
8	6, 7	eqsstri 3860	. . . . . . 7 ⊢ 𝐵 ⊆ 𝐴
9		ssfi 8455	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
10	5, 8, 9	mp2an 683	. . . . . 6 ⊢ 𝐵 ∈ Fin
11	10	elexi 3430	. . . . 5 ⊢ 𝐵 ∈ V
12	11	a1i 11	. . . 4 ⊢ (𝜑 → 𝐵 ∈ V)
13		subfacp1lem5.c	. . . . . . 7 ⊢ 𝐶 = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}
14		fzfi 13073	. . . . . . . 8 ⊢ (2...(𝑁 + 1)) ∈ Fin
15		deranglem 31690	. . . . . . . 8 ⊢ ((2...(𝑁 + 1)) ∈ Fin → {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
16	14, 15	ax-mp 5	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin
17	13, 16	eqeltri 2902	. . . . . 6 ⊢ 𝐶 ∈ Fin
18	17	elexi 3430	. . . . 5 ⊢ 𝐶 ∈ V
19	18	a1i 11	. . . 4 ⊢ (𝜑 → 𝐶 ∈ V)
20		derang.d	. . . . . . . . . . . . 13 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
21		subfac.n	. . . . . . . . . . . . 13 ⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(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 6419	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐾):𝐾–1-1-onto→𝐾
28	27	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐾):𝐾–1-1-onto→𝐾)
29	20, 21, 1, 22, 23, 24, 25, 26, 28	subfacp1lem2a 31704	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1))
30	29	simp1d 1176	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
31	30	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
32		simpr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
33		fveq1 6436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
34	33	eqeq1d 2827	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
35		fveq1 6436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑀) = (𝑏‘𝑀))
36	35	neeq1d 3058	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → ((𝑔‘𝑀) ≠ 1 ↔ (𝑏‘𝑀) ≠ 1))
37	34, 36	anbi12d 624	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
38	37, 6	elrab2 3589	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
39	32, 38	sylib 210	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
40	39	simpld 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
41		vex 3417	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ V
42		f1oeq1 6371	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
43		fveq1 6436	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
44	43	neeq1d 3058	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
45	44	ralbidv 3195	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
46	42, 45	anbi12d 624	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)))
47	41, 46, 1	elab2 3575	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
48	40, 47	sylib 210	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
49	48	simpld 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
50		f1oco 6404	. . . . . . . . . 10 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
51	31, 49, 50	syl2anc 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
52		f1of1 6381	. . . . . . . . 9 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
53		df-f1 6132	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun ^◡(𝐹 ∘ 𝑏)))
54	53	simprbi 492	. . . . . . . . 9 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun ^◡(𝐹 ∘ 𝑏))
55	51, 52, 54	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → Fun ^◡(𝐹 ∘ 𝑏))
56		f1ofn 6383	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
57		fnresdm 6237	. . . . . . . . . . 11 ⊢ ((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))) = (𝐹 ∘ 𝑏))
58		f1oeq1 6371	. . . . . . . . . . 11 ⊢ (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))) = (𝐹 ∘ 𝑏) → (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
59	51, 56, 57, 58	4syl 19	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
60	51, 59	mpbird 249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
61		f1ofo 6389	. . . . . . . . 9 ⊢ (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
62	60, 61	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
63		1ex 10359	. . . . . . . . . . 11 ⊢ 1 ∈ V
64	63, 63	f1osn 6421	. . . . . . . . . 10 ⊢ {⟨1, 1⟩}:{1}–1-1-onto→{1}
65	51, 56	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
66	22	peano2nnd 11376	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
67		nnuz 12012	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
68	66, 67	syl6eleq 2916	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘1))
69		eluzfz1 12648	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → 1 ∈ (1...(𝑁 + 1)))
70	68, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ (1...(𝑁 + 1)))
71	70	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 1 ∈ (1...(𝑁 + 1)))
72		fnressn 6681	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩})
73	65, 71, 72	syl2anc 579	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩})
74		f1of 6382	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
75	49, 74	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
76		fvco3 6526	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘1) = (𝐹‘(𝑏‘1)))
77	75, 71, 76	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏)‘1) = (𝐹‘(𝑏‘1)))
78	39	simprd 491	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1))
79	78	simpld 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) = 𝑀)
80	79	fveq2d 6441	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝑏‘1)) = (𝐹‘𝑀))
81	29	simp3d 1178	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘𝑀) = 1)
82	81	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑀) = 1)
83	77, 80, 82	3eqtrd 2865	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏)‘1) = 1)
84	83	opeq2d 4632	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ⟨1, ((𝐹 ∘ 𝑏)‘1)⟩ = ⟨1, 1⟩)
85	84	sneqd 4411	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩} = {⟨1, 1⟩})
86	73, 85	eqtrd 2861	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, 1⟩})
87		f1oeq1 6371	. . . . . . . . . . 11 ⊢ (((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, 1⟩} → (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} ↔ {⟨1, 1⟩}:{1}–1-1-onto→{1}))
88	86, 87	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} ↔ {⟨1, 1⟩}:{1}–1-1-onto→{1}))
89	64, 88	mpbiri 250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1})
90		f1ofo 6389	. . . . . . . . 9 ⊢ (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–onto→{1})
91	89, 90	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–onto→{1})
92		resdif 6402	. . . . . . . 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}))
93	55, 62, 91, 92	syl3anc 1494	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
94		fzsplit 12667	. . . . . . . . . . . 12 ⊢ (1 ∈ (1...(𝑁 + 1)) → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
95	70, 94	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
96		1z 11742	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℤ
97		fzsn 12683	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℤ → (1...1) = {1})
98	96, 97	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1...1) = {1}
99		1p1e2 11490	. . . . . . . . . . . . 13 ⊢ (1 + 1) = 2
100	99	oveq1i 6920	. . . . . . . . . . . 12 ⊢ ((1 + 1)...(𝑁 + 1)) = (2...(𝑁 + 1))
101	98, 100	uneq12i 3994	. . . . . . . . . . 11 ⊢ ((1...1) ∪ ((1 + 1)...(𝑁 + 1))) = ({1} ∪ (2...(𝑁 + 1)))
102	95, 101	syl6req 2878	. . . . . . . . . 10 ⊢ (𝜑 → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
103	70	snssd 4560	. . . . . . . . . . 11 ⊢ (𝜑 → {1} ⊆ (1...(𝑁 + 1)))
104		incom 4034	. . . . . . . . . . . 12 ⊢ ({1} ∩ (2...(𝑁 + 1))) = ((2...(𝑁 + 1)) ∩ {1})
105		1lt2 11536	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
106		1re 10363	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
107		2re 11432	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
108	106, 107	ltnlei 10484	. . . . . . . . . . . . . . 15 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
109	105, 108	mpbi 222	. . . . . . . . . . . . . 14 ⊢ ¬ 2 ≤ 1
110		elfzle1 12644	. . . . . . . . . . . . . 14 ⊢ (1 ∈ (2...(𝑁 + 1)) → 2 ≤ 1)
111	109, 110	mto 189	. . . . . . . . . . . . 13 ⊢ ¬ 1 ∈ (2...(𝑁 + 1))
112		disjsn 4467	. . . . . . . . . . . . 13 ⊢ (((2...(𝑁 + 1)) ∩ {1}) = ∅ ↔ ¬ 1 ∈ (2...(𝑁 + 1)))
113	111, 112	mpbir 223	. . . . . . . . . . . 12 ⊢ ((2...(𝑁 + 1)) ∩ {1}) = ∅
114	104, 113	eqtri 2849	. . . . . . . . . . 11 ⊢ ({1} ∩ (2...(𝑁 + 1))) = ∅
115		uneqdifeq 4282	. . . . . . . . . . 11 ⊢ (({1} ⊆ (1...(𝑁 + 1)) ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅) → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
116	103, 114, 115	sylancl 580	. . . . . . . . . 10 ⊢ (𝜑 → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
117	102, 116	mpbid 224	. . . . . . . . 9 ⊢ (𝜑 → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
118	117	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
119		reseq2 5628	. . . . . . . . . 10 ⊢ (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})) = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
120		f1oeq1 6371	. . . . . . . . . 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})))
121	119, 120	syl 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 6372	. . . . . . . . 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 6373	. . . . . . . . 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))))
124	121, 122, 123	3bitrd 297	. . . . . . . 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))))
125	118, 124	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
126	93, 125	mpbid 224	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
127	75	adantr 474	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
128		fzp1ss 12692	. . . . . . . . . . . 12 ⊢ (1 ∈ ℤ → ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1)))
129	96, 128	ax-mp 5	. . . . . . . . . . 11 ⊢ ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
130	100, 129	eqsstr3i 3861	. . . . . . . . . 10 ⊢ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
131		simpr 479	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (2...(𝑁 + 1)))
132	130, 131	sseldi 3825	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
133		fvco3 6526	. . . . . . . . 9 ⊢ ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (𝐹‘(𝑏‘𝑦)))
134	127, 132, 133	syl2anc 579	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (𝐹‘(𝑏‘𝑦)))
135	20, 21, 1, 22, 23, 24, 25, 6, 26	subfacp1lem4 31707	. . . . . . . . . . . 12 ⊢ (𝜑 → ^◡𝐹 = 𝐹)
136	135	fveq1d 6439	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
137	136	ad2antrr 717	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
138	78	simprd 491	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ≠ 1)
139	138, 82	neeqtrrd 3073	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ≠ (𝐹‘𝑀))
140	139	adantr 474	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑀) ≠ (𝐹‘𝑀))
141		fveq2 6437	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → (𝑏‘𝑦) = (𝑏‘𝑀))
142		fveq2 6437	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → (𝐹‘𝑦) = (𝐹‘𝑀))
143	141, 142	neeq12d 3060	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) ≠ (𝐹‘𝑦) ↔ (𝑏‘𝑀) ≠ (𝐹‘𝑀)))
144	140, 143	syl5ibrcom 239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑏‘𝑦) ≠ (𝐹‘𝑦)))
145	130	sseli 3823	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (2...(𝑁 + 1)) → 𝑦 ∈ (1...(𝑁 + 1)))
146	48	simprd 491	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)
147	146	r19.21bi 3141	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏‘𝑦) ≠ 𝑦)
148	145, 147	sylan2 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ≠ 𝑦)
149	148	adantrr 708	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑏‘𝑦) ≠ 𝑦)
150	25	eleq2i 2898	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝐾 ↔ 𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}))
151		eldifsn 4538	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀))
152	150, 151	bitri 267	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐾 ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀))
153	20, 21, 1, 22, 23, 24, 25, 26, 28	subfacp1lem2b 31705	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = (( I ↾ 𝐾)‘𝑦))
154		fvresi 6696	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝐾 → (( I ↾ 𝐾)‘𝑦) = 𝑦)
155	154	adantl 475	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (( I ↾ 𝐾)‘𝑦) = 𝑦)
156	153, 155	eqtrd 2861	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = 𝑦)
157	152, 156	sylan2br 588	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
158	157	adantlr 706	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
159	149, 158	neeqtrrd 3073	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑏‘𝑦) ≠ (𝐹‘𝑦))
160	159	expr 450	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 ≠ 𝑀 → (𝑏‘𝑦) ≠ (𝐹‘𝑦)))
161	144, 160	pm2.61dne 3085	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ≠ (𝐹‘𝑦))
162	161	necomd 3054	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (𝑏‘𝑦))
163	137, 162	eqnetrd 3066	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (^◡𝐹‘𝑦) ≠ (𝑏‘𝑦))
164	31	adantr 474	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
165		ffvelrn 6611	. . . . . . . . . . . 12 ⊢ ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏‘𝑦) ∈ (1...(𝑁 + 1)))
166	75, 145, 165	syl2an 589	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ∈ (1...(𝑁 + 1)))
167		f1ocnvfv 6794	. . . . . . . . . . 11 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑏‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑏‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (𝑏‘𝑦)))
168	164, 166, 167	syl2anc 579	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹‘(𝑏‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (𝑏‘𝑦)))
169	168	necon3d 3020	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((^◡𝐹‘𝑦) ≠ (𝑏‘𝑦) → (𝐹‘(𝑏‘𝑦)) ≠ 𝑦))
170	163, 169	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘(𝑏‘𝑦)) ≠ 𝑦)
171	134, 170	eqnetrd 3066	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)
172	171	ralrimiva 3175	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)
173		f1of 6382	. . . . . . . . . . . . 13 ⊢ (( I ↾ 𝐾):𝐾–1-1-onto→𝐾 → ( I ↾ 𝐾):𝐾⟶𝐾)
174	27, 173	ax-mp 5	. . . . . . . . . . . 12 ⊢ ( I ↾ 𝐾):𝐾⟶𝐾
175		difexg 5035	. . . . . . . . . . . . . 14 ⊢ ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V)
176	14, 175	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V
177	25, 176	eqeltri 2902	. . . . . . . . . . . 12 ⊢ 𝐾 ∈ V
178		fex 6750	. . . . . . . . . . . 12 ⊢ ((( I ↾ 𝐾):𝐾⟶𝐾 ∧ 𝐾 ∈ V) → ( I ↾ 𝐾) ∈ V)
179	174, 177, 178	mp2an 683	. . . . . . . . . . 11 ⊢ ( I ↾ 𝐾) ∈ V
180		prex 5132	. . . . . . . . . . 11 ⊢ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
181	179, 180	unex 7221	. . . . . . . . . 10 ⊢ (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
182	26, 181	eqeltri 2902	. . . . . . . . 9 ⊢ 𝐹 ∈ V
183	182, 41	coex 7385	. . . . . . . 8 ⊢ (𝐹 ∘ 𝑏) ∈ V
184	183	resex 5684	. . . . . . 7 ⊢ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ V
185		f1oeq1 6371	. . . . . . . 8 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
186		fveq1 6436	. . . . . . . . . . 11 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (𝑓‘𝑦) = (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
187		fvres 6456	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (2...(𝑁 + 1)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
188	186, 187	sylan9eq 2881	. . . . . . . . . 10 ⊢ ((𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑓‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
189	188	neeq1d 3058	. . . . . . . . 9 ⊢ ((𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
190	189	ralbidva 3194	. . . . . . . 8 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
191	185, 190	anbi12d 624	. . . . . . 7 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)))
192	184, 191, 13	elab2 3575	. . . . . 6 ⊢ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶 ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
193	126, 172, 192	sylanbrc 578	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶)
194	193	ex 403	. . . 4 ⊢ (𝜑 → (𝑏 ∈ 𝐵 → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶))
195	30	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
196		simpr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐 ∈ 𝐶)
197		vex 3417	. . . . . . . . . . . . 13 ⊢ 𝑐 ∈ V
198		f1oeq1 6371	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
199		fveq1 6436	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑐 → (𝑓‘𝑦) = (𝑐‘𝑦))
200	199	neeq1d 3058	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑐 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑦) ≠ 𝑦))
201	200	ralbidv 3195	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
202	198, 201	anbi12d 624	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦)))
203	197, 202, 13	elab2 3575	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
204	196, 203	sylib 210	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
205	204	simpld 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
206		f1oun 6401	. . . . . . . . . . 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))))
207	114, 114, 206	mpanr12 696	. . . . . . . . . 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))))
208	64, 205, 207	sylancr 581	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
209		f1oeq2 6372	. . . . . . . . . . . 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 6373	. . . . . . . . . . . 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))))
211	209, 210	bitrd 271	. . . . . . . . . . 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))))
212	102, 211	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
213	212	biimpa 470	. . . . . . . . 9 ⊢ ((𝜑 ∧ ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1)))) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
214	208, 213	syldan 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
215		f1oco 6404	. . . . . . . 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)))
216	195, 214, 215	syl2anc 579	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
217		f1of 6382	. . . . . . . . . . 11 ⊢ (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
218	214, 217	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
219		fvco3 6526	. . . . . . . . . 10 ⊢ ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
220	218, 219	sylan 575	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
221	136	ad2antrr 717	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
222		simpr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
223	102	ad2antrr 717	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
224	222, 223	eleqtrrd 2909	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))))
225		elun 3982	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
226	224, 225	sylib 210	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
227		nelne2 3096	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → 𝑀 ≠ 1)
228	23, 111, 227	sylancl 580	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ≠ 1)
229	228	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ 1)
230	29	simp2d 1177	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐹‘1) = 𝑀)
231	230	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘1) = 𝑀)
232		f1ofun 6384	. . . . . . . . . . . . . . . . . . 19 ⊢ (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
233	208, 232	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → Fun ({⟨1, 1⟩} ∪ 𝑐))
234		ssun1 4005	. . . . . . . . . . . . . . . . . . 19 ⊢ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐)
235	63	snid 4431	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ {1}
236	63	dmsnop 5854	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom {⟨1, 1⟩} = {1}
237	235, 236	eleqtrri 2905	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ dom {⟨1, 1⟩}
238		funssfv 6458	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 1 ∈ dom {⟨1, 1⟩}) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
239	234, 237, 238	mp3an23 1581	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun ({⟨1, 1⟩} ∪ 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
240	233, 239	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
241	63, 63	fvsn 6704	. . . . . . . . . . . . . . . . 17 ⊢ ({⟨1, 1⟩}‘1) = 1
242	240, 241	syl6eq 2877	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
243	229, 231, 242	3netr4d 3076	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1))
244		elsni 4416	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
245	244	fveq2d 6441	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {1} → (𝐹‘𝑦) = (𝐹‘1))
246	244	fveq2d 6441	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {1} → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
247	245, 246	neeq12d 3060	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {1} → ((𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1)))
248	243, 247	syl5ibrcom 239	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑦 ∈ {1} → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
249	248	imp 397	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ {1}) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
250	233	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
251		ssun2 4006	. . . . . . . . . . . . . . . . 17 ⊢ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐)
252	251	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
253		f1odm 6386	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → dom 𝑐 = (2...(𝑁 + 1)))
254	205, 253	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → dom 𝑐 = (2...(𝑁 + 1)))
255	254	eleq2d 2892	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑦 ∈ dom 𝑐 ↔ 𝑦 ∈ (2...(𝑁 + 1))))
256	255	biimpar 471	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ dom 𝑐)
257		funssfv 6458	. . . . . . . . . . . . . . . 16 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑦 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
258	250, 252, 256, 257	syl3anc 1494	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
259		f1of 6382	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
260	205, 259	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
261	23	adantr 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
262	260, 261	ffvelrnd 6614	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ∈ (2...(𝑁 + 1)))
263		nelne2 3096	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐‘𝑀) ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ 1)
264	262, 111, 263	sylancl 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ≠ 1)
265	264	adantr 474	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ 1)
266	81	ad2antrr 717	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑀) = 1)
267	265, 266	neeqtrrd 3073	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ (𝐹‘𝑀))
268		fveq2 6437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑀 → (𝑐‘𝑦) = (𝑐‘𝑀))
269	268, 142	neeq12d 3060	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑀 → ((𝑐‘𝑦) ≠ (𝐹‘𝑦) ↔ (𝑐‘𝑀) ≠ (𝐹‘𝑀)))
270	267, 269	syl5ibrcom 239	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑐‘𝑦) ≠ (𝐹‘𝑦)))
271	204	simprd 491	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦)
272	271	r19.21bi 3141	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑦) ≠ 𝑦)
273	272	adantrr 708	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑐‘𝑦) ≠ 𝑦)
274	157	adantlr 706	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
275	273, 274	neeqtrrd 3073	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑐‘𝑦) ≠ (𝐹‘𝑦))
276	275	expr 450	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 ≠ 𝑀 → (𝑐‘𝑦) ≠ (𝐹‘𝑦)))
277	270, 276	pm2.61dne 3085	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑦) ≠ (𝐹‘𝑦))
278	258, 277	eqnetrd 3066	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ≠ (𝐹‘𝑦))
279	278	necomd 3054	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
280	249, 279	jaodan 985	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1)))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
281	226, 280	syldan 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
282	221, 281	eqnetrd 3066	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (^◡𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
283	195	adantr 474	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
284	218	ffvelrnda 6613	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1)))
285		f1ocnvfv 6794	. . . . . . . . . . . 12 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
286	283, 284, 285	syl2anc 579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
287	286	necon3d 3020	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((^◡𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦))
288	282, 287	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦)
289	220, 288	eqnetrd 3066	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
290	289	ralrimiva 3175	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
291		snex 5131	. . . . . . . . . 10 ⊢ {⟨1, 1⟩} ∈ V
292	291, 197	unex 7221	. . . . . . . . 9 ⊢ ({⟨1, 1⟩} ∪ 𝑐) ∈ V
293	182, 292	coex 7385	. . . . . . . 8 ⊢ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ V
294		f1oeq1 6371	. . . . . . . . 9 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
295		fveq1 6436	. . . . . . . . . . 11 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓‘𝑦) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦))
296	295	neeq1d 3058	. . . . . . . . . 10 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
297	296	ralbidv 3195	. . . . . . . . 9 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
298	294, 297	anbi12d 624	. . . . . . . 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⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)))
299	293, 298, 1	elab2 3575	. . . . . . 7 ⊢ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
300	216, 290, 299	sylanbrc 578	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴)
301	70	adantr 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 1 ∈ (1...(𝑁 + 1)))
302		fvco3 6526	. . . . . . . . 9 ⊢ ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
303	218, 301, 302	syl2anc 579	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
304	242	fveq2d 6441	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)) = (𝐹‘1))
305	303, 304, 231	3eqtrd 2865	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀)
306	130, 23	sseldi 3825	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 + 1)))
307	306	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (1...(𝑁 + 1)))
308		fvco3 6526	. . . . . . . . . 10 ⊢ ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑀 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
309	218, 307, 308	syl2anc 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
310	251	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
311	261, 254	eleqtrrd 2909	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ dom 𝑐)
312		funssfv 6458	. . . . . . . . . . 11 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑀 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐‘𝑀))
313	233, 310, 311, 312	syl3anc 1494	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐‘𝑀))
314	313	fveq2d 6441	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)) = (𝐹‘(𝑐‘𝑀)))
315	309, 314	eqtrd 2861	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(𝑐‘𝑀)))
316	135	fveq1d 6439	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹‘1) = (𝐹‘1))
317	316, 230	eqtrd 2861	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹‘1) = 𝑀)
318	317	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (^◡𝐹‘1) = 𝑀)
319		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
320	268, 319	neeq12d 3060	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → ((𝑐‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑀) ≠ 𝑀))
321	320	rspcv 3522	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (2...(𝑁 + 1)) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦 → (𝑐‘𝑀) ≠ 𝑀))
322	261, 271, 321	sylc 65	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ≠ 𝑀)
323	322	necomd 3054	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ (𝑐‘𝑀))
324	318, 323	eqnetrd 3066	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (^◡𝐹‘1) ≠ (𝑐‘𝑀))
325	130, 262	sseldi 3825	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ∈ (1...(𝑁 + 1)))
326		f1ocnvfv 6794	. . . . . . . . . . 11 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑐‘𝑀) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑐‘𝑀)) = 1 → (^◡𝐹‘1) = (𝑐‘𝑀)))
327	195, 325, 326	syl2anc 579	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹‘(𝑐‘𝑀)) = 1 → (^◡𝐹‘1) = (𝑐‘𝑀)))
328	327	necon3d 3020	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((^◡𝐹‘1) ≠ (𝑐‘𝑀) → (𝐹‘(𝑐‘𝑀)) ≠ 1))
329	324, 328	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(𝑐‘𝑀)) ≠ 1)
330	315, 329	eqnetrd 3066	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)
331	305, 330	jca 507	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
332		fveq1 6436	. . . . . . . . 9 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘1) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1))
333	332	eqeq1d 2827	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘1) = 𝑀 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀))
334		fveq1 6436	. . . . . . . . 9 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘𝑀) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀))
335	334	neeq1d 3058	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘𝑀) ≠ 1 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
336	333, 335	anbi12d 624	. . . . . . 7 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1) ↔ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
337	336, 6	elrab2 3589	. . . . . 6 ⊢ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ∧ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
338	300, 331, 337	sylanbrc 578	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵)
339	338	ex 403	. . . 4 ⊢ (𝜑 → (𝑐 ∈ 𝐶 → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵))
340	30	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
341		f1of1 6381	. . . . . . . 8 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
342	340, 341	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
343		f1of 6382	. . . . . . . . 9 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
344	340, 343	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
345	75	adantrr 708	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
346		fco 6299	. . . . . . . 8 ⊢ ((𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
347	344, 345, 346	syl2anc 579	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
348	218	adantrl 707	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
349		cocan1 6806	. . . . . . 7 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ∧ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
350	342, 347, 348, 349	syl3anc 1494	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
351		coass 5899	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝐹) ∘ 𝑏) = (𝐹 ∘ (𝐹 ∘ 𝑏))
352	135	coeq1d 5520	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = (𝐹 ∘ 𝐹))
353		f1ococnv1 6410	. . . . . . . . . . . . 13 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (^◡𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
354	30, 353	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
355	352, 354	eqtr3d 2863	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
356	355	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
357	356	coeq1d 5520	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝐹) ∘ 𝑏) = (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏))
358		fcoi2 6320	. . . . . . . . . 10 ⊢ (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
359	345, 358	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
360	357, 359	eqtrd 2861	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝐹) ∘ 𝑏) = 𝑏)
361	351, 360	syl5eqr 2875	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ (𝐹 ∘ 𝑏)) = 𝑏)
362	361	eqeq1d 2827	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))))
363	83	adantrr 708	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏)‘1) = 1)
364	242	adantrl 707	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
365	363, 364	eqtr4d 2864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
366		fveq2 6437	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 1 → ((𝐹 ∘ 𝑏)‘𝑦) = ((𝐹 ∘ 𝑏)‘1))
367		fveq2 6437	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 1 → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
368	366, 367	eqeq12d 2840	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → (((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1)))
369	63, 368	ralsn 4444	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
370	365, 369	sylibr 226	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
371	370	biantrurd 528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))))
372		ralunb 4023	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
373	371, 372	syl6bbr 281	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
374	187	adantl 475	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
375	374	eqcomd 2831	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
376	258	adantlrl 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
377	375, 376	eqeq12d 2840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
378	377	ralbidva 3194	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
379	102	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
380	379	raleqdv 3356	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
381	373, 378, 380	3bitr3rd 302	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
382	65	adantrr 708	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
383	214	adantrl 707	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
384		f1ofn 6383	. . . . . . . . . 10 ⊢ (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
385	383, 384	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
386		eqfnfv 6565	. . . . . . . . 9 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
387	382, 385, 386	syl2anc 579	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
388		fnssres 6241	. . . . . . . . . 10 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
389	382, 130, 388	sylancl 580	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
390	205	adantrl 707	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
391		f1ofn 6383	. . . . . . . . . 10 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐 Fn (2...(𝑁 + 1)))
392	390, 391	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐 Fn (2...(𝑁 + 1)))
393		eqfnfv 6565	. . . . . . . . 9 ⊢ ((((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)) ∧ 𝑐 Fn (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
394	389, 392, 393	syl2anc 579	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
395	381, 387, 394	3bitr4d 303	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐))
396		eqcom 2832	. . . . . . 7 ⊢ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
397	395, 396	syl6bb 279	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))))
398	350, 362, 397	3bitr3d 301	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))))
399	398	ex 403	. . . 4 ⊢ (𝜑 → ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))))
400	12, 19, 194, 339, 399	en3d 8265	. . 3 ⊢ (𝜑 → 𝐵 ≈ 𝐶)
401		hashen 13434	. . . 4 ⊢ ((𝐵 ∈ Fin ∧ 𝐶 ∈ Fin) → ((♯‘𝐵) = (♯‘𝐶) ↔ 𝐵 ≈ 𝐶))
402	10, 17, 401	mp2an 683	. . 3 ⊢ ((♯‘𝐵) = (♯‘𝐶) ↔ 𝐵 ≈ 𝐶)
403	400, 402	sylibr 226	. 2 ⊢ (𝜑 → (♯‘𝐵) = (♯‘𝐶))
404	20, 21	derangen2 31698	. . . . 5 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (𝑆‘(♯‘(2...(𝑁 + 1)))))
405	20	derangval 31691	. . . . . 6 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}))
406	13	fveq2i 6440	. . . . . 6 ⊢ (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)})
407	405, 406	syl6eqr 2879	. . . . 5 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘𝐶))
408	404, 407	eqtr3d 2863	. . . 4 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶))
409	14, 408	ax-mp 5	. . 3 ⊢ (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶)
410	22, 67	syl6eleq 2916	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
411		eluzp1p1 12001	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝑁 + 1) ∈ (ℤ_≥‘(1 + 1)))
412	410, 411	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘(1 + 1)))
413		df-2 11421	. . . . . . . 8 ⊢ 2 = (1 + 1)
414	413	fveq2i 6440	. . . . . . 7 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
415	412, 414	syl6eleqr 2917	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘2))
416		hashfz 13510	. . . . . 6 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘2) → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
417	415, 416	syl 17	. . . . 5 ⊢ (𝜑 → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
418	66	nncnd 11375	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℂ)
419		2cnd 11436	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
420		1cnd 10358	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℂ)
421	418, 419, 420	subsubd 10748	. . . . 5 ⊢ (𝜑 → ((𝑁 + 1) − (2 − 1)) = (((𝑁 + 1) − 2) + 1))
422		2m1e1 11491	. . . . . . 7 ⊢ (2 − 1) = 1
423	422	oveq2i 6921	. . . . . 6 ⊢ ((𝑁 + 1) − (2 − 1)) = ((𝑁 + 1) − 1)
424	22	nncnd 11375	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
425		ax-1cn 10317	. . . . . . 7 ⊢ 1 ∈ ℂ
426		pncan 10614	. . . . . . 7 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
427	424, 425, 426	sylancl 580	. . . . . 6 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
428	423, 427	syl5eq 2873	. . . . 5 ⊢ (𝜑 → ((𝑁 + 1) − (2 − 1)) = 𝑁)
429	417, 421, 428	3eqtr2d 2867	. . . 4 ⊢ (𝜑 → (♯‘(2...(𝑁 + 1))) = 𝑁)
430	429	fveq2d 6441	. . 3 ⊢ (𝜑 → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (𝑆‘𝑁))
431	409, 430	syl5eqr 2875	. 2 ⊢ (𝜑 → (♯‘𝐶) = (𝑆‘𝑁))
432	403, 431	eqtrd 2861	1 ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 386 ∨ wo 878 = wceq 1656 ∈ wcel 2164 {cab 2811 ≠ wne 2999 ∀wral 3117 {crab 3121 Vcvv 3414 ∖ cdif 3795 ∪ cun 3796 ∩ cin 3797 ⊆ wss 3798 ∅c0 4146 {csn 4399 {cpr 4401 ⟨cop 4405 class class class wbr 4875 ↦ cmpt 4954 I cid 5251 ^◡ccnv 5345 dom cdm 5346 ↾ cres 5348 ∘ ccom 5350 Fun wfun 6121 Fn wfn 6122 ⟶wf 6123 –1-1→wf1 6124 –onto→wfo 6125 –1-1-onto→wf1o 6126 ‘cfv 6127 (class class class)co 6910 ≈ cen 8225 Fincfn 8228 ℂcc 10257 1c1 10260 + caddc 10262 < clt 10398 ≤ cle 10399 − cmin 10592 ℕcn 11357 2c2 11413 ℕ₀cn0 11625 ℤcz 11711 ℤ_≥cuz 11975 ...cfz 12626 ♯chash 13417

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-rep 4996 ax-sep 5007 ax-nul 5015 ax-pow 5067 ax-pr 5129 ax-un 7214 ax-cnex 10315 ax-resscn 10316 ax-1cn 10317 ax-icn 10318 ax-addcl 10319 ax-addrcl 10320 ax-mulcl 10321 ax-mulrcl 10322 ax-mulcom 10323 ax-addass 10324 ax-mulass 10325 ax-distr 10326 ax-i2m1 10327 ax-1ne0 10328 ax-1rid 10329 ax-rnegex 10330 ax-rrecex 10331 ax-cnre 10332 ax-pre-lttri 10333 ax-pre-lttrn 10334 ax-pre-ltadd 10335 ax-pre-mulgt0 10336

This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3or 1112 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-nel 3103 df-ral 3122 df-rex 3123 df-reu 3124 df-rmo 3125 df-rab 3126 df-v 3416 df-sbc 3663 df-csb 3758 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-pss 3814 df-nul 4147 df-if 4309 df-pw 4382 df-sn 4400 df-pr 4402 df-tp 4404 df-op 4406 df-uni 4661 df-int 4700 df-iun 4744 df-br 4876 df-opab 4938 df-mpt 4955 df-tr 4978 df-id 5252 df-eprel 5257 df-po 5265 df-so 5266 df-fr 5305 df-we 5307 df-xp 5352 df-rel 5353 df-cnv 5354 df-co 5355 df-dm 5356 df-rn 5357 df-res 5358 df-ima 5359 df-pred 5924 df-ord 5970 df-on 5971 df-lim 5972 df-suc 5973 df-iota 6090 df-fun 6129 df-fn 6130 df-f 6131 df-f1 6132 df-fo 6133 df-f1o 6134 df-fv 6135 df-riota 6871 df-ov 6913 df-oprab 6914 df-mpt2 6915 df-om 7332 df-1st 7433 df-2nd 7434 df-wrecs 7677 df-recs 7739 df-rdg 7777 df-1o 7831 df-2o 7832 df-oadd 7835 df-er 8014 df-map 8129 df-pm 8130 df-en 8229 df-dom 8230 df-sdom 8231 df-fin 8232 df-card 9085 df-cda 9312 df-pnf 10400 df-mnf 10401 df-xr 10402 df-ltxr 10403 df-le 10404 df-sub 10594 df-neg 10595 df-nn 11358 df-2 11421 df-n0 11626 df-xnn0 11698 df-z 11712 df-uz 11976 df-fz 12627 df-hash 13418

This theorem is referenced by: subfacp1lem6 31709

W3C validator