subfacp1lem3 - Mathbox for Mario Carneiro

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

Theorem subfacp1lem3 32542

Description: Lemma for subfacp1 32546. In subfacp1lem6 32545 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 that satisfy this for fixed 𝑀 = (𝑓‘1) is in bijection with 𝑁 − 1 derangements, by simply dropping the 𝑥 = 1 and 𝑥 = 𝑀 points from the function to get a derangement on 𝐾 = (1...(𝑁 − 1)) ∖ {1, 𝑀}. (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)) ∖ {𝑀})
subfacp1lem3.b	⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1)}
subfacp1lem3.c	⊢ 𝐶 = {𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}

**Assertion**
Ref	Expression
subfacp1lem3	⊢ (𝜑 → (♯‘𝐵) = (𝑆‘(𝑁 − 1)))

Distinct variable groups: 𝑓,𝑔,𝑛,𝑥,𝑦,𝐴 𝑓,𝑁,𝑔,𝑛,𝑥,𝑦 𝐵,𝑓,𝑔,𝑥,𝑦 𝑥,𝐶,𝑦 𝜑,𝑥,𝑦 𝐷,𝑛 𝑓,𝐾,𝑛,𝑥,𝑦 𝑓,𝑀,𝑔,𝑥,𝑦 𝑆,𝑛,𝑥,𝑦 Allowed substitution hints: 𝜑(𝑓,𝑔,𝑛) 𝐵(𝑛) 𝐶(𝑓,𝑔,𝑛) 𝐷(𝑥,𝑦,𝑓,𝑔) 𝑆(𝑓,𝑔) 𝐾(𝑔) 𝑀(𝑛)

