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 35211

Description: Lemma for subfacp1 35213. In subfacp1lem6 35212 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 13995	. . . . . . . 8 ⊢ (1...(𝑁 + 1)) ∈ Fin
3		deranglem 35193	. . . . . . . 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 2831	. . . . . 6 ⊢ 𝐴 ∈ Fin
6		subfacp1lem5.b	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1)}
7	6	ssrab3 4062	. . . . . 6 ⊢ 𝐵 ⊆ 𝐴
8		ssfi 9192	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
9	5, 7, 8	mp2an 692	. . . . 5 ⊢ 𝐵 ∈ Fin
10	9	elexi 3487	. . . 4 ⊢ 𝐵 ∈ V
11	10	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
12		eqid 2736	. . . 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 6861	. . . . . . . . . . . 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 35207	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1))
23	22	simp1d 1142	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
24		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
25		fveq1 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
26	25	eqeq1d 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
27		fveq1 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑀) = (𝑏‘𝑀))
28	27	neeq1d 2992	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → ((𝑔‘𝑀) ≠ 1 ↔ (𝑏‘𝑀) ≠ 1))
29	26, 28	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
30	29, 6	elrab2 3679	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
31	24, 30	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
32	31	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
33		vex 3468	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
34		f1oeq1 6811	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
35		fveq1 6880	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
36	35	neeq1d 2992	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
37	36	ralbidv 3164	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
38	34, 37	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)))
39	33, 38, 1	elab2 3666	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
40	32, 39	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
41	40	simpld 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
42		f1oco 6846	. . . . . . . . 9 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
43	23, 41, 42	syl2an2r 685	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
44		f1of1 6822	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
45		df-f1 6541	. . . . . . . . 9 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun ^◡(𝐹 ∘ 𝑏)))
46	45	simprbi 496	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun ^◡(𝐹 ∘ 𝑏))
47	43, 44, 46	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → Fun ^◡(𝐹 ∘ 𝑏))
48		f1ofn 6824	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
49		fnresdm 6662	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))) = (𝐹 ∘ 𝑏))
50		f1oeq1 6811	. . . . . . . . . 10 ⊢ (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))) = (𝐹 ∘ 𝑏) → (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
51	43, 48, 49, 50	4syl 19	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
52	43, 51	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
53		f1ofo 6830	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
54	52, 53	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
55		1ex 11236	. . . . . . . . . 10 ⊢ 1 ∈ V
56	55, 55	f1osn 6863	. . . . . . . . 9 ⊢ {⟨1, 1⟩}:{1}–1-1-onto→{1}
57	43, 48	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
58	15	peano2nnd 12262	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
59		nnuz 12900	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
60	58, 59	eleqtrdi 2845	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘1))
61		eluzfz1 13553	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → 1 ∈ (1...(𝑁 + 1)))
62	60, 61	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ (1...(𝑁 + 1)))
63	62	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 1 ∈ (1...(𝑁 + 1)))
64		fnressn 7153	. . . . . . . . . . . 12 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩})
65	57, 63, 64	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩})
66		f1of 6823	. . . . . . . . . . . . . . . 16 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
67	41, 66	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
68	67, 63	fvco3d 6984	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏)‘1) = (𝐹‘(𝑏‘1)))
69	31	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1))
70	69	simpld 494	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) = 𝑀)
71	70	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝑏‘1)) = (𝐹‘𝑀))
72	22	simp3d 1144	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑀) = 1)
73	72	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑀) = 1)
74	68, 71, 73	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏)‘1) = 1)
75	74	opeq2d 4861	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ⟨1, ((𝐹 ∘ 𝑏)‘1)⟩ = ⟨1, 1⟩)
76	75	sneqd 4618	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩} = {⟨1, 1⟩})
77	65, 76	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, 1⟩})
78	77	f1oeq1d 6818	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} ↔ {⟨1, 1⟩}:{1}–1-1-onto→{1}))
79	56, 78	mpbiri 258	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1})
80		f1ofo 6830	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–onto→{1})
81	79, 80	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–onto→{1})
82		resdif 6844	. . . . . . 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}))
83	47, 54, 81, 82	syl3anc 1373	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
84		fzsplit 13572	. . . . . . . . . . 11 ⊢ (1 ∈ (1...(𝑁 + 1)) → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
85	62, 84	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
86		1z 12627	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
87		fzsn 13588	. . . . . . . . . . . 12 ⊢ (1 ∈ ℤ → (1...1) = {1})
88	86, 87	ax-mp 5	. . . . . . . . . . 11 ⊢ (1...1) = {1}
89		1p1e2 12370	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
90	89	oveq1i 7420	. . . . . . . . . . 11 ⊢ ((1 + 1)...(𝑁 + 1)) = (2...(𝑁 + 1))
91	88, 90	uneq12i 4146	. . . . . . . . . 10 ⊢ ((1...1) ∪ ((1 + 1)...(𝑁 + 1))) = ({1} ∪ (2...(𝑁 + 1)))
92	85, 91	eqtr2di 2788	. . . . . . . . 9 ⊢ (𝜑 → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
93	62	snssd 4790	. . . . . . . . . 10 ⊢ (𝜑 → {1} ⊆ (1...(𝑁 + 1)))
94		incom 4189	. . . . . . . . . . 11 ⊢ ({1} ∩ (2...(𝑁 + 1))) = ((2...(𝑁 + 1)) ∩ {1})
95		1lt2 12416	. . . . . . . . . . . . . 14 ⊢ 1 < 2
96		1re 11240	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
97		2re 12319	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
98	96, 97	ltnlei 11361	. . . . . . . . . . . . . 14 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
99	95, 98	mpbi 230	. . . . . . . . . . . . 13 ⊢ ¬ 2 ≤ 1
100		elfzle1 13549	. . . . . . . . . . . . 13 ⊢ (1 ∈ (2...(𝑁 + 1)) → 2 ≤ 1)
101	99, 100	mto 197	. . . . . . . . . . . 12 ⊢ ¬ 1 ∈ (2...(𝑁 + 1))
102		disjsn 4692	. . . . . . . . . . . 12 ⊢ (((2...(𝑁 + 1)) ∩ {1}) = ∅ ↔ ¬ 1 ∈ (2...(𝑁 + 1)))
103	101, 102	mpbir 231	. . . . . . . . . . 11 ⊢ ((2...(𝑁 + 1)) ∩ {1}) = ∅
104	94, 103	eqtri 2759	. . . . . . . . . 10 ⊢ ({1} ∩ (2...(𝑁 + 1))) = ∅
105		uneqdifeq 4473	. . . . . . . . . 10 ⊢ (({1} ⊆ (1...(𝑁 + 1)) ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅) → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
106	93, 104, 105	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
107	92, 106	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
108	107	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
109		reseq2 5966	. . . . . . . . 9 ⊢ (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})) = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
110	109	f1oeq1d 6818	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → (((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1})))
111		f1oeq2 6812	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→((1...(𝑁 + 1)) ∖ {1})))
112		f1oeq3 6813	. . . . . . . 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))))
113	110, 111, 112	3bitrd 305	. . . . . . 7 ⊢ (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → (((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
114	108, 113	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
115	83, 114	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
116	67	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
117		fzp1ss 13597	. . . . . . . . . . 11 ⊢ (1 ∈ ℤ → ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1)))
118	86, 117	ax-mp 5	. . . . . . . . . 10 ⊢ ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
119	90, 118	eqsstrri 4011	. . . . . . . . 9 ⊢ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
120		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (2...(𝑁 + 1)))
121	119, 120	sselid 3961	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
122	116, 121	fvco3d 6984	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (𝐹‘(𝑏‘𝑦)))
123	13, 14, 1, 15, 16, 17, 18, 6, 19	subfacp1lem4 35210	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐹 = 𝐹)
124	123	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
125	124	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
126	69	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ≠ 1)
127	126, 73	neeqtrrd 3007	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ≠ (𝐹‘𝑀))
128	127	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑀) ≠ (𝐹‘𝑀))
129		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → (𝑏‘𝑦) = (𝑏‘𝑀))
130		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → (𝐹‘𝑦) = (𝐹‘𝑀))
131	129, 130	neeq12d 2994	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) ≠ (𝐹‘𝑦) ↔ (𝑏‘𝑀) ≠ (𝐹‘𝑀)))
132	128, 131	syl5ibrcom 247	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑏‘𝑦) ≠ (𝐹‘𝑦)))
133	119	sseli 3959	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (2...(𝑁 + 1)) → 𝑦 ∈ (1...(𝑁 + 1)))
134	40	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)
135	134	r19.21bi 3238	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏‘𝑦) ≠ 𝑦)
136	133, 135	sylan2 593	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ≠ 𝑦)
137	136	adantrr 717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑏‘𝑦) ≠ 𝑦)
138	18	eleq2i 2827	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐾 ↔ 𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}))
139		eldifsn 4767	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀))
140	138, 139	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐾 ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀))
141	13, 14, 1, 15, 16, 17, 18, 19, 21	subfacp1lem2b 35208	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = (( I ↾ 𝐾)‘𝑦))
142		fvresi 7170	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝐾 → (( I ↾ 𝐾)‘𝑦) = 𝑦)
143	142	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (( I ↾ 𝐾)‘𝑦) = 𝑦)
144	141, 143	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = 𝑦)
145	140, 144	sylan2br 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
146	145	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
147	137, 146	neeqtrrd 3007	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑏‘𝑦) ≠ (𝐹‘𝑦))
148	147	expr 456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 ≠ 𝑀 → (𝑏‘𝑦) ≠ (𝐹‘𝑦)))
149	132, 148	pm2.61dne 3019	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ≠ (𝐹‘𝑦))
150	149	necomd 2988	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (𝑏‘𝑦))
151	125, 150	eqnetrd 3000	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (^◡𝐹‘𝑦) ≠ (𝑏‘𝑦))
152	23	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
153		ffvelcdm 7076	. . . . . . . . . . 11 ⊢ ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏‘𝑦) ∈ (1...(𝑁 + 1)))
154	67, 133, 153	syl2an 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ∈ (1...(𝑁 + 1)))
155		f1ocnvfv 7276	. . . . . . . . . 10 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑏‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑏‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (𝑏‘𝑦)))
156	152, 154, 155	syl2an2r 685	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹‘(𝑏‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (𝑏‘𝑦)))
157	156	necon3d 2954	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((^◡𝐹‘𝑦) ≠ (𝑏‘𝑦) → (𝐹‘(𝑏‘𝑦)) ≠ 𝑦))
158	151, 157	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘(𝑏‘𝑦)) ≠ 𝑦)
159	122, 158	eqnetrd 3000	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)
160	159	ralrimiva 3133	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)
161		f1of 6823	. . . . . . . . . . . 12 ⊢ (( I ↾ 𝐾):𝐾–1-1-onto→𝐾 → ( I ↾ 𝐾):𝐾⟶𝐾)
162	20, 161	ax-mp 5	. . . . . . . . . . 11 ⊢ ( I ↾ 𝐾):𝐾⟶𝐾
163		fzfi 13995	. . . . . . . . . . . . 13 ⊢ (2...(𝑁 + 1)) ∈ Fin
164		difexg 5304	. . . . . . . . . . . . 13 ⊢ ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V)
165	163, 164	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V
166	18, 165	eqeltri 2831	. . . . . . . . . . 11 ⊢ 𝐾 ∈ V
167		fex 7223	. . . . . . . . . . 11 ⊢ ((( I ↾ 𝐾):𝐾⟶𝐾 ∧ 𝐾 ∈ V) → ( I ↾ 𝐾) ∈ V)
168	162, 166, 167	mp2an 692	. . . . . . . . . 10 ⊢ ( I ↾ 𝐾) ∈ V
169		prex 5412	. . . . . . . . . 10 ⊢ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
170	168, 169	unex 7743	. . . . . . . . 9 ⊢ (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
171	19, 170	eqeltri 2831	. . . . . . . 8 ⊢ 𝐹 ∈ V
172	171, 33	coex 7931	. . . . . . 7 ⊢ (𝐹 ∘ 𝑏) ∈ V
173	172	resex 6021	. . . . . 6 ⊢ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ V
174		f1oeq1 6811	. . . . . . 7 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
175		fveq1 6880	. . . . . . . . . 10 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (𝑓‘𝑦) = (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
176		fvres 6900	. . . . . . . . . 10 ⊢ (𝑦 ∈ (2...(𝑁 + 1)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
177	175, 176	sylan9eq 2791	. . . . . . . . 9 ⊢ ((𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑓‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
178	177	neeq1d 2992	. . . . . . . 8 ⊢ ((𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
179	178	ralbidva 3162	. . . . . . 7 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
180	174, 179	anbi12d 632	. . . . . 6 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)))
181		subfacp1lem5.c	. . . . . 6 ⊢ 𝐶 = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}
182	173, 180, 181	elab2 3666	. . . . 5 ⊢ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶 ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
183	115, 160, 182	sylanbrc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶)
184		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐 ∈ 𝐶)
185		vex 3468	. . . . . . . . . . . 12 ⊢ 𝑐 ∈ V
186		f1oeq1 6811	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
187		fveq1 6880	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑐 → (𝑓‘𝑦) = (𝑐‘𝑦))
188	187	neeq1d 2992	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑦) ≠ 𝑦))
189	188	ralbidv 3164	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
190	186, 189	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦)))
191	185, 190, 181	elab2 3666	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
192	184, 191	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
193	192	simpld 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
194		f1oun 6842	. . . . . . . . . 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))))
195	104, 104, 194	mpanr12 705	. . . . . . . . 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))))
196	56, 193, 195	sylancr 587	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
197		f1oeq2 6812	. . . . . . . . . . 11 ⊢ (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) → (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→({1} ∪ (2...(𝑁 + 1)))))
198		f1oeq3 6813	. . . . . . . . . . 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))))
199	197, 198	bitrd 279	. . . . . . . . . 10 ⊢ (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) → (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
200	92, 199	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
201	200	biimpa 476	. . . . . . . 8 ⊢ ((𝜑 ∧ ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1)))) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
202	196, 201	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
203		f1oco 6846	. . . . . . 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)))
204	23, 202, 203	syl2an2r 685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
205		f1of 6823	. . . . . . . . . 10 ⊢ (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
206	202, 205	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
207		fvco3 6983	. . . . . . . . 9 ⊢ ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
208	206, 207	sylan 580	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
209	124	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
210		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
211	92	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
212	210, 211	eleqtrrd 2838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))))
213		elun 4133	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
214	212, 213	sylib 218	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
215		nelne2 3031	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → 𝑀 ≠ 1)
216	16, 101, 215	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≠ 1)
217	216	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ 1)
218	22	simp2d 1143	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘1) = 𝑀)
219	218	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘1) = 𝑀)
220		f1ofun 6825	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
221	196, 220	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → Fun ({⟨1, 1⟩} ∪ 𝑐))
222		ssun1 4158	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐)
223	55	snid 4643	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ {1}
224	55	dmsnop 6210	. . . . . . . . . . . . . . . . . . 19 ⊢ dom {⟨1, 1⟩} = {1}
225	223, 224	eleqtrri 2834	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ dom {⟨1, 1⟩}
226		funssfv 6902	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 1 ∈ dom {⟨1, 1⟩}) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
227	222, 225, 226	mp3an23 1455	. . . . . . . . . . . . . . . . 17 ⊢ (Fun ({⟨1, 1⟩} ∪ 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
228	221, 227	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
229	55, 55	fvsn 7178	. . . . . . . . . . . . . . . 16 ⊢ ({⟨1, 1⟩}‘1) = 1
230	228, 229	eqtrdi 2787	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
231	217, 219, 230	3netr4d 3010	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1))
232		elsni 4623	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
233	232	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {1} → (𝐹‘𝑦) = (𝐹‘1))
234	232	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {1} → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
235	233, 234	neeq12d 2994	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {1} → ((𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1)))
236	231, 235	syl5ibrcom 247	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑦 ∈ {1} → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
237	236	imp 406	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ {1}) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
238	221	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
239		ssun2 4159	. . . . . . . . . . . . . . . 16 ⊢ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐)
240	239	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
241		f1odm 6827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → dom 𝑐 = (2...(𝑁 + 1)))
242	193, 241	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → dom 𝑐 = (2...(𝑁 + 1)))
243	242	eleq2d 2821	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑦 ∈ dom 𝑐 ↔ 𝑦 ∈ (2...(𝑁 + 1))))
244	243	biimpar 477	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ dom 𝑐)
245		funssfv 6902	. . . . . . . . . . . . . . 15 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑦 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
246	238, 240, 244, 245	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
247		f1of 6823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
248	193, 247	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
249	16	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
250	248, 249	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ∈ (2...(𝑁 + 1)))
251		nelne2 3031	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐‘𝑀) ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ 1)
252	250, 101, 251	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ≠ 1)
253	252	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ 1)
254	72	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑀) = 1)
255	253, 254	neeqtrrd 3007	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ (𝐹‘𝑀))
256		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑀 → (𝑐‘𝑦) = (𝑐‘𝑀))
257	256, 130	neeq12d 2994	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑀 → ((𝑐‘𝑦) ≠ (𝐹‘𝑦) ↔ (𝑐‘𝑀) ≠ (𝐹‘𝑀)))
258	255, 257	syl5ibrcom 247	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑐‘𝑦) ≠ (𝐹‘𝑦)))
259	192	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦)
260	259	r19.21bi 3238	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑦) ≠ 𝑦)
261	260	adantrr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑐‘𝑦) ≠ 𝑦)
262	145	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
263	261, 262	neeqtrrd 3007	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑐‘𝑦) ≠ (𝐹‘𝑦))
264	263	expr 456	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 ≠ 𝑀 → (𝑐‘𝑦) ≠ (𝐹‘𝑦)))
265	258, 264	pm2.61dne 3019	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑦) ≠ (𝐹‘𝑦))
266	246, 265	eqnetrd 3000	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ≠ (𝐹‘𝑦))
267	266	necomd 2988	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
268	237, 267	jaodan 959	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1)))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
269	214, 268	syldan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
270	209, 269	eqnetrd 3000	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (^◡𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
271	23	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
272	206	ffvelcdmda 7079	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1)))
273		f1ocnvfv 7276	. . . . . . . . . . 11 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
274	271, 272, 273	syl2an2r 685	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
275	274	necon3d 2954	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((^◡𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦))
276	270, 275	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦)
277	208, 276	eqnetrd 3000	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
278	277	ralrimiva 3133	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
279		snex 5411	. . . . . . . . 9 ⊢ {⟨1, 1⟩} ∈ V
280	279, 185	unex 7743	. . . . . . . 8 ⊢ ({⟨1, 1⟩} ∪ 𝑐) ∈ V
281	171, 280	coex 7931	. . . . . . 7 ⊢ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ V
282		f1oeq1 6811	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
283		fveq1 6880	. . . . . . . . . 10 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓‘𝑦) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦))
284	283	neeq1d 2992	. . . . . . . . 9 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
285	284	ralbidv 3164	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
286	282, 285	anbi12d 632	. . . . . . 7 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)))
287	281, 286, 1	elab2 3666	. . . . . 6 ⊢ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
288	204, 278, 287	sylanbrc 583	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴)
289	62	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 1 ∈ (1...(𝑁 + 1)))
290	206, 289	fvco3d 6984	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
291	230	fveq2d 6885	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)) = (𝐹‘1))
292	290, 291, 219	3eqtrd 2775	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀)
293	119, 16	sselid 3961	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 + 1)))
294	293	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (1...(𝑁 + 1)))
295	206, 294	fvco3d 6984	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
296	239	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
297	249, 242	eleqtrrd 2838	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ dom 𝑐)
298		funssfv 6902	. . . . . . . . . 10 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑀 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐‘𝑀))
299	221, 296, 297, 298	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐‘𝑀))
300	299	fveq2d 6885	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)) = (𝐹‘(𝑐‘𝑀)))
301	295, 300	eqtrd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(𝑐‘𝑀)))
302	123	fveq1d 6883	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹‘1) = (𝐹‘1))
303	302, 218	eqtrd 2771	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹‘1) = 𝑀)
304	303	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (^◡𝐹‘1) = 𝑀)
305		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
306	256, 305	neeq12d 2994	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → ((𝑐‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑀) ≠ 𝑀))
307	306, 259, 249	rspcdva 3607	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ≠ 𝑀)
308	307	necomd 2988	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ (𝑐‘𝑀))
309	304, 308	eqnetrd 3000	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (^◡𝐹‘1) ≠ (𝑐‘𝑀))
310	119, 250	sselid 3961	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ∈ (1...(𝑁 + 1)))
311		f1ocnvfv 7276	. . . . . . . . . 10 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑐‘𝑀) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑐‘𝑀)) = 1 → (^◡𝐹‘1) = (𝑐‘𝑀)))
312	23, 310, 311	syl2an2r 685	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹‘(𝑐‘𝑀)) = 1 → (^◡𝐹‘1) = (𝑐‘𝑀)))
313	312	necon3d 2954	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((^◡𝐹‘1) ≠ (𝑐‘𝑀) → (𝐹‘(𝑐‘𝑀)) ≠ 1))
314	309, 313	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(𝑐‘𝑀)) ≠ 1)
315	301, 314	eqnetrd 3000	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)
316	292, 315	jca 511	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
317		fveq1 6880	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘1) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1))
318	317	eqeq1d 2738	. . . . . . 7 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘1) = 𝑀 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀))
319		fveq1 6880	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘𝑀) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀))
320	319	neeq1d 2992	. . . . . . 7 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘𝑀) ≠ 1 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
321	318, 320	anbi12d 632	. . . . . 6 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1) ↔ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
322	321, 6	elrab2 3679	. . . . 5 ⊢ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ∧ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
323	288, 316, 322	sylanbrc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵)
324	23	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
325		f1of1 6822	. . . . . . 7 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
326	324, 325	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
327		f1of 6823	. . . . . . . 8 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
328	324, 327	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
329	67	adantrr 717	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
330	328, 329	fcod 6736	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
331	206	adantrl 716	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
332		cocan1 7289	. . . . . 6 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ∧ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
333	326, 330, 331, 332	syl3anc 1373	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
334		coass 6259	. . . . . . 7 ⊢ ((𝐹 ∘ 𝐹) ∘ 𝑏) = (𝐹 ∘ (𝐹 ∘ 𝑏))
335	123	coeq1d 5846	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = (𝐹 ∘ 𝐹))
336		f1ococnv1 6852	. . . . . . . . . . . 12 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (^◡𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
337	23, 336	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
338	335, 337	eqtr3d 2773	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
339	338	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
340	339	coeq1d 5846	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝐹) ∘ 𝑏) = (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏))
341		fcoi2 6758	. . . . . . . . 9 ⊢ (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
342	329, 341	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
343	340, 342	eqtrd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝐹) ∘ 𝑏) = 𝑏)
344	334, 343	eqtr3id 2785	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ (𝐹 ∘ 𝑏)) = 𝑏)
345	344	eqeq1d 2738	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))))
346	74	adantrr 717	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏)‘1) = 1)
347	230	adantrl 716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
348	346, 347	eqtr4d 2774	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
349		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → ((𝐹 ∘ 𝑏)‘𝑦) = ((𝐹 ∘ 𝑏)‘1))
350		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
351	349, 350	eqeq12d 2752	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → (((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1)))
352	55, 351	ralsn 4662	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
353	348, 352	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
354	353	biantrurd 532	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))))
355		ralunb 4177	. . . . . . . . 9 ⊢ (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
356	354, 355	bitr4di 289	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
357	176	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
358	357	eqcomd 2742	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
359	246	adantlrl 720	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
360	358, 359	eqeq12d 2752	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
361	360	ralbidva 3162	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
362	92	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
363	362	raleqdv 3309	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
364	356, 361, 363	3bitr3rd 310	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
365	57	adantrr 717	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
366	202	adantrl 716	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
367		f1ofn 6824	. . . . . . . . 9 ⊢ (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
368	366, 367	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
369		eqfnfv 7026	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
370	365, 368, 369	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
371		fnssres 6666	. . . . . . . . 9 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
372	365, 119, 371	sylancl 586	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
373	193	adantrl 716	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
374		f1ofn 6824	. . . . . . . . 9 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐 Fn (2...(𝑁 + 1)))
375	373, 374	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐 Fn (2...(𝑁 + 1)))
376		eqfnfv 7026	. . . . . . . 8 ⊢ ((((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)) ∧ 𝑐 Fn (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
377	372, 375, 376	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
378	364, 370, 377	3bitr4d 311	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐))
379		eqcom 2743	. . . . . 6 ⊢ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
380	378, 379	bitrdi 287	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))))
381	333, 345, 380	3bitr3d 309	. . . 4 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))))
382	12, 183, 323, 381	f1o2d 7666	. . 3 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))):𝐵–1-1-onto→𝐶)
383	11, 382	hasheqf1od 14376	. 2 ⊢ (𝜑 → (♯‘𝐵) = (♯‘𝐶))
384	13, 14	derangen2 35201	. . . . 5 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (𝑆‘(♯‘(2...(𝑁 + 1)))))
385	13	derangval 35194	. . . . . 6 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}))
386	181	fveq2i 6884	. . . . . 6 ⊢ (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)})
387	385, 386	eqtr4di 2789	. . . . 5 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘𝐶))
388	384, 387	eqtr3d 2773	. . . 4 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶))
389	163, 388	ax-mp 5	. . 3 ⊢ (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶)
390	15, 59	eleqtrdi 2845	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
391		eluzp1p1 12885	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝑁 + 1) ∈ (ℤ_≥‘(1 + 1)))
392	390, 391	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘(1 + 1)))
393		df-2 12308	. . . . . . . 8 ⊢ 2 = (1 + 1)
394	393	fveq2i 6884	. . . . . . 7 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
395	392, 394	eleqtrrdi 2846	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘2))
396		hashfz 14450	. . . . . 6 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘2) → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
397	395, 396	syl 17	. . . . 5 ⊢ (𝜑 → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
398	58	nncnd 12261	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℂ)
399		2cnd 12323	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
400		1cnd 11235	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℂ)
401	398, 399, 400	subsubd 11627	. . . . 5 ⊢ (𝜑 → ((𝑁 + 1) − (2 − 1)) = (((𝑁 + 1) − 2) + 1))
402		2m1e1 12371	. . . . . . 7 ⊢ (2 − 1) = 1
403	402	oveq2i 7421	. . . . . 6 ⊢ ((𝑁 + 1) − (2 − 1)) = ((𝑁 + 1) − 1)
404	15	nncnd 12261	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
405		ax-1cn 11192	. . . . . . 7 ⊢ 1 ∈ ℂ
406		pncan 11493	. . . . . . 7 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
407	404, 405, 406	sylancl 586	. . . . . 6 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
408	403, 407	eqtrid 2783	. . . . 5 ⊢ (𝜑 → ((𝑁 + 1) − (2 − 1)) = 𝑁)
409	397, 401, 408	3eqtr2d 2777	. . . 4 ⊢ (𝜑 → (♯‘(2...(𝑁 + 1))) = 𝑁)
410	409	fveq2d 6885	. . 3 ⊢ (𝜑 → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (𝑆‘𝑁))
411	389, 410	eqtr3id 2785	. 2 ⊢ (𝜑 → (♯‘𝐶) = (𝑆‘𝑁))
412	383, 411	eqtrd 2771	1 ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 {cab 2714 ≠ wne 2933 ∀wral 3052 {crab 3420 Vcvv 3464 ∖ cdif 3928 ∪ cun 3929 ∩ cin 3930 ⊆ wss 3931 ∅c0 4313 {csn 4606 {cpr 4608 ⟨cop 4612 class class class wbr 5124 ↦ cmpt 5206 I cid 5552 ^◡ccnv 5658 dom cdm 5659 ↾ cres 5661 ∘ ccom 5663 Fun wfun 6530 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 –onto→wfo 6534 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 Fincfn 8964 ℂcc 11132 1c1 11135 + caddc 11137 < clt 11274 ≤ cle 11275 − cmin 11471 ℕcn 12245 2c2 12300 ℕ₀cn0 12506 ℤcz 12593 ℤ_≥cuz 12857 ...cfz 13529 ♯chash 14353

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-oadd 8489 df-er 8724 df-map 8847 df-pm 8848 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-dju 9920 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-nn 12246 df-2 12308 df-n0 12507 df-xnn0 12580 df-z 12594 df-uz 12858 df-fz 13530 df-hash 14354

This theorem is referenced by: subfacp1lem6 35212

W3C validator