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 35529

Description: Lemma for subfacp1 35533. In subfacp1lem6 35532 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 13985	. . . . . . . 8 ⊢ (1...(𝑁 + 1)) ∈ Fin
3		deranglem 35513	. . . . . . . 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 2858	. . . . . 6 ⊢ 𝐴 ∈ Fin
6		subfacp1lem3.b	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1)}
7	6	ssrab3 4035	. . . . . 6 ⊢ 𝐵 ⊆ 𝐴
8		ssfi 9141	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
9	5, 7, 8	mp2an 702	. . . . 5 ⊢ 𝐵 ∈ Fin
10	9	elexi 3476	. . . 4 ⊢ 𝐵 ∈ V
11	10	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
12		eqid 2762	. . . 4 ⊢ (𝑏 ∈ 𝐵 ↦ (𝑏 ↾ 𝐾)) = (𝑏 ∈ 𝐵 ↦ (𝑏 ↾ 𝐾))
13		fveq1 6866	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
14	13	eqeq1d 2764	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
15		fveq1 6866	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑀) = (𝑏‘𝑀))
16	15	eqeq1d 2764	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → ((𝑔‘𝑀) = 1 ↔ (𝑏‘𝑀) = 1))
17	14, 16	anbi12d 641	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
18	17, 6	elrab2 3654	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
19	18	bilani 508	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
20	19	simpld 498	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
21		vex 3458	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
22		f1oeq1 6794	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
23		fveq1 6866	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
24	23	neeq1d 3016	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
25	24	ralbidv 3185	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
26	22, 25	anbi12d 641	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)))
27	21, 26, 1	elab2 3641	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
28	20, 27	sylib 220	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
29	28	simpld 498	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
30		f1of1 6805	. . . . . . . 8 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
31		df-f1 6526	. . . . . . . . 9 ⊢ (𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun ^◡𝑏))
32	31	simprbi 501	. . . . . . . 8 ⊢ (𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun ^◡𝑏)
33	29, 30, 32	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → Fun ^◡𝑏)
34		f1ofn 6807	. . . . . . . . . . 11 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏 Fn (1...(𝑁 + 1)))
35	29, 34	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 Fn (1...(𝑁 + 1)))
36		fnresdm 6640	. . . . . . . . . 10 ⊢ (𝑏 Fn (1...(𝑁 + 1)) → (𝑏 ↾ (1...(𝑁 + 1))) = 𝑏)
37		f1oeq1 6794	. . . . . . . . . 10 ⊢ ((𝑏 ↾ (1...(𝑁 + 1))) = 𝑏 → ((𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
38	35, 36, 37	3syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
39	29, 38	mpbird 259	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
40		f1ofo 6814	. . . . . . . 8 ⊢ ((𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
41	39, 40	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)))
42		ssun2 4131	. . . . . . . . . . . 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 35526	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (♯‘𝐾) = (𝑁 − 1)))
50	49	simp2d 1156	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
51	42, 50	sseqtrid 3978	. . . . . . . . . . 11 ⊢ (𝜑 → {1, 𝑀} ⊆ (1...(𝑁 + 1)))
52	51	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {1, 𝑀} ⊆ (1...(𝑁 + 1)))
53	35, 52	fnssresd 6645	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}) Fn {1, 𝑀})
54	19	simprd 499	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1))
55	54	simpld 498	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) = 𝑀)
56	47	prid2 4722	. . . . . . . . . . . 12 ⊢ 𝑀 ∈ {1, 𝑀}
57	55, 56	eqeltrdi 2870	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) ∈ {1, 𝑀})
58	54	simprd 499	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) = 1)
59		1ex 11176	. . . . . . . . . . . . 13 ⊢ 1 ∈ V
60	59	prid1 4721	. . . . . . . . . . . 12 ⊢ 1 ∈ {1, 𝑀}
61	58, 60	eqeltrdi 2870	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ∈ {1, 𝑀})
62		fveq2 6867	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑏‘𝑥) = (𝑏‘1))
63	62	eleq1d 2847	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((𝑏‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘1) ∈ {1, 𝑀}))
64		fveq2 6867	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑀 → (𝑏‘𝑥) = (𝑏‘𝑀))
65	64	eleq1d 2847	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → ((𝑏‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘𝑀) ∈ {1, 𝑀}))
66	59, 47, 63, 65	ralpr 4659	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀} ↔ ((𝑏‘1) ∈ {1, 𝑀} ∧ (𝑏‘𝑀) ∈ {1, 𝑀}))
67	57, 61, 66	sylanbrc 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀})
68		fvres 6886	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {1, 𝑀} → ((𝑏 ↾ {1, 𝑀})‘𝑥) = (𝑏‘𝑥))
69	68	eleq1d 2847	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {1, 𝑀} → (((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘𝑥) ∈ {1, 𝑀}))
70	69	ralbiia 3106	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀} ↔ ∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀})
71	67, 70	sylibr 236	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀})
72		ffnfv 7100	. . . . . . . . 9 ⊢ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀} ↔ ((𝑏 ↾ {1, 𝑀}) Fn {1, 𝑀} ∧ ∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀}))
73	53, 71, 72	sylanbrc 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀})
74		fveqeq2 6876	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) = 1 ↔ (𝑏‘𝑀) = 1))
75	74	rspcev 3581	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ {1, 𝑀} ∧ (𝑏‘𝑀) = 1) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1)
76	56, 58, 75	sylancr 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1)
77		fveqeq2 6876	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → ((𝑏‘𝑦) = 𝑀 ↔ (𝑏‘1) = 𝑀))
78	77	rspcev 3581	. . . . . . . . . . 11 ⊢ ((1 ∈ {1, 𝑀} ∧ (𝑏‘1) = 𝑀) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀)
79	60, 55, 78	sylancr 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀)
80		eqeq2 2774	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((𝑏‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 1))
81	80	rexbidv 3186	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1))
82		eqeq2 2774	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → ((𝑏‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 𝑀))
83	82	rexbidv 3186	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑀 → (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀))
84	59, 47, 81, 83	ralpr 4659	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1 ∧ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀))
85	76, 79, 84	sylanbrc 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥)
86		eqcom 2769	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ ((𝑏 ↾ {1, 𝑀})‘𝑦) = 𝑥)
87		fvres 6886	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {1, 𝑀} → ((𝑏 ↾ {1, 𝑀})‘𝑦) = (𝑏‘𝑦))
88	87	eqeq1d 2764	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {1, 𝑀} → (((𝑏 ↾ {1, 𝑀})‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 𝑥))
89	86, 88	bitrid 285	. . . . . . . . . . 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 236	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦))
93		dffo3 7083	. . . . . . . 8 ⊢ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}–onto→{1, 𝑀} ↔ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀} ∧ ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦)))
94	73, 92, 93	sylanbrc 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}):{1, 𝑀}–onto→{1, 𝑀})
95		resdif 6828	. . . . . . 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 1390	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}))
97		uncom 4111	. . . . . . . . . 10 ⊢ ({1, 𝑀} ∪ 𝐾) = (𝐾 ∪ {1, 𝑀})
98	97, 50	eqtrid 2809	. . . . . . . . 9 ⊢ (𝜑 → ({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)))
99		incom 4161	. . . . . . . . . . 11 ⊢ ({1, 𝑀} ∩ 𝐾) = (𝐾 ∩ {1, 𝑀})
100	49	simp1d 1155	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 ∩ {1, 𝑀}) = ∅)
101	99, 100	eqtrid 2809	. . . . . . . . . 10 ⊢ (𝜑 → ({1, 𝑀} ∩ 𝐾) = ∅)
102		uneqdifeq 4446	. . . . . . . . . 10 ⊢ (({1, 𝑀} ⊆ (1...(𝑁 + 1)) ∧ ({1, 𝑀} ∩ 𝐾) = ∅) → (({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾))
103	51, 101, 102	syl2anc 593	. . . . . . . . 9 ⊢ (𝜑 → (({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾))
104	98, 103	mpbid 234	. . . . . . . 8 ⊢ (𝜑 → ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾)
105	104	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾)
106		reseq2 5960	. . . . . . . . 9 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → (𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})) = (𝑏 ↾ 𝐾))
107	106	f1oeq1d 6801	. . . . . . . 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 6795	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ 𝐾):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀})))
109		f1oeq3 6796	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ 𝐾):𝐾–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
110	107, 108, 109	3bitrd 307	. . . . . . 7 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
111	105, 110	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
112	96, 111	mpbid 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾)
113		ssun1 4130	. . . . . . . 8 ⊢ 𝐾 ⊆ (𝐾 ∪ {1, 𝑀})
114	113, 50	sseqtrid 3978	. . . . . . 7 ⊢ (𝜑 → 𝐾 ⊆ (1...(𝑁 + 1)))
115	114	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐾 ⊆ (1...(𝑁 + 1)))
116	28	simprd 499	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)
117		ssralv 4005	. . . . . 6 ⊢ (𝐾 ⊆ (1...(𝑁 + 1)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦 → ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
118	115, 116, 117	sylc 65	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦)
119	21	resex 6015	. . . . . 6 ⊢ (𝑏 ↾ 𝐾) ∈ V
120		f1oeq1 6794	. . . . . . 7 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (𝑓:𝐾–1-1-onto→𝐾 ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
121		fveq1 6866	. . . . . . . . . 10 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (𝑓‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦))
122		fvres 6886	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐾 → ((𝑏 ↾ 𝐾)‘𝑦) = (𝑏‘𝑦))
123	121, 122	sylan9eq 2817	. . . . . . . . 9 ⊢ ((𝑓 = (𝑏 ↾ 𝐾) ∧ 𝑦 ∈ 𝐾) → (𝑓‘𝑦) = (𝑏‘𝑦))
124	123	neeq1d 3016	. . . . . . . 8 ⊢ ((𝑓 = (𝑏 ↾ 𝐾) ∧ 𝑦 ∈ 𝐾) → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
125	124	ralbidva 3183	. . . . . . 7 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
126	120, 125	anbi12d 641	. . . . . 6 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → ((𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦) ↔ ((𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦)))
127		subfacp1lem3.c	. . . . . 6 ⊢ 𝐶 = {𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}
128	119, 126, 127	elab2 3641	. . . . 5 ⊢ ((𝑏 ↾ 𝐾) ∈ 𝐶 ↔ ((𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
129	112, 118, 128	sylanbrc 592	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ 𝐾) ∈ 𝐶)
130	45	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑁 ∈ ℕ)
131	46	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
132		eqid 2762	. . . . . . . 8 ⊢ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})
133		vex 3458	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
134		f1oeq1 6794	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → (𝑓:𝐾–1-1-onto→𝐾 ↔ 𝑐:𝐾–1-1-onto→𝐾))
135		fveq1 6866	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → (𝑓‘𝑦) = (𝑐‘𝑦))
136	135	neeq1d 3016	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑦) ≠ 𝑦))
137	136	ralbidv 3185	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → (∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
138	134, 137	anbi12d 641	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑐 → ((𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦) ↔ (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦)))
139	133, 138, 127	elab2 3641	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
140	139	bilani 508	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
141	140	simpld 498	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:𝐾–1-1-onto→𝐾)
142	43, 44, 1, 130, 131, 47, 48, 132, 141	subfacp1lem2a 35527	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
143	142	simp1d 1155	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
144	43, 44, 1, 130, 131, 47, 48, 132, 141	subfacp1lem2b 35528	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = (𝑐‘𝑦))
145	140	simprd 499	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦)
146	145	r19.21bi 3254	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → (𝑐‘𝑦) ≠ 𝑦)
147	144, 146	eqnetrd 3024	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
148	147	ralrimiva 3154	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ 𝐾 ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
149	142	simp2d 1156	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀)
150		elfzuz 13525	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (2...(𝑁 + 1)) → 𝑀 ∈ (ℤ_≥‘2))
151		eluz2b3 12923	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (ℤ_≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
152	151	simprbi 501	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ≠ 1)
153	46, 150, 152	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≠ 1)
154	153	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ 1)
155	149, 154	eqnetrd 3024	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1)
156	142	simp3d 1157	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)
157	154	necomd 3012	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 1 ≠ 𝑀)
158	156, 157	eqnetrd 3024	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀)
159		fveq2 6867	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
160		id 22	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → 𝑦 = 1)
161	159, 160	neeq12d 3018	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1))
162		fveq2 6867	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
163		id 22	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
164	162, 163	neeq12d 3018	. . . . . . . . . 10 ⊢ (𝑦 = 𝑀 → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀))
165	59, 47, 161, 164	ralpr 4659	. . . . . . . . 9 ⊢ (∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀))
166	155, 158, 165	sylanbrc 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
167		ralunb 4149	. . . . . . . 8 ⊢ (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ (∀𝑦 ∈ 𝐾 ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ∧ ∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
168	148, 166, 167	sylanbrc 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
169	50	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
170	168, 169	raleqtrdv 3322	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
171		prex 5395	. . . . . . . 8 ⊢ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
172	133, 171	unex 7727	. . . . . . 7 ⊢ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
173		f1oeq1 6794	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
174		fveq1 6866	. . . . . . . . . 10 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑓‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))
175	174	neeq1d 3016	. . . . . . . . 9 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
176	175	ralbidv 3185	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
177	173, 176	anbi12d 641	. . . . . . 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 3641	. . . . . 6 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
179	143, 170, 178	sylanbrc 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴)
180	149, 156	jca 519	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
181		fveq1 6866	. . . . . . . 8 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑔‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
182	181	eqeq1d 2764	. . . . . . 7 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑔‘1) = 𝑀 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀))
183		fveq1 6866	. . . . . . . 8 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑔‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
184	183	eqeq1d 2764	. . . . . . 7 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑔‘𝑀) = 1 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
185	182, 184	anbi12d 641	. . . . . 6 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1) ↔ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)))
186	185, 6	elrab2 3654	. . . . 5 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐵 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴 ∧ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)))
187	179, 180, 186	sylanbrc 592	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐵)
188	55	adantrr 727	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘1) = 𝑀)
189	149	adantrl 726	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀)
190	188, 189	eqtr4d 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
191	58	adantrr 727	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘𝑀) = 1)
192	156	adantrl 726	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)
193	191, 192	eqtr4d 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
194		fveq2 6867	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → (𝑏‘𝑦) = (𝑏‘1))
195	194, 159	eqeq12d 2778	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1)))
196		fveq2 6867	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → (𝑏‘𝑦) = (𝑏‘𝑀))
197	196, 162	eqeq12d 2778	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀)))
198	59, 47, 195, 197	ralpr 4659	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ((𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ∧ (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀)))
199	190, 193, 198	sylanbrc 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))
200	199	biantrud 539	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ∧ ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))))
201		ralunb 4149	. . . . . . . 8 ⊢ (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ∧ ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
202	200, 201	bitr4di 291	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
203	144	eqeq2d 2773	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
204	203	ralbidva 3183	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
205	204	adantrl 726	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
206	50	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
207	206	raleqdv 3320	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
208	202, 205, 207	3bitr3rd 312	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
209	122	eqeq2d 2773	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐾 → ((𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ (𝑐‘𝑦) = (𝑏‘𝑦)))
210		eqcom 2769	. . . . . . . 8 ⊢ ((𝑐‘𝑦) = (𝑏‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦))
211	209, 210	bitrdi 289	. . . . . . 7 ⊢ (𝑦 ∈ 𝐾 → ((𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
212	211	ralbiia 3106	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦))
213	208, 212	bitr4di 291	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
214	35	adantrr 727	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑏 Fn (1...(𝑁 + 1)))
215	143	adantrl 726	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
216		f1ofn 6807	. . . . . . 7 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) Fn (1...(𝑁 + 1)))
217	215, 216	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) Fn (1...(𝑁 + 1)))
218		eqfnfv 7011	. . . . . 6 ⊢ ((𝑏 Fn (1...(𝑁 + 1)) ∧ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) Fn (1...(𝑁 + 1))) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
219	214, 217, 218	syl2anc 593	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
220	141	adantrl 726	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐:𝐾–1-1-onto→𝐾)
221		f1ofn 6807	. . . . . . 7 ⊢ (𝑐:𝐾–1-1-onto→𝐾 → 𝑐 Fn 𝐾)
222	220, 221	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐 Fn 𝐾)
223	114	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐾 ⊆ (1...(𝑁 + 1)))
224	214, 223	fnssresd 6645	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 ↾ 𝐾) Fn 𝐾)
225		eqfnfv 7011	. . . . . 6 ⊢ ((𝑐 Fn 𝐾 ∧ (𝑏 ↾ 𝐾) Fn 𝐾) → (𝑐 = (𝑏 ↾ 𝐾) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
226	222, 224, 225	syl2anc 593	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 = (𝑏 ↾ 𝐾) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
227	213, 219, 226	3bitr4d 313	. . . 4 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ 𝑐 = (𝑏 ↾ 𝐾)))
228	12, 129, 187, 227	f1o2d 7650	. . 3 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ (𝑏 ↾ 𝐾)):𝐵–1-1-onto→𝐶)
229	11, 228	hasheqf1od 14366	. 2 ⊢ (𝜑 → (♯‘𝐵) = (♯‘𝐶))
230	127	fveq2i 6870	. . . 4 ⊢ (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)})
231		fzfi 13985	. . . . . . 7 ⊢ (2...(𝑁 + 1)) ∈ Fin
232		diffi 9143	. . . . . . 7 ⊢ ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ Fin)
233	231, 232	ax-mp 5	. . . . . 6 ⊢ ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ Fin
234	48, 233	eqeltri 2858	. . . . 5 ⊢ 𝐾 ∈ Fin
235	43	derangval 35514	. . . . 5 ⊢ (𝐾 ∈ Fin → (𝐷‘𝐾) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}))
236	234, 235	ax-mp 5	. . . 4 ⊢ (𝐷‘𝐾) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)})
237	43, 44	derangen2 35521	. . . . 5 ⊢ (𝐾 ∈ Fin → (𝐷‘𝐾) = (𝑆‘(♯‘𝐾)))
238	234, 237	ax-mp 5	. . . 4 ⊢ (𝐷‘𝐾) = (𝑆‘(♯‘𝐾))
239	230, 236, 238	3eqtr2ri 2792	. . 3 ⊢ (𝑆‘(♯‘𝐾)) = (♯‘𝐶)
240	49	simp3d 1157	. . . 4 ⊢ (𝜑 → (♯‘𝐾) = (𝑁 − 1))
241	240	fveq2d 6871	. . 3 ⊢ (𝜑 → (𝑆‘(♯‘𝐾)) = (𝑆‘(𝑁 − 1)))
242	239, 241	eqtr3id 2811	. 2 ⊢ (𝜑 → (♯‘𝐶) = (𝑆‘(𝑁 − 1)))
243	229, 242	eqtrd 2797	1 ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘(𝑁 − 1)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1560 ∈ wcel 2142 {cab 2740 ≠ wne 2957 ∀wral 3076 ∃wrex 3086 {crab 3414 Vcvv 3454 ∖ cdif 3901 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 ∅c0 4285 {csn 4582 {cpr 4584 ⟨cop 4588 ↦ cmpt 5181 ^◡ccnv 5646 ↾ cres 5649 Fun wfun 6515 Fn wfn 6516 ⟶wf 6517 –1-1→wf1 6518 –onto→wfo 6519 –1-1-onto→wf1o 6520 ‘cfv 6521 (class class class)co 7396 Fincfn 8927 1c1 11074 + caddc 11076 − cmin 11414 ℕcn 12210 2c2 12272 ℕ₀cn0 12481 ℤ_≥cuz 12839 ...cfz 13512 ♯chash 14343

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-1st 7970 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-er 8678 df-map 8810 df-pm 8811 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-dju 9859 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-nn 12211 df-2 12280 df-n0 12482 df-xnn0 12555 df-z 12569 df-uz 12840 df-fz 13513 df-hash 14344

This theorem is referenced by: subfacp1lem6 35532

W3C validator