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
|
syl5eqr |
⊢ ( 𝜑 → ( 𝐾 ∪ { 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 ) ) ) |