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 35412

Description: Lemma for subfacp1 35414. In subfacp1lem6 35413 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 13925	. . . . . . . 8 ⊢ (1...(𝑁 + 1)) ∈ Fin
3		deranglem 35394	. . . . . . . 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 2835	. . . . . 6 ⊢ 𝐴 ∈ Fin
6		subfacp1lem5.b	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1)}
7	6	ssrab3 4013	. . . . . 6 ⊢ 𝐵 ⊆ 𝐴
8		ssfi 9097	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
9	5, 7, 8	mp2an 698	. . . . 5 ⊢ 𝐵 ∈ Fin
10	9	elexi 3453	. . . 4 ⊢ 𝐵 ∈ V
11	10	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
12		eqid 2739	. . . 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 6805	. . . . . . . . . . . 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 35408	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1))
23	22	simp1d 1148	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
24		fveq1 6826	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
25	24	eqeq1d 2741	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
26		fveq1 6826	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑀) = (𝑏‘𝑀))
27	26	neeq1d 2993	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → ((𝑔‘𝑀) ≠ 1 ↔ (𝑏‘𝑀) ≠ 1))
28	25, 27	anbi12d 638	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
29	28, 6	elrab2 3632	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
30	29	bilani 505	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
31	30	simpld 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
32		vex 3435	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
33		f1oeq1 6755	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
34		fveq1 6826	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
35	34	neeq1d 2993	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
36	35	ralbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
37	33, 36	anbi12d 638	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)))
38	32, 37, 1	elab2 3620	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
39	31, 38	sylib 219	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
40	39	simpld 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
41		f1oco 6790	. . . . . . . . 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 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
43		f1of1 6766	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
44		df-f1 6490	. . . . . . . . 9 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun ^◡(𝐹 ∘ 𝑏)))
45	44	simprbi 498	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun ^◡(𝐹 ∘ 𝑏))
46	42, 43, 45	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → Fun ^◡(𝐹 ∘ 𝑏))
47		f1ofn 6768	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
48		fnresdm 6604	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))) = (𝐹 ∘ 𝑏))
49		f1oeq1 6755	. . . . . . . . . 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 19	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
51	42, 50	mpbird 258	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
52		f1ofo 6774	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
53	51, 52	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
54		1ex 11131	. . . . . . . . . 10 ⊢ 1 ∈ V
55	54, 54	f1osn 6808	. . . . . . . . 9 ⊢ {⟨1, 1⟩}:{1}–1-1-onto→{1}
56	42, 47	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
57	15	peano2nnd 12182	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
58		nnuz 12818	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
59	57, 58	eleqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘1))
60		eluzfz1 13476	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → 1 ∈ (1...(𝑁 + 1)))
61	59, 60	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ (1...(𝑁 + 1)))
62	61	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 1 ∈ (1...(𝑁 + 1)))
63		fnressn 7101	. . . . . . . . . . . 12 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩})
64	56, 62, 63	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩})
65		f1of 6767	. . . . . . . . . . . . . . . 16 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
66	40, 65	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
67	66, 62	fvco3d 6928	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏)‘1) = (𝐹‘(𝑏‘1)))
68	30	simprd 496	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1))
69	68	simpld 495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) = 𝑀)
70	69	fveq2d 6831	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝑏‘1)) = (𝐹‘𝑀))
71	22	simp3d 1150	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑀) = 1)
72	71	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑀) = 1)
73	67, 70, 72	3eqtrd 2778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏)‘1) = 1)
74	73	opeq2d 4811	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ⟨1, ((𝐹 ∘ 𝑏)‘1)⟩ = ⟨1, 1⟩)
75	74	sneqd 4567	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩} = {⟨1, 1⟩})
76	64, 75	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, 1⟩})
77	76	f1oeq1d 6762	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} ↔ {⟨1, 1⟩}:{1}–1-1-onto→{1}))
78	55, 77	mpbiri 259	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1})
79		f1ofo 6774	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–onto→{1})
80	78, 79	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–onto→{1})
81		resdif 6788	. . . . . . 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 1379	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
83		fzsplit 13495	. . . . . . . . . . 11 ⊢ (1 ∈ (1...(𝑁 + 1)) → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
84	61, 83	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
85		1z 12548	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
86		fzsn 13511	. . . . . . . . . . . 12 ⊢ (1 ∈ ℤ → (1...1) = {1})
87	85, 86	ax-mp 5	. . . . . . . . . . 11 ⊢ (1...1) = {1}
88		1p1e2 12292	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
89	88	oveq1i 7366	. . . . . . . . . . 11 ⊢ ((1 + 1)...(𝑁 + 1)) = (2...(𝑁 + 1))
90	87, 89	uneq12i 4096	. . . . . . . . . 10 ⊢ ((1...1) ∪ ((1 + 1)...(𝑁 + 1))) = ({1} ∪ (2...(𝑁 + 1)))
91	84, 90	eqtr2di 2791	. . . . . . . . 9 ⊢ (𝜑 → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
92	61	snssd 4718	. . . . . . . . . 10 ⊢ (𝜑 → {1} ⊆ (1...(𝑁 + 1)))
93		incom 4138	. . . . . . . . . . 11 ⊢ ({1} ∩ (2...(𝑁 + 1))) = ((2...(𝑁 + 1)) ∩ {1})
94		1lt2 12338	. . . . . . . . . . . . . 14 ⊢ 1 < 2
95		1re 11135	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
96		2re 12246	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
97	95, 96	ltnlei 11258	. . . . . . . . . . . . . 14 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
98	94, 97	mpbi 231	. . . . . . . . . . . . 13 ⊢ ¬ 2 ≤ 1
99		elfzle1 13472	. . . . . . . . . . . . 13 ⊢ (1 ∈ (2...(𝑁 + 1)) → 2 ≤ 1)
100	98, 99	mto 198	. . . . . . . . . . . 12 ⊢ ¬ 1 ∈ (2...(𝑁 + 1))
101		disjsn 4643	. . . . . . . . . . . 12 ⊢ (((2...(𝑁 + 1)) ∩ {1}) = ∅ ↔ ¬ 1 ∈ (2...(𝑁 + 1)))
102	100, 101	mpbir 232	. . . . . . . . . . 11 ⊢ ((2...(𝑁 + 1)) ∩ {1}) = ∅
103	93, 102	eqtri 2762	. . . . . . . . . 10 ⊢ ({1} ∩ (2...(𝑁 + 1))) = ∅
104		uneqdifeq 4420	. . . . . . . . . 10 ⊢ (({1} ⊆ (1...(𝑁 + 1)) ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅) → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
105	92, 103, 104	sylancl 592	. . . . . . . . 9 ⊢ (𝜑 → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
106	91, 105	mpbid 233	. . . . . . . 8 ⊢ (𝜑 → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
107	106	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
108		reseq2 5926	. . . . . . . . 9 ⊢ (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})) = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
109	108	f1oeq1d 6762	. . . . . . . 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 6756	. . . . . . . 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 6757	. . . . . . . 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 306	. . . . . . 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 17	. . . . . 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 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
115	66	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
116		fzp1ss 13520	. . . . . . . . . . 11 ⊢ (1 ∈ ℤ → ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1)))
117	85, 116	ax-mp 5	. . . . . . . . . 10 ⊢ ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
118	89, 117	eqsstrri 3962	. . . . . . . . 9 ⊢ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
119		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (2...(𝑁 + 1)))
120	118, 119	sselid 3913	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
121	115, 120	fvco3d 6928	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (𝐹‘(𝑏‘𝑦)))
122	13, 14, 1, 15, 16, 17, 18, 6, 19	subfacp1lem4 35411	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐹 = 𝐹)
123	122	fveq1d 6829	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
124	123	ad2antrr 732	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
125	68	simprd 496	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ≠ 1)
126	125, 72	neeqtrrd 3008	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ≠ (𝐹‘𝑀))
127	126	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑀) ≠ (𝐹‘𝑀))
128		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → (𝑏‘𝑦) = (𝑏‘𝑀))
129		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → (𝐹‘𝑦) = (𝐹‘𝑀))
130	128, 129	neeq12d 2995	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) ≠ (𝐹‘𝑦) ↔ (𝑏‘𝑀) ≠ (𝐹‘𝑀)))
131	127, 130	syl5ibrcom 248	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑏‘𝑦) ≠ (𝐹‘𝑦)))
132	118	sseli 3911	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (2...(𝑁 + 1)) → 𝑦 ∈ (1...(𝑁 + 1)))
133	39	simprd 496	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)
134	133	r19.21bi 3231	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏‘𝑦) ≠ 𝑦)
135	132, 134	sylan2 599	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ≠ 𝑦)
136	135	adantrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑏‘𝑦) ≠ 𝑦)
137	18	eleq2i 2831	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐾 ↔ 𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}))
138		eldifsn 4719	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀))
139	137, 138	bitri 276	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐾 ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀))
140	13, 14, 1, 15, 16, 17, 18, 19, 21	subfacp1lem2b 35409	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = (( I ↾ 𝐾)‘𝑦))
141		fvresi 7117	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝐾 → (( I ↾ 𝐾)‘𝑦) = 𝑦)
142	141	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (( I ↾ 𝐾)‘𝑦) = 𝑦)
143	140, 142	eqtrd 2774	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = 𝑦)
144	139, 143	sylan2br 601	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
145	144	adantlr 721	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
146	136, 145	neeqtrrd 3008	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑏‘𝑦) ≠ (𝐹‘𝑦))
147	146	expr 457	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 ≠ 𝑀 → (𝑏‘𝑦) ≠ (𝐹‘𝑦)))
148	131, 147	pm2.61dne 3020	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ≠ (𝐹‘𝑦))
149	148	necomd 2989	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (𝑏‘𝑦))
150	124, 149	eqnetrd 3001	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (^◡𝐹‘𝑦) ≠ (𝑏‘𝑦))
151	23	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
152		ffvelcdm 7022	. . . . . . . . . . 11 ⊢ ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏‘𝑦) ∈ (1...(𝑁 + 1)))
153	66, 132, 152	syl2an 602	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ∈ (1...(𝑁 + 1)))
154		f1ocnvfv 7222	. . . . . . . . . 10 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑏‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑏‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (𝑏‘𝑦)))
155	151, 153, 154	syl2an2r 691	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹‘(𝑏‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (𝑏‘𝑦)))
156	155	necon3d 2955	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((^◡𝐹‘𝑦) ≠ (𝑏‘𝑦) → (𝐹‘(𝑏‘𝑦)) ≠ 𝑦))
157	150, 156	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘(𝑏‘𝑦)) ≠ 𝑦)
158	121, 157	eqnetrd 3001	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)
159	158	ralrimiva 3131	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)
160		f1of 6767	. . . . . . . . . . . 12 ⊢ (( I ↾ 𝐾):𝐾–1-1-onto→𝐾 → ( I ↾ 𝐾):𝐾⟶𝐾)
161	20, 160	ax-mp 5	. . . . . . . . . . 11 ⊢ ( I ↾ 𝐾):𝐾⟶𝐾
162		fzfi 13925	. . . . . . . . . . . . 13 ⊢ (2...(𝑁 + 1)) ∈ Fin
163		difexg 5257	. . . . . . . . . . . . 13 ⊢ ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V)
164	162, 163	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V
165	18, 164	eqeltri 2835	. . . . . . . . . . 11 ⊢ 𝐾 ∈ V
166		fex 7170	. . . . . . . . . . 11 ⊢ ((( I ↾ 𝐾):𝐾⟶𝐾 ∧ 𝐾 ∈ V) → ( I ↾ 𝐾) ∈ V)
167	161, 165, 166	mp2an 698	. . . . . . . . . 10 ⊢ ( I ↾ 𝐾) ∈ V
168		prex 5367	. . . . . . . . . 10 ⊢ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
169	167, 168	unex 7687	. . . . . . . . 9 ⊢ (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
170	19, 169	eqeltri 2835	. . . . . . . 8 ⊢ 𝐹 ∈ V
171	170, 32	coex 7870	. . . . . . 7 ⊢ (𝐹 ∘ 𝑏) ∈ V
172	171	resex 5981	. . . . . 6 ⊢ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ V
173		f1oeq1 6755	. . . . . . 7 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
174		fveq1 6826	. . . . . . . . . 10 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (𝑓‘𝑦) = (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
175		fvres 6846	. . . . . . . . . 10 ⊢ (𝑦 ∈ (2...(𝑁 + 1)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
176	174, 175	sylan9eq 2794	. . . . . . . . 9 ⊢ ((𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑓‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
177	176	neeq1d 2993	. . . . . . . 8 ⊢ ((𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
178	177	ralbidva 3160	. . . . . . 7 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
179	173, 178	anbi12d 638	. . . . . 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 3620	. . . . 5 ⊢ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶 ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
182	114, 159, 181	sylanbrc 589	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶)
183		vex 3435	. . . . . . . . . . . 12 ⊢ 𝑐 ∈ V
184		f1oeq1 6755	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
185		fveq1 6826	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑐 → (𝑓‘𝑦) = (𝑐‘𝑦))
186	185	neeq1d 2993	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑦) ≠ 𝑦))
187	186	ralbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
188	184, 187	anbi12d 638	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦)))
189	183, 188, 180	elab2 3620	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
190	189	bilani 505	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
191	190	simpld 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
192		f1oun 6786	. . . . . . . . . 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 711	. . . . . . . . 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 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
195		f1oeq2 6756	. . . . . . . . . . 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 6757	. . . . . . . . . . 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 280	. . . . . . . . . 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 17	. . . . . . . . 9 ⊢ (𝜑 → (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
199	198	biimpa 477	. . . . . . . 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 597	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
201		f1oco 6790	. . . . . . 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 691	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
203		f1of 6767	. . . . . . . . . 10 ⊢ (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
204	200, 203	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
205		fvco3 6927	. . . . . . . . 9 ⊢ ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
206	204, 205	sylan 586	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
207	123	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
208		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
209	91	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
210	208, 209	eleqtrrd 2842	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))))
211		elun 4083	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
212	210, 211	sylib 219	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
213		nelne2 3032	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → 𝑀 ≠ 1)
214	16, 100, 213	sylancl 592	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≠ 1)
215	214	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ 1)
216	22	simp2d 1149	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘1) = 𝑀)
217	216	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘1) = 𝑀)
218		f1ofun 6769	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
219	194, 218	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → Fun ({⟨1, 1⟩} ∪ 𝑐))
220		ssun1 4107	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐)
221	54	snid 4594	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ {1}
222	54	dmsnop 6167	. . . . . . . . . . . . . . . . . . 19 ⊢ dom {⟨1, 1⟩} = {1}
223	221, 222	eleqtrri 2838	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ dom {⟨1, 1⟩}
224		funssfv 6848	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 1 ∈ dom {⟨1, 1⟩}) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
225	220, 223, 224	mp3an23 1461	. . . . . . . . . . . . . . . . 17 ⊢ (Fun ({⟨1, 1⟩} ∪ 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
226	219, 225	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
227	54, 54	fvsn 7125	. . . . . . . . . . . . . . . 16 ⊢ ({⟨1, 1⟩}‘1) = 1
228	226, 227	eqtrdi 2790	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
229	215, 217, 228	3netr4d 3011	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1))
230		elsni 4572	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
231	230	fveq2d 6831	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {1} → (𝐹‘𝑦) = (𝐹‘1))
232	230	fveq2d 6831	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {1} → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
233	231, 232	neeq12d 2995	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {1} → ((𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1)))
234	229, 233	syl5ibrcom 248	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑦 ∈ {1} → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
235	234	imp 407	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ {1}) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
236	219	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
237		ssun2 4108	. . . . . . . . . . . . . . . 16 ⊢ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐)
238	237	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
239		f1odm 6771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → dom 𝑐 = (2...(𝑁 + 1)))
240	191, 239	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → dom 𝑐 = (2...(𝑁 + 1)))
241	240	eleq2d 2825	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑦 ∈ dom 𝑐 ↔ 𝑦 ∈ (2...(𝑁 + 1))))
242	241	biimpar 478	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ dom 𝑐)
243		funssfv 6848	. . . . . . . . . . . . . . 15 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑦 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
244	236, 238, 242, 243	syl3anc 1379	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
245		f1of 6767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
246	191, 245	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
247	16	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
248	246, 247	ffvelcdmd 7026	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ∈ (2...(𝑁 + 1)))
249		nelne2 3032	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐‘𝑀) ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ 1)
250	248, 100, 249	sylancl 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ≠ 1)
251	250	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ 1)
252	71	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑀) = 1)
253	251, 252	neeqtrrd 3008	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ (𝐹‘𝑀))
254		fveq2 6827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑀 → (𝑐‘𝑦) = (𝑐‘𝑀))
255	254, 129	neeq12d 2995	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑀 → ((𝑐‘𝑦) ≠ (𝐹‘𝑦) ↔ (𝑐‘𝑀) ≠ (𝐹‘𝑀)))
256	253, 255	syl5ibrcom 248	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑐‘𝑦) ≠ (𝐹‘𝑦)))
257	190	simprd 496	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦)
258	257	r19.21bi 3231	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑦) ≠ 𝑦)
259	258	adantrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑐‘𝑦) ≠ 𝑦)
260	144	adantlr 721	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
261	259, 260	neeqtrrd 3008	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑐‘𝑦) ≠ (𝐹‘𝑦))
262	261	expr 457	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 ≠ 𝑀 → (𝑐‘𝑦) ≠ (𝐹‘𝑦)))
263	256, 262	pm2.61dne 3020	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑦) ≠ (𝐹‘𝑦))
264	244, 263	eqnetrd 3001	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ≠ (𝐹‘𝑦))
265	264	necomd 2989	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
266	235, 265	jaodan 965	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1)))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
267	212, 266	syldan 597	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
268	207, 267	eqnetrd 3001	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (^◡𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
269	23	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
270	204	ffvelcdmda 7025	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1)))
271		f1ocnvfv 7222	. . . . . . . . . . 11 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
272	269, 270, 271	syl2an2r 691	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
273	272	necon3d 2955	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((^◡𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦))
274	268, 273	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦)
275	206, 274	eqnetrd 3001	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
276	275	ralrimiva 3131	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
277		snex 5368	. . . . . . . . 9 ⊢ {⟨1, 1⟩} ∈ V
278	277, 183	unex 7687	. . . . . . . 8 ⊢ ({⟨1, 1⟩} ∪ 𝑐) ∈ V
279	170, 278	coex 7870	. . . . . . 7 ⊢ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ V
280		f1oeq1 6755	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
281		fveq1 6826	. . . . . . . . . 10 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓‘𝑦) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦))
282	281	neeq1d 2993	. . . . . . . . 9 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
283	282	ralbidv 3162	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
284	280, 283	anbi12d 638	. . . . . . 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 3620	. . . . . 6 ⊢ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
286	202, 276, 285	sylanbrc 589	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴)
287	61	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 1 ∈ (1...(𝑁 + 1)))
288	204, 287	fvco3d 6928	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
289	228	fveq2d 6831	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)) = (𝐹‘1))
290	288, 289, 217	3eqtrd 2778	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀)
291	118, 16	sselid 3913	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 + 1)))
292	291	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (1...(𝑁 + 1)))
293	204, 292	fvco3d 6928	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
294	237	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
295	247, 240	eleqtrrd 2842	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ dom 𝑐)
296		funssfv 6848	. . . . . . . . . 10 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑀 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐‘𝑀))
297	219, 294, 295, 296	syl3anc 1379	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐‘𝑀))
298	297	fveq2d 6831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)) = (𝐹‘(𝑐‘𝑀)))
299	293, 298	eqtrd 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(𝑐‘𝑀)))
300	122	fveq1d 6829	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹‘1) = (𝐹‘1))
301	300, 216	eqtrd 2774	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹‘1) = 𝑀)
302	301	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (^◡𝐹‘1) = 𝑀)
303		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
304	254, 303	neeq12d 2995	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → ((𝑐‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑀) ≠ 𝑀))
305	304, 257, 247	rspcdva 3561	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ≠ 𝑀)
306	305	necomd 2989	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ (𝑐‘𝑀))
307	302, 306	eqnetrd 3001	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (^◡𝐹‘1) ≠ (𝑐‘𝑀))
308	118, 248	sselid 3913	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ∈ (1...(𝑁 + 1)))
309		f1ocnvfv 7222	. . . . . . . . . 10 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑐‘𝑀) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑐‘𝑀)) = 1 → (^◡𝐹‘1) = (𝑐‘𝑀)))
310	23, 308, 309	syl2an2r 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹‘(𝑐‘𝑀)) = 1 → (^◡𝐹‘1) = (𝑐‘𝑀)))
311	310	necon3d 2955	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((^◡𝐹‘1) ≠ (𝑐‘𝑀) → (𝐹‘(𝑐‘𝑀)) ≠ 1))
312	307, 311	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(𝑐‘𝑀)) ≠ 1)
313	299, 312	eqnetrd 3001	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)
314	290, 313	jca 516	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
315		fveq1 6826	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘1) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1))
316	315	eqeq1d 2741	. . . . . . 7 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘1) = 𝑀 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀))
317		fveq1 6826	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘𝑀) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀))
318	317	neeq1d 2993	. . . . . . 7 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘𝑀) ≠ 1 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
319	316, 318	anbi12d 638	. . . . . 6 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1) ↔ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
320	319, 6	elrab2 3632	. . . . 5 ⊢ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ∧ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
321	286, 314, 320	sylanbrc 589	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵)
322	23	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
323		f1of1 6766	. . . . . . 7 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
324	322, 323	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
325		f1of 6767	. . . . . . . 8 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
326	322, 325	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
327	66	adantrr 723	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
328	326, 327	fcod 6680	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
329	204	adantrl 722	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
330		cocan1 7235	. . . . . 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 1379	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
332		coass 6217	. . . . . . 7 ⊢ ((𝐹 ∘ 𝐹) ∘ 𝑏) = (𝐹 ∘ (𝐹 ∘ 𝑏))
333	122	coeq1d 5803	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = (𝐹 ∘ 𝐹))
334		f1ococnv1 6796	. . . . . . . . . . . 12 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (^◡𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
335	23, 334	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
336	333, 335	eqtr3d 2776	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
337	336	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
338	337	coeq1d 5803	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝐹) ∘ 𝑏) = (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏))
339		fcoi2 6702	. . . . . . . . 9 ⊢ (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
340	327, 339	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
341	338, 340	eqtrd 2774	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝐹) ∘ 𝑏) = 𝑏)
342	332, 341	eqtr3id 2788	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ (𝐹 ∘ 𝑏)) = 𝑏)
343	342	eqeq1d 2741	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))))
344	73	adantrr 723	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏)‘1) = 1)
345	228	adantrl 722	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
346	344, 345	eqtr4d 2777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
347		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → ((𝐹 ∘ 𝑏)‘𝑦) = ((𝐹 ∘ 𝑏)‘1))
348		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
349	347, 348	eqeq12d 2755	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → (((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1)))
350	54, 349	ralsn 4613	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
351	346, 350	sylibr 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
352	351	biantrurd 537	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))))
353		ralunb 4126	. . . . . . . . 9 ⊢ (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
354	352, 353	bitr4di 290	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
355	175	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
356	355	eqcomd 2745	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
357	244	adantlrl 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
358	356, 357	eqeq12d 2755	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
359	358	ralbidva 3160	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
360	91	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
361	360	raleqdv 3297	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
362	354, 359, 361	3bitr3rd 311	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
363	56	adantrr 723	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
364	200	adantrl 722	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
365		f1ofn 6768	. . . . . . . . 9 ⊢ (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
366	364, 365	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
367		eqfnfv 6971	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
368	363, 366, 367	syl2anc 590	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
369		fnssres 6608	. . . . . . . . 9 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
370	363, 118, 369	sylancl 592	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
371	191	adantrl 722	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
372		f1ofn 6768	. . . . . . . . 9 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐 Fn (2...(𝑁 + 1)))
373	371, 372	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐 Fn (2...(𝑁 + 1)))
374		eqfnfv 6971	. . . . . . . 8 ⊢ ((((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)) ∧ 𝑐 Fn (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
375	370, 373, 374	syl2anc 590	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
376	362, 368, 375	3bitr4d 312	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐))
377		eqcom 2746	. . . . . 6 ⊢ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
378	376, 377	bitrdi 288	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))))
379	331, 343, 378	3bitr3d 310	. . . 4 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))))
380	12, 182, 321, 379	f1o2d 7610	. . 3 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))):𝐵–1-1-onto→𝐶)
381	11, 380	hasheqf1od 14306	. 2 ⊢ (𝜑 → (♯‘𝐵) = (♯‘𝐶))
382	13, 14	derangen2 35402	. . . . 5 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (𝑆‘(♯‘(2...(𝑁 + 1)))))
383	13	derangval 35395	. . . . . 6 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}))
384	180	fveq2i 6830	. . . . . 6 ⊢ (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)})
385	383, 384	eqtr4di 2792	. . . . 5 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘𝐶))
386	382, 385	eqtr3d 2776	. . . 4 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶))
387	162, 386	ax-mp 5	. . 3 ⊢ (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶)
388	15, 58	eleqtrdi 2849	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
389		eluzp1p1 12807	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝑁 + 1) ∈ (ℤ_≥‘(1 + 1)))
390	388, 389	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘(1 + 1)))
391		df-2 12235	. . . . . . . 8 ⊢ 2 = (1 + 1)
392	391	fveq2i 6830	. . . . . . 7 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
393	390, 392	eleqtrrdi 2850	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘2))
394		hashfz 14380	. . . . . 6 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘2) → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
395	393, 394	syl 17	. . . . 5 ⊢ (𝜑 → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
396	57	nncnd 12181	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℂ)
397		2cnd 12250	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
398		1cnd 11130	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℂ)
399	396, 397, 398	subsubd 11524	. . . . 5 ⊢ (𝜑 → ((𝑁 + 1) − (2 − 1)) = (((𝑁 + 1) − 2) + 1))
400		2m1e1 12293	. . . . . . 7 ⊢ (2 − 1) = 1
401	400	oveq2i 7367	. . . . . 6 ⊢ ((𝑁 + 1) − (2 − 1)) = ((𝑁 + 1) − 1)
402	15	nncnd 12181	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
403		ax-1cn 11087	. . . . . . 7 ⊢ 1 ∈ ℂ
404		pncan 11390	. . . . . . 7 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
405	402, 403, 404	sylancl 592	. . . . . 6 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
406	401, 405	eqtrid 2786	. . . . 5 ⊢ (𝜑 → ((𝑁 + 1) − (2 − 1)) = 𝑁)
407	395, 399, 406	3eqtr2d 2780	. . . 4 ⊢ (𝜑 → (♯‘(2...(𝑁 + 1))) = 𝑁)
408	407	fveq2d 6831	. . 3 ⊢ (𝜑 → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (𝑆‘𝑁))
409	387, 408	eqtr3id 2788	. 2 ⊢ (𝜑 → (♯‘𝐶) = (𝑆‘𝑁))
410	381, 409	eqtrd 2774	1 ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 = wceq 1547 ∈ wcel 2119 {cab 2717 ≠ wne 2934 ∀wral 3053 {crab 3391 Vcvv 3431 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4261 {csn 4555 {cpr 4557 ⟨cop 4561 class class class wbr 5072 ↦ cmpt 5153 I cid 5512 ^◡ccnv 5617 dom cdm 5618 ↾ cres 5620 ∘ ccom 5622 Fun wfun 6479 Fn wfn 6480 ⟶wf 6481 –1-1→wf1 6482 –onto→wfo 6483 –1-1-onto→wf1o 6484 ‘cfv 6485 (class class class)co 7356 Fincfn 8883 ℂcc 11027 1c1 11030 + caddc 11032 < clt 11170 ≤ cle 11171 − cmin 11368 ℕcn 12165 2c2 12227 ℕ₀cn0 12428 ℤcz 12515 ℤ_≥cuz 12779 ...cfz 13452 ♯chash 14283

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-er 8633 df-map 8765 df-pm 8766 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-dju 9816 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-2 12235 df-n0 12429 df-xnn0 12502 df-z 12516 df-uz 12780 df-fz 13453 df-hash 14284

This theorem is referenced by: subfacp1lem6 35413

W3C validator