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	syl5bb	$⊢ 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	syl5eq	$⊢ φ \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	syl5eq	$⊢ φ \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		f1oeq1	$⊢ {b ↾}_{((1 \dots N + 1) ∖ \{1, M\})} = {b ↾}_{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	108 109	syl	$⊢ (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\})$
111		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\})$
112		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)$
113	110 111 112	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)$
114	107 113	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)$
115	98 114	mpbid	$⊢ (φ \land b \in B) \to ({b ↾}_{K}) : K \underset{1-1 onto}{⟶} K$
116		ssun1	$⊢ K \subseteq K \cup \{1, M\}$
117	116 52	sseqtrid	$⊢ φ \to K \subseteq (1 \dots N + 1)$
118	117	adantr	$⊢ (φ \land b \in B) \to K \subseteq (1 \dots N + 1)$
119	36	simprd	$⊢ (φ \land b \in B) \to \forall y \in (1 \dots N + 1) b (y) \neq y$
120		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)$
121	118 119 120	sylc	$⊢ (φ \land b \in B) \to \forall y \in K b (y) \neq y$
122	29	resex	$⊢ {b ↾}_{K} \in V$
123		f1oeq1	$⊢ f = {b ↾}_{K} \to (f : K \underset{1-1 onto}{⟶} K \leftrightarrow ({b ↾}_{K}) : K \underset{1-1 onto}{⟶} K)$
124		fveq1	$⊢ f = {b ↾}_{K} \to f (y) = ({b ↾}_{K}) (y)$
125		fvres	$⊢ y \in K \to ({b ↾}_{K}) (y) = b (y)$
126	124 125	sylan9eq	$⊢ (f = {b ↾}_{K} \land y \in K) \to f (y) = b (y)$
127	126	neeq1d	$⊢ (f = {b ↾}_{K} \land y \in K) \to (f (y) \neq y \leftrightarrow b (y) \neq y)$
128	127	ralbidva	$⊢ f = {b ↾}_{K} \to (\forall y \in K f (y) \neq y \leftrightarrow \forall y \in K b (y) \neq y)$
129	123 128	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))$
130	122 129 9	elab2	$⊢ {b ↾}_{K} \in C \leftrightarrow (({b ↾}_{K}) : K \underset{1-1 onto}{⟶} K \land \forall y \in K b (y) \neq y)$
131	115 121 130	sylanbrc	$⊢ (φ \land b \in B) \to {b ↾}_{K} \in C$
132	4	adantr	$⊢ (φ \land c \in C) \to N \in ℕ$
133	5	adantr	$⊢ (φ \land c \in C) \to M \in (2 \dots N + 1)$
134		eqid	$⊢ c \cup \{⟨1, M⟩, ⟨M, 1⟩\} = c \cup \{⟨1, M⟩, ⟨M, 1⟩\}$
135		simpr	$⊢ (φ \land c \in C) \to c \in C$
136		vex	$⊢ c \in V$
137		f1oeq1	$⊢ f = c \to (f : K \underset{1-1 onto}{⟶} K \leftrightarrow c : K \underset{1-1 onto}{⟶} K)$
138		fveq1	$⊢ f = c \to f (y) = c (y)$
139	138	neeq1d	$⊢ f = c \to (f (y) \neq y \leftrightarrow c (y) \neq y)$
140	139	ralbidv	$⊢ f = c \to (\forall y \in K f (y) \neq y \leftrightarrow \forall y \in K c (y) \neq y)$
141	137 140	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))$
142	136 141 9	elab2	$⊢ c \in C \leftrightarrow (c : K \underset{1-1 onto}{⟶} K \land \forall y \in K c (y) \neq y)$
143	135 142	sylib	$⊢ (φ \land c \in C) \to (c : K \underset{1-1 onto}{⟶} K \land \forall y \in K c (y) \neq y)$
144	143	simpld	$⊢ (φ \land c \in C) \to c : K \underset{1-1 onto}{⟶} K$
145	1 2 3 132 133 6 7 134 144	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)$
146	145	simp1d	$⊢ (φ \land c \in C) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
147	1 2 3 132 133 6 7 134 144	subfacp1lem2b	$⊢ ((φ \land c \in C) \land y \in K) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) = c (y)$
148	143	simprd	$⊢ (φ \land c \in C) \to \forall y \in K c (y) \neq y$
149	148	r19.21bi	$⊢ ((φ \land c \in C) \land y \in K) \to c (y) \neq y$
150	147 149	eqnetrd	$⊢ ((φ \land c \in C) \land y \in K) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y$
151	150	ralrimiva	$⊢ (φ \land c \in C) \to \forall y \in K (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y$
152	145	simp2d	$⊢ (φ \land c \in C) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M$
153		elfzuz	$⊢ M \in (2 \dots N + 1) \to M \in ℤ_{\geq 2}$
154		eluz2b3	$⊢ M \in ℤ_{\geq 2} \leftrightarrow (M \in ℕ \land M \neq 1)$
155	154	simprbi	$⊢ M \in ℤ_{\geq 2} \to M \neq 1$
156	5 153 155	3syl	$⊢ φ \to M \neq 1$
157	156	adantr	$⊢ (φ \land c \in C) \to M \neq 1$
158	152 157	eqnetrd	$⊢ (φ \land c \in C) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) \neq 1$
159	145	simp3d	$⊢ (φ \land c \in C) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1$
160	157	necomd	$⊢ (φ \land c \in C) \to 1 \neq M$
161	159 160	eqnetrd	$⊢ (φ \land c \in C) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) \neq M$
162		fveq2	$⊢ y = 1 \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1)$
163		id	$⊢ y = 1 \to y = 1$
164	162 163	neeq12d	$⊢ y = 1 \to ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) \neq 1)$
165		fveq2	$⊢ y = M \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M)$
166		id	$⊢ y = M \to y = M$
167	165 166	neeq12d	$⊢ y = M \to ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) \neq M)$
168	61 6 164 167	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)$
169	158 161 168	sylanbrc	$⊢ (φ \land c \in C) \to \forall y \in \{1, M\} (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y$
170		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)$
171	151 169 170	sylanbrc	$⊢ (φ \land c \in C) \to \forall y \in (K \cup \{1, M\}) (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y$
172	52	adantr	$⊢ (φ \land c \in C) \to K \cup \{1, M\} = (1 \dots N + 1)$
173	172	raleqdv	$⊢ (φ \land c \in C) \to (\forall y \in (K \cup \{1, M\}) (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y \leftrightarrow \forall y \in (1 \dots N + 1) (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y)$
174	171 173	mpbid	$⊢ (φ \land c \in C) \to \forall y \in (1 \dots N + 1) (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y$
175		prex	$⊢ \{⟨1, M⟩, ⟨M, 1⟩\} \in V$
176	136 175	unex	$⊢ c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \in V$
177		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))$
178		fveq1	$⊢ f = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to f (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y)$
179	178	neeq1d	$⊢ f = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to (f (y) \neq y \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \neq y)$
180	179	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)$
181	177 180	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))$
182	176 181 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)$
183	146 174 182	sylanbrc	$⊢ (φ \land c \in C) \to c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \in A$
184	152 159	jca	$⊢ (φ \land c \in C) \to ((c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M \land (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1)$
185		fveq1	$⊢ g = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to g (1) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1)$
186	185	eqeq1d	$⊢ g = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to (g (1) = M \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M)$
187		fveq1	$⊢ g = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to g (M) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M)$
188	187	eqeq1d	$⊢ g = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to (g (M) = 1 \leftrightarrow (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1)$
189	186 188	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))$
190	189 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))$
191	183 184 190	sylanbrc	$⊢ (φ \land c \in C) \to c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \in B$
192	57	adantrr	$⊢ (φ \land (b \in B \land c \in C)) \to b (1) = M$
193	152	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1) = M$
194	192 193	eqtr4d	$⊢ (φ \land (b \in B \land c \in C)) \to b (1) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1)$
195	60	adantrr	$⊢ (φ \land (b \in B \land c \in C)) \to b (M) = 1$
196	159	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M) = 1$
197	195 196	eqtr4d	$⊢ (φ \land (b \in B \land c \in C)) \to b (M) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M)$
198		fveq2	$⊢ y = 1 \to b (y) = b (1)$
199	198 162	eqeq12d	$⊢ y = 1 \to (b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow b (1) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (1))$
200		fveq2	$⊢ y = M \to b (y) = b (M)$
201	200 165	eqeq12d	$⊢ y = M \to (b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow b (M) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (M))$
202	61 6 199 201	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))$
203	194 197 202	sylanbrc	$⊢ (φ \land (b \in B \land c \in C)) \to \forall y \in \{1, M\} b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y)$
204	203	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)))$
205		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))$
206	204 205	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))$
207	147	eqeq2d	$⊢ ((φ \land c \in C) \land y \in K) \to (b (y) = (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) (y) \leftrightarrow b (y) = c (y))$
208	207	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))$
209	208	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))$
210	52	adantr	$⊢ (φ \land (b \in B \land c \in C)) \to K \cup \{1, M\} = (1 \dots N + 1)$
211	210	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))$
212	206 209 211	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))$
213	125	eqeq2d	$⊢ y \in K \to (c (y) = ({b ↾}_{K}) (y) \leftrightarrow c (y) = b (y))$
214		eqcom	$⊢ c (y) = b (y) \leftrightarrow b (y) = c (y)$
215	213 214	syl6bb	$⊢ y \in K \to (c (y) = ({b ↾}_{K}) (y) \leftrightarrow b (y) = c (y))$
216	215	ralbiia	$⊢ \forall y \in K c (y) = ({b ↾}_{K}) (y) \leftrightarrow \forall y \in K b (y) = c (y)$
217	212 216	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))$
218	43	adantrr	$⊢ (φ \land (b \in B \land c \in C)) \to b Fn (1 \dots N + 1)$
219	146	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)$
220		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)$
221	219 220	syl	$⊢ (φ \land (b \in B \land c \in C)) \to (c \cup \{⟨1, M⟩, ⟨M, 1⟩\}) Fn (1 \dots N + 1)$
222		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))$
223	218 221 222	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))$
224	144	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to c : K \underset{1-1 onto}{⟶} K$
225		f1ofn	$⊢ c : K \underset{1-1 onto}{⟶} K \to c Fn K$
226	224 225	syl	$⊢ (φ \land (b \in B \land c \in C)) \to c Fn K$
227	117	adantr	$⊢ (φ \land (b \in B \land c \in C)) \to K \subseteq (1 \dots N + 1)$
228	218 227	fnssresd	$⊢ (φ \land (b \in B \land c \in C)) \to ({b ↾}_{K}) Fn K$
229		eqfnfv	$⊢ (c Fn K \land ({b ↾}_{K}) Fn K) \to (c = {b ↾}_{K} \leftrightarrow \forall y \in K c (y) = ({b ↾}_{K}) (y))$
230	226 228 229	syl2anc	$⊢ (φ \land (b \in B \land c \in C)) \to (c = {b ↾}_{K} \leftrightarrow \forall y \in K c (y) = ({b ↾}_{K}) (y))$
231	217 223 230	3bitr4d	$⊢ (φ \land (b \in B \land c \in C)) \to (b = c \cup \{⟨1, M⟩, ⟨M, 1⟩\} \leftrightarrow c = {b ↾}_{K})$
232	19 131 191 231	f1o2d	$⊢ φ \to (b \in B ⟼ {b ↾}_{K}) : B \underset{1-1 onto}{⟶} C$
233	18 232	hasheqf1od	$⊢ φ \to \|B\| = \|C\|$
234	9	fveq2i	$⊢ \|C\| = \|\{f \| (f : K \underset{1-1 onto}{⟶} K \land \forall y \in K f (y) \neq y)\}\|$
235		fzfi	$⊢ (2 \dots N + 1) \in Fin$
236		diffi	$⊢ (2 \dots N + 1) \in Fin \to (2 \dots N + 1) ∖ \{M\} \in Fin$
237	235 236	ax-mp	$⊢ (2 \dots N + 1) ∖ \{M\} \in Fin$
238	7 237	eqeltri	$⊢ K \in Fin$
239	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)\}\|$
240	238 239	ax-mp	$⊢ D (K) = \|\{f \| (f : K \underset{1-1 onto}{⟶} K \land \forall y \in K f (y) \neq y)\}\|$
241	1 2	derangen2	$⊢ K \in Fin \to D (K) = S (\|K\|)$
242	238 241	ax-mp	$⊢ D (K) = S (\|K\|)$
243	234 240 242	3eqtr2ri	$⊢ S (\|K\|) = \|C\|$
244	51	simp3d	$⊢ φ \to \|K\| = N - 1$
245	244	fveq2d	$⊢ φ \to S (\|K\|) = S (N - 1)$
246	243 245	syl5eqr	$⊢ φ \to \|C\| = S (N - 1)$
247	233 246	eqtrd	$⊢ φ \to \|B\| = S (N - 1)$

Metamath Proof Explorer

Theorem subfacp1lem3

Proof