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 35574

Description: Lemma for subfacp1 35576. In subfacp1lem6 35575 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	. . . . . . 7 ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}
2		fzfi 14007	. . . . . . . 8 ⊢ (1...(𝑁 + 1)) ∈ Fin
3		deranglem 35556	. . . . . . . 8 ⊢ ((1...(𝑁 + 1)) ∈ Fin → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
4	2, 3	ax-mp 5	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin
5	1, 4	eqeltri 2865	. . . . . 6 ⊢ 𝐴 ∈ Fin
6		subfacp1lem5.b	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1)}
7	6	ssrab3 4044	. . . . . 6 ⊢ 𝐵 ⊆ 𝐴
8		ssfi 9156	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
9	5, 7, 8	mp2an 704	. . . . 5 ⊢ 𝐵 ∈ Fin
10	9	elexi 3485	. . . 4 ⊢ 𝐵 ∈ V
11	10	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
12		eqid 2769	. . . 4 ⊢ (𝑏 ∈ 𝐵 ↦ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))) = (𝑏 ∈ 𝐵 ↦ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
13		derang.d	. . . . . . . . . . 11 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
14		subfac.n	. . . . . . . . . . 11 ⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(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 6860	. . . . . . . . . . . 12 ⊢ ( I ↾ 𝐾):𝐾–1-1-onto→𝐾
21	20	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ( I ↾ 𝐾):𝐾–1-1-onto→𝐾)
22	13, 14, 1, 15, 16, 17, 18, 19, 21	subfacp1lem2a 35570	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1))
23	22	simp1d 1158	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
24		fveq1 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
25	24	eqeq1d 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
26		fveq1 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑀) = (𝑏‘𝑀))
27	26	neeq1d 3023	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → ((𝑔‘𝑀) ≠ 1 ↔ (𝑏‘𝑀) ≠ 1))
28	25, 27	anbi12d 643	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
29	28, 6	elrab2 3663	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
30	29	bilani 509	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
31	30	simpld 499	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
32		vex 3467	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
33		f1oeq1 6809	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
34		fveq1 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
35	34	neeq1d 3023	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
36	35	ralbidv 3194	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
37	33, 36	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)))
38	32, 37, 1	elab2 3650	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
39	31, 38	sylib 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
40	39	simpld 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
41		f1oco 6845	. . . . . . . . 9 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
42	23, 40, 41	syl2an2r 697	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
43		f1of1 6820	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
44		df-f1 6542	. . . . . . . . 9 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun ^◡(𝐹 ∘ 𝑏)))
45	44	simprbi 502	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun ^◡(𝐹 ∘ 𝑏))
46	42, 43, 45	3syl 19	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → Fun ^◡(𝐹 ∘ 𝑏))
47		f1ofn 6822	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
48		fnresdm 6655	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))) = (𝐹 ∘ 𝑏))
49		f1oeq1 6809	. . . . . . . . . 10 ⊢ (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))) = (𝐹 ∘ 𝑏) → (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
50	42, 47, 48, 49	4syl 20	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
51	42, 50	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
52		f1ofo 6829	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
53	51, 52	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
54		1ex 11202	. . . . . . . . . 10 ⊢ 1 ∈ V
55	54, 54	f1osn 6863	. . . . . . . . 9 ⊢ {⟨1, 1⟩}:{1}–1-1-onto→{1}
56	42, 47	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
57	15	peano2nnd 12249	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
58		nnuz 12900	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
59	57, 58	eleqtrdi 2879	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘1))
60		eluzfz1 13558	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → 1 ∈ (1...(𝑁 + 1)))
61	59, 60	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ (1...(𝑁 + 1)))
62	61	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 1 ∈ (1...(𝑁 + 1)))
63		fnressn 7156	. . . . . . . . . . . 12 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩})
64	56, 62, 63	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩})
65		f1of 6821	. . . . . . . . . . . . . . . 16 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
66	40, 65	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
67	66, 62	fvco3d 6983	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏)‘1) = (𝐹‘(𝑏‘1)))
68	30	simprd 500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1))
69	68	simpld 499	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) = 𝑀)
70	69	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝑏‘1)) = (𝐹‘𝑀))
71	22	simp3d 1160	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑀) = 1)
72	71	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑀) = 1)
73	67, 70, 72	3eqtrd 2808	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏)‘1) = 1)
74	73	opeq2d 4849	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ⟨1, ((𝐹 ∘ 𝑏)‘1)⟩ = ⟨1, 1⟩)
75	74	sneqd 4606	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩} = {⟨1, 1⟩})
76	64, 75	eqtrd 2804	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, 1⟩})
77	76	f1oeq1d 6816	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} ↔ {⟨1, 1⟩}:{1}–1-1-onto→{1}))
78	55, 77	mpbiri 261	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1})
79		f1ofo 6829	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–onto→{1})
80	78, 79	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–onto→{1})
81		resdif 6843	. . . . . . 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}))
82	46, 53, 80, 81	syl3anc 1396	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
83		fzsplit 13577	. . . . . . . . . . 11 ⊢ (1 ∈ (1...(𝑁 + 1)) → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
84	61, 83	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
85		1z 12623	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
86		fzsn 13593	. . . . . . . . . . . 12 ⊢ (1 ∈ ℤ → (1...1) = {1})
87	85, 86	ax-mp 5	. . . . . . . . . . 11 ⊢ (1...1) = {1}
88		1p1e2 12363	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
89	88	oveq1i 7421	. . . . . . . . . . 11 ⊢ ((1 + 1)...(𝑁 + 1)) = (2...(𝑁 + 1))
90	87, 89	uneq12i 4128	. . . . . . . . . 10 ⊢ ((1...1) ∪ ((1 + 1)...(𝑁 + 1))) = ({1} ∪ (2...(𝑁 + 1)))
91	84, 90	eqtr2di 2821	. . . . . . . . 9 ⊢ (𝜑 → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
92	61	snssd 4757	. . . . . . . . . 10 ⊢ (𝜑 → {1} ⊆ (1...(𝑁 + 1)))
93		incom 4170	. . . . . . . . . . 11 ⊢ ({1} ∩ (2...(𝑁 + 1))) = ((2...(𝑁 + 1)) ∩ {1})
94		1lt2 12412	. . . . . . . . . . . . . 14 ⊢ 1 < 2
95		1re 11207	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
96		2re 12314	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
97	95, 96	ltnlei 11330	. . . . . . . . . . . . . 14 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
98	94, 97	mpbi 233	. . . . . . . . . . . . 13 ⊢ ¬ 2 ≤ 1
99		elfzle1 13554	. . . . . . . . . . . . 13 ⊢ (1 ∈ (2...(𝑁 + 1)) → 2 ≤ 1)
100	98, 99	mto 200	. . . . . . . . . . . 12 ⊢ ¬ 1 ∈ (2...(𝑁 + 1))
101		disjsn 4682	. . . . . . . . . . . 12 ⊢ (((2...(𝑁 + 1)) ∩ {1}) = ∅ ↔ ¬ 1 ∈ (2...(𝑁 + 1)))
102	100, 101	mpbir 234	. . . . . . . . . . 11 ⊢ ((2...(𝑁 + 1)) ∩ {1}) = ∅
103	93, 102	eqtri 2792	. . . . . . . . . 10 ⊢ ({1} ∩ (2...(𝑁 + 1))) = ∅
104		uneqdifeq 4458	. . . . . . . . . 10 ⊢ (({1} ⊆ (1...(𝑁 + 1)) ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅) → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
105	92, 103, 104	sylancl 597	. . . . . . . . 9 ⊢ (𝜑 → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
106	91, 105	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
107	106	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
108		reseq2 5974	. . . . . . . . 9 ⊢ (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})) = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
109	108	f1oeq1d 6816	. . . . . . . 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})))
110		f1oeq2 6810	. . . . . . . 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})))
111		f1oeq3 6811	. . . . . . . 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))))
112	109, 110, 111	3bitrd 308	. . . . . . 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))))
113	107, 112	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
114	82, 113	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
115	66	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
116		fzp1ss 13602	. . . . . . . . . . 11 ⊢ (1 ∈ ℤ → ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1)))
117	85, 116	ax-mp 5	. . . . . . . . . 10 ⊢ ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
118	89, 117	eqsstrri 3992	. . . . . . . . 9 ⊢ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
119		simpr 489	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (2...(𝑁 + 1)))
120	118, 119	sselid 3943	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
121	115, 120	fvco3d 6983	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (𝐹‘(𝑏‘𝑦)))
122	13, 14, 1, 15, 16, 17, 18, 6, 19	subfacp1lem4 35573	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐹 = 𝐹)
123	122	fveq1d 6884	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
124	123	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
125	68	simprd 500	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ≠ 1)
126	125, 72	neeqtrrd 3038	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ≠ (𝐹‘𝑀))
127	126	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑀) ≠ (𝐹‘𝑀))
128		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → (𝑏‘𝑦) = (𝑏‘𝑀))
129		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → (𝐹‘𝑦) = (𝐹‘𝑀))
130	128, 129	neeq12d 3025	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) ≠ (𝐹‘𝑦) ↔ (𝑏‘𝑀) ≠ (𝐹‘𝑀)))
131	127, 130	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑏‘𝑦) ≠ (𝐹‘𝑦)))
132	118	sseli 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (2...(𝑁 + 1)) → 𝑦 ∈ (1...(𝑁 + 1)))
133	39	simprd 500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)
134	133	r19.21bi 3263	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏‘𝑦) ≠ 𝑦)
135	132, 134	sylan2 604	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ≠ 𝑦)
136	135	adantrr 729	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑏‘𝑦) ≠ 𝑦)
137	18	eleq2i 2861	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐾 ↔ 𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}))
138		eldifsn 4758	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀))
139	137, 138	bitri 278	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐾 ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀))
140	13, 14, 1, 15, 16, 17, 18, 19, 21	subfacp1lem2b 35571	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = (( I ↾ 𝐾)‘𝑦))
141		fvresi 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝐾 → (( I ↾ 𝐾)‘𝑦) = 𝑦)
142	141	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (( I ↾ 𝐾)‘𝑦) = 𝑦)
143	140, 142	eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = 𝑦)
144	139, 143	sylan2br 606	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
145	144	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
146	136, 145	neeqtrrd 3038	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑏‘𝑦) ≠ (𝐹‘𝑦))
147	146	expr 461	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 ≠ 𝑀 → (𝑏‘𝑦) ≠ (𝐹‘𝑦)))
148	131, 147	pm2.61dne 3050	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ≠ (𝐹‘𝑦))
149	148	necomd 3019	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (𝑏‘𝑦))
150	124, 149	eqnetrd 3031	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (^◡𝐹‘𝑦) ≠ (𝑏‘𝑦))
151	23	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
152		ffvelcdm 7077	. . . . . . . . . . 11 ⊢ ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏‘𝑦) ∈ (1...(𝑁 + 1)))
153	66, 132, 152	syl2an 607	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ∈ (1...(𝑁 + 1)))
154		f1ocnvfv 7277	. . . . . . . . . 10 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑏‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑏‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (𝑏‘𝑦)))
155	151, 153, 154	syl2an2r 697	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹‘(𝑏‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (𝑏‘𝑦)))
156	155	necon3d 2985	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((^◡𝐹‘𝑦) ≠ (𝑏‘𝑦) → (𝐹‘(𝑏‘𝑦)) ≠ 𝑦))
157	150, 156	mpd 16	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘(𝑏‘𝑦)) ≠ 𝑦)
158	121, 157	eqnetrd 3031	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)
159	158	ralrimiva 3163	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)
160		f1of 6821	. . . . . . . . . . . 12 ⊢ (( I ↾ 𝐾):𝐾–1-1-onto→𝐾 → ( I ↾ 𝐾):𝐾⟶𝐾)
161	20, 160	ax-mp 5	. . . . . . . . . . 11 ⊢ ( I ↾ 𝐾):𝐾⟶𝐾
162		fzfi 14007	. . . . . . . . . . . . 13 ⊢ (2...(𝑁 + 1)) ∈ Fin
163		difexg 5300	. . . . . . . . . . . . 13 ⊢ ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V)
164	162, 163	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V
165	18, 164	eqeltri 2865	. . . . . . . . . . 11 ⊢ 𝐾 ∈ V
166		fex 7225	. . . . . . . . . . 11 ⊢ ((( I ↾ 𝐾):𝐾⟶𝐾 ∧ 𝐾 ∈ V) → ( I ↾ 𝐾) ∈ V)
167	161, 165, 166	mp2an 704	. . . . . . . . . 10 ⊢ ( I ↾ 𝐾) ∈ V
168		prex 5410	. . . . . . . . . 10 ⊢ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
169	167, 168	unex 7742	. . . . . . . . 9 ⊢ (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
170	19, 169	eqeltri 2865	. . . . . . . 8 ⊢ 𝐹 ∈ V
171	170, 32	coex 7926	. . . . . . 7 ⊢ (𝐹 ∘ 𝑏) ∈ V
172	171	resex 6029	. . . . . 6 ⊢ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ V
173		f1oeq1 6809	. . . . . . 7 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
174		fveq1 6881	. . . . . . . . . 10 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (𝑓‘𝑦) = (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
175		fvres 6901	. . . . . . . . . 10 ⊢ (𝑦 ∈ (2...(𝑁 + 1)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
176	174, 175	sylan9eq 2824	. . . . . . . . 9 ⊢ ((𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑓‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
177	176	neeq1d 3023	. . . . . . . 8 ⊢ ((𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
178	177	ralbidva 3192	. . . . . . 7 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
179	173, 178	anbi12d 643	. . . . . 6 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)))
180		subfacp1lem5.c	. . . . . 6 ⊢ 𝐶 = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}
181	172, 179, 180	elab2 3650	. . . . 5 ⊢ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶 ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
182	114, 159, 181	sylanbrc 594	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶)
183		vex 3467	. . . . . . . . . . . 12 ⊢ 𝑐 ∈ V
184		f1oeq1 6809	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
185		fveq1 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑐 → (𝑓‘𝑦) = (𝑐‘𝑦))
186	185	neeq1d 3023	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑦) ≠ 𝑦))
187	186	ralbidv 3194	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
188	184, 187	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦)))
189	183, 188, 180	elab2 3650	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
190	189	bilani 509	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
191	190	simpld 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
192		f1oun 6841	. . . . . . . . . 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))))
193	103, 103, 192	mpanr12 717	. . . . . . . . 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))))
194	55, 191, 193	sylancr 598	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
195		f1oeq2 6810	. . . . . . . . . . 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)))))
196		f1oeq3 6811	. . . . . . . . . . 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))))
197	195, 196	bitrd 282	. . . . . . . . . 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))))
198	91, 197	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
199	198	biimpa 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1)))) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
200	194, 199	syldan 602	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
201		f1oco 6845	. . . . . . 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)))
202	23, 200, 201	syl2an2r 697	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
203		f1of 6821	. . . . . . . . . 10 ⊢ (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
204	200, 203	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
205		fvco3 6982	. . . . . . . . 9 ⊢ ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
206	204, 205	sylan 591	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
207	123	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
208		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
209	91	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
210	208, 209	eleqtrrd 2872	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))))
211		elun 4115	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
212	210, 211	sylib 221	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
213		nelne2 3062	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → 𝑀 ≠ 1)
214	16, 100, 213	sylancl 597	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≠ 1)
215	214	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ 1)
216	22	simp2d 1159	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘1) = 𝑀)
217	216	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘1) = 𝑀)
218		f1ofun 6823	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
219	194, 218	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → Fun ({⟨1, 1⟩} ∪ 𝑐))
220		ssun1 4139	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐)
221	54	snid 4633	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ {1}
222	54	dmsnop 6218	. . . . . . . . . . . . . . . . . . 19 ⊢ dom {⟨1, 1⟩} = {1}
223	221, 222	eleqtrri 2868	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ dom {⟨1, 1⟩}
224		funssfv 6903	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 1 ∈ dom {⟨1, 1⟩}) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
225	220, 223, 224	mp3an23 1479	. . . . . . . . . . . . . . . . 17 ⊢ (Fun ({⟨1, 1⟩} ∪ 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
226	219, 225	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
227	54, 54	fvsn 7180	. . . . . . . . . . . . . . . 16 ⊢ ({⟨1, 1⟩}‘1) = 1
228	226, 227	eqtrdi 2820	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
229	215, 217, 228	3netr4d 3041	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1))
230		elsni 4611	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
231	230	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {1} → (𝐹‘𝑦) = (𝐹‘1))
232	230	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {1} → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
233	231, 232	neeq12d 3025	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {1} → ((𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1)))
234	229, 233	syl5ibrcom 250	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑦 ∈ {1} → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
235	234	imp 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ {1}) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
236	219	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
237		ssun2 4140	. . . . . . . . . . . . . . . 16 ⊢ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐)
238	237	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
239		f1odm 6825	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → dom 𝑐 = (2...(𝑁 + 1)))
240	191, 239	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → dom 𝑐 = (2...(𝑁 + 1)))
241	240	eleq2d 2855	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑦 ∈ dom 𝑐 ↔ 𝑦 ∈ (2...(𝑁 + 1))))
242	241	biimpar 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ dom 𝑐)
243		funssfv 6903	. . . . . . . . . . . . . . 15 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑦 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
244	236, 238, 242, 243	syl3anc 1396	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
245		f1of 6821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
246	191, 245	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
247	16	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
248	246, 247	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ∈ (2...(𝑁 + 1)))
249		nelne2 3062	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐‘𝑀) ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ 1)
250	248, 100, 249	sylancl 597	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ≠ 1)
251	250	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ 1)
252	71	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑀) = 1)
253	251, 252	neeqtrrd 3038	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ (𝐹‘𝑀))
254		fveq2 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑀 → (𝑐‘𝑦) = (𝑐‘𝑀))
255	254, 129	neeq12d 3025	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑀 → ((𝑐‘𝑦) ≠ (𝐹‘𝑦) ↔ (𝑐‘𝑀) ≠ (𝐹‘𝑀)))
256	253, 255	syl5ibrcom 250	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑐‘𝑦) ≠ (𝐹‘𝑦)))
257	190	simprd 500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦)
258	257	r19.21bi 3263	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑦) ≠ 𝑦)
259	258	adantrr 729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑐‘𝑦) ≠ 𝑦)
260	144	adantlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
261	259, 260	neeqtrrd 3038	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑐‘𝑦) ≠ (𝐹‘𝑦))
262	261	expr 461	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 ≠ 𝑀 → (𝑐‘𝑦) ≠ (𝐹‘𝑦)))
263	256, 262	pm2.61dne 3050	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑦) ≠ (𝐹‘𝑦))
264	244, 263	eqnetrd 3031	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ≠ (𝐹‘𝑦))
265	264	necomd 3019	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
266	235, 265	jaodan 972	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1)))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
267	212, 266	syldan 602	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
268	207, 267	eqnetrd 3031	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (^◡𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
269	23	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
270	204	ffvelcdmda 7080	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1)))
271		f1ocnvfv 7277	. . . . . . . . . . 11 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
272	269, 270, 271	syl2an2r 697	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
273	272	necon3d 2985	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((^◡𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦))
274	268, 273	mpd 16	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦)
275	206, 274	eqnetrd 3031	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
276	275	ralrimiva 3163	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
277		snex 5411	. . . . . . . . 9 ⊢ {⟨1, 1⟩} ∈ V
278	277, 183	unex 7742	. . . . . . . 8 ⊢ ({⟨1, 1⟩} ∪ 𝑐) ∈ V
279	170, 278	coex 7926	. . . . . . 7 ⊢ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ V
280		f1oeq1 6809	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
281		fveq1 6881	. . . . . . . . . 10 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓‘𝑦) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦))
282	281	neeq1d 3023	. . . . . . . . 9 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
283	282	ralbidv 3194	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
284	280, 283	anbi12d 643	. . . . . . 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⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)))
285	279, 284, 1	elab2 3650	. . . . . 6 ⊢ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
286	202, 276, 285	sylanbrc 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴)
287	61	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 1 ∈ (1...(𝑁 + 1)))
288	204, 287	fvco3d 6983	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
289	228	fveq2d 6886	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)) = (𝐹‘1))
290	288, 289, 217	3eqtrd 2808	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀)
291	118, 16	sselid 3943	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 + 1)))
292	291	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (1...(𝑁 + 1)))
293	204, 292	fvco3d 6983	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
294	237	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
295	247, 240	eleqtrrd 2872	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ dom 𝑐)
296		funssfv 6903	. . . . . . . . . 10 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑀 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐‘𝑀))
297	219, 294, 295, 296	syl3anc 1396	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐‘𝑀))
298	297	fveq2d 6886	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)) = (𝐹‘(𝑐‘𝑀)))
299	293, 298	eqtrd 2804	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(𝑐‘𝑀)))
300	122	fveq1d 6884	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹‘1) = (𝐹‘1))
301	300, 216	eqtrd 2804	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹‘1) = 𝑀)
302	301	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (^◡𝐹‘1) = 𝑀)
303		id 23	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
304	254, 303	neeq12d 3025	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → ((𝑐‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑀) ≠ 𝑀))
305	304, 257, 247	rspcdva 3591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ≠ 𝑀)
306	305	necomd 3019	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ (𝑐‘𝑀))
307	302, 306	eqnetrd 3031	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (^◡𝐹‘1) ≠ (𝑐‘𝑀))
308	118, 248	sselid 3943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ∈ (1...(𝑁 + 1)))
309		f1ocnvfv 7277	. . . . . . . . . 10 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑐‘𝑀) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑐‘𝑀)) = 1 → (^◡𝐹‘1) = (𝑐‘𝑀)))
310	23, 308, 309	syl2an2r 697	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹‘(𝑐‘𝑀)) = 1 → (^◡𝐹‘1) = (𝑐‘𝑀)))
311	310	necon3d 2985	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((^◡𝐹‘1) ≠ (𝑐‘𝑀) → (𝐹‘(𝑐‘𝑀)) ≠ 1))
312	307, 311	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(𝑐‘𝑀)) ≠ 1)
313	299, 312	eqnetrd 3031	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)
314	290, 313	jca 520	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
315		fveq1 6881	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘1) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1))
316	315	eqeq1d 2771	. . . . . . 7 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘1) = 𝑀 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀))
317		fveq1 6881	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘𝑀) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀))
318	317	neeq1d 3023	. . . . . . 7 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘𝑀) ≠ 1 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
319	316, 318	anbi12d 643	. . . . . 6 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1) ↔ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
320	319, 6	elrab2 3663	. . . . 5 ⊢ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ∧ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
321	286, 314, 320	sylanbrc 594	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵)
322	23	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
323		f1of1 6820	. . . . . . 7 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
324	322, 323	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
325		f1of 6821	. . . . . . . 8 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
326	322, 325	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
327	66	adantrr 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
328	326, 327	fcod 6732	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
329	204	adantrl 728	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
330		cocan1 7290	. . . . . 6 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ∧ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
331	324, 328, 329, 330	syl3anc 1396	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
332		coass 6268	. . . . . . 7 ⊢ ((𝐹 ∘ 𝐹) ∘ 𝑏) = (𝐹 ∘ (𝐹 ∘ 𝑏))
333	122	coeq1d 5848	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = (𝐹 ∘ 𝐹))
334		f1ococnv1 6851	. . . . . . . . . . . 12 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (^◡𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
335	23, 334	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
336	333, 335	eqtr3d 2806	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
337	336	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
338	337	coeq1d 5848	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝐹) ∘ 𝑏) = (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏))
339		fcoi2 6754	. . . . . . . . 9 ⊢ (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
340	327, 339	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
341	338, 340	eqtrd 2804	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝐹) ∘ 𝑏) = 𝑏)
342	332, 341	eqtr3id 2818	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ (𝐹 ∘ 𝑏)) = 𝑏)
343	342	eqeq1d 2771	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))))
344	73	adantrr 729	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏)‘1) = 1)
345	228	adantrl 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
346	344, 345	eqtr4d 2807	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
347		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → ((𝐹 ∘ 𝑏)‘𝑦) = ((𝐹 ∘ 𝑏)‘1))
348		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
349	347, 348	eqeq12d 2785	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → (((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1)))
350	54, 349	ralsn 4652	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
351	346, 350	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
352	351	biantrurd 541	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))))
353		ralunb 4158	. . . . . . . . 9 ⊢ (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
354	352, 353	bitr4di 292	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
355	175	adantl 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
356	355	eqcomd 2775	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
357	244	adantlrl 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
358	356, 357	eqeq12d 2785	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
359	358	ralbidva 3192	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
360	91	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
361	360	raleqdv 3329	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
362	354, 359, 361	3bitr3rd 313	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
363	56	adantrr 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
364	200	adantrl 728	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
365		f1ofn 6822	. . . . . . . . 9 ⊢ (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
366	364, 365	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
367		eqfnfv 7026	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
368	363, 366, 367	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
369		fnssres 6659	. . . . . . . . 9 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
370	363, 118, 369	sylancl 597	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
371	191	adantrl 728	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
372		f1ofn 6822	. . . . . . . . 9 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐 Fn (2...(𝑁 + 1)))
373	371, 372	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐 Fn (2...(𝑁 + 1)))
374		eqfnfv 7026	. . . . . . . 8 ⊢ ((((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)) ∧ 𝑐 Fn (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
375	370, 373, 374	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
376	362, 368, 375	3bitr4d 314	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐))
377		eqcom 2776	. . . . . 6 ⊢ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
378	376, 377	bitrdi 290	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))))
379	331, 343, 378	3bitr3d 312	. . . 4 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))))
380	12, 182, 321, 379	f1o2d 7665	. . 3 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))):𝐵–1-1-onto→𝐶)
381	11, 380	hasheqf1od 14388	. 2 ⊢ (𝜑 → (♯‘𝐵) = (♯‘𝐶))
382	13, 14	derangen2 35564	. . . . 5 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (𝑆‘(♯‘(2...(𝑁 + 1)))))
383	13	derangval 35557	. . . . . 6 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}))
384	180	fveq2i 6885	. . . . . 6 ⊢ (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)})
385	383, 384	eqtr4di 2822	. . . . 5 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘𝐶))
386	382, 385	eqtr3d 2806	. . . 4 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶))
387	162, 386	ax-mp 5	. . 3 ⊢ (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶)
388	15, 58	eleqtrdi 2879	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
389		eluzp1p1 12889	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝑁 + 1) ∈ (ℤ_≥‘(1 + 1)))
390	388, 389	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘(1 + 1)))
391		df-2 12302	. . . . . . . 8 ⊢ 2 = (1 + 1)
392	391	fveq2i 6885	. . . . . . 7 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
393	390, 392	eleqtrrdi 2880	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘2))
394		hashfz 14463	. . . . . 6 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘2) → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
395	393, 394	syl 18	. . . . 5 ⊢ (𝜑 → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
396	57	nncnd 12248	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℂ)
397		2cnd 12318	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
398		1cnd 11201	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℂ)
399	396, 397, 398	subsubd 11596	. . . . 5 ⊢ (𝜑 → ((𝑁 + 1) − (2 − 1)) = (((𝑁 + 1) − 2) + 1))
400		2m1e1 12364	. . . . . . 7 ⊢ (2 − 1) = 1
401	400	oveq2i 7422	. . . . . 6 ⊢ ((𝑁 + 1) − (2 − 1)) = ((𝑁 + 1) − 1)
402	15	nncnd 12248	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
403		ax-1cn 11157	. . . . . . 7 ⊢ 1 ∈ ℂ
404		pncan 11462	. . . . . . 7 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
405	402, 403, 404	sylancl 597	. . . . . 6 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
406	401, 405	eqtrid 2816	. . . . 5 ⊢ (𝜑 → ((𝑁 + 1) − (2 − 1)) = 𝑁)
407	395, 399, 406	3eqtr2d 2810	. . . 4 ⊢ (𝜑 → (♯‘(2...(𝑁 + 1))) = 𝑁)
408	407	fveq2d 6886	. . 3 ⊢ (𝜑 → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (𝑆‘𝑁))
409	387, 408	eqtr3id 2818	. 2 ⊢ (𝜑 → (♯‘𝐶) = (𝑆‘𝑁))
410	381, 409	eqtrd 2804	1 ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1567 ∈ wcel 2149 {cab 2747 ≠ wne 2964 ∀wral 3085 {crab 3423 Vcvv 3463 ∖ cdif 3910 ∪ cun 3911 ∩ cin 3912 ⊆ wss 3913 ∅c0 4294 {csn 4594 {cpr 4596 ⟨cop 4600 class class class wbr 5113 ↦ cmpt 5196 I cid 5556 ^◡ccnv 5661 dom cdm 5662 ↾ cres 5664 ∘ ccom 5666 Fun wfun 6531 Fn wfn 6532 ⟶wf 6533 –1-1→wf1 6534 –onto→wfo 6535 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7411 Fincfn 8942 ℂcc 11097 1c1 11100 + caddc 11102 < clt 11242 ≤ cle 11243 − cmin 11440 ℕcn 12232 2c2 12294 ℕ₀cn0 12503 ℤcz 12590 ℤ_≥cuz 12861 ...cfz 13534 ♯chash 14365

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-oadd 8456 df-er 8693 df-map 8825 df-pm 8826 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-n0 12504 df-xnn0 12577 df-z 12591 df-uz 12862 df-fz 13535 df-hash 14366

This theorem is referenced by: subfacp1lem6 35575

W3C validator