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 = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
	subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
	subfacp1lem.a	$⊢ A = \{f \| (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y)\}$
	subfacp1lem1.n	$⊢ φ \to N \in ℕ$
	subfacp1lem1.m	$⊢ φ \to M \in (2 \dots N + 1)$
	subfacp1lem1.x	$⊢ M \in V$
	subfacp1lem1.k	$⊢ K = (2 \dots N + 1) ∖ \{M\}$
	subfacp1lem3.b	$⊢ B = \{g \in A \| (g (1) = M \land g (M) = 1)\}$
	subfacp1lem3.c	$⊢ C = \{f \| (f : K \underset{1-1 onto}{⟶} K \land \forall y \in K f (y) \neq y)\}$
Assertion	subfacp1lem3	$⊢ φ \to \|B\| = S (N - 1)$

Proof

Step	Hyp	Ref	Expression
1		derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
2		subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
3		subfacp1lem.a	$⊢ A = \{f \| (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y)\}$
4		subfacp1lem1.n	$⊢ φ \to N \in ℕ$
5		subfacp1lem1.m	$⊢ φ \to M \in (2 \dots N + 1)$
6		subfacp1lem1.x	$⊢ M \in V$
7		subfacp1lem1.k	$⊢ K = (2 \dots N + 1) ∖ \{M\}$
8		subfacp1lem3.b	$⊢ B = \{g \in A \| (g (1) = M \land g (M) = 1)\}$
9		subfacp1lem3.c	$⊢ C = \{f \| (f : K \underset{1-1 onto}{⟶} K \land \forall y \in K f (y) \neq y)\}$
10		fzfi	$⊢ (1 \dots N + 1) \in Fin$
11		deranglem	$⊢ (1 \dots N + 1) \in Fin \to \{f \| (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y)\} \in Fin$
12	10 11	ax-mp	$⊢ \{f \| (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y)\} \in Fin$
13	3 12	eqeltri	$⊢ A \in Fin$
14	8	ssrab3	$⊢ B \subseteq A$
15		ssfi	$⊢ (A \in Fin \land B \subseteq A) \to B \in Fin$
16	13 14 15	mp2an	$⊢ B \in Fin$
17	16	elexi	$⊢ B \in V$
18	17	a1i	$⊢ φ \to B \in V$
19		eqid	$⊢ (b \in B ⟼ {b ↾}_{K}) = (b \in B ⟼ {b ↾}_{K})$
20		simpr	$⊢ (φ \land b \in B) \to b \in B$
21		fveq1	$⊢ g = b \to g (1) = b (1)$
22	21	eqeq1d	$⊢ g = b \to (g (1) = M \leftrightarrow b (1) = M)$
23		fveq1	$⊢ g = b \to g (M) = b (M)$
24	23	eqeq1d	$⊢ g = b \to (g (M) = 1 \leftrightarrow b (M) = 1)$
25	22 24	anbi12d	$⊢ g = b \to ((g (1) = M \land g (M) = 1) \leftrightarrow (b (1) = M \land b (M) = 1))$
26	25 8	elrab2	$⊢ b \in B \leftrightarrow (b \in A \land (b (1) = M \land b (M) = 1))$
27	20 26	sylib	$⊢ (φ \land b \in B) \to (b \in A \land (b (1) = M \land b (M) = 1))$
28	27	simpld	$⊢ (φ \land b \in B) \to b \in A$
29		vex	$⊢ b \in V$
30		f1oeq1	$⊢ f = b \to (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \leftrightarrow b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
31		fveq1	$⊢ f = b \to f (y) = b (y)$
32	31	neeq1d	$⊢ f = b \to (f (y) \neq y \leftrightarrow b (y) \neq y)$
33	32	ralbidv	$⊢ f = b \to (\forall y \in (1 \dots N + 1) f (y) \neq y \leftrightarrow \forall y \in (1 \dots N + 1) b (y) \neq y)$
34	30 33	anbi12d	$⊢ f = b \to ((f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y) \leftrightarrow (b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) b (y) \neq y))$
35	29 34 3	elab2	$⊢ b \in A \leftrightarrow (b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) b (y) \neq y)$
36	28 35	sylib	$⊢ (φ \land b \in B) \to (b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) b (y) \neq y)$
37	36	simpld	$⊢ (φ \land b \in B) \to b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
38		f1of1	$⊢ b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to b : (1 \dots N + 1) \underset{1-1}{⟶} (1 \dots N + 1)$
39		df-f1	$⊢ b : (1 \dots N + 1) \underset{1-1}{⟶} (1 \dots N + 1) \leftrightarrow (b : (1 \dots N + 1) ⟶ (1 \dots N + 1) \land Fun b^{-1})$
40	39	simprbi	$⊢ b : (1 \dots N + 1) \underset{1-1}{⟶} (1 \dots N + 1) \to Fun b^{-1}$
41	37 38 40	3syl	$⊢ (φ \land b \in B) \to Fun b^{-1}$
42		f1ofn	$⊢ b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to b Fn (1 \dots N + 1)$
43	37 42	syl	$⊢ (φ \land b \in B) \to b Fn (1 \dots N + 1)$
44		fnresdm	$⊢ b Fn (1 \dots N + 1) \to {b ↾}_{(1 \dots N + 1)} = b$
45		f1oeq1	$⊢ {b ↾}_{(1 \dots N + 1)} = b \to (({b ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \leftrightarrow b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
46	43 44 45	3syl	$⊢ (φ \land b \in B) \to (({b ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \leftrightarrow b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
47	37 46	mpbird	$⊢ (φ \land b \in B) \to ({b ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
48		f1ofo	$⊢ ({b ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to ({b ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{onto}{⟶} (1 \dots N + 1)$
49	47 48	syl	$⊢ (φ \land b \in B) \to ({b ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{onto}{⟶} (1 \dots N + 1)$
50		ssun2	$⊢ \{1, M\} \subseteq K \cup \{1, M\}$
51	1 2 3 4 5 6 7	subfacp1lem1	$⊢ φ \to (K \cap \{1, M\} = \emptyset \land K \cup \{1, M\} = (1 \dots N + 1) \land \|K\| = N - 1)$
52	51	simp2d	$⊢ φ \to K \cup \{1, M\} = (1 \dots N + 1)$
53	50 52	sseqtrid	$⊢ φ \to \{1, M\} \subseteq (1 \dots N + 1)$
54	53	adantr	$⊢ (φ \land b \in B) \to \{1, M\} \subseteq (1 \dots N + 1)$
55	43 54	fnssresd	$⊢ (φ \land b \in B) \to ({b ↾}_{\{1, M\}}) Fn \{1, M\}$
56	27	simprd	$⊢ (φ \land b \in B) \to (b (1) = M \land b (M) = 1)$
57	56	simpld	$⊢ (φ \land b \in B) \to b (1) = M$
58	6	prid2	$⊢ M \in \{1, M\}$
59	57 58	eqeltrdi	$⊢ (φ \land b \in B) \to b (1) \in \{1, M\}$
60	56	simprd	$⊢ (φ \land b \in B) \to b (M) = 1$
61		1ex	$⊢ 1 \in V$
62	61	prid1	$⊢ 1 \in \{1, M\}$
63	60 62	eqeltrdi	$⊢ (φ \land b \in B) \to b (M) \in \{1, M\}$
64		fveq2	$⊢ x = 1 \to b (x) = b (1)$
65	64	eleq1d	$⊢ x = 1 \to (b (x) \in \{1, M\} \leftrightarrow b (1) \in \{1, M\})$
66		fveq2	$⊢ x = M \to b (x) = b (M)$
67	66	eleq1d	$⊢ x = M \to (b (x) \in \{1, M\} \leftrightarrow b (M) \in \{1, M\})$
68	61 6 65 67	ralpr	$⊢ \forall x \in \{1, M\} b (x) \in \{1, M\} \leftrightarrow (b (1) \in \{1, M\} \land b (M) \in \{1, M\})$
69	59 63 68	sylanbrc	$⊢ (φ \land b \in B) \to \forall x \in \{1, M\} b (x) \in \{1, M\}$
70		fvres	$⊢ x \in \{1, M\} \to ({b ↾}_{\{1, M\}}) (x) = b (x)$
71	70	eleq1d	$⊢ x \in \{1, M\} \to (({b ↾}_{\{1, M\}}) (x) \in \{1, M\} \leftrightarrow b (x) \in \{1, M\})$
72	71	ralbiia	$⊢ \forall x \in \{1, M\} ({b ↾}_{\{1, M\}}) (x) \in \{1, M\} \leftrightarrow \forall x \in \{1, M\} b (x) \in \{1, M\}$
73	69 72	sylibr	$⊢ (φ \land b \in B) \to \forall x \in \{1, M\} ({b ↾}_{\{1, M\}}) (x) \in \{1, M\}$
74		ffnfv	$⊢ ({b ↾}_{\{1, M\}}) : \{1, M\} ⟶ \{1, M\} \leftrightarrow (({b ↾}_{\{1, M\}}) Fn \{1, M\} \land \forall x \in \{1, M\} ({b ↾}_{\{1, M\}}) (x) \in \{1, M\})$
75	55 73 74	sylanbrc	$⊢ (φ \land b \in B) \to ({b ↾}_{\{1, M\}}) : \{1, M\} ⟶ \{1, M\}$
76		fveqeq2	$⊢ y = M \to (b (y) = 1 \leftrightarrow b (M) = 1)$
77	76	rspcev	$⊢ (M \in \{1, M\} \land b (M) = 1) \to \exists y \in \{1, M\} b (y) = 1$
78	58 60 77	sylancr	$⊢ (φ \land b \in B) \to \exists y \in \{1, M\} b (y) = 1$
79		fveqeq2	$⊢ y = 1 \to (b (y) = M \leftrightarrow b (1) = M)$
80	79	rspcev	$⊢ (1 \in \{1, M\} \land b (1) = M) \to \exists y \in \{1, M\} b (y) = M$
81	62 57 80	sylancr	$⊢ (φ \land b \in B) \to \exists y \in \{1, M\} b (y) = M$
82		eqeq2	$⊢ x = 1 \to (b (y) = x \leftrightarrow b (y) = 1)$
83	82	rexbidv	$⊢ x = 1 \to (\exists y \in \{1, M\} b (y) = x \leftrightarrow \exists y \in \{1, M\} b (y) = 1)$
84		eqeq2	$⊢ x = M \to (b (y) = x \leftrightarrow b (y) = M)$
85	84	rexbidv	$⊢ x = M \to (\exists y \in \{1, M\} b (y) = x \leftrightarrow \exists y \in \{1, M\} b (y) = M)$
86	61 6 83 85	ralpr	$⊢ \forall x \in \{1, M\} \exists y \in \{1, M\} b (y) = x \leftrightarrow (\exists y \in \{1, M\} b (y) = 1 \land \exists y \in \{1, M\} b (y) = M)$
87	78 81 86	sylanbrc	$⊢ (φ \land b \in B) \to \forall x \in \{1, M\} \exists y \in \{1, M\} b (y) = x$
88		eqcom	$⊢ x = ({b ↾}_{\{1, M\}}) (y) \leftrightarrow ({b ↾}_{\{1, M\}}) (y) = x$
89		fvres	$⊢ y \in \{1, M\} \to ({b ↾}_{\{1, M\}}) (y) = b (y)$
90	89	eqeq1d	$⊢ y \in \{1, M\} \to (({b ↾}_{\{1, M\}}) (y) = x \leftrightarrow b (y) = x)$
91	88 90	bitrid	$⊢ y \in \{1, M\} \to (x = ({b ↾}_{\{1, M\}}) (y) \leftrightarrow b (y) = x)$
92	91	rexbiia	$⊢ \exists y \in \{1, M\} x = ({b ↾}_{\{1, M\}}) (y) \leftrightarrow \exists y \in \{1, M\} b (y) = x$
93	92	ralbii	$⊢ \forall x \in \{1, M\} \exists y \in \{1, M\} x = ({b ↾}_{\{1, M\}}) (y) \leftrightarrow \forall x \in \{1, M\} \exists y \in \{1, M\} b (y) = x$
94	87 93	sylibr	$⊢ (φ \land b \in B) \to \forall x \in \{1, M\} \exists y \in \{1, M\} x = ({b ↾}_{\{1, M\}}) (y)$
95		dffo3	$⊢ ({b ↾}_{\{1, M\}}) : \{1, M\} \underset{onto}{⟶} \{1, M\} \leftrightarrow (({b ↾}_{\{1, M\}}) : \{1, M\} ⟶ \{1, M\} \land \forall x \in \{1, M\} \exists y \in \{1, M\} x = ({b ↾}_{\{1, M\}}) (y))$
96	75 94 95	sylanbrc	$⊢ (φ \land b \in B) \to ({b ↾}_{\{1, M\}}) : \{1, M\} \underset{onto}{⟶} \{1, M\}$
97		resdif	$⊢ (Fun b^{-1} \land ({b ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{onto}{⟶} (1 \dots N + 1) \land ({b ↾}_{\{1, M\}}) : \{1, M\} \underset{onto}{⟶} \{1, M\}) \to ({b ↾}_{((1 \dots N + 1) ∖ \{1, M\})}) : (1 \dots N + 1) ∖ \{1, M\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1, M\}$
98	41 49 96 97	syl3anc	$⊢ (φ \land b \in B) \to ({b ↾}_{((1 \dots N + 1) ∖ \{1, M\})}) : (1 \dots N + 1) ∖ \{1, M\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1, M\}$
99		uncom	$⊢ \{1, M\} \cup K = K \cup \{1, M\}$
100	99 52	eqtrid	$⊢ φ \to \{1, M\} \cup K = (1 \dots N + 1)$
101		incom	$⊢ \{1, M\} \cap K = K \cap \{1, M\}$
102	51	simp1d	$⊢ φ \to K \cap \{1, M\} = \emptyset$
103	101 102	eqtrid	$⊢ φ \to \{1, M\} \cap K = \emptyset$
104		uneqdifeq	$⊢ (\{1, M\} \subseteq (1 \dots N + 1) \land \{1, M\} \cap K = \emptyset) \to (\{1, M\} \cup K = (1 \dots N + 1) \leftrightarrow (1 \dots N + 1) ∖ \{1, M\} = K)$
105	53 103 104	syl2anc	$⊢ φ \to (\{1, M\} \cup K = (1 \dots N + 1) \leftrightarrow (1 \dots N + 1) ∖ \{1, M\} = K)$
106	100 105	mpbid	$⊢ φ \to (1 \dots N + 1) ∖ \{1, M\} = K$
107	106	adantr	$⊢ (φ \land b \in B) \to (1 \dots N + 1) ∖ \{1, M\} = K$
108		reseq2	$⊢ (1 \dots N + 1) ∖ \{1, M\} = K \to {b ↾}_{((1 \dots N + 1) ∖ \{1, M\})} = {b ↾}_{K}$
109	108	f1oeq1d	$⊢ (1 \dots N + 1) ∖ \{1, M\} = K \to (({b ↾}_{((1 \dots N + 1) ∖ \{1, M\})}) : (1 \dots N + 1) ∖ \{1, M\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1, M\} \leftrightarrow ({b ↾}_{K}) : (1 \dots N + 1) ∖ \{1, M\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1, M\})$
110		f1oeq2	$⊢ (1 \dots N + 1) ∖ \{1, M\} = K \to (({b ↾}_{K}) : (1 \dots N + 1) ∖ \{1, M\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1, M\} \leftrightarrow ({b ↾}_{K}) : K \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1, M\})$
111		f1oeq3	$⊢ (1 \dots N + 1) ∖ \{1, M\} = K \to (({b ↾}_{K}) : K \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1, M\} \leftrightarrow ({b ↾}_{K}) : K \underset{1-1 onto}{⟶} K)$
112	109 110 111	3bitrd	$⊢ (1 \dots N + 1) ∖ \{1, M\} = K \to (({b ↾}_{((1 \dots N + 1) ∖ \{1, M\})}) : (1 \dots N + 1) ∖ \{1, M\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1, M\} \leftrightarrow ({b ↾}_{K}) : K \underset{1-1 onto}{⟶} K)$
113	107 112	syl	$⊢ (φ \land b \in B) \to (({b ↾}_{((1 \dots N + 1) ∖ \{1, M\})}) : (1 \dots N + 1) ∖ \{1, M\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1, M\} \leftrightarrow ({b ↾}_{K}) : K \underset{1-1 onto}{⟶} K)$
114	98 113	mpbid	$⊢ (φ \land b \in B) \to ({b ↾}_{K}) : K \underset{1-1 onto}{⟶} K$
115		ssun1	$⊢ K \subseteq K \cup \{1, M\}$
116	115 52	sseqtrid	$⊢ φ \to K \subseteq (1 \dots N + 1)$
117	116	adantr	$⊢ (φ \land b \in B) \to K \subseteq (1 \dots N + 1)$
118	36	simprd	$⊢ (φ \land b \in B) \to \forall y \in (1 \dots N + 1) b (y) \neq y$
119		ssralv	$⊢ K \subseteq (1 \dots N + 1) \to (\forall y \in (1 \dots N + 1) b (y) \neq y \to \forall y \in K b (y) \neq y)$
120	117 118 119	sylc	$⊢ (φ \land b \in B) \to \forall y \in K b (y) \neq y$
121	29	resex	$⊢ {b ↾}_{K} \in V$
122		f1oeq1	$⊢ f = {b ↾}_{K} \to (f : K \underset{1-1 onto}{⟶} K \leftrightarrow ({b ↾}_{K}) : K \underset{1-1 onto}{⟶} K)$
123		fveq1	$⊢ f = {b ↾}_{K} \to f (y) = ({b ↾}_{K}) (y)$
124		fvres	$⊢ y \in K \to ({b ↾}_{K}) (y) = b (y)$
125	123 124	sylan9eq	$⊢ (f = {b ↾}_{K} \land y \in K) \to f (y) = b (y)$
126	125	neeq1d	$⊢ (f = {b ↾}_{K} \land y \in K) \to (f (y) \neq y \leftrightarrow b (y) \neq y)$
127	126	ralbidva	$⊢ f = {b ↾}_{K} \to (\forall y \in K f (y) \neq y \leftrightarrow \forall y \in K b (y) \neq y)$
128	122 127	anbi12d	$⊢ f = {b ↾}_{K} \to ((f : K \underset{1-1 onto}{⟶} K \land \forall y \in K f (y) \neq y) \leftrightarrow (({b ↾}_{K}) : K \underset{1-1 onto}{⟶} K \land \forall y \in K b (y) \neq y))$
129	121 128 9	elab2	$⊢ {b ↾}_{K} \in C \leftrightarrow (({b ↾}_{K}) : K \underset{1-1 onto}{⟶} K \land \forall y \in K b (y) \neq y)$
130	114 120 129	sylanbrc	$⊢ (φ \land b \in B) \to {b ↾}_{K} \in C$
131	4	adantr	$⊢ (φ \land c \in C) \to N \in ℕ$
132	5	adantr	$⊢ (φ \land c \in C) \to M \in (2 \dots N + 1)$
133		eqid	$⊢ c \cup \{⟨1, M⟩, ⟨M, 1⟩\} = c \cup \{⟨1, M⟩, ⟨M, 1⟩\}$
134		simpr	$⊢ (φ \land c \in C) \to c \in C$
135		vex	$⊢ c \in V$
136		f1oeq1	$⊢ f = c \to (f : K \underset{1-1 onto}{⟶} K \leftrightarrow c : K \underset{1-1 onto}{⟶} K)$
137		fveq1	$⊢ f = c \to f (y) = c (y)$
138	137	neeq1d	$⊢ f = c \to (f (y) \neq y \leftrightarrow c (y) \neq y)$
139	138	ralbidv	$⊢ f = c \to (\forall y \in K f (y) \neq y \leftrightarrow \forall y \in K c (y) \neq y)$
140	136 139	anbi12d	$⊢ f = c \to ((f : K \underset{1-1 onto}{⟶} K \land \forall y \in K f (y) \neq y) \leftrightarrow (c : K \underset{1-1 onto}{⟶} K \land \forall y \in K c (y) \neq y))$
141	135 140 9	elab2	$⊢ c \in C \leftrightarrow (c : K \underset{1-1 onto}{⟶} K \land \forall y \in K c (y) \neq y)$
142	134 141	sylib	$⊢ (φ \land c \in C) \to (c : K \underset{1-1 onto}{⟶} K \land \forall y \in K c (y) \neq y)$
143	142	simpld	$⊢ (φ \land c \in C) \to c : K \underset{1-1 onto}{⟶} K$
144	1 2 3 131 132 6 7 133 143	subfacp1lem2a	$⊢ (φ \land c \in C) \to ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M \land (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1)$
145	144	simp1d	$⊢ (φ \land c \in C) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
146	1 2 3 131 132 6 7 133 143	subfacp1lem2b	$⊢ ((φ \land c \in C) \land y \in K) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) = c (y)$
147	142	simprd	$⊢ (φ \land c \in C) \to \forall y \in K c (y) \neq y$
148	147	r19.21bi	$⊢ ((φ \land c \in C) \land y \in K) \to c (y) \neq y$
149	146 148	eqnetrd	$⊢ ((φ \land c \in C) \land y \in K) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y$
150	149	ralrimiva	$⊢ (φ \land c \in C) \to \forall y \in K (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y$
151	144	simp2d	$⊢ (φ \land c \in C) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M$
152		elfzuz	$⊢ M \in (2 \dots N + 1) \to M \in ℤ_{\geq 2}$
153		eluz2b3	$⊢ M \in ℤ_{\geq 2} \leftrightarrow (M \in ℕ \land M \neq 1)$
154	153	simprbi	$⊢ M \in ℤ_{\geq 2} \to M \neq 1$
155	5 152 154	3syl	$⊢ φ \to M \neq 1$
156	155	adantr	$⊢ (φ \land c \in C) \to M \neq 1$
157	151 156	eqnetrd	$⊢ (φ \land c \in C) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) \neq 1$
158	144	simp3d	$⊢ (φ \land c \in C) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1$
159	156	necomd	$⊢ (φ \land c \in C) \to 1 \neq M$
160	158 159	eqnetrd	$⊢ (φ \land c \in C) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) \neq M$
161		fveq2	$⊢ y = 1 \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1)$
162		id	$⊢ y = 1 \to y = 1$
163	161 162	neeq12d	$⊢ y = 1 \to ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) \neq 1)$
164		fveq2	$⊢ y = M \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M)$
165		id	$⊢ y = M \to y = M$
166	164 165	neeq12d	$⊢ y = M \to ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) \neq M)$
167	61 6 163 166	ralpr	$⊢ \forall y \in \{1, M\} (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y \leftrightarrow ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) \neq 1 \land (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) \neq M)$
168	157 160 167	sylanbrc	$⊢ (φ \land c \in C) \to \forall y \in \{1, M\} (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y$
169		ralunb	$⊢ \forall y \in (K \cup \{1, M\}) (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y \leftrightarrow (\forall y \in K (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y \land \forall y \in \{1, M\} (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y)$
170	150 168 169	sylanbrc	$⊢ (φ \land c \in C) \to \forall y \in (K \cup \{1, M\}) (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y$
171	52	adantr	$⊢ (φ \land c \in C) \to K \cup \{1, M\} = (1 \dots N + 1)$
172	170 171	raleqtrdv	$⊢ (φ \land c \in C) \to \forall y \in (1 \dots N + 1) (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y$
173		prex	$⊢ \{⟨1, M⟩, ⟨M, 1⟩\} \in V$
174	135 173	unex	$⊢ c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \in V$
175		f1oeq1	$⊢ f = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
176		fveq1	$⊢ f = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to f (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y)$
177	176	neeq1d	$⊢ f = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to (f (y) \neq y \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y)$
178	177	ralbidv	$⊢ f = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to (\forall y \in (1 \dots N + 1) f (y) \neq y \leftrightarrow \forall y \in (1 \dots N + 1) (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y)$
179	175 178	anbi12d	$⊢ f = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to ((f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y) \leftrightarrow ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y))$
180	174 179 3	elab2	$⊢ c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \in A \leftrightarrow ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y)$
181	145 172 180	sylanbrc	$⊢ (φ \land c \in C) \to c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \in A$
182	151 158	jca	$⊢ (φ \land c \in C) \to ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M \land (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1)$
183		fveq1	$⊢ g = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to g (1) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1)$
184	183	eqeq1d	$⊢ g = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to (g (1) = M \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M)$
185		fveq1	$⊢ g = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to g (M) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M)$
186	185	eqeq1d	$⊢ g = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to (g (M) = 1 \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1)$
187	184 186	anbi12d	$⊢ g = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to ((g (1) = M \land g (M) = 1) \leftrightarrow ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M \land (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1))$
188	187 8	elrab2	$⊢ c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \in B \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \in A \land ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M \land (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1))$
189	181 182 188	sylanbrc	$⊢ (φ \land c \in C) \to c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \in B$
190	57	adantrr	$⊢ (φ \land (b \in B \land c \in C)) \to b (1) = M$
191	151	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M$
192	190 191	eqtr4d	$⊢ (φ \land (b \in B \land c \in C)) \to b (1) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1)$
193	60	adantrr	$⊢ (φ \land (b \in B \land c \in C)) \to b (M) = 1$
194	158	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1$
195	193 194	eqtr4d	$⊢ (φ \land (b \in B \land c \in C)) \to b (M) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M)$
196		fveq2	$⊢ y = 1 \to b (y) = b (1)$
197	196 161	eqeq12d	$⊢ y = 1 \to (b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow b (1) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1))$
198		fveq2	$⊢ y = M \to b (y) = b (M)$
199	198 164	eqeq12d	$⊢ y = M \to (b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow b (M) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M))$
200	61 6 197 199	ralpr	$⊢ \forall y \in \{1, M\} b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow (b (1) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) \land b (M) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M))$
201	192 195 200	sylanbrc	$⊢ (φ \land (b \in B \land c \in C)) \to \forall y \in \{1, M\} b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y)$
202	201	biantrud	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in K b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow (\forall y \in K b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \land \forall y \in \{1, M\} b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y)))$
203		ralunb	$⊢ \forall y \in (K \cup \{1, M\}) b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow (\forall y \in K b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \land \forall y \in \{1, M\} b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y))$
204	202 203	bitr4di	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in K b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow \forall y \in (K \cup \{1, M\}) b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y))$
205	146	eqeq2d	$⊢ ((φ \land c \in C) \land y \in K) \to (b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow b (y) = c (y))$
206	205	ralbidva	$⊢ (φ \land c \in C) \to (\forall y \in K b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow \forall y \in K b (y) = c (y))$
207	206	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in K b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow \forall y \in K b (y) = c (y))$
208	52	adantr	$⊢ (φ \land (b \in B \land c \in C)) \to K \cup \{1, M\} = (1 \dots N + 1)$
209	208	raleqdv	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in (K \cup \{1, M\}) b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow \forall y \in (1 \dots N + 1) b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y))$
210	204 207 209	3bitr3rd	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in (1 \dots N + 1) b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow \forall y \in K b (y) = c (y))$
211	124	eqeq2d	$⊢ y \in K \to (c (y) = ({b ↾}_{K}) (y) \leftrightarrow c (y) = b (y))$
212		eqcom	$⊢ c (y) = b (y) \leftrightarrow b (y) = c (y)$
213	211 212	bitrdi	$⊢ y \in K \to (c (y) = ({b ↾}_{K}) (y) \leftrightarrow b (y) = c (y))$
214	213	ralbiia	$⊢ \forall y \in K c (y) = ({b ↾}_{K}) (y) \leftrightarrow \forall y \in K b (y) = c (y)$
215	210 214	bitr4di	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in (1 \dots N + 1) b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow \forall y \in K c (y) = ({b ↾}_{K}) (y))$
216	43	adantrr	$⊢ (φ \land (b \in B \land c \in C)) \to b Fn (1 \dots N + 1)$
217	145	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
218		f1ofn	$⊢ (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) Fn (1 \dots N + 1)$
219	217 218	syl	$⊢ (φ \land (b \in B \land c \in C)) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) Fn (1 \dots N + 1)$
220		eqfnfv	$⊢ (b Fn (1 \dots N + 1) \land (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) Fn (1 \dots N + 1)) \to (b = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \leftrightarrow \forall y \in (1 \dots N + 1) b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y))$
221	216 219 220	syl2anc	$⊢ (φ \land (b \in B \land c \in C)) \to (b = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \leftrightarrow \forall y \in (1 \dots N + 1) b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y))$
222	143	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to c : K \underset{1-1 onto}{⟶} K$
223		f1ofn	$⊢ c : K \underset{1-1 onto}{⟶} K \to c Fn K$
224	222 223	syl	$⊢ (φ \land (b \in B \land c \in C)) \to c Fn K$
225	116	adantr	$⊢ (φ \land (b \in B \land c \in C)) \to K \subseteq (1 \dots N + 1)$
226	216 225	fnssresd	$⊢ (φ \land (b \in B \land c \in C)) \to ({b ↾}_{K}) Fn K$
227		eqfnfv	$⊢ (c Fn K \land ({b ↾}_{K}) Fn K) \to (c = {b ↾}_{K} \leftrightarrow \forall y \in K c (y) = ({b ↾}_{K}) (y))$
228	224 226 227	syl2anc	$⊢ (φ \land (b \in B \land c \in C)) \to (c = {b ↾}_{K} \leftrightarrow \forall y \in K c (y) = ({b ↾}_{K}) (y))$
229	215 221 228	3bitr4d	$⊢ (φ \land (b \in B \land c \in C)) \to (b = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \leftrightarrow c = {b ↾}_{K})$
230	19 130 189 229	f1o2d	$⊢ φ \to (b \in B ⟼ {b ↾}_{K}) : B \underset{1-1 onto}{⟶} C$
231	18 230	hasheqf1od	$⊢ φ \to \|B\| = \|C\|$
232	9	fveq2i	$⊢ \|C\| = \|\{f \| (f : K \underset{1-1 onto}{⟶} K \land \forall y \in K f (y) \neq y)\}\|$
233		fzfi	$⊢ (2 \dots N + 1) \in Fin$
234		diffi	$⊢ (2 \dots N + 1) \in Fin \to (2 \dots N + 1) ∖ \{M\} \in Fin$
235	233 234	ax-mp	$⊢ (2 \dots N + 1) ∖ \{M\} \in Fin$
236	7 235	eqeltri	$⊢ K \in Fin$
237	1	derangval	$⊢ K \in Fin \to D (K) = \|\{f \| (f : K \underset{1-1 onto}{⟶} K \land \forall y \in K f (y) \neq y)\}\|$
238	236 237	ax-mp	$⊢ D (K) = \|\{f \| (f : K \underset{1-1 onto}{⟶} K \land \forall y \in K f (y) \neq y)\}\|$
239	1 2	derangen2	$⊢ K \in Fin \to D (K) = S (\|K\|)$
240	236 239	ax-mp	$⊢ D (K) = S (\|K\|)$
241	232 238 240	3eqtr2ri	$⊢ S (\|K\|) = \|C\|$
242	51	simp3d	$⊢ φ \to \|K\| = N - 1$
243	242	fveq2d	$⊢ φ \to S (\|K\|) = S (N - 1)$
244	241 243	eqtr3id	$⊢ φ \to \|C\| = S (N - 1)$
245	231 244	eqtrd	$⊢ φ \to \|B\| = S (N - 1)$

Metamath Proof Explorer

Theorem subfacp1lem3

Proof