# Metamath Proof Explorer

## 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 ${⊢}{D}=\left({x}\in \mathrm{Fin}⟼\left|\left\{{f}|\left({f}:{x}\underset{1-1 onto}{⟶}{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}\right|\right)$
subfac.n ${⊢}{S}=\left({n}\in {ℕ}_{0}⟼{D}\left(\left(1\dots {n}\right)\right)\right)$
subfacp1lem.a ${⊢}{A}=\left\{{f}|\left({f}:\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\wedge \forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}$
subfacp1lem1.n ${⊢}{\phi }\to {N}\in ℕ$
subfacp1lem1.m ${⊢}{\phi }\to {M}\in \left(2\dots {N}+1\right)$
subfacp1lem1.x ${⊢}{M}\in \mathrm{V}$
subfacp1lem1.k ${⊢}{K}=\left(2\dots {N}+1\right)\setminus \left\{{M}\right\}$
Assertion subfacp1lem1 ${⊢}{\phi }\to \left({K}\cap \left\{1,{M}\right\}=\varnothing \wedge {K}\cup \left\{1,{M}\right\}=\left(1\dots {N}+1\right)\wedge \left|{K}\right|={N}-1\right)$

### Proof

Step Hyp Ref Expression
1 derang.d ${⊢}{D}=\left({x}\in \mathrm{Fin}⟼\left|\left\{{f}|\left({f}:{x}\underset{1-1 onto}{⟶}{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}\right|\right)$
2 subfac.n ${⊢}{S}=\left({n}\in {ℕ}_{0}⟼{D}\left(\left(1\dots {n}\right)\right)\right)$
3 subfacp1lem.a ${⊢}{A}=\left\{{f}|\left({f}:\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\wedge \forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}$
4 subfacp1lem1.n ${⊢}{\phi }\to {N}\in ℕ$
5 subfacp1lem1.m ${⊢}{\phi }\to {M}\in \left(2\dots {N}+1\right)$
6 subfacp1lem1.x ${⊢}{M}\in \mathrm{V}$
7 subfacp1lem1.k ${⊢}{K}=\left(2\dots {N}+1\right)\setminus \left\{{M}\right\}$
8 disj ${⊢}{K}\cap \left\{1,{M}\right\}=\varnothing ↔\forall {x}\in {K}\phantom{\rule{.4em}{0ex}}¬{x}\in \left\{1,{M}\right\}$
9 eldifi ${⊢}{x}\in \left(\left(2\dots {N}+1\right)\setminus \left\{{M}\right\}\right)\to {x}\in \left(2\dots {N}+1\right)$
10 elfzle1 ${⊢}{x}\in \left(2\dots {N}+1\right)\to 2\le {x}$
11 1lt2 ${⊢}1<2$
12 1re ${⊢}1\in ℝ$
13 2re ${⊢}2\in ℝ$
14 12 13 ltnlei ${⊢}1<2↔¬2\le 1$
15 11 14 mpbi ${⊢}¬2\le 1$
16 breq2 ${⊢}{x}=1\to \left(2\le {x}↔2\le 1\right)$
17 15 16 mtbiri ${⊢}{x}=1\to ¬2\le {x}$
18 17 necon2ai ${⊢}2\le {x}\to {x}\ne 1$
19 9 10 18 3syl ${⊢}{x}\in \left(\left(2\dots {N}+1\right)\setminus \left\{{M}\right\}\right)\to {x}\ne 1$
20 eldifsni ${⊢}{x}\in \left(\left(2\dots {N}+1\right)\setminus \left\{{M}\right\}\right)\to {x}\ne {M}$
21 19 20 jca ${⊢}{x}\in \left(\left(2\dots {N}+1\right)\setminus \left\{{M}\right\}\right)\to \left({x}\ne 1\wedge {x}\ne {M}\right)$
22 21 7 eleq2s ${⊢}{x}\in {K}\to \left({x}\ne 1\wedge {x}\ne {M}\right)$
23 neanior ${⊢}\left({x}\ne 1\wedge {x}\ne {M}\right)↔¬\left({x}=1\vee {x}={M}\right)$
24 22 23 sylib ${⊢}{x}\in {K}\to ¬\left({x}=1\vee {x}={M}\right)$
25 vex ${⊢}{x}\in \mathrm{V}$
26 25 elpr ${⊢}{x}\in \left\{1,{M}\right\}↔\left({x}=1\vee {x}={M}\right)$
27 24 26 sylnibr ${⊢}{x}\in {K}\to ¬{x}\in \left\{1,{M}\right\}$
28 8 27 mprgbir ${⊢}{K}\cap \left\{1,{M}\right\}=\varnothing$
29 28 a1i ${⊢}{\phi }\to {K}\cap \left\{1,{M}\right\}=\varnothing$
30 uncom ${⊢}\left\{1\right\}\cup \left({K}\cup \left\{{M}\right\}\right)=\left({K}\cup \left\{{M}\right\}\right)\cup \left\{1\right\}$
31 1z ${⊢}1\in ℤ$
32 fzsn ${⊢}1\in ℤ\to \left(1\dots 1\right)=\left\{1\right\}$
33 31 32 ax-mp ${⊢}\left(1\dots 1\right)=\left\{1\right\}$
34 7 uneq1i ${⊢}{K}\cup \left\{{M}\right\}=\left(\left(2\dots {N}+1\right)\setminus \left\{{M}\right\}\right)\cup \left\{{M}\right\}$
35 undif1 ${⊢}\left(\left(2\dots {N}+1\right)\setminus \left\{{M}\right\}\right)\cup \left\{{M}\right\}=\left(2\dots {N}+1\right)\cup \left\{{M}\right\}$
36 34 35 eqtr2i ${⊢}\left(2\dots {N}+1\right)\cup \left\{{M}\right\}={K}\cup \left\{{M}\right\}$
37 33 36 uneq12i ${⊢}\left(1\dots 1\right)\cup \left(\left(2\dots {N}+1\right)\cup \left\{{M}\right\}\right)=\left\{1\right\}\cup \left({K}\cup \left\{{M}\right\}\right)$
38 df-pr ${⊢}\left\{1,{M}\right\}=\left\{1\right\}\cup \left\{{M}\right\}$
39 38 equncomi ${⊢}\left\{1,{M}\right\}=\left\{{M}\right\}\cup \left\{1\right\}$
40 39 uneq2i ${⊢}{K}\cup \left\{1,{M}\right\}={K}\cup \left(\left\{{M}\right\}\cup \left\{1\right\}\right)$
41 unass ${⊢}\left({K}\cup \left\{{M}\right\}\right)\cup \left\{1\right\}={K}\cup \left(\left\{{M}\right\}\cup \left\{1\right\}\right)$
42 40 41 eqtr4i ${⊢}{K}\cup \left\{1,{M}\right\}=\left({K}\cup \left\{{M}\right\}\right)\cup \left\{1\right\}$
43 30 37 42 3eqtr4i ${⊢}\left(1\dots 1\right)\cup \left(\left(2\dots {N}+1\right)\cup \left\{{M}\right\}\right)={K}\cup \left\{1,{M}\right\}$
44 5 snssd ${⊢}{\phi }\to \left\{{M}\right\}\subseteq \left(2\dots {N}+1\right)$
45 ssequn2 ${⊢}\left\{{M}\right\}\subseteq \left(2\dots {N}+1\right)↔\left(2\dots {N}+1\right)\cup \left\{{M}\right\}=\left(2\dots {N}+1\right)$
46 44 45 sylib ${⊢}{\phi }\to \left(2\dots {N}+1\right)\cup \left\{{M}\right\}=\left(2\dots {N}+1\right)$
47 df-2 ${⊢}2=1+1$
48 47 oveq1i ${⊢}\left(2\dots {N}+1\right)=\left(1+1\dots {N}+1\right)$
49 46 48 syl6eq ${⊢}{\phi }\to \left(2\dots {N}+1\right)\cup \left\{{M}\right\}=\left(1+1\dots {N}+1\right)$
50 49 uneq2d ${⊢}{\phi }\to \left(1\dots 1\right)\cup \left(\left(2\dots {N}+1\right)\cup \left\{{M}\right\}\right)=\left(1\dots 1\right)\cup \left(1+1\dots {N}+1\right)$
51 4 peano2nnd ${⊢}{\phi }\to {N}+1\in ℕ$
52 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
53 51 52 eleqtrdi ${⊢}{\phi }\to {N}+1\in {ℤ}_{\ge 1}$
54 eluzfz1 ${⊢}{N}+1\in {ℤ}_{\ge 1}\to 1\in \left(1\dots {N}+1\right)$
55 fzsplit ${⊢}1\in \left(1\dots {N}+1\right)\to \left(1\dots {N}+1\right)=\left(1\dots 1\right)\cup \left(1+1\dots {N}+1\right)$
56 53 54 55 3syl ${⊢}{\phi }\to \left(1\dots {N}+1\right)=\left(1\dots 1\right)\cup \left(1+1\dots {N}+1\right)$
57 50 56 eqtr4d ${⊢}{\phi }\to \left(1\dots 1\right)\cup \left(\left(2\dots {N}+1\right)\cup \left\{{M}\right\}\right)=\left(1\dots {N}+1\right)$
58 43 57 syl5eqr ${⊢}{\phi }\to {K}\cup \left\{1,{M}\right\}=\left(1\dots {N}+1\right)$
59 47 oveq2i ${⊢}{N}+1-2={N}+1-\left(1+1\right)$
60 fzfi ${⊢}\left(2\dots {N}+1\right)\in \mathrm{Fin}$
61 diffi ${⊢}\left(2\dots {N}+1\right)\in \mathrm{Fin}\to \left(2\dots {N}+1\right)\setminus \left\{{M}\right\}\in \mathrm{Fin}$
62 60 61 ax-mp ${⊢}\left(2\dots {N}+1\right)\setminus \left\{{M}\right\}\in \mathrm{Fin}$
63 7 62 eqeltri ${⊢}{K}\in \mathrm{Fin}$
64 prfi ${⊢}\left\{1,{M}\right\}\in \mathrm{Fin}$
65 hashun ${⊢}\left({K}\in \mathrm{Fin}\wedge \left\{1,{M}\right\}\in \mathrm{Fin}\wedge {K}\cap \left\{1,{M}\right\}=\varnothing \right)\to \left|{K}\cup \left\{1,{M}\right\}\right|=\left|{K}\right|+\left|\left\{1,{M}\right\}\right|$
66 63 64 28 65 mp3an ${⊢}\left|{K}\cup \left\{1,{M}\right\}\right|=\left|{K}\right|+\left|\left\{1,{M}\right\}\right|$
67 58 fveq2d ${⊢}{\phi }\to \left|{K}\cup \left\{1,{M}\right\}\right|=\left|\left(1\dots {N}+1\right)\right|$
68 neeq1 ${⊢}{x}={M}\to \left({x}\ne 1↔{M}\ne 1\right)$
69 10 18 syl ${⊢}{x}\in \left(2\dots {N}+1\right)\to {x}\ne 1$
70 68 69 vtoclga ${⊢}{M}\in \left(2\dots {N}+1\right)\to {M}\ne 1$
71 5 70 syl ${⊢}{\phi }\to {M}\ne 1$
72 71 necomd ${⊢}{\phi }\to 1\ne {M}$
73 1ex ${⊢}1\in \mathrm{V}$
74 hashprg ${⊢}\left(1\in \mathrm{V}\wedge {M}\in \mathrm{V}\right)\to \left(1\ne {M}↔\left|\left\{1,{M}\right\}\right|=2\right)$
75 73 6 74 mp2an ${⊢}1\ne {M}↔\left|\left\{1,{M}\right\}\right|=2$
76 72 75 sylib ${⊢}{\phi }\to \left|\left\{1,{M}\right\}\right|=2$
77 76 oveq2d ${⊢}{\phi }\to \left|{K}\right|+\left|\left\{1,{M}\right\}\right|=\left|{K}\right|+2$
78 66 67 77 3eqtr3a ${⊢}{\phi }\to \left|\left(1\dots {N}+1\right)\right|=\left|{K}\right|+2$
79 51 nnnn0d ${⊢}{\phi }\to {N}+1\in {ℕ}_{0}$
80 hashfz1 ${⊢}{N}+1\in {ℕ}_{0}\to \left|\left(1\dots {N}+1\right)\right|={N}+1$
81 79 80 syl ${⊢}{\phi }\to \left|\left(1\dots {N}+1\right)\right|={N}+1$
82 78 81 eqtr3d ${⊢}{\phi }\to \left|{K}\right|+2={N}+1$
83 51 nncnd ${⊢}{\phi }\to {N}+1\in ℂ$
84 2cnd ${⊢}{\phi }\to 2\in ℂ$
85 hashcl ${⊢}{K}\in \mathrm{Fin}\to \left|{K}\right|\in {ℕ}_{0}$
86 63 85 ax-mp ${⊢}\left|{K}\right|\in {ℕ}_{0}$
87 86 nn0cni ${⊢}\left|{K}\right|\in ℂ$
88 87 a1i ${⊢}{\phi }\to \left|{K}\right|\in ℂ$
89 83 84 88 subadd2d ${⊢}{\phi }\to \left({N}+1-2=\left|{K}\right|↔\left|{K}\right|+2={N}+1\right)$
90 82 89 mpbird ${⊢}{\phi }\to {N}+1-2=\left|{K}\right|$
91 4 nncnd ${⊢}{\phi }\to {N}\in ℂ$
92 1cnd ${⊢}{\phi }\to 1\in ℂ$
93 91 92 92 pnpcan2d ${⊢}{\phi }\to {N}+1-\left(1+1\right)={N}-1$
94 59 90 93 3eqtr3a ${⊢}{\phi }\to \left|{K}\right|={N}-1$
95 29 58 94 3jca ${⊢}{\phi }\to \left({K}\cap \left\{1,{M}\right\}=\varnothing \wedge {K}\cup \left\{1,{M}\right\}=\left(1\dots {N}+1\right)\wedge \left|{K}\right|={N}-1\right)$