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

Metamath Proof Explorer

Theorem subfacp1lem3

Proof