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 36037

Description: Lemma for subfacp1 36041. In subfacp1lem6 36040 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	. . . . . . 7 ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}
2		fzfi 14122	. . . . . . . 8 ⊢ (1...(𝑁 + 1)) ∈ Fin
3		deranglem 36021	. . . . . . . 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 2856	. . . . . 6 ⊢ 𝐴 ∈ Fin
6		subfacp1lem3.b	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1)}
7	6	ssrab3 4006	. . . . . 6 ⊢ 𝐵 ⊆ 𝐴
8		ssfi 9195	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
9	5, 7, 8	mp2an 705	. . . . 5 ⊢ 𝐵 ∈ Fin
10	9	elexi 3472	. . . 4 ⊢ 𝐵 ∈ V
11	10	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
12		eqid 2760	. . . 4 ⊢ (𝑏 ∈ 𝐵 ↦ (𝑏 ↾ 𝐾)) = (𝑏 ∈ 𝐵 ↦ (𝑏 ↾ 𝐾))
13		fveq1 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
14	13	eqeq1d 2762	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
15		fveq1 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑀) = (𝑏‘𝑀))
16	15	eqeq1d 2762	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → ((𝑔‘𝑀) = 1 ↔ (𝑏‘𝑀) = 1))
17	14, 16	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
18	17, 6	elrab2 3648	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
19	18	bilani 510	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
20	19	simpld 500	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
21		vex 3454	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
22		f1oeq1 6817	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
23		fveq1 6889	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
24	23	neeq1d 3014	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
25	24	ralbidv 3185	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
26	22, 25	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)))
27	21, 26, 1	elab2 3635	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
28	20, 27	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
29	28	simpld 500	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
30		f1of1 6828	. . . . . . . 8 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
31		df-f1 6548	. . . . . . . . 9 ⊢ (𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun ^◡𝑏))
32	31	simprbi 503	. . . . . . . 8 ⊢ (𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun ^◡𝑏)
33	29, 30, 32	3syl 19	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → Fun ^◡𝑏)
34		f1ofn 6830	. . . . . . . . . . 11 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏 Fn (1...(𝑁 + 1)))
35	29, 34	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 Fn (1...(𝑁 + 1)))
36		fnresdm 6663	. . . . . . . . . 10 ⊢ (𝑏 Fn (1...(𝑁 + 1)) → (𝑏 ↾ (1...(𝑁 + 1))) = 𝑏)
37		f1oeq1 6817	. . . . . . . . . 10 ⊢ ((𝑏 ↾ (1...(𝑁 + 1))) = 𝑏 → ((𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
38	35, 36, 37	3syl 19	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
39	29, 38	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
40		f1ofo 6837	. . . . . . . 8 ⊢ ((𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
41	39, 40	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
42		ssun2 4176	. . . . . . . . . . . 12 ⊢ {1, 𝑀} ⊆ (𝐾 ∪ {1, 𝑀})
43		derang.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
44		subfac.n	. . . . . . . . . . . . . 14 ⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(1...𝑛)))
45		subfacp1lem1.n	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
46		subfacp1lem1.m	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))
47		subfacp1lem1.x	. . . . . . . . . . . . . 14 ⊢ 𝑀 ∈ V
48		subfacp1lem1.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})
49	43, 44, 1, 45, 46, 47, 48	subfacp1lem1 36034	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (♯‘𝐾) = (𝑁 − 1)))
50	49	simp2d 1161	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
51	42, 50	sseqtrid 3951	. . . . . . . . . . 11 ⊢ (𝜑 → {1, 𝑀} ⊆ (1...(𝑁 + 1)))
52	51	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {1, 𝑀} ⊆ (1...(𝑁 + 1)))
53	35, 52	fnssresd 6668	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}) Fn {1, 𝑀})
54	19	simprd 501	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1))
55	54	simpld 500	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) = 𝑀)
56	47	prid2 4720	. . . . . . . . . . . 12 ⊢ 𝑀 ∈ {1, 𝑀}
57	55, 56	eqeltrdi 2868	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) ∈ {1, 𝑀})
58	54	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) = 1)
59		1ex 11310	. . . . . . . . . . . . 13 ⊢ 1 ∈ V
60	59	prid1 4719	. . . . . . . . . . . 12 ⊢ 1 ∈ {1, 𝑀}
61	58, 60	eqeltrdi 2868	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ∈ {1, 𝑀})
62		fveq2 6890	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑏‘𝑥) = (𝑏‘1))
63	62	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((𝑏‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘1) ∈ {1, 𝑀}))
64		fveq2 6890	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑀 → (𝑏‘𝑥) = (𝑏‘𝑀))
65	64	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → ((𝑏‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘𝑀) ∈ {1, 𝑀}))
66	59, 47, 63, 65	ralpr 4657	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀} ↔ ((𝑏‘1) ∈ {1, 𝑀} ∧ (𝑏‘𝑀) ∈ {1, 𝑀}))
67	57, 61, 66	sylanbrc 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀})
68		fvres 6909	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {1, 𝑀} → ((𝑏 ↾ {1, 𝑀})‘𝑥) = (𝑏‘𝑥))
69	68	eleq1d 2845	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {1, 𝑀} → (((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘𝑥) ∈ {1, 𝑀}))
70	69	ralbiia 3106	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀} ↔ ∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀})
71	67, 70	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀})
72		ffnfv 7124	. . . . . . . . 9 ⊢ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀} ↔ ((𝑏 ↾ {1, 𝑀}) Fn {1, 𝑀} ∧ ∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀}))
73	53, 71, 72	sylanbrc 595	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀})
74		fveqeq2 6899	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) = 1 ↔ (𝑏‘𝑀) = 1))
75	74	rspcev 3576	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ {1, 𝑀} ∧ (𝑏‘𝑀) = 1) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1)
76	56, 58, 75	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1)
77		fveqeq2 6899	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → ((𝑏‘𝑦) = 𝑀 ↔ (𝑏‘1) = 𝑀))
78	77	rspcev 3576	. . . . . . . . . . 11 ⊢ ((1 ∈ {1, 𝑀} ∧ (𝑏‘1) = 𝑀) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀)
79	60, 55, 78	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀)
80		eqeq2 2772	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((𝑏‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 1))
81	80	rexbidv 3186	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1))
82		eqeq2 2772	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → ((𝑏‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 𝑀))
83	82	rexbidv 3186	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑀 → (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀))
84	59, 47, 81, 83	ralpr 4657	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1 ∧ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀))
85	76, 79, 84	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥)
86		eqcom 2767	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ ((𝑏 ↾ {1, 𝑀})‘𝑦) = 𝑥)
87		fvres 6909	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {1, 𝑀} → ((𝑏 ↾ {1, 𝑀})‘𝑦) = (𝑏‘𝑦))
88	87	eqeq1d 2762	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {1, 𝑀} → (((𝑏 ↾ {1, 𝑀})‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 𝑥))
89	86, 88	bitrid 286	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {1, 𝑀} → (𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ (𝑏‘𝑦) = 𝑥))
90	89	rexbiia 3107	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥)
91	90	ralbii 3108	. . . . . . . . 9 ⊢ (∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥)
92	85, 91	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦))
93		dffo3 7107	. . . . . . . 8 ⊢ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}–onto→{1, 𝑀} ↔ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀} ∧ ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦)))
94	73, 92, 93	sylanbrc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}):{1, 𝑀}–onto→{1, 𝑀})
95		resdif 6851	. . . . . . 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, 𝑀}))
96	33, 41, 94, 95	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}))
97		uncom 4156	. . . . . . . . . 10 ⊢ ({1, 𝑀} ∪ 𝐾) = (𝐾 ∪ {1, 𝑀})
98	97, 50	eqtrid 2807	. . . . . . . . 9 ⊢ (𝜑 → ({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)))
99		incom 4105	. . . . . . . . . . 11 ⊢ ({1, 𝑀} ∩ 𝐾) = (𝐾 ∩ {1, 𝑀})
100	49	simp1d 1160	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 ∩ {1, 𝑀}) = ∅)
101	99, 100	eqtrid 2807	. . . . . . . . . 10 ⊢ (𝜑 → ({1, 𝑀} ∩ 𝐾) = ∅)
102		uneqdifeq 4447	. . . . . . . . . 10 ⊢ (({1, 𝑀} ⊆ (1...(𝑁 + 1)) ∧ ({1, 𝑀} ∩ 𝐾) = ∅) → (({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾))
103	51, 101, 102	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾))
104	98, 103	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾)
105	104	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾)
106		reseq2 5966	. . . . . . . . 9 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → (𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})) = (𝑏 ↾ 𝐾))
107	106	f1oeq1d 6824	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀})))
108		f1oeq2 6818	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ 𝐾):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀})))
109		f1oeq3 6819	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ 𝐾):𝐾–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
110	107, 108, 109	3bitrd 308	. . . . . . 7 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
111	105, 110	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
112	96, 111	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾)
113		ssun1 4175	. . . . . . . 8 ⊢ 𝐾 ⊆ (𝐾 ∪ {1, 𝑀})
114	113, 50	sseqtrid 3951	. . . . . . 7 ⊢ (𝜑 → 𝐾 ⊆ (1...(𝑁 + 1)))
115	114	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐾 ⊆ (1...(𝑁 + 1)))
116	28	simprd 501	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)
117		ssralv 3978	. . . . . 6 ⊢ (𝐾 ⊆ (1...(𝑁 + 1)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦 → ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
118	115, 116, 117	sylc 66	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦)
119	21	resex 6020	. . . . . 6 ⊢ (𝑏 ↾ 𝐾) ∈ V
120		f1oeq1 6817	. . . . . . 7 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (𝑓:𝐾–1-1-onto→𝐾 ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
121		fveq1 6889	. . . . . . . . . 10 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (𝑓‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦))
122		fvres 6909	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐾 → ((𝑏 ↾ 𝐾)‘𝑦) = (𝑏‘𝑦))
123	121, 122	sylan9eq 2815	. . . . . . . . 9 ⊢ ((𝑓 = (𝑏 ↾ 𝐾) ∧ 𝑦 ∈ 𝐾) → (𝑓‘𝑦) = (𝑏‘𝑦))
124	123	neeq1d 3014	. . . . . . . 8 ⊢ ((𝑓 = (𝑏 ↾ 𝐾) ∧ 𝑦 ∈ 𝐾) → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
125	124	ralbidva 3183	. . . . . . 7 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
126	120, 125	anbi12d 644	. . . . . 6 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → ((𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦) ↔ ((𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦)))
127		subfacp1lem3.c	. . . . . 6 ⊢ 𝐶 = {𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}
128	119, 126, 127	elab2 3635	. . . . 5 ⊢ ((𝑏 ↾ 𝐾) ∈ 𝐶 ↔ ((𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
129	112, 118, 128	sylanbrc 595	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ 𝐾) ∈ 𝐶)
130	45	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑁 ∈ ℕ)
131	46	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
132		eqid 2760	. . . . . . . 8 ⊢ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})
133		vex 3454	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
134		f1oeq1 6817	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → (𝑓:𝐾–1-1-onto→𝐾 ↔ 𝑐:𝐾–1-1-onto→𝐾))
135		fveq1 6889	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → (𝑓‘𝑦) = (𝑐‘𝑦))
136	135	neeq1d 3014	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑦) ≠ 𝑦))
137	136	ralbidv 3185	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → (∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
138	134, 137	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑐 → ((𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦) ↔ (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦)))
139	133, 138, 127	elab2 3635	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
140	139	bilani 510	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
141	140	simpld 500	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:𝐾–1-1-onto→𝐾)
142	43, 44, 1, 130, 131, 47, 48, 132, 141	subfacp1lem2a 36035	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
143	142	simp1d 1160	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
144	43, 44, 1, 130, 131, 47, 48, 132, 141	subfacp1lem2b 36036	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = (𝑐‘𝑦))
145	140	simprd 501	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦)
146	145	r19.21bi 3254	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → (𝑐‘𝑦) ≠ 𝑦)
147	144, 146	eqnetrd 3022	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
148	147	ralrimiva 3154	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ 𝐾 ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
149	142	simp2d 1161	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀)
150		elfzuz 13659	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (2...(𝑁 + 1)) → 𝑀 ∈ (ℤ_≥‘2))
151		eluz2b3 13056	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (ℤ_≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
152	151	simprbi 503	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ≠ 1)
153	46, 150, 152	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≠ 1)
154	153	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ 1)
155	149, 154	eqnetrd 3022	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1)
156	142	simp3d 1162	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)
157	154	necomd 3010	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 1 ≠ 𝑀)
158	156, 157	eqnetrd 3022	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀)
159		fveq2 6890	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
160		id 23	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → 𝑦 = 1)
161	159, 160	neeq12d 3016	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1))
162		fveq2 6890	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
163		id 23	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
164	162, 163	neeq12d 3016	. . . . . . . . . 10 ⊢ (𝑦 = 𝑀 → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀))
165	59, 47, 161, 164	ralpr 4657	. . . . . . . . 9 ⊢ (∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀))
166	155, 158, 165	sylanbrc 595	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
167		ralunb 4194	. . . . . . . 8 ⊢ (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ (∀𝑦 ∈ 𝐾 ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ∧ ∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
168	148, 166, 167	sylanbrc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
169	50	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
170	168, 169	raleqtrdv 3321	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
171		prex 5396	. . . . . . . 8 ⊢ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
172	133, 171	unex 7765	. . . . . . 7 ⊢ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
173		f1oeq1 6817	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
174		fveq1 6889	. . . . . . . . . 10 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑓‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))
175	174	neeq1d 3014	. . . . . . . . 9 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
176	175	ralbidv 3185	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
177	173, 176	anbi12d 644	. . . . . . 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⟩})‘𝑦) ≠ 𝑦)))
178	172, 177, 1	elab2 3635	. . . . . 6 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
179	143, 170, 178	sylanbrc 595	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴)
180	149, 156	jca 521	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
181		fveq1 6889	. . . . . . . 8 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑔‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
182	181	eqeq1d 2762	. . . . . . 7 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑔‘1) = 𝑀 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀))
183		fveq1 6889	. . . . . . . 8 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑔‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
184	183	eqeq1d 2762	. . . . . . 7 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑔‘𝑀) = 1 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
185	182, 184	anbi12d 644	. . . . . 6 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1) ↔ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)))
186	185, 6	elrab2 3648	. . . . 5 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐵 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴 ∧ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)))
187	179, 180, 186	sylanbrc 595	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐵)
188	55	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘1) = 𝑀)
189	149	adantrl 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀)
190	188, 189	eqtr4d 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
191	58	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘𝑀) = 1)
192	156	adantrl 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)
193	191, 192	eqtr4d 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
194		fveq2 6890	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → (𝑏‘𝑦) = (𝑏‘1))
195	194, 159	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1)))
196		fveq2 6890	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → (𝑏‘𝑦) = (𝑏‘𝑀))
197	196, 162	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀)))
198	59, 47, 195, 197	ralpr 4657	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ((𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ∧ (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀)))
199	190, 193, 198	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))
200	199	biantrud 541	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ∧ ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))))
201		ralunb 4194	. . . . . . . 8 ⊢ (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ∧ ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
202	200, 201	bitr4di 292	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
203	144	eqeq2d 2771	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
204	203	ralbidva 3183	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
205	204	adantrl 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
206	50	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
207	206	raleqdv 3319	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
208	202, 205, 207	3bitr3rd 313	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
209	122	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐾 → ((𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ (𝑐‘𝑦) = (𝑏‘𝑦)))
210		eqcom 2767	. . . . . . . 8 ⊢ ((𝑐‘𝑦) = (𝑏‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦))
211	209, 210	bitrdi 290	. . . . . . 7 ⊢ (𝑦 ∈ 𝐾 → ((𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
212	211	ralbiia 3106	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦))
213	208, 212	bitr4di 292	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
214	35	adantrr 730	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑏 Fn (1...(𝑁 + 1)))
215	143	adantrl 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
216		f1ofn 6830	. . . . . . 7 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) Fn (1...(𝑁 + 1)))
217	215, 216	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) Fn (1...(𝑁 + 1)))
218		eqfnfv 7034	. . . . . 6 ⊢ ((𝑏 Fn (1...(𝑁 + 1)) ∧ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) Fn (1...(𝑁 + 1))) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
219	214, 217, 218	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
220	141	adantrl 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐:𝐾–1-1-onto→𝐾)
221		f1ofn 6830	. . . . . . 7 ⊢ (𝑐:𝐾–1-1-onto→𝐾 → 𝑐 Fn 𝐾)
222	220, 221	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐 Fn 𝐾)
223	114	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐾 ⊆ (1...(𝑁 + 1)))
224	214, 223	fnssresd 6668	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 ↾ 𝐾) Fn 𝐾)
225		eqfnfv 7034	. . . . . 6 ⊢ ((𝑐 Fn 𝐾 ∧ (𝑏 ↾ 𝐾) Fn 𝐾) → (𝑐 = (𝑏 ↾ 𝐾) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
226	222, 224, 225	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 = (𝑏 ↾ 𝐾) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
227	213, 219, 226	3bitr4d 314	. . . 4 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ 𝑐 = (𝑏 ↾ 𝐾)))
228	12, 129, 187, 227	f1o2d 7679	. . 3 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ (𝑏 ↾ 𝐾)):𝐵–1-1-onto→𝐶)
229	11, 228	hasheqf1od 14504	. 2 ⊢ (𝜑 → (♯‘𝐵) = (♯‘𝐶))
230	127	fveq2i 6893	. . . 4 ⊢ (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)})
231		fzfi 14122	. . . . . . 7 ⊢ (2...(𝑁 + 1)) ∈ Fin
232		diffi 9197	. . . . . . 7 ⊢ ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ Fin)
233	231, 232	ax-mp 5	. . . . . 6 ⊢ ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ Fin
234	48, 233	eqeltri 2856	. . . . 5 ⊢ 𝐾 ∈ Fin
235	43	derangval 36022	. . . . 5 ⊢ (𝐾 ∈ Fin → (𝐷‘𝐾) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}))
236	234, 235	ax-mp 5	. . . 4 ⊢ (𝐷‘𝐾) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)})
237	43, 44	derangen2 36029	. . . . 5 ⊢ (𝐾 ∈ Fin → (𝐷‘𝐾) = (𝑆‘(♯‘𝐾)))
238	234, 237	ax-mp 5	. . . 4 ⊢ (𝐷‘𝐾) = (𝑆‘(♯‘𝐾))
239	230, 236, 238	3eqtr2ri 2790	. . 3 ⊢ (𝑆‘(♯‘𝐾)) = (♯‘𝐶)
240	49	simp3d 1162	. . . 4 ⊢ (𝜑 → (♯‘𝐾) = (𝑁 − 1))
241	240	fveq2d 6894	. . 3 ⊢ (𝜑 → (𝑆‘(♯‘𝐾)) = (𝑆‘(𝑁 − 1)))
242	239, 241	eqtr3id 2809	. 2 ⊢ (𝜑 → (♯‘𝐶) = (𝑆‘(𝑁 − 1)))
243	229, 242	eqtrd 2795	1 ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘(𝑁 − 1)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 {cab 2738 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ⊆ wss 3896 ∖ cdif 4044 ∩ cin 4088 ∪ cun 4148 ∅c0 4277 {csn 4584 {cpr 4586 ⟨cop 4834 ↦ cmpt 5185 ^◡ccnv 5650 ↾ cres 5653 Fun wfun 6537 Fn wfn 6538 ⟶wf 6539 –1-1→wf1 6540 –onto→wfo 6541 –1-1-onto→wf1o 6542 ‘cfv 6543 (class class class)co 7424 Fincfn 8980 1c1 11208 + caddc 11210 − cmin 11548 ℕcn 12342 2c2 12404 ℕ₀cn0 12613 ℤ_≥cuz 12972 ...cfz 13646 ♯chash 14481

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7882 df-1st 8005 df-2nd 8006 df-frecs 8306 df-wrecs 8337 df-recs 8386 df-rdg 8425 df-1o 8483 df-2o 8484 df-oadd 8487 df-er 8724 df-map 8856 df-pm 8857 df-en 8981 df-dom 8982 df-sdom 8983 df-fin 8984 df-dju 9989 df-card 10027 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-nn 12343 df-2 12412 df-n0 12614 df-xnn0 12687 df-z 12701 df-uz 12973 df-fz 13647 df-hash 14482

This theorem is used by: subfacp1lem6 36040

W3C validator