subfacp1lem2a

Description: Lemma for subfacp1 . Properties of a bijection on K augmented with the two-element flip to get a bijection on K u. { 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\}$
	subfacp1lem2.5	$⊢ F = G \cup \{⟨1, M⟩, ⟨M, 1⟩\}$
	subfacp1lem2.6	$⊢ φ \to G : K \underset{1-1 onto}{⟶} K$
Assertion	subfacp1lem2a	$⊢ φ \to (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land F (1) = M \land F (M) = 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		subfacp1lem2.5	$⊢ F = G \cup \{⟨1, M⟩, ⟨M, 1⟩\}$
9		subfacp1lem2.6	$⊢ φ \to G : K \underset{1-1 onto}{⟶} K$
10		1z	$⊢ 1 \in ℤ$
11		f1oprswap	$⊢ (1 \in ℤ \land M \in V) \to \{⟨1, M⟩, ⟨M, 1⟩\} : \{1, M\} \underset{1-1 onto}{⟶} \{1, M\}$
12	10 6 11	mp2an	$⊢ \{⟨1, M⟩, ⟨M, 1⟩\} : \{1, M\} \underset{1-1 onto}{⟶} \{1, M\}$
13	12	a1i	$⊢ φ \to \{⟨1, M⟩, ⟨M, 1⟩\} : \{1, M\} \underset{1-1 onto}{⟶} \{1, M\}$
14	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)$
15	14	simp1d	$⊢ φ \to K \cap \{1, M\} = \emptyset$
16		f1oun	$⊢ ((G : K \underset{1-1 onto}{⟶} K \land \{⟨1, M⟩, ⟨M, 1⟩\} : \{1, M\} \underset{1-1 onto}{⟶} \{1, M\}) \land (K \cap \{1, M\} = \emptyset \land K \cap \{1, M\} = \emptyset)) \to (G \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : K \cup \{1, M\} \underset{1-1 onto}{⟶} K \cup \{1, M\}$
17	9 13 15 15 16	syl22anc	$⊢ φ \to (G \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : K \cup \{1, M\} \underset{1-1 onto}{⟶} K \cup \{1, M\}$
18	14	simp2d	$⊢ φ \to K \cup \{1, M\} = (1 \dots N + 1)$
19		f1oeq1	$⊢ F = G \cup \{⟨1, M⟩, ⟨M, 1⟩\} \to (F : K \cup \{1, M\} \underset{1-1 onto}{⟶} K \cup \{1, M\} \leftrightarrow (G \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : K \cup \{1, M\} \underset{1-1 onto}{⟶} K \cup \{1, M\})$
20	8 19	ax-mp	$⊢ F : K \cup \{1, M\} \underset{1-1 onto}{⟶} K \cup \{1, M\} \leftrightarrow (G \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : K \cup \{1, M\} \underset{1-1 onto}{⟶} K \cup \{1, M\}$
21		f1oeq2	$⊢ K \cup \{1, M\} = (1 \dots N + 1) \to (F : K \cup \{1, M\} \underset{1-1 onto}{⟶} K \cup \{1, M\} \leftrightarrow F : (1 \dots N + 1) \underset{1-1 onto}{⟶} K \cup \{1, M\})$
22	20 21	bitr3id	$⊢ K \cup \{1, M\} = (1 \dots N + 1) \to ((G \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : K \cup \{1, M\} \underset{1-1 onto}{⟶} K \cup \{1, M\} \leftrightarrow F : (1 \dots N + 1) \underset{1-1 onto}{⟶} K \cup \{1, M\})$
23		f1oeq3	$⊢ K \cup \{1, M\} = (1 \dots N + 1) \to (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} K \cup \{1, M\} \leftrightarrow F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
24	22 23	bitrd	$⊢ K \cup \{1, M\} = (1 \dots N + 1) \to ((G \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : K \cup \{1, M\} \underset{1-1 onto}{⟶} K \cup \{1, M\} \leftrightarrow F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
25	18 24	syl	$⊢ φ \to ((G \cup \{⟨1, M⟩, ⟨M, 1⟩\}) : K \cup \{1, M\} \underset{1-1 onto}{⟶} K \cup \{1, M\} \leftrightarrow F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
26	17 25	mpbid	$⊢ φ \to F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
27		f1ofun	$⊢ F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to Fun F$
28	26 27	syl	$⊢ φ \to Fun F$
29		snsspr1	$⊢ \{⟨1, M⟩\} \subseteq \{⟨1, M⟩, ⟨M, 1⟩\}$
30		ssun2	$⊢ \{⟨1, M⟩, ⟨M, 1⟩\} \subseteq G \cup \{⟨1, M⟩, ⟨M, 1⟩\}$
31	30 8	sseqtrri	$⊢ \{⟨1, M⟩, ⟨M, 1⟩\} \subseteq F$
32	29 31	sstri	$⊢ \{⟨1, M⟩\} \subseteq F$
33		1ex	$⊢ 1 \in V$
34	33	snid	$⊢ 1 \in \{1\}$
35	6	dmsnop	$⊢ dom \{⟨1, M⟩\} = \{1\}$
36	34 35	eleqtrri	$⊢ 1 \in dom \{⟨1, M⟩\}$
37		funssfv	$⊢ (Fun F \land \{⟨1, M⟩\} \subseteq F \land 1 \in dom \{⟨1, M⟩\}) \to F (1) = \{⟨1, M⟩\} (1)$
38	32 36 37	mp3an23	$⊢ Fun F \to F (1) = \{⟨1, M⟩\} (1)$
39	28 38	syl	$⊢ φ \to F (1) = \{⟨1, M⟩\} (1)$
40	33 6	fvsn	$⊢ \{⟨1, M⟩\} (1) = M$
41	39 40	eqtrdi	$⊢ φ \to F (1) = M$
42		snsspr2	$⊢ \{⟨M, 1⟩\} \subseteq \{⟨1, M⟩, ⟨M, 1⟩\}$
43	42 31	sstri	$⊢ \{⟨M, 1⟩\} \subseteq F$
44	6	snid	$⊢ M \in \{M\}$
45	33	dmsnop	$⊢ dom \{⟨M, 1⟩\} = \{M\}$
46	44 45	eleqtrri	$⊢ M \in dom \{⟨M, 1⟩\}$
47		funssfv	$⊢ (Fun F \land \{⟨M, 1⟩\} \subseteq F \land M \in dom \{⟨M, 1⟩\}) \to F (M) = \{⟨M, 1⟩\} (M)$
48	43 46 47	mp3an23	$⊢ Fun F \to F (M) = \{⟨M, 1⟩\} (M)$
49	28 48	syl	$⊢ φ \to F (M) = \{⟨M, 1⟩\} (M)$
50	6 33	fvsn	$⊢ \{⟨M, 1⟩\} (M) = 1$
51	49 50	eqtrdi	$⊢ φ \to F (M) = 1$
52	26 41 51	3jca	$⊢ φ \to (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land F (1) = M \land F (M) = 1)$

Metamath Proof Explorer

Theorem subfacp1lem2a

Proof