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

Metamath Proof Explorer

Theorem subfacp1lem3

Proof