# Metamath Proof Explorer

## Theorem subfacp1lem3

Description: Lemma for subfacp1 . In subfacp1lem6 we cut up the set of all derangements on 1 ... ( N + 1 ) first according to the value at 1 , and then by whether or not ( f( f1 ) ) = 1 . In this lemma, we show that the subset of all N + 1 derangements that satisfy this for fixed M = ( f1 ) is in bijection with N - 1 derangements, by simply dropping the x = 1 and x = M points from the function to get a derangement on K = ( 1 ... ( N - 1 ) ) \ { 1 , M } . (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\}$
subfacp1lem3.b ${⊢}{B}=\left\{{g}\in {A}|\left({g}\left(1\right)={M}\wedge {g}\left({M}\right)=1\right)\right\}$
subfacp1lem3.c ${⊢}{C}=\left\{{f}|\left({f}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}$
Assertion subfacp1lem3 ${⊢}{\phi }\to \left|{B}\right|={S}\left({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 subfacp1lem3.b ${⊢}{B}=\left\{{g}\in {A}|\left({g}\left(1\right)={M}\wedge {g}\left({M}\right)=1\right)\right\}$
9 subfacp1lem3.c ${⊢}{C}=\left\{{f}|\left({f}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}$
10 fzfi ${⊢}\left(1\dots {N}+1\right)\in \mathrm{Fin}$
11 deranglem ${⊢}\left(1\dots {N}+1\right)\in \mathrm{Fin}\to \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\}\in \mathrm{Fin}$
12 10 11 ax-mp ${⊢}\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\}\in \mathrm{Fin}$
13 3 12 eqeltri ${⊢}{A}\in \mathrm{Fin}$
14 ssrab2 ${⊢}\left\{{g}\in {A}|\left({g}\left(1\right)={M}\wedge {g}\left({M}\right)=1\right)\right\}\subseteq {A}$
15 8 14 eqsstri ${⊢}{B}\subseteq {A}$
16 ssfi ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\subseteq {A}\right)\to {B}\in \mathrm{Fin}$
17 13 15 16 mp2an ${⊢}{B}\in \mathrm{Fin}$
18 17 elexi ${⊢}{B}\in \mathrm{V}$
19 18 a1i ${⊢}{\phi }\to {B}\in \mathrm{V}$
20 fzfi ${⊢}\left(2\dots {N}+1\right)\in \mathrm{Fin}$
21 diffi ${⊢}\left(2\dots {N}+1\right)\in \mathrm{Fin}\to \left(2\dots {N}+1\right)\setminus \left\{{M}\right\}\in \mathrm{Fin}$
22 20 21 ax-mp ${⊢}\left(2\dots {N}+1\right)\setminus \left\{{M}\right\}\in \mathrm{Fin}$
23 7 22 eqeltri ${⊢}{K}\in \mathrm{Fin}$
24 deranglem ${⊢}{K}\in \mathrm{Fin}\to \left\{{f}|\left({f}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}\in \mathrm{Fin}$
25 23 24 ax-mp ${⊢}\left\{{f}|\left({f}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}\in \mathrm{Fin}$
26 9 25 eqeltri ${⊢}{C}\in \mathrm{Fin}$
27 26 elexi ${⊢}{C}\in \mathrm{V}$
28 27 a1i ${⊢}{\phi }\to {C}\in \mathrm{V}$
29 simpr ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to {b}\in {B}$
30 fveq1 ${⊢}{g}={b}\to {g}\left(1\right)={b}\left(1\right)$
31 30 eqeq1d ${⊢}{g}={b}\to \left({g}\left(1\right)={M}↔{b}\left(1\right)={M}\right)$
32 fveq1 ${⊢}{g}={b}\to {g}\left({M}\right)={b}\left({M}\right)$
33 32 eqeq1d ${⊢}{g}={b}\to \left({g}\left({M}\right)=1↔{b}\left({M}\right)=1\right)$
34 31 33 anbi12d ${⊢}{g}={b}\to \left(\left({g}\left(1\right)={M}\wedge {g}\left({M}\right)=1\right)↔\left({b}\left(1\right)={M}\wedge {b}\left({M}\right)=1\right)\right)$
35 34 8 elrab2 ${⊢}{b}\in {B}↔\left({b}\in {A}\wedge \left({b}\left(1\right)={M}\wedge {b}\left({M}\right)=1\right)\right)$
36 29 35 sylib ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left({b}\in {A}\wedge \left({b}\left(1\right)={M}\wedge {b}\left({M}\right)=1\right)\right)$
37 36 simpld ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to {b}\in {A}$
38 vex ${⊢}{b}\in \mathrm{V}$
39 f1oeq1 ${⊢}{f}={b}\to \left({f}:\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)↔{b}:\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\right)$
40 fveq1 ${⊢}{f}={b}\to {f}\left({y}\right)={b}\left({y}\right)$
41 40 neeq1d ${⊢}{f}={b}\to \left({f}\left({y}\right)\ne {y}↔{b}\left({y}\right)\ne {y}\right)$
42 41 ralbidv ${⊢}{f}={b}\to \left(\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}↔\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\ne {y}\right)$
43 39 42 anbi12d ${⊢}{f}={b}\to \left(\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)↔\left({b}:\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}}{b}\left({y}\right)\ne {y}\right)\right)$
44 38 43 3 elab2 ${⊢}{b}\in {A}↔\left({b}:\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}}{b}\left({y}\right)\ne {y}\right)$
45 37 44 sylib ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left({b}:\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}}{b}\left({y}\right)\ne {y}\right)$
46 45 simpld ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to {b}:\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)$
47 f1of1 ${⊢}{b}:\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\to {b}:\left(1\dots {N}+1\right)\underset{1-1}{⟶}\left(1\dots {N}+1\right)$
48 df-f1 ${⊢}{b}:\left(1\dots {N}+1\right)\underset{1-1}{⟶}\left(1\dots {N}+1\right)↔\left({b}:\left(1\dots {N}+1\right)⟶\left(1\dots {N}+1\right)\wedge \mathrm{Fun}{{b}}^{-1}\right)$
49 48 simprbi ${⊢}{b}:\left(1\dots {N}+1\right)\underset{1-1}{⟶}\left(1\dots {N}+1\right)\to \mathrm{Fun}{{b}}^{-1}$
50 46 47 49 3syl ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \mathrm{Fun}{{b}}^{-1}$
51 f1ofn ${⊢}{b}:\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\to {b}Fn\left(1\dots {N}+1\right)$
52 46 51 syl ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to {b}Fn\left(1\dots {N}+1\right)$
53 fnresdm ${⊢}{b}Fn\left(1\dots {N}+1\right)\to {{b}↾}_{\left(1\dots {N}+1\right)}={b}$
54 f1oeq1 ${⊢}{{b}↾}_{\left(1\dots {N}+1\right)}={b}\to \left(\left({{b}↾}_{\left(1\dots {N}+1\right)}\right):\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)↔{b}:\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\right)$
55 52 53 54 3syl ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left(\left({{b}↾}_{\left(1\dots {N}+1\right)}\right):\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)↔{b}:\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\right)$
56 46 55 mpbird ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left({{b}↾}_{\left(1\dots {N}+1\right)}\right):\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)$
57 f1ofo ${⊢}\left({{b}↾}_{\left(1\dots {N}+1\right)}\right):\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\to \left({{b}↾}_{\left(1\dots {N}+1\right)}\right):\left(1\dots {N}+1\right)\underset{onto}{⟶}\left(1\dots {N}+1\right)$
58 56 57 syl ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left({{b}↾}_{\left(1\dots {N}+1\right)}\right):\left(1\dots {N}+1\right)\underset{onto}{⟶}\left(1\dots {N}+1\right)$
59 ssun2 ${⊢}\left\{1,{M}\right\}\subseteq {K}\cup \left\{1,{M}\right\}$
60 1 2 3 4 5 6 7 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)$
61 60 simp2d ${⊢}{\phi }\to {K}\cup \left\{1,{M}\right\}=\left(1\dots {N}+1\right)$
62 59 61 sseqtrid ${⊢}{\phi }\to \left\{1,{M}\right\}\subseteq \left(1\dots {N}+1\right)$
63 62 adantr ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left\{1,{M}\right\}\subseteq \left(1\dots {N}+1\right)$
64 fnssres ${⊢}\left({b}Fn\left(1\dots {N}+1\right)\wedge \left\{1,{M}\right\}\subseteq \left(1\dots {N}+1\right)\right)\to \left({{b}↾}_{\left\{1,{M}\right\}}\right)Fn\left\{1,{M}\right\}$
65 52 63 64 syl2anc ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left({{b}↾}_{\left\{1,{M}\right\}}\right)Fn\left\{1,{M}\right\}$
66 36 simprd ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left({b}\left(1\right)={M}\wedge {b}\left({M}\right)=1\right)$
67 66 simpld ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to {b}\left(1\right)={M}$
68 6 prid2 ${⊢}{M}\in \left\{1,{M}\right\}$
69 67 68 syl6eqel ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to {b}\left(1\right)\in \left\{1,{M}\right\}$
70 66 simprd ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to {b}\left({M}\right)=1$
71 1ex ${⊢}1\in \mathrm{V}$
72 71 prid1 ${⊢}1\in \left\{1,{M}\right\}$
73 70 72 syl6eqel ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to {b}\left({M}\right)\in \left\{1,{M}\right\}$
74 fveq2 ${⊢}{x}=1\to {b}\left({x}\right)={b}\left(1\right)$
75 74 eleq1d ${⊢}{x}=1\to \left({b}\left({x}\right)\in \left\{1,{M}\right\}↔{b}\left(1\right)\in \left\{1,{M}\right\}\right)$
76 fveq2 ${⊢}{x}={M}\to {b}\left({x}\right)={b}\left({M}\right)$
77 76 eleq1d ${⊢}{x}={M}\to \left({b}\left({x}\right)\in \left\{1,{M}\right\}↔{b}\left({M}\right)\in \left\{1,{M}\right\}\right)$
78 71 6 75 77 ralpr ${⊢}\forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({x}\right)\in \left\{1,{M}\right\}↔\left({b}\left(1\right)\in \left\{1,{M}\right\}\wedge {b}\left({M}\right)\in \left\{1,{M}\right\}\right)$
79 69 73 78 sylanbrc ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({x}\right)\in \left\{1,{M}\right\}$
80 fvres ${⊢}{x}\in \left\{1,{M}\right\}\to \left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({x}\right)={b}\left({x}\right)$
81 80 eleq1d ${⊢}{x}\in \left\{1,{M}\right\}\to \left(\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({x}\right)\in \left\{1,{M}\right\}↔{b}\left({x}\right)\in \left\{1,{M}\right\}\right)$
82 81 ralbiia ${⊢}\forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({x}\right)\in \left\{1,{M}\right\}↔\forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({x}\right)\in \left\{1,{M}\right\}$
83 79 82 sylibr ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({x}\right)\in \left\{1,{M}\right\}$
84 ffnfv ${⊢}\left({{b}↾}_{\left\{1,{M}\right\}}\right):\left\{1,{M}\right\}⟶\left\{1,{M}\right\}↔\left(\left({{b}↾}_{\left\{1,{M}\right\}}\right)Fn\left\{1,{M}\right\}\wedge \forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({x}\right)\in \left\{1,{M}\right\}\right)$
85 65 83 84 sylanbrc ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left({{b}↾}_{\left\{1,{M}\right\}}\right):\left\{1,{M}\right\}⟶\left\{1,{M}\right\}$
86 fveqeq2 ${⊢}{y}={M}\to \left({b}\left({y}\right)=1↔{b}\left({M}\right)=1\right)$
87 86 rspcev ${⊢}\left({M}\in \left\{1,{M}\right\}\wedge {b}\left({M}\right)=1\right)\to \exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=1$
88 68 70 87 sylancr ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=1$
89 fveqeq2 ${⊢}{y}=1\to \left({b}\left({y}\right)={M}↔{b}\left(1\right)={M}\right)$
90 89 rspcev ${⊢}\left(1\in \left\{1,{M}\right\}\wedge {b}\left(1\right)={M}\right)\to \exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={M}$
91 72 67 90 sylancr ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={M}$
92 eqeq2 ${⊢}{x}=1\to \left({b}\left({y}\right)={x}↔{b}\left({y}\right)=1\right)$
93 92 rexbidv ${⊢}{x}=1\to \left(\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={x}↔\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=1\right)$
94 eqeq2 ${⊢}{x}={M}\to \left({b}\left({y}\right)={x}↔{b}\left({y}\right)={M}\right)$
95 94 rexbidv ${⊢}{x}={M}\to \left(\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={x}↔\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={M}\right)$
96 71 6 93 95 ralpr ${⊢}\forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={x}↔\left(\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=1\wedge \exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={M}\right)$
97 88 91 96 sylanbrc ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={x}$
98 eqcom ${⊢}{x}=\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({y}\right)↔\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({y}\right)={x}$
99 fvres ${⊢}{y}\in \left\{1,{M}\right\}\to \left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({y}\right)={b}\left({y}\right)$
100 99 eqeq1d ${⊢}{y}\in \left\{1,{M}\right\}\to \left(\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({y}\right)={x}↔{b}\left({y}\right)={x}\right)$
101 98 100 syl5bb ${⊢}{y}\in \left\{1,{M}\right\}\to \left({x}=\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({y}\right)↔{b}\left({y}\right)={x}\right)$
102 101 rexbiia ${⊢}\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{x}=\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({y}\right)↔\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={x}$
103 102 ralbii ${⊢}\forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{x}=\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({y}\right)↔\forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={x}$
104 97 103 sylibr ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{x}=\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({y}\right)$
105 dffo3 ${⊢}\left({{b}↾}_{\left\{1,{M}\right\}}\right):\left\{1,{M}\right\}\underset{onto}{⟶}\left\{1,{M}\right\}↔\left(\left({{b}↾}_{\left\{1,{M}\right\}}\right):\left\{1,{M}\right\}⟶\left\{1,{M}\right\}\wedge \forall {x}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\exists {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{x}=\left({{b}↾}_{\left\{1,{M}\right\}}\right)\left({y}\right)\right)$
106 85 104 105 sylanbrc ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left({{b}↾}_{\left\{1,{M}\right\}}\right):\left\{1,{M}\right\}\underset{onto}{⟶}\left\{1,{M}\right\}$
107 resdif ${⊢}\left(\mathrm{Fun}{{b}}^{-1}\wedge \left({{b}↾}_{\left(1\dots {N}+1\right)}\right):\left(1\dots {N}+1\right)\underset{onto}{⟶}\left(1\dots {N}+1\right)\wedge \left({{b}↾}_{\left\{1,{M}\right\}}\right):\left\{1,{M}\right\}\underset{onto}{⟶}\left\{1,{M}\right\}\right)\to \left({{b}↾}_{\left(\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)}\right):\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}$
108 50 58 106 107 syl3anc ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left({{b}↾}_{\left(\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)}\right):\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}$
109 uncom ${⊢}\left\{1,{M}\right\}\cup {K}={K}\cup \left\{1,{M}\right\}$
110 109 61 syl5eq ${⊢}{\phi }\to \left\{1,{M}\right\}\cup {K}=\left(1\dots {N}+1\right)$
111 incom ${⊢}\left\{1,{M}\right\}\cap {K}={K}\cap \left\{1,{M}\right\}$
112 60 simp1d ${⊢}{\phi }\to {K}\cap \left\{1,{M}\right\}=\varnothing$
113 111 112 syl5eq ${⊢}{\phi }\to \left\{1,{M}\right\}\cap {K}=\varnothing$
114 uneqdifeq ${⊢}\left(\left\{1,{M}\right\}\subseteq \left(1\dots {N}+1\right)\wedge \left\{1,{M}\right\}\cap {K}=\varnothing \right)\to \left(\left\{1,{M}\right\}\cup {K}=\left(1\dots {N}+1\right)↔\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}={K}\right)$
115 62 113 114 syl2anc ${⊢}{\phi }\to \left(\left\{1,{M}\right\}\cup {K}=\left(1\dots {N}+1\right)↔\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}={K}\right)$
116 110 115 mpbid ${⊢}{\phi }\to \left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}={K}$
117 116 adantr ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}={K}$
118 reseq2 ${⊢}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}={K}\to {{b}↾}_{\left(\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)}={{b}↾}_{{K}}$
119 f1oeq1 ${⊢}{{b}↾}_{\left(\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)}={{b}↾}_{{K}}\to \left(\left({{b}↾}_{\left(\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)}\right):\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}↔\left({{b}↾}_{{K}}\right):\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)$
120 118 119 syl ${⊢}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}={K}\to \left(\left({{b}↾}_{\left(\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)}\right):\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}↔\left({{b}↾}_{{K}}\right):\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)$
121 f1oeq2 ${⊢}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}={K}\to \left(\left({{b}↾}_{{K}}\right):\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}↔\left({{b}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)$
122 f1oeq3 ${⊢}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}={K}\to \left(\left({{b}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}↔\left({{b}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{K}\right)$
123 120 121 122 3bitrd ${⊢}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}={K}\to \left(\left({{b}↾}_{\left(\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)}\right):\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}↔\left({{b}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{K}\right)$
124 117 123 syl ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left(\left({{b}↾}_{\left(\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\right)}\right):\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\setminus \left\{1,{M}\right\}↔\left({{b}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{K}\right)$
125 108 124 mpbid ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \left({{b}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{K}$
126 ssun1 ${⊢}{K}\subseteq {K}\cup \left\{1,{M}\right\}$
127 126 61 sseqtrid ${⊢}{\phi }\to {K}\subseteq \left(1\dots {N}+1\right)$
128 127 adantr ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to {K}\subseteq \left(1\dots {N}+1\right)$
129 45 simprd ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\ne {y}$
130 ssralv ${⊢}{K}\subseteq \left(1\dots {N}+1\right)\to \left(\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\ne {y}\to \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\ne {y}\right)$
131 128 129 130 sylc ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\ne {y}$
132 38 resex ${⊢}{{b}↾}_{{K}}\in \mathrm{V}$
133 f1oeq1 ${⊢}{f}={{b}↾}_{{K}}\to \left({f}:{K}\underset{1-1 onto}{⟶}{K}↔\left({{b}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{K}\right)$
134 fveq1 ${⊢}{f}={{b}↾}_{{K}}\to {f}\left({y}\right)=\left({{b}↾}_{{K}}\right)\left({y}\right)$
135 fvres ${⊢}{y}\in {K}\to \left({{b}↾}_{{K}}\right)\left({y}\right)={b}\left({y}\right)$
136 134 135 sylan9eq ${⊢}\left({f}={{b}↾}_{{K}}\wedge {y}\in {K}\right)\to {f}\left({y}\right)={b}\left({y}\right)$
137 136 neeq1d ${⊢}\left({f}={{b}↾}_{{K}}\wedge {y}\in {K}\right)\to \left({f}\left({y}\right)\ne {y}↔{b}\left({y}\right)\ne {y}\right)$
138 137 ralbidva ${⊢}{f}={{b}↾}_{{K}}\to \left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}↔\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\ne {y}\right)$
139 133 138 anbi12d ${⊢}{f}={{b}↾}_{{K}}\to \left(\left({f}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)↔\left(\left({{b}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\ne {y}\right)\right)$
140 132 139 9 elab2 ${⊢}{{b}↾}_{{K}}\in {C}↔\left(\left({{b}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\ne {y}\right)$
141 125 131 140 sylanbrc ${⊢}\left({\phi }\wedge {b}\in {B}\right)\to {{b}↾}_{{K}}\in {C}$
142 141 ex ${⊢}{\phi }\to \left({b}\in {B}\to {{b}↾}_{{K}}\in {C}\right)$
143 4 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to {N}\in ℕ$
144 5 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to {M}\in \left(2\dots {N}+1\right)$
145 eqid ${⊢}{c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}$
146 simpr ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to {c}\in {C}$
147 vex ${⊢}{c}\in \mathrm{V}$
148 f1oeq1 ${⊢}{f}={c}\to \left({f}:{K}\underset{1-1 onto}{⟶}{K}↔{c}:{K}\underset{1-1 onto}{⟶}{K}\right)$
149 fveq1 ${⊢}{f}={c}\to {f}\left({y}\right)={c}\left({y}\right)$
150 149 neeq1d ${⊢}{f}={c}\to \left({f}\left({y}\right)\ne {y}↔{c}\left({y}\right)\ne {y}\right)$
151 150 ralbidv ${⊢}{f}={c}\to \left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}↔\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{c}\left({y}\right)\ne {y}\right)$
152 148 151 anbi12d ${⊢}{f}={c}\to \left(\left({f}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)↔\left({c}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{c}\left({y}\right)\ne {y}\right)\right)$
153 147 152 9 elab2 ${⊢}{c}\in {C}↔\left({c}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{c}\left({y}\right)\ne {y}\right)$
154 146 153 sylib ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \left({c}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{c}\left({y}\right)\ne {y}\right)$
155 154 simpld ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to {c}:{K}\underset{1-1 onto}{⟶}{K}$
156 1 2 3 143 144 6 7 145 155 subfacp1lem2a ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \left(\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right):\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\wedge \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)={M}\wedge \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)=1\right)$
157 156 simp1d ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right):\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)$
158 1 2 3 143 144 6 7 145 155 subfacp1lem2b ${⊢}\left(\left({\phi }\wedge {c}\in {C}\right)\wedge {y}\in {K}\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)={c}\left({y}\right)$
159 154 simprd ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{c}\left({y}\right)\ne {y}$
160 159 r19.21bi ${⊢}\left(\left({\phi }\wedge {c}\in {C}\right)\wedge {y}\in {K}\right)\to {c}\left({y}\right)\ne {y}$
161 158 160 eqnetrd ${⊢}\left(\left({\phi }\wedge {c}\in {C}\right)\wedge {y}\in {K}\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}$
162 161 ralrimiva ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}$
163 156 simp2d ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)={M}$
164 elfzuz ${⊢}{M}\in \left(2\dots {N}+1\right)\to {M}\in {ℤ}_{\ge 2}$
165 eluz2b3 ${⊢}{M}\in {ℤ}_{\ge 2}↔\left({M}\in ℕ\wedge {M}\ne 1\right)$
166 165 simprbi ${⊢}{M}\in {ℤ}_{\ge 2}\to {M}\ne 1$
167 5 164 166 3syl ${⊢}{\phi }\to {M}\ne 1$
168 167 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to {M}\ne 1$
169 163 168 eqnetrd ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)\ne 1$
170 156 simp3d ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)=1$
171 168 necomd ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to 1\ne {M}$
172 170 171 eqnetrd ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)\ne {M}$
173 fveq2 ${⊢}{y}=1\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)$
174 id ${⊢}{y}=1\to {y}=1$
175 173 174 neeq12d ${⊢}{y}=1\to \left(\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}↔\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)\ne 1\right)$
176 fveq2 ${⊢}{y}={M}\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)$
177 id ${⊢}{y}={M}\to {y}={M}$
178 176 177 neeq12d ${⊢}{y}={M}\to \left(\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}↔\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)\ne {M}\right)$
179 71 6 175 178 ralpr ${⊢}\forall {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}↔\left(\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)\ne 1\wedge \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)\ne {M}\right)$
180 169 172 179 sylanbrc ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \forall {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}$
181 ralunb ${⊢}\forall {y}\in \left({K}\cup \left\{1,{M}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}↔\left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}\wedge \forall {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}\right)$
182 162 180 181 sylanbrc ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \forall {y}\in \left({K}\cup \left\{1,{M}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}$
183 61 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to {K}\cup \left\{1,{M}\right\}=\left(1\dots {N}+1\right)$
184 183 raleqdv ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \left(\forall {y}\in \left({K}\cup \left\{1,{M}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}↔\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}\right)$
185 182 184 mpbid ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}$
186 prex ${⊢}\left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\in \mathrm{V}$
187 147 186 unex ${⊢}{c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\in \mathrm{V}$
188 f1oeq1 ${⊢}{f}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\to \left({f}:\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)↔\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right):\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\right)$
189 fveq1 ${⊢}{f}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\to {f}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)$
190 189 neeq1d ${⊢}{f}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\to \left({f}\left({y}\right)\ne {y}↔\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}\right)$
191 190 ralbidv ${⊢}{f}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\to \left(\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}↔\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}\right)$
192 188 191 anbi12d ${⊢}{f}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\to \left(\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)↔\left(\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right):\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}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}\right)\right)$
193 187 192 3 elab2 ${⊢}{c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\in {A}↔\left(\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right):\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}}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\ne {y}\right)$
194 157 185 193 sylanbrc ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to {c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\in {A}$
195 163 170 jca ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \left(\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)={M}\wedge \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)=1\right)$
196 fveq1 ${⊢}{g}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\to {g}\left(1\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)$
197 196 eqeq1d ${⊢}{g}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\to \left({g}\left(1\right)={M}↔\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)={M}\right)$
198 fveq1 ${⊢}{g}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\to {g}\left({M}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)$
199 198 eqeq1d ${⊢}{g}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\to \left({g}\left({M}\right)=1↔\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)=1\right)$
200 197 199 anbi12d ${⊢}{g}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\to \left(\left({g}\left(1\right)={M}\wedge {g}\left({M}\right)=1\right)↔\left(\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)={M}\wedge \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)=1\right)\right)$
201 200 8 elrab2 ${⊢}{c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\in {B}↔\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\in {A}\wedge \left(\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)={M}\wedge \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)=1\right)\right)$
202 194 195 201 sylanbrc ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to {c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\in {B}$
203 202 ex ${⊢}{\phi }\to \left({c}\in {C}\to {c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\in {B}\right)$
204 67 adantrr ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {b}\left(1\right)={M}$
205 163 adantrl ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)={M}$
206 204 205 eqtr4d ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {b}\left(1\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)$
207 70 adantrr ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {b}\left({M}\right)=1$
208 170 adantrl ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)=1$
209 207 208 eqtr4d ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {b}\left({M}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)$
210 fveq2 ${⊢}{y}=1\to {b}\left({y}\right)={b}\left(1\right)$
211 210 173 eqeq12d ${⊢}{y}=1\to \left({b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔{b}\left(1\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)\right)$
212 fveq2 ${⊢}{y}={M}\to {b}\left({y}\right)={b}\left({M}\right)$
213 212 176 eqeq12d ${⊢}{y}={M}\to \left({b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔{b}\left({M}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)\right)$
214 71 6 211 213 ralpr ${⊢}\forall {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔\left({b}\left(1\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left(1\right)\wedge {b}\left({M}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({M}\right)\right)$
215 206 209 214 sylanbrc ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \forall {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)$
216 215 biantrud ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔\left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\wedge \forall {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\right)\right)$
217 ralunb ${⊢}\forall {y}\in \left({K}\cup \left\{1,{M}\right\}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔\left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\wedge \forall {y}\in \left\{1,{M}\right\}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\right)$
218 216 217 syl6bbr ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔\forall {y}\in \left({K}\cup \left\{1,{M}\right\}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\right)$
219 158 eqeq2d ${⊢}\left(\left({\phi }\wedge {c}\in {C}\right)\wedge {y}\in {K}\right)\to \left({b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔{b}\left({y}\right)={c}\left({y}\right)\right)$
220 219 ralbidva ${⊢}\left({\phi }\wedge {c}\in {C}\right)\to \left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={c}\left({y}\right)\right)$
221 220 adantrl ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={c}\left({y}\right)\right)$
222 61 adantr ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {K}\cup \left\{1,{M}\right\}=\left(1\dots {N}+1\right)$
223 222 raleqdv ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left(\forall {y}\in \left({K}\cup \left\{1,{M}\right\}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\right)$
224 218 221 223 3bitr3rd ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left(\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={c}\left({y}\right)\right)$
225 135 eqeq2d ${⊢}{y}\in {K}\to \left({c}\left({y}\right)=\left({{b}↾}_{{K}}\right)\left({y}\right)↔{c}\left({y}\right)={b}\left({y}\right)\right)$
226 eqcom ${⊢}{c}\left({y}\right)={b}\left({y}\right)↔{b}\left({y}\right)={c}\left({y}\right)$
227 225 226 syl6bb ${⊢}{y}\in {K}\to \left({c}\left({y}\right)=\left({{b}↾}_{{K}}\right)\left({y}\right)↔{b}\left({y}\right)={c}\left({y}\right)\right)$
228 227 ralbiia ${⊢}\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{c}\left({y}\right)=\left({{b}↾}_{{K}}\right)\left({y}\right)↔\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)={c}\left({y}\right)$
229 224 228 syl6bbr ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left(\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)↔\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{c}\left({y}\right)=\left({{b}↾}_{{K}}\right)\left({y}\right)\right)$
230 52 adantrr ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {b}Fn\left(1\dots {N}+1\right)$
231 157 adantrl ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right):\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)$
232 f1ofn ${⊢}\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right):\left(1\dots {N}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {N}+1\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)Fn\left(1\dots {N}+1\right)$
233 231 232 syl ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)Fn\left(1\dots {N}+1\right)$
234 eqfnfv ${⊢}\left({b}Fn\left(1\dots {N}+1\right)\wedge \left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)Fn\left(1\dots {N}+1\right)\right)\to \left({b}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}↔\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\right)$
235 230 233 234 syl2anc ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left({b}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}↔\forall {y}\in \left(1\dots {N}+1\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\left({c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}\right)\left({y}\right)\right)$
236 155 adantrl ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {c}:{K}\underset{1-1 onto}{⟶}{K}$
237 f1ofn ${⊢}{c}:{K}\underset{1-1 onto}{⟶}{K}\to {c}Fn{K}$
238 236 237 syl ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {c}Fn{K}$
239 127 adantr ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {K}\subseteq \left(1\dots {N}+1\right)$
240 fnssres ${⊢}\left({b}Fn\left(1\dots {N}+1\right)\wedge {K}\subseteq \left(1\dots {N}+1\right)\right)\to \left({{b}↾}_{{K}}\right)Fn{K}$
241 230 239 240 syl2anc ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left({{b}↾}_{{K}}\right)Fn{K}$
242 eqfnfv ${⊢}\left({c}Fn{K}\wedge \left({{b}↾}_{{K}}\right)Fn{K}\right)\to \left({c}={{b}↾}_{{K}}↔\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{c}\left({y}\right)=\left({{b}↾}_{{K}}\right)\left({y}\right)\right)$
243 238 241 242 syl2anc ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left({c}={{b}↾}_{{K}}↔\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{c}\left({y}\right)=\left({{b}↾}_{{K}}\right)\left({y}\right)\right)$
244 229 235 243 3bitr4d ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to \left({b}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}↔{c}={{b}↾}_{{K}}\right)$
245 244 ex ${⊢}{\phi }\to \left(\left({b}\in {B}\wedge {c}\in {C}\right)\to \left({b}={c}\cup \left\{⟨1,{M}⟩,⟨{M},1⟩\right\}↔{c}={{b}↾}_{{K}}\right)\right)$
246 19 28 142 203 245 en3d ${⊢}{\phi }\to {B}\approx {C}$
247 hashen ${⊢}\left({B}\in \mathrm{Fin}\wedge {C}\in \mathrm{Fin}\right)\to \left(\left|{B}\right|=\left|{C}\right|↔{B}\approx {C}\right)$
248 17 26 247 mp2an ${⊢}\left|{B}\right|=\left|{C}\right|↔{B}\approx {C}$
249 246 248 sylibr ${⊢}{\phi }\to \left|{B}\right|=\left|{C}\right|$
250 9 fveq2i ${⊢}\left|{C}\right|=\left|\left\{{f}|\left({f}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}\right|$
251 1 derangval ${⊢}{K}\in \mathrm{Fin}\to {D}\left({K}\right)=\left|\left\{{f}|\left({f}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}\right|$
252 23 251 ax-mp ${⊢}{D}\left({K}\right)=\left|\left\{{f}|\left({f}:{K}\underset{1-1 onto}{⟶}{K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\ne {y}\right)\right\}\right|$
253 1 2 derangen2 ${⊢}{K}\in \mathrm{Fin}\to {D}\left({K}\right)={S}\left(\left|{K}\right|\right)$
254 23 253 ax-mp ${⊢}{D}\left({K}\right)={S}\left(\left|{K}\right|\right)$
255 250 252 254 3eqtr2ri ${⊢}{S}\left(\left|{K}\right|\right)=\left|{C}\right|$
256 60 simp3d ${⊢}{\phi }\to \left|{K}\right|={N}-1$
257 256 fveq2d ${⊢}{\phi }\to {S}\left(\left|{K}\right|\right)={S}\left({N}-1\right)$
258 255 257 syl5eqr ${⊢}{\phi }\to \left|{C}\right|={S}\left({N}-1\right)$
259 249 258 eqtrd ${⊢}{\phi }\to \left|{B}\right|={S}\left({N}-1\right)$