Theorem subfacp1lem1

Description: Lemma for subfacp1 . The set K together with { 1 , M } partitions the set 1 ... ( N + 1 ) . (Contributed by Mario Carneiro, 23-Jan-2015)

	Ref	Expression
Hypotheses	derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
	subfac.n	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 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 ) ) ∖ { 𝑀 } )
Assertion	subfacp1lem1	⊢ ( 𝜑 → ( ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ ∧ ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) ∧ ( ♯ ‘ 𝐾 ) = ( 𝑁 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2		subfac.n	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3		subfacp1lem.a	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) }
4		subfacp1lem1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		subfacp1lem1.m	⊢ ( 𝜑 → 𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
6		subfacp1lem1.x	⊢ 𝑀 ∈ V
7		subfacp1lem1.k	⊢ 𝐾 = ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } )
8		disj	⊢ ( ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ ↔ ∀ 𝑥 ∈ 𝐾 ¬ 𝑥 ∈ { 1 , 𝑀 } )
9		eldifi	⊢ ( 𝑥 ∈ ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) → 𝑥 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
10		elfzle1	⊢ ( 𝑥 ∈ ( 2 ... ( 𝑁 + 1 ) ) → 2 ≤ 𝑥 )
11		1lt2	⊢ 1 < 2
12		1re	⊢ 1 ∈ ℝ
13		2re	⊢ 2 ∈ ℝ
14	12 13	ltnlei	⊢ ( 1 < 2 ↔ ¬ 2 ≤ 1 )
15	11 14	mpbi	⊢ ¬ 2 ≤ 1
16		breq2	⊢ ( 𝑥 = 1 → ( 2 ≤ 𝑥 ↔ 2 ≤ 1 ) )
17	15 16	mtbiri	⊢ ( 𝑥 = 1 → ¬ 2 ≤ 𝑥 )
18	17	necon2ai	⊢ ( 2 ≤ 𝑥 → 𝑥 ≠ 1 )
19	9 10 18	3syl	⊢ ( 𝑥 ∈ ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) → 𝑥 ≠ 1 )
20		eldifsni	⊢ ( 𝑥 ∈ ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) → 𝑥 ≠ 𝑀 )
21	19 20	jca	⊢ ( 𝑥 ∈ ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) → ( 𝑥 ≠ 1 ∧ 𝑥 ≠ 𝑀 ) )
22	21 7	eleq2s	⊢ ( 𝑥 ∈ 𝐾 → ( 𝑥 ≠ 1 ∧ 𝑥 ≠ 𝑀 ) )
23		neanior	⊢ ( ( 𝑥 ≠ 1 ∧ 𝑥 ≠ 𝑀 ) ↔ ¬ ( 𝑥 = 1 ∨ 𝑥 = 𝑀 ) )
24	22 23	sylib	⊢ ( 𝑥 ∈ 𝐾 → ¬ ( 𝑥 = 1 ∨ 𝑥 = 𝑀 ) )
25		vex	⊢ 𝑥 ∈ V
26	25	elpr	⊢ ( 𝑥 ∈ { 1 , 𝑀 } ↔ ( 𝑥 = 1 ∨ 𝑥 = 𝑀 ) )
27	24 26	sylnibr	⊢ ( 𝑥 ∈ 𝐾 → ¬ 𝑥 ∈ { 1 , 𝑀 } )
28	8 27	mprgbir	⊢ ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅
29	28	a1i	⊢ ( 𝜑 → ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ )
30		uncom	⊢ ( { 1 } ∪ ( 𝐾 ∪ { 𝑀 } ) ) = ( ( 𝐾 ∪ { 𝑀 } ) ∪ { 1 } )
31		1z	⊢ 1 ∈ ℤ
32		fzsn	⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
33	31 32	ax-mp	⊢ ( 1 ... 1 ) = { 1 }
34	7	uneq1i	⊢ ( 𝐾 ∪ { 𝑀 } ) = ( ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∪ { 𝑀 } )
35		undif1	⊢ ( ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∪ { 𝑀 } ) = ( ( 2 ... ( 𝑁 + 1 ) ) ∪ { 𝑀 } )
36	34 35	eqtr2i	⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∪ { 𝑀 } ) = ( 𝐾 ∪ { 𝑀 } )
37	33 36	uneq12i	⊢ ( ( 1 ... 1 ) ∪ ( ( 2 ... ( 𝑁 + 1 ) ) ∪ { 𝑀 } ) ) = ( { 1 } ∪ ( 𝐾 ∪ { 𝑀 } ) )
38		df-pr	⊢ { 1 , 𝑀 } = ( { 1 } ∪ { 𝑀 } )
39	38	equncomi	⊢ { 1 , 𝑀 } = ( { 𝑀 } ∪ { 1 } )
40	39	uneq2i	⊢ ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 𝐾 ∪ ( { 𝑀 } ∪ { 1 } ) )
41		unass	⊢ ( ( 𝐾 ∪ { 𝑀 } ) ∪ { 1 } ) = ( 𝐾 ∪ ( { 𝑀 } ∪ { 1 } ) )
42	40 41	eqtr4i	⊢ ( 𝐾 ∪ { 1 , 𝑀 } ) = ( ( 𝐾 ∪ { 𝑀 } ) ∪ { 1 } )
43	30 37 42	3eqtr4i	⊢ ( ( 1 ... 1 ) ∪ ( ( 2 ... ( 𝑁 + 1 ) ) ∪ { 𝑀 } ) ) = ( 𝐾 ∪ { 1 , 𝑀 } )
44	5	snssd	⊢ ( 𝜑 → { 𝑀 } ⊆ ( 2 ... ( 𝑁 + 1 ) ) )
45		ssequn2	⊢ ( { 𝑀 } ⊆ ( 2 ... ( 𝑁 + 1 ) ) ↔ ( ( 2 ... ( 𝑁 + 1 ) ) ∪ { 𝑀 } ) = ( 2 ... ( 𝑁 + 1 ) ) )
46	44 45	sylib	⊢ ( 𝜑 → ( ( 2 ... ( 𝑁 + 1 ) ) ∪ { 𝑀 } ) = ( 2 ... ( 𝑁 + 1 ) ) )
47		df-2	⊢ 2 = ( 1 + 1 )
48	47	oveq1i	⊢ ( 2 ... ( 𝑁 + 1 ) ) = ( ( 1 + 1 ) ... ( 𝑁 + 1 ) )
49	46 48	eqtrdi	⊢ ( 𝜑 → ( ( 2 ... ( 𝑁 + 1 ) ) ∪ { 𝑀 } ) = ( ( 1 + 1 ) ... ( 𝑁 + 1 ) ) )
50	49	uneq2d	⊢ ( 𝜑 → ( ( 1 ... 1 ) ∪ ( ( 2 ... ( 𝑁 + 1 ) ) ∪ { 𝑀 } ) ) = ( ( 1 ... 1 ) ∪ ( ( 1 + 1 ) ... ( 𝑁 + 1 ) ) ) )
51	4	peano2nnd	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
52		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
53	51 52	eleqtrdi	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
54		eluzfz1	⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
55		fzsplit	⊢ ( 1 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( 1 ... ( 𝑁 + 1 ) ) = ( ( 1 ... 1 ) ∪ ( ( 1 + 1 ) ... ( 𝑁 + 1 ) ) ) )
56	53 54 55	3syl	⊢ ( 𝜑 → ( 1 ... ( 𝑁 + 1 ) ) = ( ( 1 ... 1 ) ∪ ( ( 1 + 1 ) ... ( 𝑁 + 1 ) ) ) )
57	50 56	eqtr4d	⊢ ( 𝜑 → ( ( 1 ... 1 ) ∪ ( ( 2 ... ( 𝑁 + 1 ) ) ∪ { 𝑀 } ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
58	43 57	eqtr3id	⊢ ( 𝜑 → ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) )
59	47	oveq2i	⊢ ( ( 𝑁 + 1 ) − 2 ) = ( ( 𝑁 + 1 ) − ( 1 + 1 ) )
60		fzfi	⊢ ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin
61		diffi	⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin → ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∈ Fin )
62	60 61	ax-mp	⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∈ Fin
63	7 62	eqeltri	⊢ 𝐾 ∈ Fin
64		prfi	⊢ { 1 , 𝑀 } ∈ Fin
65		hashun	⊢ ( ( 𝐾 ∈ Fin ∧ { 1 , 𝑀 } ∈ Fin ∧ ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ ) → ( ♯ ‘ ( 𝐾 ∪ { 1 , 𝑀 } ) ) = ( ( ♯ ‘ 𝐾 ) + ( ♯ ‘ { 1 , 𝑀 } ) ) )
66	63 64 28 65	mp3an	⊢ ( ♯ ‘ ( 𝐾 ∪ { 1 , 𝑀 } ) ) = ( ( ♯ ‘ 𝐾 ) + ( ♯ ‘ { 1 , 𝑀 } ) )
67	58	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐾 ∪ { 1 , 𝑀 } ) ) = ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
68		neeq1	⊢ ( 𝑥 = 𝑀 → ( 𝑥 ≠ 1 ↔ 𝑀 ≠ 1 ) )
69	10 18	syl	⊢ ( 𝑥 ∈ ( 2 ... ( 𝑁 + 1 ) ) → 𝑥 ≠ 1 )
70	68 69	vtoclga	⊢ ( 𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) → 𝑀 ≠ 1 )
71	5 70	syl	⊢ ( 𝜑 → 𝑀 ≠ 1 )
72	71	necomd	⊢ ( 𝜑 → 1 ≠ 𝑀 )
73		1ex	⊢ 1 ∈ V
74		hashprg	⊢ ( ( 1 ∈ V ∧ 𝑀 ∈ V ) → ( 1 ≠ 𝑀 ↔ ( ♯ ‘ { 1 , 𝑀 } ) = 2 ) )
75	73 6 74	mp2an	⊢ ( 1 ≠ 𝑀 ↔ ( ♯ ‘ { 1 , 𝑀 } ) = 2 )
76	72 75	sylib	⊢ ( 𝜑 → ( ♯ ‘ { 1 , 𝑀 } ) = 2 )
77	76	oveq2d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) + ( ♯ ‘ { 1 , 𝑀 } ) ) = ( ( ♯ ‘ 𝐾 ) + 2 ) )
78	66 67 77	3eqtr3a	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( ( ♯ ‘ 𝐾 ) + 2 ) )
79	51	nnnn0d	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
80		hashfz1	⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
81	79 80	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
82	78 81	eqtr3d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) + 2 ) = ( 𝑁 + 1 ) )
83	51	nncnd	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℂ )
84		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
85		hashcl	⊢ ( 𝐾 ∈ Fin → ( ♯ ‘ 𝐾 ) ∈ ℕ0 )
86	63 85	ax-mp	⊢ ( ♯ ‘ 𝐾 ) ∈ ℕ0
87	86	nn0cni	⊢ ( ♯ ‘ 𝐾 ) ∈ ℂ
88	87	a1i	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℂ )
89	83 84 88	subadd2d	⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) − 2 ) = ( ♯ ‘ 𝐾 ) ↔ ( ( ♯ ‘ 𝐾 ) + 2 ) = ( 𝑁 + 1 ) ) )
90	82 89	mpbird	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 2 ) = ( ♯ ‘ 𝐾 ) )
91	4	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
92		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
93	91 92 92	pnpcan2d	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − ( 1 + 1 ) ) = ( 𝑁 − 1 ) )
94	59 90 93	3eqtr3a	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) = ( 𝑁 − 1 ) )
95	29 58 94	3jca	⊢ ( 𝜑 → ( ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ ∧ ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) ∧ ( ♯ ‘ 𝐾 ) = ( 𝑁 − 1 ) ) )