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 35410

Description: Lemma for subfacp1 35414. In subfacp1lem6 35413 we cut up the set of all derangements on 1...(𝑁 + 1) first according to the value at 1, and then by whether or not (𝑓‘(𝑓‘1)) = 1. In this lemma, we show that the subset of all 𝑁 + 1 derangements 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 13925	. . . . . . . 8 ⊢ (1...(𝑁 + 1)) ∈ Fin
3		deranglem 35394	. . . . . . . 8 ⊢ ((1...(𝑁 + 1)) ∈ Fin → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
4	2, 3	ax-mp 5	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin
5	1, 4	eqeltri 2835	. . . . . 6 ⊢ 𝐴 ∈ Fin
6		subfacp1lem3.b	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1)}
7	6	ssrab3 4013	. . . . . 6 ⊢ 𝐵 ⊆ 𝐴
8		ssfi 9097	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
9	5, 7, 8	mp2an 698	. . . . 5 ⊢ 𝐵 ∈ Fin
10	9	elexi 3453	. . . 4 ⊢ 𝐵 ∈ V
11	10	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
12		eqid 2739	. . . 4 ⊢ (𝑏 ∈ 𝐵 ↦ (𝑏 ↾ 𝐾)) = (𝑏 ∈ 𝐵 ↦ (𝑏 ↾ 𝐾))
13		fveq1 6826	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (𝑔‘1) = (𝑏‘1))
14	13	eqeq1d 2741	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → ((𝑔‘1) = 𝑀 ↔ (𝑏‘1) = 𝑀))
15		fveq1 6826	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑀) = (𝑏‘𝑀))
16	15	eqeq1d 2741	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → ((𝑔‘𝑀) = 1 ↔ (𝑏‘𝑀) = 1))
17	14, 16	anbi12d 638	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1) ↔ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
18	17, 6	elrab2 3632	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
19	18	bilani 505	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ 𝐴 ∧ ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1)))
20	19	simpld 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
21		vex 3435	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
22		f1oeq1 6755	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
23		fveq1 6826	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
24	23	neeq1d 2993	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
25	24	ralbidv 3162	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
26	22, 25	anbi12d 638	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)))
27	21, 26, 1	elab2 3620	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝐴 ↔ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
28	20, 27	sylib 219	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦))
29	28	simpld 495	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
30		f1of1 6766	. . . . . . . 8 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)))
31		df-f1 6490	. . . . . . . . 9 ⊢ (𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) ↔ (𝑏:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ Fun ^◡𝑏))
32	31	simprbi 498	. . . . . . . 8 ⊢ (𝑏:(1...(𝑁 + 1))–1-1→(1...(𝑁 + 1)) → Fun ^◡𝑏)
33	29, 30, 32	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → Fun ^◡𝑏)
34		f1ofn 6768	. . . . . . . . . . 11 ⊢ (𝑏:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑏 Fn (1...(𝑁 + 1)))
35	29, 34	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 Fn (1...(𝑁 + 1)))
36		fnresdm 6604	. . . . . . . . . 10 ⊢ (𝑏 Fn (1...(𝑁 + 1)) → (𝑏 ↾ (1...(𝑁 + 1))) = 𝑏)
37		f1oeq1 6755	. . . . . . . . . 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 258	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
40		f1ofo 6774	. . . . . . . 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 4108	. . . . . . . . . . . 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 35407	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (♯‘𝐾) = (𝑁 − 1)))
50	49	simp2d 1149	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
51	42, 50	sseqtrid 3957	. . . . . . . . . . 11 ⊢ (𝜑 → {1, 𝑀} ⊆ (1...(𝑁 + 1)))
52	51	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {1, 𝑀} ⊆ (1...(𝑁 + 1)))
53	35, 52	fnssresd 6609	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}) Fn {1, 𝑀})
54	19	simprd 496	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏‘1) = 𝑀 ∧ (𝑏‘𝑀) = 1))
55	54	simpld 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) = 𝑀)
56	47	prid2 4695	. . . . . . . . . . . 12 ⊢ 𝑀 ∈ {1, 𝑀}
57	55, 56	eqeltrdi 2847	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘1) ∈ {1, 𝑀})
58	54	simprd 496	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) = 1)
59		1ex 11131	. . . . . . . . . . . . 13 ⊢ 1 ∈ V
60	59	prid1 4694	. . . . . . . . . . . 12 ⊢ 1 ∈ {1, 𝑀}
61	58, 60	eqeltrdi 2847	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏‘𝑀) ∈ {1, 𝑀})
62		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑏‘𝑥) = (𝑏‘1))
63	62	eleq1d 2824	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((𝑏‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘1) ∈ {1, 𝑀}))
64		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑀 → (𝑏‘𝑥) = (𝑏‘𝑀))
65	64	eleq1d 2824	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → ((𝑏‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘𝑀) ∈ {1, 𝑀}))
66	59, 47, 63, 65	ralpr 4632	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀} ↔ ((𝑏‘1) ∈ {1, 𝑀} ∧ (𝑏‘𝑀) ∈ {1, 𝑀}))
67	57, 61, 66	sylanbrc 589	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀})
68		fvres 6846	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {1, 𝑀} → ((𝑏 ↾ {1, 𝑀})‘𝑥) = (𝑏‘𝑥))
69	68	eleq1d 2824	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {1, 𝑀} → (((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀} ↔ (𝑏‘𝑥) ∈ {1, 𝑀}))
70	69	ralbiia 3083	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀} ↔ ∀𝑥 ∈ {1, 𝑀} (𝑏‘𝑥) ∈ {1, 𝑀})
71	67, 70	sylibr 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀})
72		ffnfv 7060	. . . . . . . . 9 ⊢ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀} ↔ ((𝑏 ↾ {1, 𝑀}) Fn {1, 𝑀} ∧ ∀𝑥 ∈ {1, 𝑀} ((𝑏 ↾ {1, 𝑀})‘𝑥) ∈ {1, 𝑀}))
73	53, 71, 72	sylanbrc 589	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀})
74		fveqeq2 6836	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) = 1 ↔ (𝑏‘𝑀) = 1))
75	74	rspcev 3560	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ {1, 𝑀} ∧ (𝑏‘𝑀) = 1) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1)
76	56, 58, 75	sylancr 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1)
77		fveqeq2 6836	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → ((𝑏‘𝑦) = 𝑀 ↔ (𝑏‘1) = 𝑀))
78	77	rspcev 3560	. . . . . . . . . . 11 ⊢ ((1 ∈ {1, 𝑀} ∧ (𝑏‘1) = 𝑀) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀)
79	60, 55, 78	sylancr 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀)
80		eqeq2 2751	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((𝑏‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 1))
81	80	rexbidv 3163	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1))
82		eqeq2 2751	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → ((𝑏‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 𝑀))
83	82	rexbidv 3163	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑀 → (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀))
84	59, 47, 81, 83	ralpr 4632	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥 ↔ (∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 1 ∧ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑀))
85	76, 79, 84	sylanbrc 589	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥)
86		eqcom 2746	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ ((𝑏 ↾ {1, 𝑀})‘𝑦) = 𝑥)
87		fvres 6846	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {1, 𝑀} → ((𝑏 ↾ {1, 𝑀})‘𝑦) = (𝑏‘𝑦))
88	87	eqeq1d 2741	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {1, 𝑀} → (((𝑏 ↾ {1, 𝑀})‘𝑦) = 𝑥 ↔ (𝑏‘𝑦) = 𝑥))
89	86, 88	bitrid 284	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {1, 𝑀} → (𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ (𝑏‘𝑦) = 𝑥))
90	89	rexbiia 3084	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ ∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥)
91	90	ralbii 3085	. . . . . . . . 9 ⊢ (∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦) ↔ ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = 𝑥)
92	85, 91	sylibr 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦))
93		dffo3 7043	. . . . . . . 8 ⊢ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}–onto→{1, 𝑀} ↔ ((𝑏 ↾ {1, 𝑀}):{1, 𝑀}⟶{1, 𝑀} ∧ ∀𝑥 ∈ {1, 𝑀}∃𝑦 ∈ {1, 𝑀}𝑥 = ((𝑏 ↾ {1, 𝑀})‘𝑦)))
94	73, 92, 93	sylanbrc 589	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ {1, 𝑀}):{1, 𝑀}–onto→{1, 𝑀})
95		resdif 6788	. . . . . . 7 ⊢ ((Fun ^◡𝑏 ∧ (𝑏 ↾ (1...(𝑁 + 1))):(1...(𝑁 + 1))–onto→(1...(𝑁 + 1)) ∧ (𝑏 ↾ {1, 𝑀}):{1, 𝑀}–onto→{1, 𝑀}) → (𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}))
96	33, 41, 94, 95	syl3anc 1379	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}))
97		uncom 4088	. . . . . . . . . 10 ⊢ ({1, 𝑀} ∪ 𝐾) = (𝐾 ∪ {1, 𝑀})
98	97, 50	eqtrid 2786	. . . . . . . . 9 ⊢ (𝜑 → ({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)))
99		incom 4138	. . . . . . . . . . 11 ⊢ ({1, 𝑀} ∩ 𝐾) = (𝐾 ∩ {1, 𝑀})
100	49	simp1d 1148	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 ∩ {1, 𝑀}) = ∅)
101	99, 100	eqtrid 2786	. . . . . . . . . 10 ⊢ (𝜑 → ({1, 𝑀} ∩ 𝐾) = ∅)
102		uneqdifeq 4420	. . . . . . . . . 10 ⊢ (({1, 𝑀} ⊆ (1...(𝑁 + 1)) ∧ ({1, 𝑀} ∩ 𝐾) = ∅) → (({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾))
103	51, 101, 102	syl2anc 590	. . . . . . . . 9 ⊢ (𝜑 → (({1, 𝑀} ∪ 𝐾) = (1...(𝑁 + 1)) ↔ ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾))
104	98, 103	mpbid 233	. . . . . . . 8 ⊢ (𝜑 → ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾)
105	104	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾)
106		reseq2 5926	. . . . . . . . 9 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → (𝑏 ↾ ((1...(𝑁 + 1)) ∖ {1, 𝑀})) = (𝑏 ↾ 𝐾))
107	106	f1oeq1d 6762	. . . . . . . 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 6756	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ 𝐾):((1...(𝑁 + 1)) ∖ {1, 𝑀})–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀})))
109		f1oeq3 6757	. . . . . . . 8 ⊢ (((1...(𝑁 + 1)) ∖ {1, 𝑀}) = 𝐾 → ((𝑏 ↾ 𝐾):𝐾–1-1-onto→((1...(𝑁 + 1)) ∖ {1, 𝑀}) ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
110	107, 108, 109	3bitrd 306	. . . . . . 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 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾)
113		ssun1 4107	. . . . . . . 8 ⊢ 𝐾 ⊆ (𝐾 ∪ {1, 𝑀})
114	113, 50	sseqtrid 3957	. . . . . . 7 ⊢ (𝜑 → 𝐾 ⊆ (1...(𝑁 + 1)))
115	114	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐾 ⊆ (1...(𝑁 + 1)))
116	28	simprd 496	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦)
117		ssralv 3983	. . . . . 6 ⊢ (𝐾 ⊆ (1...(𝑁 + 1)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) ≠ 𝑦 → ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
118	115, 116, 117	sylc 65	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦)
119	21	resex 5981	. . . . . 6 ⊢ (𝑏 ↾ 𝐾) ∈ V
120		f1oeq1 6755	. . . . . . 7 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (𝑓:𝐾–1-1-onto→𝐾 ↔ (𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾))
121		fveq1 6826	. . . . . . . . . 10 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (𝑓‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦))
122		fvres 6846	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐾 → ((𝑏 ↾ 𝐾)‘𝑦) = (𝑏‘𝑦))
123	121, 122	sylan9eq 2794	. . . . . . . . 9 ⊢ ((𝑓 = (𝑏 ↾ 𝐾) ∧ 𝑦 ∈ 𝐾) → (𝑓‘𝑦) = (𝑏‘𝑦))
124	123	neeq1d 2993	. . . . . . . 8 ⊢ ((𝑓 = (𝑏 ↾ 𝐾) ∧ 𝑦 ∈ 𝐾) → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑏‘𝑦) ≠ 𝑦))
125	124	ralbidva 3160	. . . . . . 7 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → (∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
126	120, 125	anbi12d 638	. . . . . 6 ⊢ (𝑓 = (𝑏 ↾ 𝐾) → ((𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦) ↔ ((𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦)))
127		subfacp1lem3.c	. . . . . 6 ⊢ 𝐶 = {𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}
128	119, 126, 127	elab2 3620	. . . . 5 ⊢ ((𝑏 ↾ 𝐾) ∈ 𝐶 ↔ ((𝑏 ↾ 𝐾):𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) ≠ 𝑦))
129	112, 118, 128	sylanbrc 589	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ 𝐾) ∈ 𝐶)
130	45	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑁 ∈ ℕ)
131	46	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ∈ (2...(𝑁 + 1)))
132		eqid 2739	. . . . . . . 8 ⊢ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})
133		vex 3435	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
134		f1oeq1 6755	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → (𝑓:𝐾–1-1-onto→𝐾 ↔ 𝑐:𝐾–1-1-onto→𝐾))
135		fveq1 6826	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → (𝑓‘𝑦) = (𝑐‘𝑦))
136	135	neeq1d 2993	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑐‘𝑦) ≠ 𝑦))
137	136	ralbidv 3162	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → (∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
138	134, 137	anbi12d 638	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑐 → ((𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦) ↔ (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦)))
139	133, 138, 127	elab2 3620	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐶 ↔ (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
140	139	bilani 505	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦))
141	140	simpld 495	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐:𝐾–1-1-onto→𝐾)
142	43, 44, 1, 130, 131, 47, 48, 132, 141	subfacp1lem2a 35408	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
143	142	simp1d 1148	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
144	43, 44, 1, 130, 131, 47, 48, 132, 141	subfacp1lem2b 35409	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = (𝑐‘𝑦))
145	140	simprd 496	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) ≠ 𝑦)
146	145	r19.21bi 3231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → (𝑐‘𝑦) ≠ 𝑦)
147	144, 146	eqnetrd 3001	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
148	147	ralrimiva 3131	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ 𝐾 ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
149	142	simp2d 1149	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀)
150		elfzuz 13465	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (2...(𝑁 + 1)) → 𝑀 ∈ (ℤ_≥‘2))
151		eluz2b3 12863	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (ℤ_≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
152	151	simprbi 498	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ≠ 1)
153	46, 150, 152	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≠ 1)
154	153	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑀 ≠ 1)
155	149, 154	eqnetrd 3001	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1)
156	142	simp3d 1150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)
157	154	necomd 2989	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 1 ≠ 𝑀)
158	156, 157	eqnetrd 3001	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀)
159		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
160		id 22	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → 𝑦 = 1)
161	159, 160	neeq12d 2995	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1))
162		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
163		id 22	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
164	162, 163	neeq12d 2995	. . . . . . . . . 10 ⊢ (𝑦 = 𝑀 → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀))
165	59, 47, 161, 164	ralpr 4632	. . . . . . . . 9 ⊢ (∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ≠ 1 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) ≠ 𝑀))
166	155, 158, 165	sylanbrc 589	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
167		ralunb 4126	. . . . . . . 8 ⊢ (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ↔ (∀𝑦 ∈ 𝐾 ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦 ∧ ∀𝑦 ∈ {1, 𝑀} ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
168	148, 166, 167	sylanbrc 589	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
169	50	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
170	168, 169	raleqtrdv 3299	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)
171		prex 5367	. . . . . . . 8 ⊢ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩} ∈ V
172	133, 171	unex 7687	. . . . . . 7 ⊢ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ V
173		f1oeq1 6755	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ↔ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))))
174		fveq1 6826	. . . . . . . . . 10 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑓‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))
175	174	neeq1d 2993	. . . . . . . . 9 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑓‘𝑦) ≠ 𝑦 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
176	175	ralbidv 3162	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
177	173, 176	anbi12d 638	. . . . . . 7 ⊢ (𝑓 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦) ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦)))
178	172, 177, 1	elab2 3620	. . . . . 6 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ≠ 𝑦))
179	143, 170, 178	sylanbrc 589	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴)
180	149, 156	jca 516	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
181		fveq1 6826	. . . . . . . 8 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑔‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
182	181	eqeq1d 2741	. . . . . . 7 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑔‘1) = 𝑀 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀))
183		fveq1 6826	. . . . . . . 8 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (𝑔‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
184	183	eqeq1d 2741	. . . . . . 7 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → ((𝑔‘𝑀) = 1 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1))
185	182, 184	anbi12d 638	. . . . . 6 ⊢ (𝑔 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) → (((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1) ↔ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)))
186	185, 6	elrab2 3632	. . . . 5 ⊢ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐵 ↔ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐴 ∧ (((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀 ∧ ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)))
187	179, 180, 186	sylanbrc 589	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ∈ 𝐵)
188	55	adantrr 723	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘1) = 𝑀)
189	149	adantrl 722	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) = 𝑀)
190	188, 189	eqtr4d 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1))
191	58	adantrr 723	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘𝑀) = 1)
192	156	adantrl 722	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀) = 1)
193	191, 192	eqtr4d 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀))
194		fveq2 6827	. . . . . . . . . . . 12 ⊢ (𝑦 = 1 → (𝑏‘𝑦) = (𝑏‘1))
195	194, 159	eqeq12d 2755	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1)))
196		fveq2 6827	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑀 → (𝑏‘𝑦) = (𝑏‘𝑀))
197	196, 162	eqeq12d 2755	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑀 → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀)))
198	59, 47, 195, 197	ralpr 4632	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ((𝑏‘1) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘1) ∧ (𝑏‘𝑀) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑀)))
199	190, 193, 198	sylanbrc 589	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))
200	199	biantrud 536	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ∧ ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦))))
201		ralunb 4126	. . . . . . . 8 ⊢ (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ∧ ∀𝑦 ∈ {1, 𝑀} (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
202	200, 201	bitr4di 290	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
203	144	eqeq2d 2750	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐶) ∧ 𝑦 ∈ 𝐾) → ((𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
204	203	ralbidva 3160	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
205	204	adantrl 722	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
206	50	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
207	206	raleqdv 3297	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (𝐾 ∪ {1, 𝑀})(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
208	202, 205, 207	3bitr3rd 311	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦)))
209	122	eqeq2d 2750	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐾 → ((𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ (𝑐‘𝑦) = (𝑏‘𝑦)))
210		eqcom 2746	. . . . . . . 8 ⊢ ((𝑐‘𝑦) = (𝑏‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦))
211	209, 210	bitrdi 288	. . . . . . 7 ⊢ (𝑦 ∈ 𝐾 → ((𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
212	211	ralbiia 3083	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑏‘𝑦) = (𝑐‘𝑦))
213	208, 212	bitr4di 290	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
214	35	adantrr 723	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑏 Fn (1...(𝑁 + 1)))
215	143	adantrl 722	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
216		f1ofn 6768	. . . . . . 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 6971	. . . . . 6 ⊢ ((𝑏 Fn (1...(𝑁 + 1)) ∧ (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) Fn (1...(𝑁 + 1))) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
219	214, 217, 218	syl2anc 590	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑏‘𝑦) = ((𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})‘𝑦)))
220	141	adantrl 722	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐:𝐾–1-1-onto→𝐾)
221		f1ofn 6768	. . . . . . 7 ⊢ (𝑐:𝐾–1-1-onto→𝐾 → 𝑐 Fn 𝐾)
222	220, 221	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝑐 Fn 𝐾)
223	114	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → 𝐾 ⊆ (1...(𝑁 + 1)))
224	214, 223	fnssresd 6609	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 ↾ 𝐾) Fn 𝐾)
225		eqfnfv 6971	. . . . . 6 ⊢ ((𝑐 Fn 𝐾 ∧ (𝑏 ↾ 𝐾) Fn 𝐾) → (𝑐 = (𝑏 ↾ 𝐾) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
226	222, 224, 225	syl2anc 590	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑐 = (𝑏 ↾ 𝐾) ↔ ∀𝑦 ∈ 𝐾 (𝑐‘𝑦) = ((𝑏 ↾ 𝐾)‘𝑦)))
227	213, 219, 226	3bitr4d 312	. . . 4 ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (𝑏 = (𝑐 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) ↔ 𝑐 = (𝑏 ↾ 𝐾)))
228	12, 129, 187, 227	f1o2d 7610	. . 3 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ (𝑏 ↾ 𝐾)):𝐵–1-1-onto→𝐶)
229	11, 228	hasheqf1od 14306	. 2 ⊢ (𝜑 → (♯‘𝐵) = (♯‘𝐶))
230	127	fveq2i 6830	. . . 4 ⊢ (♯‘𝐶) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)})
231		fzfi 13925	. . . . . . 7 ⊢ (2...(𝑁 + 1)) ∈ Fin
232		diffi 9099	. . . . . . 7 ⊢ ((2...(𝑁 + 1)) ∈ Fin → ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ Fin)
233	231, 232	ax-mp 5	. . . . . 6 ⊢ ((2...(𝑁 + 1)) ∖ {𝑀}) ∈ Fin
234	48, 233	eqeltri 2835	. . . . 5 ⊢ 𝐾 ∈ Fin
235	43	derangval 35395	. . . . 5 ⊢ (𝐾 ∈ Fin → (𝐷‘𝐾) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}))
236	234, 235	ax-mp 5	. . . 4 ⊢ (𝐷‘𝐾) = (♯‘{𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)})
237	43, 44	derangen2 35402	. . . . 5 ⊢ (𝐾 ∈ Fin → (𝐷‘𝐾) = (𝑆‘(♯‘𝐾)))
238	234, 237	ax-mp 5	. . . 4 ⊢ (𝐷‘𝐾) = (𝑆‘(♯‘𝐾))
239	230, 236, 238	3eqtr2ri 2769	. . 3 ⊢ (𝑆‘(♯‘𝐾)) = (♯‘𝐶)
240	49	simp3d 1150	. . . 4 ⊢ (𝜑 → (♯‘𝐾) = (𝑁 − 1))
241	240	fveq2d 6831	. . 3 ⊢ (𝜑 → (𝑆‘(♯‘𝐾)) = (𝑆‘(𝑁 − 1)))
242	239, 241	eqtr3id 2788	. 2 ⊢ (𝜑 → (♯‘𝐶) = (𝑆‘(𝑁 − 1)))
243	229, 242	eqtrd 2774	1 ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘(𝑁 − 1)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1547 ∈ wcel 2119 {cab 2717 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 {crab 3391 Vcvv 3431 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4261 {csn 4555 {cpr 4557 ⟨cop 4561 ↦ cmpt 5153 ^◡ccnv 5617 ↾ cres 5620 Fun wfun 6479 Fn wfn 6480 ⟶wf 6481 –1-1→wf1 6482 –onto→wfo 6483 –1-1-onto→wf1o 6484 ‘cfv 6485 (class class class)co 7356 Fincfn 8883 1c1 11030 + caddc 11032 − cmin 11368 ℕcn 12165 2c2 12227 ℕ₀cn0 12428 ℤ_≥cuz 12779 ...cfz 13452 ♯chash 14283

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

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

This theorem is referenced by: subfacp1lem6 35413

W3C validator