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 35676

Description: Lemma for subfacp1 35678. In subfacp1lem6 35677 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 14004	. . . . . . . 8 ⊢ (1...(𝑁 + 1)) ∈ Fin
3		deranglem 35658	. . . . . . . 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 2859	. . . . . 6 ⊢ 𝐴 ∈ Fin
6		subfacp1lem5.b	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1)}
7	6	ssrab3 4036	. . . . . 6 ⊢ 𝐵 ⊆ 𝐴
8		ssfi 9153	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
9	5, 7, 8	mp2an 704	. . . . 5 ⊢ 𝐵 ∈ Fin
10	9	elexi 3477	. . . 4 ⊢ 𝐵 ∈ V
11	10	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
12		eqid 2763	. . . 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 6859	. . . . . . . . . . . 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 35672	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1))
23	22	simp1d 1160	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
24		fveq1 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
25	24	eqeq1d 2765	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
26		fveq1 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑀) = (𝑏‘𝑀))
27	26	neeq1d 3017	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → ((𝑔‘𝑀) ≠ 1 ↔ (𝑏‘𝑀) ≠ 1))
28	25, 27	anbi12d 643	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
29	28, 6	elrab2 3654	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
30	29	bilani 509	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1)))
31	30	simpld 499	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
32		vex 3459	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
33		f1oeq1 6808	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
34		fveq1 6880	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
35	34	neeq1d 3017	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
36	35	ralbidv 3188	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
37	33, 36	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)))
38	32, 37, 1	elab2 3641	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
39	31, 38	sylib 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
40	39	simpld 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
41		f1oco 6844	. . . . . . . . 9 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
42	23, 40, 41	syl2an2r 697	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
43		f1of1 6819	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
44		df-f1 6541	. . . . . . . . 9 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun ^◡(𝐹 ∘ 𝑏)))
45	44	simprbi 502	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun ^◡(𝐹 ∘ 𝑏))
46	42, 43, 45	3syl 19	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → Fun ^◡(𝐹 ∘ 𝑏))
47		f1ofn 6821	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
48		fnresdm 6654	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))) = (𝐹 ∘ 𝑏))
49		f1oeq1 6808	. . . . . . . . . 10 ⊢ (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))) = (𝐹 ∘ 𝑏) → (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
50	42, 47, 48, 49	4syl 20	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ 𝑏):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
51	42, 50	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
52		f1ofo 6828	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
53	51, 52	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
54		1ex 11198	. . . . . . . . . 10 ⊢ 1 ∈ V
55	54, 54	f1osn 6862	. . . . . . . . 9 ⊢ {⟨1, 1⟩}:{1}–1-1-onto→{1}
56	42, 47	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
57	15	peano2nnd 12245	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
58		nnuz 12896	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
59	57, 58	eleqtrdi 2873	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘1))
60		eluzfz1 13554	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → 1 ∈ (1...(𝑁 + 1)))
61	59, 60	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ (1...(𝑁 + 1)))
62	61	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 1 ∈ (1...(𝑁 + 1)))
63		fnressn 7155	. . . . . . . . . . . 12 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩})
64	56, 62, 63	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩})
65		f1of 6820	. . . . . . . . . . . . . . . 16 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
66	40, 65	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
67	66, 62	fvco3d 6982	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏)‘1) = (𝐹‘(𝑏‘1)))
68	30	simprd 500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) ≠ 1))
69	68	simpld 499	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) = 𝑀)
70	69	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝑏‘1)) = (𝐹‘𝑀))
71	22	simp3d 1162	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑀) = 1)
72	71	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑀) = 1)
73	67, 70, 72	3eqtrd 2802	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏)‘1) = 1)
74	73	opeq2d 4845	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ⟨1, ((𝐹 ∘ 𝑏)‘1)⟩ = ⟨1, 1⟩)
75	74	sneqd 4601	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {⟨1, ((𝐹 ∘ 𝑏)‘1)⟩} = {⟨1, 1⟩})
76	64, 75	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}) = {⟨1, 1⟩})
77	76	f1oeq1d 6815	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} ↔ {⟨1, 1⟩}:{1}–1-1-onto→{1}))
78	55, 77	mpbiri 261	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1})
79		f1ofo 6828	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) ↾ {1}):{1}–1-1-onto→{1} → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–onto→{1})
80	78, 79	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ {1}):{1}–onto→{1})
81		resdif 6842	. . . . . . 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 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}))
83		fzsplit 13574	. . . . . . . . . . 11 ⊢ (1 ∈ (1...(𝑁 + 1)) → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
84	61, 83	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1))))
85		1z 12619	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
86		fzsn 13590	. . . . . . . . . . . 12 ⊢ (1 ∈ ℤ → (1...1) = {1})
87	85, 86	ax-mp 5	. . . . . . . . . . 11 ⊢ (1...1) = {1}
88		1p1e2 12359	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
89	88	oveq1i 7420	. . . . . . . . . . 11 ⊢ ((1 + 1)...(𝑁 + 1)) = (2...(𝑁 + 1))
90	87, 89	uneq12i 4120	. . . . . . . . . 10 ⊢ ((1...1) ∪ ((1 + 1)...(𝑁 + 1))) = ({1} ∪ (2...(𝑁 + 1)))
91	84, 90	eqtr2di 2815	. . . . . . . . 9 ⊢ (𝜑 → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
92	61	snssd 4752	. . . . . . . . . 10 ⊢ (𝜑 → {1} ⊆ (1...(𝑁 + 1)))
93		incom 4162	. . . . . . . . . . 11 ⊢ ({1} ∩ (2...(𝑁 + 1))) = ((2...(𝑁 + 1)) ∩ {1})
94		1lt2 12408	. . . . . . . . . . . . . 14 ⊢ 1 < 2
95		1re 11203	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
96		2re 12310	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
97	95, 96	ltnlei 11326	. . . . . . . . . . . . . 14 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
98	94, 97	mpbi 233	. . . . . . . . . . . . 13 ⊢ ¬ 2 ≤ 1
99		elfzle1 13550	. . . . . . . . . . . . 13 ⊢ (1 ∈ (2...(𝑁 + 1)) → 2 ≤ 1)
100	98, 99	mto 200	. . . . . . . . . . . 12 ⊢ ¬ 1 ∈ (2...(𝑁 + 1))
101		disjsn 4677	. . . . . . . . . . . 12 ⊢ (((2...(𝑁 + 1)) ∩ {1}) = ∅ ↔ ¬ 1 ∈ (2...(𝑁 + 1)))
102	100, 101	mpbir 234	. . . . . . . . . . 11 ⊢ ((2...(𝑁 + 1)) ∩ {1}) = ∅
103	93, 102	eqtri 2786	. . . . . . . . . 10 ⊢ ({1} ∩ (2...(𝑁 + 1))) = ∅
104		uneqdifeq 4453	. . . . . . . . . 10 ⊢ (({1} ⊆ (1...(𝑁 + 1)) ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅) → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
105	92, 103, 104	sylancl 597	. . . . . . . . 9 ⊢ (𝜑 → (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1))))
106	91, 105	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
107	106	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)))
108		reseq2 5973	. . . . . . . . 9 ⊢ (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → ((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})) = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
109	108	f1oeq1d 6815	. . . . . . . 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 6809	. . . . . . . 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 6810	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
112	109, 110, 111	3bitrd 308	. . . . . . 7 ⊢ (((1...(𝑁 + 1)) ∖ {1}) = (2...(𝑁 + 1)) → (((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
113	107, 112	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (((𝐹 ∘ 𝑏) ↾ ((1...(𝑁 + 1)) ∖ {1})):((1...(𝑁 + 1)) ∖ {1})–1-1-onto→((1...(𝑁 + 1)) ∖ {1}) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
114	82, 113	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
115	66	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
116		fzp1ss 13599	. . . . . . . . . . 11 ⊢ (1 ∈ ℤ → ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1)))
117	85, 116	ax-mp 5	. . . . . . . . . 10 ⊢ ((1 + 1)...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
118	89, 117	eqsstrri 3984	. . . . . . . . 9 ⊢ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))
119		simpr 489	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (2...(𝑁 + 1)))
120	118, 119	sselid 3935	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
121	115, 120	fvco3d 6982	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (𝐹‘(𝑏‘𝑦)))
122	13, 14, 1, 15, 16, 17, 18, 6, 19	subfacp1lem4 35675	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐹 = 𝐹)
123	122	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
124	123	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
125	68	simprd 500	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ≠ 1)
126	125, 72	neeqtrrd 3032	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ≠ (𝐹‘𝑀))
127	126	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑀) ≠ (𝐹‘𝑀))
128		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → (𝑏‘𝑦) = (𝑏‘𝑀))
129		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → (𝐹‘𝑦) = (𝐹‘𝑀))
130	128, 129	neeq12d 3019	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) ≠ (𝐹‘𝑦) ↔ (𝑏‘𝑀) ≠ (𝐹‘𝑀)))
131	127, 130	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑏‘𝑦) ≠ (𝐹‘𝑦)))
132	118	sseli 3933	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (2...(𝑁 + 1)) → 𝑦 ∈ (1...(𝑁 + 1)))
133	39	simprd 500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)
134	133	r19.21bi 3257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏‘𝑦) ≠ 𝑦)
135	132, 134	sylan2 604	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ≠ 𝑦)
136	135	adantrr 729	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑏‘𝑦) ≠ 𝑦)
137	18	eleq2i 2855	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐾 ↔ 𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}))
138		eldifsn 4753	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀))
139	137, 138	bitri 278	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐾 ↔ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀))
140	13, 14, 1, 15, 16, 17, 18, 19, 21	subfacp1lem2b 35673	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = (( I ↾ 𝐾)‘𝑦))
141		fvresi 7171	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝐾 → (( I ↾ 𝐾)‘𝑦) = 𝑦)
142	141	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (( I ↾ 𝐾)‘𝑦) = 𝑦)
143	140, 142	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = 𝑦)
144	139, 143	sylan2br 606	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
145	144	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
146	136, 145	neeqtrrd 3032	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑏‘𝑦) ≠ (𝐹‘𝑦))
147	146	expr 461	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 ≠ 𝑀 → (𝑏‘𝑦) ≠ (𝐹‘𝑦)))
148	131, 147	pm2.61dne 3044	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ≠ (𝐹‘𝑦))
149	148	necomd 3013	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (𝑏‘𝑦))
150	124, 149	eqnetrd 3025	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (^◡𝐹‘𝑦) ≠ (𝑏‘𝑦))
151	23	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
152		ffvelcdm 7076	. . . . . . . . . . 11 ⊢ ((𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑏‘𝑦) ∈ (1...(𝑁 + 1)))
153	66, 132, 152	syl2an 607	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑏‘𝑦) ∈ (1...(𝑁 + 1)))
154		f1ocnvfv 7276	. . . . . . . . . 10 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑏‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑏‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (𝑏‘𝑦)))
155	151, 153, 154	syl2an2r 697	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹‘(𝑏‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (𝑏‘𝑦)))
156	155	necon3d 2979	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((^◡𝐹‘𝑦) ≠ (𝑏‘𝑦) → (𝐹‘(𝑏‘𝑦)) ≠ 𝑦))
157	150, 156	mpd 16	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘(𝑏‘𝑦)) ≠ 𝑦)
158	121, 157	eqnetrd 3025	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)
159	158	ralrimiva 3157	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)
160		f1of 6820	. . . . . . . . . . . 12 ⊢ (( I ↾ 𝐾):𝐾–1-1-onto→𝐾 → ( I ↾ 𝐾):𝐾⟶𝐾)
161	20, 160	ax-mp 5	. . . . . . . . . . 11 ⊢ ( I ↾ 𝐾):𝐾⟶𝐾
162		fzfi 14004	. . . . . . . . . . . . 13 ⊢ (2...(𝑁 + 1)) ∈ Fin
163		difexg 5300	. . . . . . . . . . . . 13 ⊢ ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V)
164	162, 163	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ V
165	18, 164	eqeltri 2859	. . . . . . . . . . 11 ⊢ 𝐾 ∈ V
166		fex 7224	. . . . . . . . . . 11 ⊢ ((( I ↾ 𝐾):𝐾⟶𝐾 ∧ 𝐾 ∈ V) → ( I ↾ 𝐾) ∈ V)
167	161, 165, 166	mp2an 704	. . . . . . . . . 10 ⊢ ( I ↾ 𝐾) ∈ V
168		prex 5409	. . . . . . . . . 10 ⊢ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
169	167, 168	unex 7742	. . . . . . . . 9 ⊢ (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
170	19, 169	eqeltri 2859	. . . . . . . 8 ⊢ 𝐹 ∈ V
171	170, 32	coex 7923	. . . . . . 7 ⊢ (𝐹 ∘ 𝑏) ∈ V
172	171	resex 6028	. . . . . 6 ⊢ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ V
173		f1oeq1 6808	. . . . . . 7 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
174		fveq1 6880	. . . . . . . . . 10 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (𝑓‘𝑦) = (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
175		fvres 6900	. . . . . . . . . 10 ⊢ (𝑦 ∈ (2...(𝑁 + 1)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
176	174, 175	sylan9eq 2818	. . . . . . . . 9 ⊢ ((𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑓‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
177	176	neeq1d 3017	. . . . . . . 8 ⊢ ((𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
178	177	ralbidva 3186	. . . . . . 7 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
179	173, 178	anbi12d 643	. . . . . 6 ⊢ (𝑓 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦)))
180		subfacp1lem5.c	. . . . . 6 ⊢ 𝐶 = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}
181	172, 179, 180	elab2 3641	. . . . 5 ⊢ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶 ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))):(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) ≠ 𝑦))
182	114, 159, 181	sylanbrc 594	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) ∈ 𝐶)
183		vex 3459	. . . . . . . . . . . 12 ⊢ 𝑐 ∈ V
184		f1oeq1 6808	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
185		fveq1 6880	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑐 → (𝑓‘𝑦) = (𝑐‘𝑦))
186	185	neeq1d 3017	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑦) ≠ 𝑦))
187	186	ralbidv 3188	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
188	184, 187	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → ((𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦)))
189	183, 188, 180	elab2 3641	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
190	189	bilani 509	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦))
191	190	simpld 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
192		f1oun 6840	. . . . . . . . . 10 ⊢ ((({⟨1, 1⟩}:{1}–1-1-onto→{1} ∧ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))) ∧ (({1} ∩ (2...(𝑁 + 1))) = ∅ ∧ ({1} ∩ (2...(𝑁 + 1))) = ∅)) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
193	103, 103, 192	mpanr12 717	. . . . . . . . 9 ⊢ (({⟨1, 1⟩}:{1}–1-1-onto→{1} ∧ 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
194	55, 191, 193	sylancr 598	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))))
195		f1oeq2 6809	. . . . . . . . . . 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 6810	. . . . . . . . . . 11 ⊢ (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) → (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
197	195, 196	bitrd 282	. . . . . . . . . 10 ⊢ (({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)) → (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
198	91, 197	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) ↔ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
199	198	biimpa 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1)))) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
200	194, 199	syldan 602	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
201		f1oco 6844	. . . . . . 7 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
202	23, 200, 201	syl2an2r 697	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
203		f1of 6820	. . . . . . . . . 10 ⊢ (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
204	200, 203	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
205		fvco3 6981	. . . . . . . . 9 ⊢ ((({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
206	204, 205	sylan 591	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
207	123	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (^◡𝐹‘𝑦) = (𝐹‘𝑦))
208		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ (1...(𝑁 + 1)))
209	91	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
210	208, 209	eleqtrrd 2866	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → 𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))))
211		elun 4107	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ({1} ∪ (2...(𝑁 + 1))) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
212	210, 211	sylib 221	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1))))
213		nelne2 3056	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → 𝑀 ≠ 1)
214	16, 100, 213	sylancl 597	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≠ 1)
215	214	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ 1)
216	22	simp2d 1161	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘1) = 𝑀)
217	216	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘1) = 𝑀)
218		f1ofun 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨1, 1⟩} ∪ 𝑐):({1} ∪ (2...(𝑁 + 1)))–1-1-onto→({1} ∪ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
219	194, 218	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → Fun ({⟨1, 1⟩} ∪ 𝑐))
220		ssun1 4131	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐)
221	54	snid 4628	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ {1}
222	54	dmsnop 6217	. . . . . . . . . . . . . . . . . . 19 ⊢ dom {⟨1, 1⟩} = {1}
223	221, 222	eleqtrri 2862	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ dom {⟨1, 1⟩}
224		funssfv 6902	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ {⟨1, 1⟩} ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 1 ∈ dom {⟨1, 1⟩}) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
225	220, 223, 224	mp3an23 1482	. . . . . . . . . . . . . . . . 17 ⊢ (Fun ({⟨1, 1⟩} ∪ 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
226	219, 225	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = ({⟨1, 1⟩}‘1))
227	54, 54	fvsn 7179	. . . . . . . . . . . . . . . 16 ⊢ ({⟨1, 1⟩}‘1) = 1
228	226, 227	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
229	215, 217, 228	3netr4d 3035	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1))
230		elsni 4606	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
231	230	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {1} → (𝐹‘𝑦) = (𝐹‘1))
232	230	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {1} → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
233	231, 232	neeq12d 3019	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {1} → ((𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (𝐹‘1) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘1)))
234	229, 233	syl5ibrcom 250	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑦 ∈ {1} → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
235	234	imp 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ {1}) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
236	219	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → Fun ({⟨1, 1⟩} ∪ 𝑐))
237		ssun2 4132	. . . . . . . . . . . . . . . 16 ⊢ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐)
238	237	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
239		f1odm 6824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → dom 𝑐 = (2...(𝑁 + 1)))
240	191, 239	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → dom 𝑐 = (2...(𝑁 + 1)))
241	240	eleq2d 2849	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑦 ∈ dom 𝑐 ↔ 𝑦 ∈ (2...(𝑁 + 1))))
242	241	biimpar 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → 𝑦 ∈ dom 𝑐)
243		funssfv 6902	. . . . . . . . . . . . . . 15 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑦 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
244	236, 238, 242, 243	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
245		f1of 6820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
246	191, 245	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:(2...(𝑁 + 1))⟶(2...(𝑁 + 1)))
247	16	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
248	246, 247	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ∈ (2...(𝑁 + 1)))
249		nelne2 3056	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐‘𝑀) ∈ (2...(𝑁 + 1)) ∧ ¬ 1 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ 1)
250	248, 100, 249	sylancl 597	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ≠ 1)
251	250	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ 1)
252	71	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑀) = 1)
253	251, 252	neeqtrrd 3032	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑀) ≠ (𝐹‘𝑀))
254		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑀 → (𝑐‘𝑦) = (𝑐‘𝑀))
255	254, 129	neeq12d 3019	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑀 → ((𝑐‘𝑦) ≠ (𝐹‘𝑦) ↔ (𝑐‘𝑀) ≠ (𝐹‘𝑀)))
256	253, 255	syl5ibrcom 250	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 = 𝑀 → (𝑐‘𝑦) ≠ (𝐹‘𝑦)))
257	190	simprd 500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (2...(𝑁 + 1))(𝑐‘𝑦) ≠ 𝑦)
258	257	r19.21bi 3257	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑦) ≠ 𝑦)
259	258	adantrr 729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑐‘𝑦) ≠ 𝑦)
260	144	adantlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝐹‘𝑦) = 𝑦)
261	259, 260	neeqtrrd 3032	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ (2...(𝑁 + 1)) ∧ 𝑦 ≠ 𝑀)) → (𝑐‘𝑦) ≠ (𝐹‘𝑦))
262	261	expr 461	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑦 ≠ 𝑀 → (𝑐‘𝑦) ≠ (𝐹‘𝑦)))
263	256, 262	pm2.61dne 3044	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝑐‘𝑦) ≠ (𝐹‘𝑦))
264	244, 263	eqnetrd 3025	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ≠ (𝐹‘𝑦))
265	264	necomd 3013	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
266	235, 265	jaodan 972	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ (𝑦 ∈ {1} ∨ 𝑦 ∈ (2...(𝑁 + 1)))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
267	212, 266	syldan 602	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
268	207, 267	eqnetrd 3025	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (^◡𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
269	23	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
270	204	ffvelcdmda 7079	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1)))
271		f1ocnvfv 7276	. . . . . . . . . . 11 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
272	269, 270, 271	syl2an2r 697	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) = 𝑦 → (^◡𝐹‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
273	272	necon3d 2979	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((^◡𝐹‘𝑦) ≠ (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦))
274	268, 273	mpd 16	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑦)) ≠ 𝑦)
275	206, 274	eqnetrd 3025	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ (1...(𝑁 + 1))) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
276	275	ralrimiva 3157	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)
277		snex 5410	. . . . . . . . 9 ⊢ {⟨1, 1⟩} ∈ V
278	277, 183	unex 7742	. . . . . . . 8 ⊢ ({⟨1, 1⟩} ∪ 𝑐) ∈ V
279	170, 278	coex 7923	. . . . . . 7 ⊢ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ V
280		f1oeq1 6808	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
281		fveq1 6880	. . . . . . . . . 10 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑓‘𝑦) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦))
282	281	neeq1d 3017	. . . . . . . . 9 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
283	282	ralbidv 3188	. . . . . . . 8 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
284	280, 283	anbi12d 643	. . . . . . 7 ⊢ (𝑓 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦)))
285	279, 284, 1	elab2 3641	. . . . . 6 ⊢ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑦) ≠ 𝑦))
286	202, 276, 285	sylanbrc 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴)
287	61	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 1 ∈ (1...(𝑁 + 1)))
288	204, 287	fvco3d 6982	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)))
289	228	fveq2d 6885	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘1)) = (𝐹‘1))
290	288, 289, 217	3eqtrd 2802	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀)
291	118, 16	sselid 3935	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 + 1)))
292	291	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (1...(𝑁 + 1)))
293	204, 292	fvco3d 6982	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)))
294	237	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐))
295	247, 240	eleqtrrd 2866	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ dom 𝑐)
296		funssfv 6902	. . . . . . . . . 10 ⊢ ((Fun ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑐 ⊆ ({⟨1, 1⟩} ∪ 𝑐) ∧ 𝑀 ∈ dom 𝑐) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐‘𝑀))
297	219, 294, 295, 296	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑀) = (𝑐‘𝑀))
298	297	fveq2d 6885	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(({⟨1, 1⟩} ∪ 𝑐)‘𝑀)) = (𝐹‘(𝑐‘𝑀)))
299	293, 298	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) = (𝐹‘(𝑐‘𝑀)))
300	122	fveq1d 6883	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹‘1) = (𝐹‘1))
301	300, 216	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹‘1) = 𝑀)
302	301	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (^◡𝐹‘1) = 𝑀)
303		id 23	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
304	254, 303	neeq12d 3019	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → ((𝑐‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑀) ≠ 𝑀))
305	304, 257, 247	rspcdva 3582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ≠ 𝑀)
306	305	necomd 3013	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ (𝑐‘𝑀))
307	302, 306	eqnetrd 3025	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (^◡𝐹‘1) ≠ (𝑐‘𝑀))
308	118, 248	sselid 3935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐‘𝑀) ∈ (1...(𝑁 + 1)))
309		f1ocnvfv 7276	. . . . . . . . . 10 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝑐‘𝑀) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝑐‘𝑀)) = 1 → (^◡𝐹‘1) = (𝑐‘𝑀)))
310	23, 308, 309	syl2an2r 697	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹‘(𝑐‘𝑀)) = 1 → (^◡𝐹‘1) = (𝑐‘𝑀)))
311	310	necon3d 2979	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((^◡𝐹‘1) ≠ (𝑐‘𝑀) → (𝐹‘(𝑐‘𝑀)) ≠ 1))
312	307, 311	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹‘(𝑐‘𝑀)) ≠ 1)
313	299, 312	eqnetrd 3025	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)
314	290, 313	jca 520	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
315		fveq1 6880	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘1) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1))
316	315	eqeq1d 2765	. . . . . . 7 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘1) = 𝑀 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀))
317		fveq1 6880	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (𝑔‘𝑀) = ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀))
318	317	neeq1d 3017	. . . . . . 7 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → ((𝑔‘𝑀) ≠ 1 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1))
319	316, 318	anbi12d 643	. . . . . 6 ⊢ (𝑔 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1) ↔ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
320	319, 6	elrab2 3654	. . . . 5 ⊢ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵 ↔ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐴 ∧ (((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘1) = 𝑀 ∧ ((𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))‘𝑀) ≠ 1)))
321	286, 314, 320	sylanbrc 594	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ∈ 𝐵)
322	23	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
323		f1of1 6819	. . . . . . 7 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
324	322, 323	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
325		f1of 6820	. . . . . . . 8 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
326	322, 325	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
327	66	adantrr 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
328	326, 327	fcod 6731	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝑏):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
329	204	adantrl 728	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
330		cocan1 7289	. . . . . 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 1398	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ (𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐)))
332		coass 6267	. . . . . . 7 ⊢ ((𝐹 ∘ 𝐹) ∘ 𝑏) = (𝐹 ∘ (𝐹 ∘ 𝑏))
333	122	coeq1d 5847	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = (𝐹 ∘ 𝐹))
334		f1ococnv1 6850	. . . . . . . . . . . 12 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (^◡𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
335	23, 334	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
336	333, 335	eqtr3d 2800	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
337	336	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝐹) = ( I ↾ (1...(𝑁 + 1))))
338	337	coeq1d 5847	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝐹) ∘ 𝑏) = (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏))
339		fcoi2 6753	. . . . . . . . 9 ⊢ (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
340	327, 339	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (( I ↾ (1...(𝑁 + 1))) ∘ 𝑏) = 𝑏)
341	338, 340	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝐹) ∘ 𝑏) = 𝑏)
342	332, 341	eqtr3id 2812	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ (𝐹 ∘ 𝑏)) = 𝑏)
343	342	eqeq1d 2765	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ (𝐹 ∘ 𝑏)) = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐))))
344	73	adantrr 729	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏)‘1) = 1)
345	228	adantrl 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (({⟨1, 1⟩} ∪ 𝑐)‘1) = 1)
346	344, 345	eqtr4d 2801	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
347		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → ((𝐹 ∘ 𝑏)‘𝑦) = ((𝐹 ∘ 𝑏)‘1))
348		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
349	347, 348	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → (((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1)))
350	54, 349	ralsn 4647	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ((𝐹 ∘ 𝑏)‘1) = (({⟨1, 1⟩} ∪ 𝑐)‘1))
351	346, 350	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))
352	351	biantrurd 541	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦))))
353		ralunb 4150	. . . . . . . . 9 ⊢ (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (∀𝑦 ∈ {1} ((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
354	352, 353	bitr4di 292	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
355	175	adantl 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = ((𝐹 ∘ 𝑏)‘𝑦))
356	355	eqcomd 2769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → ((𝐹 ∘ 𝑏)‘𝑦) = (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦))
357	244	adantlrl 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) = (𝑐‘𝑦))
358	356, 357	eqeq12d 2779	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑦 ∈ (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
359	358	ralbidva 3186	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (2...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
360	91	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({1} ∪ (2...(𝑁 + 1))) = (1...(𝑁 + 1)))
361	360	raleqdv 3323	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ ({1} ∪ (2...(𝑁 + 1)))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
362	354, 359, 361	3bitr3rd 313	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦) ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
363	56	adantrr 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)))
364	200	adantrl 728	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
365		f1ofn 6821	. . . . . . . . 9 ⊢ (({⟨1, 1⟩} ∪ 𝑐):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
366	364, 365	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1)))
367		eqfnfv 7025	. . . . . . . 8 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ ({⟨1, 1⟩} ∪ 𝑐) Fn (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
368	363, 366, 367	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝐹 ∘ 𝑏)‘𝑦) = (({⟨1, 1⟩} ∪ 𝑐)‘𝑦)))
369		fnssres 6658	. . . . . . . . 9 ⊢ (((𝐹 ∘ 𝑏) Fn (1...(𝑁 + 1)) ∧ (2...(𝑁 + 1)) ⊆ (1...(𝑁 + 1))) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
370	363, 118, 369	sylancl 597	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)))
371	191	adantrl 728	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)))
372		f1ofn 6821	. . . . . . . . 9 ⊢ (𝑐:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) → 𝑐 Fn (2...(𝑁 + 1)))
373	371, 372	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐 Fn (2...(𝑁 + 1)))
374		eqfnfv 7025	. . . . . . . 8 ⊢ ((((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) Fn (2...(𝑁 + 1)) ∧ 𝑐 Fn (2...(𝑁 + 1))) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
375	370, 373, 374	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))‘𝑦) = (𝑐‘𝑦)))
376	362, 368, 375	3bitr4d 314	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐))
377		eqcom 2770	. . . . . 6 ⊢ (((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))) = 𝑐 ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1))))
378	376, 377	bitrdi 290	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝐹 ∘ 𝑏) = ({⟨1, 1⟩} ∪ 𝑐) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))))
379	331, 343, 378	3bitr3d 312	. . . 4 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝐹 ∘ ({⟨1, 1⟩} ∪ 𝑐)) ↔ 𝑐 = ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))))
380	12, 182, 321, 379	f1o2d 7664	. . 3 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ ((𝐹 ∘ 𝑏) ↾ (2...(𝑁 + 1)))):𝐵–1-1-onto→𝐶)
381	11, 380	hasheqf1od 14385	. 2 ⊢ (𝜑 → (♯‘𝐵) = (♯‘𝐶))
382	13, 14	derangen2 35666	. . . . 5 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (𝑆‘(♯‘(2...(𝑁 + 1)))))
383	13	derangval 35659	. . . . . 6 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}))
384	180	fveq2i 6884	. . . . . 6 ⊢ (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)})
385	383, 384	eqtr4di 2816	. . . . 5 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝐷‘(2...(𝑁 + 1))) = (♯‘𝐶))
386	382, 385	eqtr3d 2800	. . . 4 ⊢ ((2...(𝑁 + 1)) ∈ Fin → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶))
387	162, 386	ax-mp 5	. . 3 ⊢ (𝑆‘(♯‘(2...(𝑁 + 1)))) = (♯‘𝐶)
388	15, 58	eleqtrdi 2873	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
389		eluzp1p1 12885	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝑁 + 1) ∈ (ℤ_≥‘(1 + 1)))
390	388, 389	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘(1 + 1)))
391		df-2 12298	. . . . . . . 8 ⊢ 2 = (1 + 1)
392	391	fveq2i 6884	. . . . . . 7 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
393	390, 392	eleqtrrdi 2874	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘2))
394		hashfz 14460	. . . . . 6 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘2) → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
395	393, 394	syl 18	. . . . 5 ⊢ (𝜑 → (♯‘(2...(𝑁 + 1))) = (((𝑁 + 1) − 2) + 1))
396	57	nncnd 12244	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℂ)
397		2cnd 12314	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
398		1cnd 11197	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℂ)
399	396, 397, 398	subsubd 11592	. . . . 5 ⊢ (𝜑 → ((𝑁 + 1) − (2 − 1)) = (((𝑁 + 1) − 2) + 1))
400		2m1e1 12360	. . . . . . 7 ⊢ (2 − 1) = 1
401	400	oveq2i 7421	. . . . . 6 ⊢ ((𝑁 + 1) − (2 − 1)) = ((𝑁 + 1) − 1)
402	15	nncnd 12244	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
403		ax-1cn 11153	. . . . . . 7 ⊢ 1 ∈ ℂ
404		pncan 11458	. . . . . . 7 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
405	402, 403, 404	sylancl 597	. . . . . 6 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
406	401, 405	eqtrid 2810	. . . . 5 ⊢ (𝜑 → ((𝑁 + 1) − (2 − 1)) = 𝑁)
407	395, 399, 406	3eqtr2d 2804	. . . 4 ⊢ (𝜑 → (♯‘(2...(𝑁 + 1))) = 𝑁)
408	407	fveq2d 6885	. . 3 ⊢ (𝜑 → (𝑆‘(♯‘(2...(𝑁 + 1)))) = (𝑆‘𝑁))
409	387, 408	eqtr3id 2812	. 2 ⊢ (𝜑 → (♯‘𝐶) = (𝑆‘𝑁))
410	381, 409	eqtrd 2798	1 ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1570 ∈ wcel 2143 {cab 2741 ≠ wne 2958 ∀wral 3079 {crab 3416 Vcvv 3455 ∖ cdif 3902 ∪ cun 3903 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 {csn 4589 {cpr 4591 ⟨cop 4595 class class class wbr 5109 ↦ cmpt 5192 I cid 5555 ^◡ccnv 5660 dom cdm 5661 ↾ cres 5663 ∘ ccom 5665 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 8939 ℂcc 11093 1c1 11096 + caddc 11098 < clt 11238 ≤ cle 11239 − cmin 11436 ℕcn 12228 2c2 12290 ℕ₀cn0 12499 ℤcz 12586 ℤ_≥cuz 12857 ...cfz 13530 ♯chash 14362

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 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 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-oadd 8453 df-er 8690 df-map 8822 df-pm 8823 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-dju 9883 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-n0 12500 df-xnn0 12573 df-z 12587 df-uz 12858 df-fz 13531 df-hash 14363

This theorem is referenced by: subfacp1lem6 35677

W3C validator