derangenlem

		Ref	Expression
	Hypothesis	derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
	Assertion	derangenlem	$⊢ (A \approx B \land B \in Fin) \to D (A) \leq D (B)$

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		simpl	$⊢ (A \approx B \land B \in Fin) \to A \approx B$
3		bren	$⊢ A \approx B \leftrightarrow \exists s s : A \underset{1-1 onto}{⟶} B$
4	2 3	sylib	$⊢ (A \approx B \land B \in Fin) \to \exists s s : A \underset{1-1 onto}{⟶} B$
5		deranglem	$⊢ B \in Fin \to \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\} \in Fin$
6	5	adantl	$⊢ (A \approx B \land B \in Fin) \to \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\} \in Fin$
7		f1oco	$⊢ (s : A \underset{1-1 onto}{⟶} B \land g : A \underset{1-1 onto}{⟶} A) \to (s \circ g) : A \underset{1-1 onto}{⟶} B$
8	7	ad2ant2lr	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \to (s \circ g) : A \underset{1-1 onto}{⟶} B$
9		f1ocnv	$⊢ s : A \underset{1-1 onto}{⟶} B \to s^{-1} : B \underset{1-1 onto}{⟶} A$
10	9	ad2antlr	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \to s^{-1} : B \underset{1-1 onto}{⟶} A$
11		f1oco	$⊢ ((s \circ g) : A \underset{1-1 onto}{⟶} B \land s^{-1} : B \underset{1-1 onto}{⟶} A) \to ((s \circ g) \circ s^{-1}) : B \underset{1-1 onto}{⟶} B$
12	8 10 11	syl2anc	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \to ((s \circ g) \circ s^{-1}) : B \underset{1-1 onto}{⟶} B$
13		coass	$⊢ (s \circ g) \circ s^{-1} = s \circ (g \circ s^{-1})$
14	13	fveq1i	$⊢ ((s \circ g) \circ s^{-1}) (z) = (s \circ (g \circ s^{-1})) (z)$
15		simprl	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \to g : A \underset{1-1 onto}{⟶} A$
16		f1oco	$⊢ (g : A \underset{1-1 onto}{⟶} A \land s^{-1} : B \underset{1-1 onto}{⟶} A) \to (g \circ s^{-1}) : B \underset{1-1 onto}{⟶} A$
17	15 10 16	syl2anc	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \to (g \circ s^{-1}) : B \underset{1-1 onto}{⟶} A$
18		f1of	$⊢ (g \circ s^{-1}) : B \underset{1-1 onto}{⟶} A \to (g \circ s^{-1}) : B ⟶ A$
19	17 18	syl	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \to (g \circ s^{-1}) : B ⟶ A$
20		fvco3	$⊢ ((g \circ s^{-1}) : B ⟶ A \land z \in B) \to (s \circ (g \circ s^{-1})) (z) = s ((g \circ s^{-1}) (z))$
21	19 20	sylan	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to (s \circ (g \circ s^{-1})) (z) = s ((g \circ s^{-1}) (z))$
22	14 21	eqtrid	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to ((s \circ g) \circ s^{-1}) (z) = s ((g \circ s^{-1}) (z))$
23		f1of	$⊢ s^{-1} : B \underset{1-1 onto}{⟶} A \to s^{-1} : B ⟶ A$
24	10 23	syl	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \to s^{-1} : B ⟶ A$
25		fvco3	$⊢ (s^{-1} : B ⟶ A \land z \in B) \to (g \circ s^{-1}) (z) = g (s^{-1} (z))$
26	24 25	sylan	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to (g \circ s^{-1}) (z) = g (s^{-1} (z))$
27	24	ffvelcdmda	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to s^{-1} (z) \in A$
28		simplrr	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to \forall y \in A g (y) \neq y$
29		fveq2	$⊢ y = s^{-1} (z) \to g (y) = g (s^{-1} (z))$
30		id	$⊢ y = s^{-1} (z) \to y = s^{-1} (z)$
31	29 30	neeq12d	$⊢ y = s^{-1} (z) \to (g (y) \neq y \leftrightarrow g (s^{-1} (z)) \neq s^{-1} (z))$
32	31	rspcv	$⊢ s^{-1} (z) \in A \to (\forall y \in A g (y) \neq y \to g (s^{-1} (z)) \neq s^{-1} (z))$
33	27 28 32	sylc	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to g (s^{-1} (z)) \neq s^{-1} (z)$
34	26 33	eqnetrd	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to (g \circ s^{-1}) (z) \neq s^{-1} (z)$
35	34	necomd	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to s^{-1} (z) \neq (g \circ s^{-1}) (z)$
36		simpllr	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to s : A \underset{1-1 onto}{⟶} B$
37	19	ffvelcdmda	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to (g \circ s^{-1}) (z) \in A$
38		f1ocnvfv	$⊢ (s : A \underset{1-1 onto}{⟶} B \land (g \circ s^{-1}) (z) \in A) \to (s ((g \circ s^{-1}) (z)) = z \to s^{-1} (z) = (g \circ s^{-1}) (z))$
39	36 37 38	syl2anc	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to (s ((g \circ s^{-1}) (z)) = z \to s^{-1} (z) = (g \circ s^{-1}) (z))$
40	39	necon3d	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to (s^{-1} (z) \neq (g \circ s^{-1}) (z) \to s ((g \circ s^{-1}) (z)) \neq z)$
41	35 40	mpd	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to s ((g \circ s^{-1}) (z)) \neq z$
42	22 41	eqnetrd	$⊢ ((((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \land z \in B) \to ((s \circ g) \circ s^{-1}) (z) \neq z$
43	42	ralrimiva	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \to \forall z \in B ((s \circ g) \circ s^{-1}) (z) \neq z$
44		fveq2	$⊢ z = y \to ((s \circ g) \circ s^{-1}) (z) = ((s \circ g) \circ s^{-1}) (y)$
45		id	$⊢ z = y \to z = y$
46	44 45	neeq12d	$⊢ z = y \to (((s \circ g) \circ s^{-1}) (z) \neq z \leftrightarrow ((s \circ g) \circ s^{-1}) (y) \neq y)$
47	46	cbvralvw	$⊢ \forall z \in B ((s \circ g) \circ s^{-1}) (z) \neq z \leftrightarrow \forall y \in B ((s \circ g) \circ s^{-1}) (y) \neq y$
48	43 47	sylib	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \to \forall y \in B ((s \circ g) \circ s^{-1}) (y) \neq y$
49	12 48	jca	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)) \to (((s \circ g) \circ s^{-1}) : B \underset{1-1 onto}{⟶} B \land \forall y \in B ((s \circ g) \circ s^{-1}) (y) \neq y)$
50	49	ex	$⊢ ((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \to ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \to (((s \circ g) \circ s^{-1}) : B \underset{1-1 onto}{⟶} B \land \forall y \in B ((s \circ g) \circ s^{-1}) (y) \neq y))$
51		vex	$⊢ g \in V$
52		f1oeq1	$⊢ f = g \to (f : A \underset{1-1 onto}{⟶} A \leftrightarrow g : A \underset{1-1 onto}{⟶} A)$
53		fveq1	$⊢ f = g \to f (y) = g (y)$
54	53	neeq1d	$⊢ f = g \to (f (y) \neq y \leftrightarrow g (y) \neq y)$
55	54	ralbidv	$⊢ f = g \to (\forall y \in A f (y) \neq y \leftrightarrow \forall y \in A g (y) \neq y)$
56	52 55	anbi12d	$⊢ f = g \to ((f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y) \leftrightarrow (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y))$
57	51 56	elab	$⊢ g \in \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} \leftrightarrow (g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y)$
58		vex	$⊢ s \in V$
59	58 51	coex	$⊢ s \circ g \in V$
60	58	cnvex	$⊢ s^{-1} \in V$
61	59 60	coex	$⊢ (s \circ g) \circ s^{-1} \in V$
62		f1oeq1	$⊢ f = (s \circ g) \circ s^{-1} \to (f : B \underset{1-1 onto}{⟶} B \leftrightarrow ((s \circ g) \circ s^{-1}) : B \underset{1-1 onto}{⟶} B)$
63		fveq1	$⊢ f = (s \circ g) \circ s^{-1} \to f (y) = ((s \circ g) \circ s^{-1}) (y)$
64	63	neeq1d	$⊢ f = (s \circ g) \circ s^{-1} \to (f (y) \neq y \leftrightarrow ((s \circ g) \circ s^{-1}) (y) \neq y)$
65	64	ralbidv	$⊢ f = (s \circ g) \circ s^{-1} \to (\forall y \in B f (y) \neq y \leftrightarrow \forall y \in B ((s \circ g) \circ s^{-1}) (y) \neq y)$
66	62 65	anbi12d	$⊢ f = (s \circ g) \circ s^{-1} \to ((f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y) \leftrightarrow (((s \circ g) \circ s^{-1}) : B \underset{1-1 onto}{⟶} B \land \forall y \in B ((s \circ g) \circ s^{-1}) (y) \neq y))$
67	61 66	elab	$⊢ (s \circ g) \circ s^{-1} \in \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\} \leftrightarrow (((s \circ g) \circ s^{-1}) : B \underset{1-1 onto}{⟶} B \land \forall y \in B ((s \circ g) \circ s^{-1}) (y) \neq y)$
68	50 57 67	3imtr4g	$⊢ ((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \to (g \in \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} \to (s \circ g) \circ s^{-1} \in \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\})$
69		vex	$⊢ h \in V$
70		f1oeq1	$⊢ f = h \to (f : A \underset{1-1 onto}{⟶} A \leftrightarrow h : A \underset{1-1 onto}{⟶} A)$
71		fveq1	$⊢ f = h \to f (y) = h (y)$
72	71	neeq1d	$⊢ f = h \to (f (y) \neq y \leftrightarrow h (y) \neq y)$
73	72	ralbidv	$⊢ f = h \to (\forall y \in A f (y) \neq y \leftrightarrow \forall y \in A h (y) \neq y)$
74	70 73	anbi12d	$⊢ f = h \to ((f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y) \leftrightarrow (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))$
75	69 74	elab	$⊢ h \in \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} \leftrightarrow (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y)$
76	57 75	anbi12i	$⊢ (g \in \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} \land h \in \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}) \leftrightarrow ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))$
77	9	ad2antlr	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to s^{-1} : B \underset{1-1 onto}{⟶} A$
78		f1ofo	$⊢ s^{-1} : B \underset{1-1 onto}{⟶} A \to s^{-1} : B \underset{onto}{⟶} A$
79	77 78	syl	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to s^{-1} : B \underset{onto}{⟶} A$
80	8	adantrr	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to (s \circ g) : A \underset{1-1 onto}{⟶} B$
81		f1ofn	$⊢ (s \circ g) : A \underset{1-1 onto}{⟶} B \to (s \circ g) Fn A$
82	80 81	syl	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to (s \circ g) Fn A$
83		simplr	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to s : A \underset{1-1 onto}{⟶} B$
84		simprrl	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to h : A \underset{1-1 onto}{⟶} A$
85		f1oco	$⊢ (s : A \underset{1-1 onto}{⟶} B \land h : A \underset{1-1 onto}{⟶} A) \to (s \circ h) : A \underset{1-1 onto}{⟶} B$
86	83 84 85	syl2anc	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to (s \circ h) : A \underset{1-1 onto}{⟶} B$
87		f1ofn	$⊢ (s \circ h) : A \underset{1-1 onto}{⟶} B \to (s \circ h) Fn A$
88	86 87	syl	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to (s \circ h) Fn A$
89		cocan2	$⊢ (s^{-1} : B \underset{onto}{⟶} A \land (s \circ g) Fn A \land (s \circ h) Fn A) \to ((s \circ g) \circ s^{-1} = (s \circ h) \circ s^{-1} \leftrightarrow s \circ g = s \circ h)$
90	79 82 88 89	syl3anc	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to ((s \circ g) \circ s^{-1} = (s \circ h) \circ s^{-1} \leftrightarrow s \circ g = s \circ h)$
91		f1of1	$⊢ s : A \underset{1-1 onto}{⟶} B \to s : A \underset{1-1}{⟶} B$
92	91	ad2antlr	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to s : A \underset{1-1}{⟶} B$
93		simprll	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to g : A \underset{1-1 onto}{⟶} A$
94		f1of	$⊢ g : A \underset{1-1 onto}{⟶} A \to g : A ⟶ A$
95	93 94	syl	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to g : A ⟶ A$
96		f1of	$⊢ h : A \underset{1-1 onto}{⟶} A \to h : A ⟶ A$
97	84 96	syl	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to h : A ⟶ A$
98		cocan1	$⊢ (s : A \underset{1-1}{⟶} B \land g : A ⟶ A \land h : A ⟶ A) \to (s \circ g = s \circ h \leftrightarrow g = h)$
99	92 95 97 98	syl3anc	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to (s \circ g = s \circ h \leftrightarrow g = h)$
100	90 99	bitrd	$⊢ (((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \land ((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y))) \to ((s \circ g) \circ s^{-1} = (s \circ h) \circ s^{-1} \leftrightarrow g = h)$
101	100	ex	$⊢ ((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \to (((g : A \underset{1-1 onto}{⟶} A \land \forall y \in A g (y) \neq y) \land (h : A \underset{1-1 onto}{⟶} A \land \forall y \in A h (y) \neq y)) \to ((s \circ g) \circ s^{-1} = (s \circ h) \circ s^{-1} \leftrightarrow g = h))$
102	76 101	biimtrid	$⊢ ((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \to ((g \in \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} \land h \in \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}) \to ((s \circ g) \circ s^{-1} = (s \circ h) \circ s^{-1} \leftrightarrow g = h))$
103	68 102	dom2d	$⊢ ((A \approx B \land B \in Fin) \land s : A \underset{1-1 onto}{⟶} B) \to (\{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\} \in Fin \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} ≼ \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\})$
104	103	ex	$⊢ (A \approx B \land B \in Fin) \to (s : A \underset{1-1 onto}{⟶} B \to (\{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\} \in Fin \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} ≼ \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\}))$
105	104	exlimdv	$⊢ (A \approx B \land B \in Fin) \to (\exists s s : A \underset{1-1 onto}{⟶} B \to (\{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\} \in Fin \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} ≼ \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\}))$
106	4 6 105	mp2d	$⊢ (A \approx B \land B \in Fin) \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} ≼ \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\}$
107		enfii	$⊢ (B \in Fin \land A \approx B) \to A \in Fin$
108	107	ancoms	$⊢ (A \approx B \land B \in Fin) \to A \in Fin$
109		deranglem	$⊢ A \in Fin \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} \in Fin$
110	108 109	syl	$⊢ (A \approx B \land B \in Fin) \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} \in Fin$
111		hashdom	$⊢ (\{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} \in Fin \land \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\} \in Fin) \to (\|\{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}\| \leq \|\{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\}\| \leftrightarrow \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} ≼ \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\})$
112	110 6 111	syl2anc	$⊢ (A \approx B \land B \in Fin) \to (\|\{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}\| \leq \|\{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\}\| \leftrightarrow \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} ≼ \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\})$
113	106 112	mpbird	$⊢ (A \approx B \land B \in Fin) \to \|\{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}\| \leq \|\{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\}\|$
114	1	derangval	$⊢ A \in Fin \to D (A) = \|\{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}\|$
115	108 114	syl	$⊢ (A \approx B \land B \in Fin) \to D (A) = \|\{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}\|$
116	1	derangval	$⊢ B \in Fin \to D (B) = \|\{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\}\|$
117	116	adantl	$⊢ (A \approx B \land B \in Fin) \to D (B) = \|\{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\}\|$
118	113 115 117	3brtr4d	$⊢ (A \approx B \land B \in Fin) \to D (A) \leq D (B)$

Metamath Proof Explorer

Theorem derangenlem

Proof