Proof of Theorem subfacp1lem3 Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		subfacp1lem.a	. . . . . . . 8 ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}
2		fzfi 13335	. . . . . . . . 9 ⊢ (1...(𝑁 + 1)) ∈ Fin
3		deranglem 32526	. . . . . . . . 9 ⊢ ((1...(𝑁 + 1)) ∈ Fin → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
4	2, 3	ax-mp 5	. . . . . . . 8 ⊢ {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin
5	1, 4	eqeltri 2886	. . . . . . 7 ⊢ 𝐴 ∈ Fin
6		subfacp1lem3.b	. . . . . . . 8 ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1)}
7		ssrab2 4007	. . . . . . . 8 ⊢ {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1)} ⊆ 𝐴
8	6, 7	eqsstri 3949	. . . . . . 7 ⊢ 𝐵 ⊆ 𝐴
9		ssfi 8722	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
10	5, 8, 9	mp2an 691	. . . . . 6 ⊢ 𝐵 ∈ Fin
11	10	elexi 3460	. . . . 5 ⊢ 𝐵 ∈ V
12	11	a1i 11	. . . 4 ⊢ (𝜑 → 𝐵 ∈ V)
13		subfacp1lem3.c	. . . . . . 7 ⊢ 𝐶 = {𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}
14		subfacp1lem1.k	. . . . . . . . 9 ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})
15		fzfi 13335	. . . . . . . . . 10 ⊢ (2...(𝑁 + 1)) ∈ Fin
16		diffi 8734	. . . . . . . . . 10 ⊢ ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ Fin)
17	15, 16	ax-mp 5	. . . . . . . . 9 ⊢ ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ Fin
18	14, 17	eqeltri 2886	. . . . . . . 8 ⊢ 𝐾 ∈ Fin
19		deranglem 32526	. . . . . . . 8 ⊢ (𝐾 ∈ Fin → {𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
20	18, 19	ax-mp 5	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin
21	13, 20	eqeltri 2886	. . . . . 6 ⊢ 𝐶 ∈ Fin
22	21	elexi 3460	. . . . 5 ⊢ 𝐶 ∈ V
23	22	a1i 11	. . . 4 ⊢ (𝜑 → 𝐶 ∈ V)
24		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
25		fveq1 6644	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
26	25	eqeq1d 2800	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
27		fveq1 6644	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑀) = (𝑏‘𝑀))
28	27	eqeq1d 2800	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → ((𝑔‘𝑀) = 1 ↔ (𝑏‘𝑀) = 1))
29	26, 28	anbi12d 633	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
30	29, 6	elrab2 3631	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
31	24, 30	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
32	31	simpld 498	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
33		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
34		f1oeq1 6579	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
35		fveq1 6644	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
36	35	neeq1d 3046	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
37	36	ralbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
38	34, 37	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)))
39	33, 38, 1	elab2 3618	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
40	32, 39	sylib 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
41	40	simpld 498	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
42		f1of1 6589	. . . . . . . . 9 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
43		df-f1 6329	. . . . . . . . . 10 ⊢ (𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun ^◡𝑏))
44	43	simprbi 500	. . . . . . . . 9 ⊢ (𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun ^◡𝑏)
45	41, 42, 44	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → Fun ^◡𝑏)
46		f1ofn 6591	. . . . . . . . . . . 12 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏 Fn (1...(𝑁 + 1)))
47	41, 46	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 Fn (1...(𝑁 + 1)))
48		fnresdm 6438	. . . . . . . . . . 11 ⊢ (𝑏 Fn (1...(𝑁 + 1)) → (𝑏 ↾ (1...(𝑁 + 1))) = 𝑏)
49		f1oeq1 6579	. . . . . . . . . . 11 ⊢ ((𝑏 ↾ (1...(𝑁 + 1))) = 𝑏 → ((𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
50	47, 48, 49	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
51	41, 50	mpbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
52		f1ofo 6597	. . . . . . . . 9 ⊢ ((𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
53	51, 52	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
54		ssun2 4100	. . . . . . . . . . . . 13 ⊢ {1, 𝑀} ⊆ (𝐾 ∪ {1, 𝑀})
55		derang.d	. . . . . . . . . . . . . . 15 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
56		subfac.n	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(1...𝑛)))
57		subfacp1lem1.n	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℕ)
58		subfacp1lem1.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))
59		subfacp1lem1.x	. . . . . . . . . . . . . . 15 ⊢ 𝑀 ∈ V
60	55, 56, 1, 57, 58, 59, 14	subfacp1lem1 32539	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (♯‘𝐾) = (𝑁 − 1)))
61	60	simp2d 1140	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
62	54, 61	sseqtrid 3967	. . . . . . . . . . . 12 ⊢ (𝜑 → {1, 𝑀} ⊆ (1...(𝑁 + 1)))
63	62	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {1, 𝑀} ⊆ (1...(𝑁 + 1)))
64		fnssres 6442	. . . . . . . . . . 11 ⊢ ((𝑏 Fn (1...(𝑁 + 1)) ∧ {1, 𝑀} ⊆ (1...(𝑁 + 1))) → (𝑏 ↾ {1, 𝑀}) Fn {1, 𝑀})
65	47, 63, 64	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}) Fn {1, 𝑀})
66	31	simprd 499	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1))
67	66	simpld 498	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) = 𝑀)
68	59	prid2 4659	. . . . . . . . . . . . 13 ⊢ 𝑀 ∈ {1, 𝑀}
69	67, 68	eqeltrdi 2898	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) ∈ {1, 𝑀})
70	66	simprd 499	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) = 1)
71		1ex 10626	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
72	71	prid1 4658	. . . . . . . . . . . . 13 ⊢ 1 ∈ {1, 𝑀}
73	70, 72	eqeltrdi 2898	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ∈ {1, 𝑀})
74		fveq2 6645	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑏‘𝑥) = (𝑏‘1))
75	74	eleq1d 2874	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → ((𝑏‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘1) ∈ {1, 𝑀}))
76		fveq2 6645	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑀 → (𝑏‘𝑥) = (𝑏‘𝑀))
77	76	eleq1d 2874	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑀 → ((𝑏‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘𝑀) ∈ {1, 𝑀}))
78	71, 59, 75, 77	ralpr 4596	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀} ↔ ((𝑏‘1) ∈ {1, 𝑀} ∧ (𝑏‘𝑀) ∈ {1, 𝑀}))
79	69, 73, 78	sylanbrc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀})
80		fvres 6664	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {1, 𝑀} → ((𝑏 ↾ {1, 𝑀})‘𝑥) = (𝑏‘𝑥))
81	80	eleq1d 2874	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {1, 𝑀} → (((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘𝑥) ∈ {1, 𝑀}))
82	81	ralbiia 3132	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀} ↔ ∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀})
83	79, 82	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀})
84		ffnfv 6859	. . . . . . . . . 10 ⊢ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀} ↔ ((𝑏 ↾ {1, 𝑀}) Fn {1, 𝑀} ∧ ∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀}))
85	65, 83, 84	sylanbrc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀})
86		fveqeq2 6654	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) = 1 ↔ (𝑏‘𝑀) = 1))
87	86	rspcev 3571	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ {1, 𝑀} ∧ (𝑏‘𝑀) = 1) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1)
88	68, 70, 87	sylancr 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1)
89		fveqeq2 6654	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → ((𝑏‘𝑦) = 𝑀 ↔ (𝑏‘1) = 𝑀))
90	89	rspcev 3571	. . . . . . . . . . . 12 ⊢ ((1 ∈ {1, 𝑀} ∧ (𝑏‘1) = 𝑀) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀)
91	72, 67, 90	sylancr 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀)
92		eqeq2 2810	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → ((𝑏‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 1))
93	92	rexbidv 3256	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1))
94		eqeq2 2810	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑀 → ((𝑏‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 𝑀))
95	94	rexbidv 3256	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀))
96	71, 59, 93, 95	ralpr 4596	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1 ∧ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀))
97	88, 91, 96	sylanbrc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥)
98		eqcom 2805	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ ((𝑏 ↾ {1, 𝑀})‘𝑦) = 𝑥)
99		fvres 6664	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {1, 𝑀} → ((𝑏 ↾ {1, 𝑀})‘𝑦) = (𝑏‘𝑦))
100	99	eqeq1d 2800	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {1, 𝑀} → (((𝑏 ↾ {1, 𝑀})‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 𝑥))
101	98, 100	syl5bb 286	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {1, 𝑀} → (𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ (𝑏‘𝑦) = 𝑥))
102	101	rexbiia 3209	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥)
103	102	ralbii 3133	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥)
104	97, 103	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦))
105		dffo3 6845	. . . . . . . . 9 ⊢ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}–onto→{1, 𝑀} ↔ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀} ∧ ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦)))
106	85, 104, 105	sylanbrc 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}):{1, 𝑀}–onto→{1, 𝑀})
107		resdif 6610	. . . . . . . 8 ⊢ ((Fun ^◡𝑏 ∧ (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)) ∧ (𝑏 ↾ {1, 𝑀}):{1, 𝑀}–onto→{1, 𝑀}) → (𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}))
108	45, 53, 106, 107	syl3anc 1368	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}))
109		uncom 4080	. . . . . . . . . . 11 ⊢ ({1, 𝑀} ∪ 𝐾) = (𝐾 ∪ {1, 𝑀})
110	109, 61	syl5eq 2845	. . . . . . . . . 10 ⊢ (𝜑 → ({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)))
111		incom 4128	. . . . . . . . . . . 12 ⊢ ({1, 𝑀} ∩ 𝐾) = (𝐾 ∩ {1, 𝑀})
112	60	simp1d 1139	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 ∩ {1, 𝑀}) = ∅)
113	111, 112	syl5eq 2845	. . . . . . . . . . 11 ⊢ (𝜑 → ({1, 𝑀} ∩ 𝐾) = ∅)
114		uneqdifeq 4396	. . . . . . . . . . 11 ⊢ (({1, 𝑀} ⊆ (1...(𝑁 + 1)) ∧ ({1, 𝑀} ∩ 𝐾) = ∅) → (({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾))
115	62, 113, 114	syl2anc 587	. . . . . . . . . 10 ⊢ (𝜑 → (({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾))
116	110, 115	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾)
117	116	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾)
118		reseq2 5813	. . . . . . . . . 10 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → (𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})) = (𝑏 ↾ 𝐾))
119		f1oeq1 6579	. . . . . . . . . 10 ⊢ ((𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})) = (𝑏 ↾ 𝐾) → ((𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀})))
120	118, 119	syl 17	. . . . . . . . 9 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀})))
121		f1oeq2 6580	. . . . . . . . 9 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ 𝐾):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀})))
122		f1oeq3 6581	. . . . . . . . 9 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ 𝐾):𝐾–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
123	120, 121, 122	3bitrd 308	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
124	117, 123	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
125	108, 124	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾)
126		ssun1 4099	. . . . . . . . 9 ⊢ 𝐾 ⊆ (𝐾 ∪ {1, 𝑀})
127	126, 61	sseqtrid 3967	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ⊆ (1...(𝑁 + 1)))
128	127	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐾 ⊆ (1...(𝑁 + 1)))
129	40	simprd 499	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)
130		ssralv 3981	. . . . . . 7 ⊢ (𝐾 ⊆ (1...(𝑁 + 1)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦 → ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
131	128, 129, 130	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦)
132	33	resex 5866	. . . . . . 7 ⊢ (𝑏 ↾ 𝐾) ∈ V
133		f1oeq1 6579	. . . . . . . 8 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (𝑓:𝐾–1-1-onto→𝐾 ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
134		fveq1 6644	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (𝑓‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦))
135		fvres 6664	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐾 → ((𝑏 ↾ 𝐾)‘𝑦) = (𝑏‘𝑦))
136	134, 135	sylan9eq 2853	. . . . . . . . . 10 ⊢ ((𝑓 = (𝑏 ↾ 𝐾) ∧ 𝑦 ∈ 𝐾) → (𝑓‘𝑦) = (𝑏‘𝑦))
137	136	neeq1d 3046	. . . . . . . . 9 ⊢ ((𝑓 = (𝑏 ↾ 𝐾) ∧ 𝑦 ∈ 𝐾) → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
138	137	ralbidva 3161	. . . . . . . 8 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
139	133, 138	anbi12d 633	. . . . . . 7 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → ((𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦) ↔ ((𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦)))
140	132, 139, 13	elab2 3618	. . . . . 6 ⊢ ((𝑏 ↾ 𝐾) ∈ 𝐶 ↔ ((𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
141	125, 131, 140	sylanbrc 586	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ 𝐾) ∈ 𝐶)
142	141	ex 416	. . . 4 ⊢ (𝜑 → (𝑏 ∈ 𝐵 → (𝑏 ↾ 𝐾) ∈ 𝐶))
143	57	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑁 ∈ ℕ)
144	58	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
145		eqid 2798	. . . . . . . . 9 ⊢ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})
146		simpr 488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐 ∈ 𝐶)
147		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑐 ∈ V
148		f1oeq1 6579	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑓:𝐾–1-1-onto→𝐾 ↔ 𝑐:𝐾–1-1-onto→𝐾))
149		fveq1 6644	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑐 → (𝑓‘𝑦) = (𝑐‘𝑦))
150	149	neeq1d 3046	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑦) ≠ 𝑦))
151	150	ralbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
152	148, 151	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → ((𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦) ↔ (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦)))
153	147, 152, 13	elab2 3618	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
154	146, 153	sylib 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
155	154	simpld 498	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:𝐾–1-1-onto→𝐾)
156	55, 56, 1, 143, 144, 59, 14, 145, 155	subfacp1lem2a 32540	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
157	156	simp1d 1139	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
158	55, 56, 1, 143, 144, 59, 14, 145, 155	subfacp1lem2b 32541	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = (𝑐‘𝑦))
159	154	simprd 499	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦)
160	159	r19.21bi 3173	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → (𝑐‘𝑦) ≠ 𝑦)
161	158, 160	eqnetrd 3054	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
162	161	ralrimiva 3149	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ 𝐾 ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
163	156	simp2d 1140	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀)
164		elfzuz 12898	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (2...(𝑁 + 1)) → 𝑀 ∈ (ℤ_≥‘2))
165		eluz2b3 12310	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
166	165	simprbi 500	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ≠ 1)
167	58, 164, 166	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ≠ 1)
168	167	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ 1)
169	163, 168	eqnetrd 3054	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1)
170	156	simp3d 1141	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)
171	168	necomd 3042	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 1 ≠ 𝑀)
172	170, 171	eqnetrd 3054	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀)
173		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
174		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → 𝑦 = 1)
175	173, 174	neeq12d 3048	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1))
176		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
177		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
178	176, 177	neeq12d 3048	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀))
179	71, 59, 175, 178	ralpr 4596	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀))
180	169, 172, 179	sylanbrc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
181		ralunb 4118	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ (∀𝑦 ∈ 𝐾 ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ∧ ∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
182	162, 180, 181	sylanbrc 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
183	61	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
184	183	raleqdv 3364	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
185	182, 184	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
186		prex 5298	. . . . . . . . 9 ⊢ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
187	147, 186	unex 7449	. . . . . . . 8 ⊢ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
188		f1oeq1 6579	. . . . . . . . 9 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
189		fveq1 6644	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑓‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))
190	189	neeq1d 3046	. . . . . . . . . 10 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
191	190	ralbidv 3162	. . . . . . . . 9 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
192	188, 191	anbi12d 633	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)))
193	187, 192, 1	elab2 3618	. . . . . . 7 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
194	157, 185, 193	sylanbrc 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴)
195	163, 170	jca 515	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
196		fveq1 6644	. . . . . . . . 9 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑔‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
197	196	eqeq1d 2800	. . . . . . . 8 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑔‘1) = 𝑀 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀))
198		fveq1 6644	. . . . . . . . 9 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑔‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
199	198	eqeq1d 2800	. . . . . . . 8 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑔‘𝑀) = 1 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
200	197, 199	anbi12d 633	. . . . . . 7 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1) ↔ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)))
201	200, 6	elrab2 3631	. . . . . 6 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐵 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴 ∧ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)))
202	194, 195, 201	sylanbrc 586	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐵)
203	202	ex 416	. . . 4 ⊢ (𝜑 → (𝑐 ∈ 𝐶 → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐵))
204	67	adantrr 716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘1) = 𝑀)
205	163	adantrl 715	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀)
206	204, 205	eqtr4d 2836	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
207	70	adantrr 716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘𝑀) = 1)
208	170	adantrl 715	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)
209	207, 208	eqtr4d 2836	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
210		fveq2 6645	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1 → (𝑏‘𝑦) = (𝑏‘1))
211	210, 173	eqeq12d 2814	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1)))
212		fveq2 6645	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → (𝑏‘𝑦) = (𝑏‘𝑀))
213	212, 176	eqeq12d 2814	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀)))
214	71, 59, 211, 213	ralpr 4596	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ((𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ∧ (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀)))
215	206, 209, 214	sylanbrc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))
216	215	biantrud 535	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ∧ ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))))
217		ralunb 4118	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ∧ ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
218	216, 217	syl6bbr 292	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
219	158	eqeq2d 2809	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
220	219	ralbidva 3161	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
221	220	adantrl 715	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
222	61	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
223	222	raleqdv 3364	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
224	218, 221, 223	3bitr3rd 313	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
225	135	eqeq2d 2809	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝐾 → ((𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ (𝑐‘𝑦) = (𝑏‘𝑦)))
226		eqcom 2805	. . . . . . . . 9 ⊢ ((𝑐‘𝑦) = (𝑏‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦))
227	225, 226	syl6bb 290	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐾 → ((𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
228	227	ralbiia 3132	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦))
229	224, 228	syl6bbr 292	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
230	47	adantrr 716	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑏 Fn (1...(𝑁 + 1)))
231	157	adantrl 715	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
232		f1ofn 6591	. . . . . . . 8 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) Fn (1...(𝑁 + 1)))
233	231, 232	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) Fn (1...(𝑁 + 1)))
234		eqfnfv 6779	. . . . . . 7 ⊢ ((𝑏 Fn (1...(𝑁 + 1)) ∧ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) Fn (1...(𝑁 + 1))) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
235	230, 233, 234	syl2anc 587	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
236	155	adantrl 715	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐:𝐾–1-1-onto→𝐾)
237		f1ofn 6591	. . . . . . . 8 ⊢ (𝑐:𝐾–1-1-onto→𝐾 → 𝑐 Fn 𝐾)
238	236, 237	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐 Fn 𝐾)
239	127	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐾 ⊆ (1...(𝑁 + 1)))
240		fnssres 6442	. . . . . . . 8 ⊢ ((𝑏 Fn (1...(𝑁 + 1)) ∧ 𝐾 ⊆ (1...(𝑁 + 1))) → (𝑏 ↾ 𝐾) Fn 𝐾)
241	230, 239, 240	syl2anc 587	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 ↾ 𝐾) Fn 𝐾)
242		eqfnfv 6779	. . . . . . 7 ⊢ ((𝑐 Fn 𝐾 ∧ (𝑏 ↾ 𝐾) Fn 𝐾) → (𝑐 = (𝑏 ↾ 𝐾) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
243	238, 241, 242	syl2anc 587	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 = (𝑏 ↾ 𝐾) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
244	229, 235, 243	3bitr4d 314	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ 𝑐 = (𝑏 ↾ 𝐾)))
245	244	ex 416	. . . 4 ⊢ (𝜑 → ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ 𝑐 = (𝑏 ↾ 𝐾))))
246	12, 23, 142, 203, 245	en3d 8529	. . 3 ⊢ (𝜑 → 𝐵 ≈ 𝐶)
247		hashen 13703	. . . 4 ⊢ ((𝐵 ∈ Fin ∧ 𝐶 ∈ Fin) → ((♯‘𝐵) = (♯‘𝐶) ↔ 𝐵 ≈ 𝐶))
248	10, 21, 247	mp2an 691	. . 3 ⊢ ((♯‘𝐵) = (♯‘𝐶) ↔ 𝐵 ≈ 𝐶)
249	246, 248	sylibr 237	. 2 ⊢ (𝜑 → (♯‘𝐵) = (♯‘𝐶))
250	13	fveq2i 6648	. . . 4 ⊢ (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)})
251	55	derangval 32527	. . . . 5 ⊢ (𝐾 ∈ Fin → (𝐷‘𝐾) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}))
252	18, 251	ax-mp 5	. . . 4 ⊢ (𝐷‘𝐾) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)})
253	55, 56	derangen2 32534	. . . . 5 ⊢ (𝐾 ∈ Fin → (𝐷‘𝐾) = (𝑆‘(♯‘𝐾)))
254	18, 253	ax-mp 5	. . . 4 ⊢ (𝐷‘𝐾) = (𝑆‘(♯‘𝐾))
255	250, 252, 254	3eqtr2ri 2828	. . 3 ⊢ (𝑆‘(♯‘𝐾)) = (♯‘𝐶)
256	60	simp3d 1141	. . . 4 ⊢ (𝜑 → (♯‘𝐾) = (𝑁 − 1))
257	256	fveq2d 6649	. . 3 ⊢ (𝜑 → (𝑆‘(♯‘𝐾)) = (𝑆‘(𝑁 − 1)))
258	255, 257	syl5eqr 2847	. 2 ⊢ (𝜑 → (♯‘𝐶) = (𝑆‘(𝑁 − 1)))
259	249, 258	eqtrd 2833	1 ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘(𝑁 − 1)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 {cab 2776 ≠ wne 2987 ∀wral 3106 ∃wrex 3107 {crab 3110 Vcvv 3441 ∖ cdif 3878 ∪ cun 3879 ∩ cin 3880 ⊆ wss 3881 ∅c0 4243 {csn 4525 {cpr 4527 ⟨cop 4531 class class class wbr 5030 ↦ cmpt 5110 ^◡ccnv 5518 ↾ cres 5521 Fun wfun 6318 Fn wfn 6319 ⟶wf 6320 –1-1→wf1 6321 –onto→wfo 6322 –1-1-onto→wf1o 6323 ‘cfv 6324 (class class class)co 7135 ≈ cen 8489 Fincfn 8492 1c1 10527 + caddc 10529 − cmin 10859 ℕcn 11625 2c2 11680 ℕ₀cn0 11885 ℤ_≥cuz 12231 ...cfz 12885 ♯chash 13686

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-2o 8086 df-oadd 8089 df-er 8272 df-map 8391 df-pm 8392 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-dju 9314 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-nn 11626 df-2 11688 df-n0 11886 df-xnn0 11956 df-z 11970 df-uz 12232 df-fz 12886 df-hash 13687

This theorem is referenced by: subfacp1lem6 32545

W3C validator