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