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		bren	$⊢ A \approx B \leftrightarrow \exists s s : A \underset{1-1 onto}{⟶} B$
3	2	birani	$⊢ (A \approx B \land B \in Fin) \to \exists s s : A \underset{1-1 onto}{⟶} B$
4		deranglem	$⊢ B \in Fin \to \{f \| (f : B \underset{1-1 onto}{⟶} B \land \forall y \in B f (y) \neq y)\} \in Fin$
5	4	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$
6		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$
7	6	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$
8		f1ocnv	$⊢ s : A \underset{1-1 onto}{⟶} B \to s^{-1} : B \underset{1-1 onto}{⟶} A$
9	8	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$
10		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$
11	7 9 10	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$
12		coass	$⊢ (s \circ g) \circ s^{-1} = s \circ (g \circ s^{-1})$
13	12	fveq1i	$⊢ ((s \circ g) \circ s^{-1}) (z) = (s \circ (g \circ s^{-1})) (z)$
14		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$
15		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$
16	14 9 15	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$
17		f1of	$⊢ (g \circ s^{-1}) : B \underset{1-1 onto}{⟶} A \to (g \circ s^{-1}) : B ⟶ A$
18	16 17	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$
19		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))$
20	18 19	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))$
21	13 20	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))$
22		f1of	$⊢ s^{-1} : B \underset{1-1 onto}{⟶} A \to s^{-1} : B ⟶ A$
23	9 22	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$
24		fvco3	$⊢ (s^{-1} : B ⟶ A \land z \in B) \to (g \circ s^{-1}) (z) = g (s^{-1} (z))$
25	23 24	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))$
26	23	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$
27		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$
28		fveq2	$⊢ y = s^{-1} (z) \to g (y) = g (s^{-1} (z))$
29		id	$⊢ y = s^{-1} (z) \to y = s^{-1} (z)$
30	28 29	neeq12d	$⊢ y = s^{-1} (z) \to (g (y) \neq y \leftrightarrow g (s^{-1} (z)) \neq s^{-1} (z))$
31	30	rspcv	$⊢ s^{-1} (z) \in A \to (\forall y \in A g (y) \neq y \to g (s^{-1} (z)) \neq s^{-1} (z))$
32	26 27 31	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)$
33	25 32	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)$
34	33	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)$
35		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$
36	18	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$
37		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))$
38	35 36 37	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))$
39	38	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)$
40	34 39	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$
41	21 40	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$
42	41	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$
43		fveq2	$⊢ z = y \to ((s \circ g) \circ s^{-1}) (z) = ((s \circ g) \circ s^{-1}) (y)$
44		id	$⊢ z = y \to z = y$
45	43 44	neeq12d	$⊢ z = y \to (((s \circ g) \circ s^{-1}) (z) \neq z \leftrightarrow ((s \circ g) \circ s^{-1}) (y) \neq y)$
46	45	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$
47	42 46	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$
48	11 47	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)$
49	48	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))$
50		vex	$⊢ g \in V$
51		f1oeq1	$⊢ f = g \to (f : A \underset{1-1 onto}{⟶} A \leftrightarrow g : A \underset{1-1 onto}{⟶} A)$
52		fveq1	$⊢ f = g \to f (y) = g (y)$
53	52	neeq1d	$⊢ f = g \to (f (y) \neq y \leftrightarrow g (y) \neq y)$
54	53	ralbidv	$⊢ f = g \to (\forall y \in A f (y) \neq y \leftrightarrow \forall y \in A g (y) \neq y)$
55	51 54	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))$
56	50 55	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)$
57		vex	$⊢ s \in V$
58	57 50	coex	$⊢ s \circ g \in V$
59	57	cnvex	$⊢ s^{-1} \in V$
60	58 59	coex	$⊢ (s \circ g) \circ s^{-1} \in V$
61		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)$
62		fveq1	$⊢ f = (s \circ g) \circ s^{-1} \to f (y) = ((s \circ g) \circ s^{-1}) (y)$
63	62	neeq1d	$⊢ f = (s \circ g) \circ s^{-1} \to (f (y) \neq y \leftrightarrow ((s \circ g) \circ s^{-1}) (y) \neq y)$
64	63	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)$
65	61 64	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))$
66	60 65	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)$
67	49 56 66	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)\})$
68		vex	$⊢ h \in V$
69		f1oeq1	$⊢ f = h \to (f : A \underset{1-1 onto}{⟶} A \leftrightarrow h : A \underset{1-1 onto}{⟶} A)$
70		fveq1	$⊢ f = h \to f (y) = h (y)$
71	70	neeq1d	$⊢ f = h \to (f (y) \neq y \leftrightarrow h (y) \neq y)$
72	71	ralbidv	$⊢ f = h \to (\forall y \in A f (y) \neq y \leftrightarrow \forall y \in A h (y) \neq y)$
73	69 72	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))$
74	68 73	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)$
75	56 74	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))$
76	8	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$
77		f1ofo	$⊢ s^{-1} : B \underset{1-1 onto}{⟶} A \to s^{-1} : B \underset{onto}{⟶} A$
78	76 77	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$
79	7	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$
80		f1ofn	$⊢ (s \circ g) : A \underset{1-1 onto}{⟶} B \to (s \circ g) Fn A$
81	79 80	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$
82		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$
83		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$
84		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$
85	82 83 84	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$
86		f1ofn	$⊢ (s \circ h) : A \underset{1-1 onto}{⟶} B \to (s \circ h) Fn A$
87	85 86	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$
88		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)$
89	78 81 87 88	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)$
90		f1of1	$⊢ s : A \underset{1-1 onto}{⟶} B \to s : A \underset{1-1}{⟶} B$
91	90	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$
92		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$
93		f1of	$⊢ g : A \underset{1-1 onto}{⟶} A \to g : A ⟶ A$
94	92 93	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$
95		f1of	$⊢ h : A \underset{1-1 onto}{⟶} A \to h : A ⟶ A$
96	83 95	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$
97		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)$
98	91 94 96 97	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)$
99	89 98	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)$
100	99	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))$
101	75 100	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))$
102	67 101	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)\})$
103	102	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)\}))$
104	103	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)\}))$
105	3 5 104	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)\}$
106		enfii	$⊢ (B \in Fin \land A \approx B) \to A \in Fin$
107	106	ancoms	$⊢ (A \approx B \land B \in Fin) \to A \in Fin$
108		deranglem	$⊢ A \in Fin \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\} \in Fin$
109	107 108	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$
110		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)\})$
111	109 5 110	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)\})$
112	105 111	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)\}\|$
113	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)\}\|$
114	107 113	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)\}\|$
115	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)\}\|$
116	115	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)\}\|$
117	112 114 116	3brtr4d	$⊢ (A \approx B \land B \in Fin) \to D (A) \leq D (B)$

Metamath Proof Explorer

Theorem derangenlem

Proof