subfacp1lem2b

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	subfacp1lem2b	$⊢ (φ \land X \in K) \to F (X) = G (X)$

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	1 2 3 4 5 6 7 8 9	subfacp1lem2a	$⊢ φ \to (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land F (1) = M \land F (M) = 1)$
11	10	simp1d	$⊢ φ \to F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
12		f1ofun	$⊢ F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to Fun F$
13	11 12	syl	$⊢ φ \to Fun F$
14	13	adantr	$⊢ (φ \land X \in K) \to Fun F$
15		ssun1	$⊢ G \subseteq G \cup \{⟨1, M⟩, ⟨M, 1⟩\}$
16	15 8	sseqtrri	$⊢ G \subseteq F$
17	16	a1i	$⊢ (φ \land X \in K) \to G \subseteq F$
18		f1odm	$⊢ G : K \underset{1-1 onto}{⟶} K \to dom G = K$
19	9 18	syl	$⊢ φ \to dom G = K$
20	19	eleq2d	$⊢ φ \to (X \in dom G \leftrightarrow X \in K)$
21	20	biimpar	$⊢ (φ \land X \in K) \to X \in dom G$
22		funssfv	$⊢ (Fun F \land G \subseteq F \land X \in dom G) \to F (X) = G (X)$
23	14 17 21 22	syl3anc	$⊢ (φ \land X \in K) \to F (X) = G (X)$

Metamath Proof Explorer

Theorem subfacp1lem2b

Proof