subfacp1lem1

Description: Lemma for subfacp1 . The set K together with { 1 , M } partitions the set 1 ... ( N + 1 ) . (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\}$
Assertion	subfacp1lem1	$⊢ φ \to (K \cap \{1, M\} = \emptyset \land K \cup \{1, M\} = (1 \dots N + 1) \land \|K\| = 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		disj	$⊢ K \cap \{1, M\} = \emptyset \leftrightarrow \forall x \in K \neg x \in \{1, M\}$
9		eldifi	$⊢ x \in ((2 \dots N + 1) ∖ \{M\}) \to x \in (2 \dots N + 1)$
10		elfzle1	$⊢ x \in (2 \dots N + 1) \to 2 \leq x$
11		1lt2	$⊢ 1 < 2$
12		1re	$⊢ 1 \in ℝ$
13		2re	$⊢ 2 \in ℝ$
14	12 13	ltnlei	$⊢ 1 < 2 \leftrightarrow \neg 2 \leq 1$
15	11 14	mpbi	$⊢ \neg 2 \leq 1$
16		breq2	$⊢ x = 1 \to (2 \leq x \leftrightarrow 2 \leq 1)$
17	15 16	mtbiri	$⊢ x = 1 \to \neg 2 \leq x$
18	17	necon2ai	$⊢ 2 \leq x \to x \neq 1$
19	9 10 18	3syl	$⊢ x \in ((2 \dots N + 1) ∖ \{M\}) \to x \neq 1$
20		eldifsni	$⊢ x \in ((2 \dots N + 1) ∖ \{M\}) \to x \neq M$
21	19 20	jca	$⊢ x \in ((2 \dots N + 1) ∖ \{M\}) \to (x \neq 1 \land x \neq M)$
22	21 7	eleq2s	$⊢ x \in K \to (x \neq 1 \land x \neq M)$
23		neanior	$⊢ (x \neq 1 \land x \neq M) \leftrightarrow \neg (x = 1 \lor x = M)$
24	22 23	sylib	$⊢ x \in K \to \neg (x = 1 \lor x = M)$
25		vex	$⊢ x \in V$
26	25	elpr	$⊢ x \in \{1, M\} \leftrightarrow (x = 1 \lor x = M)$
27	24 26	sylnibr	$⊢ x \in K \to \neg x \in \{1, M\}$
28	8 27	mprgbir	$⊢ K \cap \{1, M\} = \emptyset$
29	28	a1i	$⊢ φ \to K \cap \{1, M\} = \emptyset$
30		uncom	$⊢ \{1\} \cup (K \cup \{M\}) = (K \cup \{M\}) \cup \{1\}$
31		1z	$⊢ 1 \in ℤ$
32		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
33	31 32	ax-mp	$⊢ (1 \dots 1) = \{1\}$
34	7	uneq1i	$⊢ K \cup \{M\} = ((2 \dots N + 1) ∖ \{M\}) \cup \{M\}$
35		undif1	$⊢ ((2 \dots N + 1) ∖ \{M\}) \cup \{M\} = (2 \dots N + 1) \cup \{M\}$
36	34 35	eqtr2i	$⊢ (2 \dots N + 1) \cup \{M\} = K \cup \{M\}$
37	33 36	uneq12i	$⊢ (1 \dots 1) \cup ((2 \dots N + 1) \cup \{M\}) = \{1\} \cup (K \cup \{M\})$
38		df-pr	$⊢ \{1, M\} = \{1\} \cup \{M\}$
39	38	equncomi	$⊢ \{1, M\} = \{M\} \cup \{1\}$
40	39	uneq2i	$⊢ K \cup \{1, M\} = K \cup (\{M\} \cup \{1\})$
41		unass	$⊢ (K \cup \{M\}) \cup \{1\} = K \cup (\{M\} \cup \{1\})$
42	40 41	eqtr4i	$⊢ K \cup \{1, M\} = (K \cup \{M\}) \cup \{1\}$
43	30 37 42	3eqtr4i	$⊢ (1 \dots 1) \cup ((2 \dots N + 1) \cup \{M\}) = K \cup \{1, M\}$
44	5	snssd	$⊢ φ \to \{M\} \subseteq (2 \dots N + 1)$
45		ssequn2	$⊢ \{M\} \subseteq (2 \dots N + 1) \leftrightarrow (2 \dots N + 1) \cup \{M\} = (2 \dots N + 1)$
46	44 45	sylib	$⊢ φ \to (2 \dots N + 1) \cup \{M\} = (2 \dots N + 1)$
47		df-2	$⊢ 2 = 1 + 1$
48	47	oveq1i	$⊢ (2 \dots N + 1) = (1 + 1 \dots N + 1)$
49	46 48	eqtrdi	$⊢ φ \to (2 \dots N + 1) \cup \{M\} = (1 + 1 \dots N + 1)$
50	49	uneq2d	$⊢ φ \to (1 \dots 1) \cup ((2 \dots N + 1) \cup \{M\}) = (1 \dots 1) \cup (1 + 1 \dots N + 1)$
51	4	peano2nnd	$⊢ φ \to N + 1 \in ℕ$
52		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
53	51 52	eleqtrdi	$⊢ φ \to N + 1 \in ℤ_{\geq 1}$
54		eluzfz1	$⊢ N + 1 \in ℤ_{\geq 1} \to 1 \in (1 \dots N + 1)$
55		fzsplit	$⊢ 1 \in (1 \dots N + 1) \to (1 \dots N + 1) = (1 \dots 1) \cup (1 + 1 \dots N + 1)$
56	53 54 55	3syl	$⊢ φ \to (1 \dots N + 1) = (1 \dots 1) \cup (1 + 1 \dots N + 1)$
57	50 56	eqtr4d	$⊢ φ \to (1 \dots 1) \cup ((2 \dots N + 1) \cup \{M\}) = (1 \dots N + 1)$
58	43 57	eqtr3id	$⊢ φ \to K \cup \{1, M\} = (1 \dots N + 1)$
59	47	oveq2i	$⊢ N + 1 - 2 = N + 1 - (1 + 1)$
60		fzfi	$⊢ (2 \dots N + 1) \in Fin$
61		diffi	$⊢ (2 \dots N + 1) \in Fin \to (2 \dots N + 1) ∖ \{M\} \in Fin$
62	60 61	ax-mp	$⊢ (2 \dots N + 1) ∖ \{M\} \in Fin$
63	7 62	eqeltri	$⊢ K \in Fin$
64		prfi	$⊢ \{1, M\} \in Fin$
65		hashun	$⊢ (K \in Fin \land \{1, M\} \in Fin \land K \cap \{1, M\} = \emptyset) \to \|K \cup \{1, M\}\| = \|K\| + \|\{1, M\}\|$
66	63 64 28 65	mp3an	$⊢ \|K \cup \{1, M\}\| = \|K\| + \|\{1, M\}\|$
67	58	fveq2d	$⊢ φ \to \|K \cup \{1, M\}\| = \|(1 \dots N + 1)\|$
68		neeq1	$⊢ x = M \to (x \neq 1 \leftrightarrow M \neq 1)$
69	10 18	syl	$⊢ x \in (2 \dots N + 1) \to x \neq 1$
70	68 69	vtoclga	$⊢ M \in (2 \dots N + 1) \to M \neq 1$
71	5 70	syl	$⊢ φ \to M \neq 1$
72	71	necomd	$⊢ φ \to 1 \neq M$
73		1ex	$⊢ 1 \in V$
74		hashprg	$⊢ (1 \in V \land M \in V) \to (1 \neq M \leftrightarrow \|\{1, M\}\| = 2)$
75	73 6 74	mp2an	$⊢ 1 \neq M \leftrightarrow \|\{1, M\}\| = 2$
76	72 75	sylib	$⊢ φ \to \|\{1, M\}\| = 2$
77	76	oveq2d	$⊢ φ \to \|K\| + \|\{1, M\}\| = \|K\| + 2$
78	66 67 77	3eqtr3a	$⊢ φ \to \|(1 \dots N + 1)\| = \|K\| + 2$
79	51	nnnn0d	$⊢ φ \to N + 1 \in ℕ_{0}$
80		hashfz1	$⊢ N + 1 \in ℕ_{0} \to \|(1 \dots N + 1)\| = N + 1$
81	79 80	syl	$⊢ φ \to \|(1 \dots N + 1)\| = N + 1$
82	78 81	eqtr3d	$⊢ φ \to \|K\| + 2 = N + 1$
83	51	nncnd	$⊢ φ \to N + 1 \in ℂ$
84		2cnd	$⊢ φ \to 2 \in ℂ$
85		hashcl	$⊢ K \in Fin \to \|K\| \in ℕ_{0}$
86	63 85	ax-mp	$⊢ \|K\| \in ℕ_{0}$
87	86	nn0cni	$⊢ \|K\| \in ℂ$
88	87	a1i	$⊢ φ \to \|K\| \in ℂ$
89	83 84 88	subadd2d	$⊢ φ \to (N + 1 - 2 = \|K\| \leftrightarrow \|K\| + 2 = N + 1)$
90	82 89	mpbird	$⊢ φ \to N + 1 - 2 = \|K\|$
91	4	nncnd	$⊢ φ \to N \in ℂ$
92		1cnd	$⊢ φ \to 1 \in ℂ$
93	91 92 92	pnpcan2d	$⊢ φ \to N + 1 - (1 + 1) = N - 1$
94	59 90 93	3eqtr3a	$⊢ φ \to \|K\| = N - 1$
95	29 58 94	3jca	$⊢ φ \to (K \cap \{1, M\} = \emptyset \land K \cup \{1, M\} = (1 \dots N + 1) \land \|K\| = N - 1)$

Metamath Proof Explorer

Theorem subfacp1lem1

Proof