Metamath Proof Explorer

Theorem derangenlem

Description: One half of derangen . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypothesis derang.d 
|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
Assertion derangenlem 
|- ( ( A ~~ B /\ B e. Fin ) -> ( D ` A ) <_ ( D ` B ) )

Proof

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