Metamath Proof Explorer

Theorem hashf1

Description: The permutation number | A | ! x. ( | B | _C | A | ) = | B | ! / ( | B | - | A | ) ! counts the number of injections from A to B . (Contributed by Mario Carneiro, 21-Jan-2015)

Ref Expression
Assertion hashf1 
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` { f | f : A -1-1-> B } ) = ( ( ! ` ( # ` A ) ) x. ( ( # ` B ) _C ( # ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 f1eq2 
 |-  ( x = (/) -> ( f : x -1-1-> B <-> f : (/) -1-1-> B ) )
2 f1fn 
 |-  ( f : (/) -1-1-> B -> f Fn (/) )
3 fn0 
 |-  ( f Fn (/) <-> f = (/) )
4 2 3 sylib 
 |-  ( f : (/) -1-1-> B -> f = (/) )
5 f10 
 |-  (/) : (/) -1-1-> B
6 f1eq1 
 |-  ( f = (/) -> ( f : (/) -1-1-> B <-> (/) : (/) -1-1-> B ) )
7 5 6 mpbiri 
 |-  ( f = (/) -> f : (/) -1-1-> B )
8 4 7 impbii 
 |-  ( f : (/) -1-1-> B <-> f = (/) )
9 velsn 
 |-  ( f e. { (/) } <-> f = (/) )
10 8 9 bitr4i 
 |-  ( f : (/) -1-1-> B <-> f e. { (/) } )
11 1 10 bitrdi 
 |-  ( x = (/) -> ( f : x -1-1-> B <-> f e. { (/) } ) )
12 11 abbi1dv 
 |-  ( x = (/) -> { f | f : x -1-1-> B } = { (/) } )
13 12 fveq2d 
 |-  ( x = (/) -> ( # ` { f | f : x -1-1-> B } ) = ( # ` { (/) } ) )
14 0ex 
 |-  (/) e. _V
15 hashsng 
 |-  ( (/) e. _V -> ( # ` { (/) } ) = 1 )
16 14 15 ax-mp 
 |-  ( # ` { (/) } ) = 1
17 13 16 eqtrdi 
 |-  ( x = (/) -> ( # ` { f | f : x -1-1-> B } ) = 1 )
18 fveq2 
 |-  ( x = (/) -> ( # ` x ) = ( # ` (/) ) )
19 hash0 
 |-  ( # ` (/) ) = 0
20 18 19 eqtrdi 
 |-  ( x = (/) -> ( # ` x ) = 0 )
21 20 fveq2d 
 |-  ( x = (/) -> ( ! ` ( # ` x ) ) = ( ! ` 0 ) )
22 fac0 
 |-  ( ! ` 0 ) = 1
23 21 22 eqtrdi 
 |-  ( x = (/) -> ( ! ` ( # ` x ) ) = 1 )
24 20 oveq2d 
 |-  ( x = (/) -> ( ( # ` B ) _C ( # ` x ) ) = ( ( # ` B ) _C 0 ) )
25 23 24 oveq12d 
 |-  ( x = (/) -> ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) = ( 1 x. ( ( # ` B ) _C 0 ) ) )
26 17 25 eqeq12d 
 |-  ( x = (/) -> ( ( # ` { f | f : x -1-1-> B } ) = ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) <-> 1 = ( 1 x. ( ( # ` B ) _C 0 ) ) ) )
27 26 imbi2d 
 |-  ( x = (/) -> ( ( B e. Fin -> ( # ` { f | f : x -1-1-> B } ) = ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) ) <-> ( B e. Fin -> 1 = ( 1 x. ( ( # ` B ) _C 0 ) ) ) ) )
28 f1eq2 
 |-  ( x = y -> ( f : x -1-1-> B <-> f : y -1-1-> B ) )
29 28 abbidv 
 |-  ( x = y -> { f | f : x -1-1-> B } = { f | f : y -1-1-> B } )
30 29 fveq2d 
 |-  ( x = y -> ( # ` { f | f : x -1-1-> B } ) = ( # ` { f | f : y -1-1-> B } ) )
31 2fveq3 
 |-  ( x = y -> ( ! ` ( # ` x ) ) = ( ! ` ( # ` y ) ) )
32 fveq2 
 |-  ( x = y -> ( # ` x ) = ( # ` y ) )
33 32 oveq2d 
 |-  ( x = y -> ( ( # ` B ) _C ( # ` x ) ) = ( ( # ` B ) _C ( # ` y ) ) )
34 31 33 oveq12d 
 |-  ( x = y -> ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) = ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) )
35 30 34 eqeq12d 
 |-  ( x = y -> ( ( # ` { f | f : x -1-1-> B } ) = ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) <-> ( # ` { f | f : y -1-1-> B } ) = ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) ) )
36 35 imbi2d 
 |-  ( x = y -> ( ( B e. Fin -> ( # ` { f | f : x -1-1-> B } ) = ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) ) <-> ( B e. Fin -> ( # ` { f | f : y -1-1-> B } ) = ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) ) ) )
37 f1eq2 
 |-  ( x = ( y u. { z } ) -> ( f : x -1-1-> B <-> f : ( y u. { z } ) -1-1-> B ) )
38 37 abbidv 
 |-  ( x = ( y u. { z } ) -> { f | f : x -1-1-> B } = { f | f : ( y u. { z } ) -1-1-> B } )
39 38 fveq2d 
 |-  ( x = ( y u. { z } ) -> ( # ` { f | f : x -1-1-> B } ) = ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) )
40 2fveq3 
 |-  ( x = ( y u. { z } ) -> ( ! ` ( # ` x ) ) = ( ! ` ( # ` ( y u. { z } ) ) ) )
41 fveq2 
 |-  ( x = ( y u. { z } ) -> ( # ` x ) = ( # ` ( y u. { z } ) ) )
42 41 oveq2d 
 |-  ( x = ( y u. { z } ) -> ( ( # ` B ) _C ( # ` x ) ) = ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) )
43 40 42 oveq12d 
 |-  ( x = ( y u. { z } ) -> ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) )
44 39 43 eqeq12d 
 |-  ( x = ( y u. { z } ) -> ( ( # ` { f | f : x -1-1-> B } ) = ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) <-> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) ) )
45 44 imbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( B e. Fin -> ( # ` { f | f : x -1-1-> B } ) = ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) ) <-> ( B e. Fin -> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) ) ) )
46 f1eq2 
 |-  ( x = A -> ( f : x -1-1-> B <-> f : A -1-1-> B ) )
47 46 abbidv 
 |-  ( x = A -> { f | f : x -1-1-> B } = { f | f : A -1-1-> B } )
48 47 fveq2d 
 |-  ( x = A -> ( # ` { f | f : x -1-1-> B } ) = ( # ` { f | f : A -1-1-> B } ) )
49 2fveq3 
 |-  ( x = A -> ( ! ` ( # ` x ) ) = ( ! ` ( # ` A ) ) )
50 fveq2 
 |-  ( x = A -> ( # ` x ) = ( # ` A ) )
51 50 oveq2d 
 |-  ( x = A -> ( ( # ` B ) _C ( # ` x ) ) = ( ( # ` B ) _C ( # ` A ) ) )
52 49 51 oveq12d 
 |-  ( x = A -> ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) = ( ( ! ` ( # ` A ) ) x. ( ( # ` B ) _C ( # ` A ) ) ) )
53 48 52 eqeq12d 
 |-  ( x = A -> ( ( # ` { f | f : x -1-1-> B } ) = ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) <-> ( # ` { f | f : A -1-1-> B } ) = ( ( ! ` ( # ` A ) ) x. ( ( # ` B ) _C ( # ` A ) ) ) ) )
54 53 imbi2d 
 |-  ( x = A -> ( ( B e. Fin -> ( # ` { f | f : x -1-1-> B } ) = ( ( ! ` ( # ` x ) ) x. ( ( # ` B ) _C ( # ` x ) ) ) ) <-> ( B e. Fin -> ( # ` { f | f : A -1-1-> B } ) = ( ( ! ` ( # ` A ) ) x. ( ( # ` B ) _C ( # ` A ) ) ) ) ) )
55 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
56 bcn0 
 |-  ( ( # ` B ) e. NN0 -> ( ( # ` B ) _C 0 ) = 1 )
57 55 56 syl 
 |-  ( B e. Fin -> ( ( # ` B ) _C 0 ) = 1 )
58 57 oveq2d 
 |-  ( B e. Fin -> ( 1 x. ( ( # ` B ) _C 0 ) ) = ( 1 x. 1 ) )
59 1t1e1 
 |-  ( 1 x. 1 ) = 1
60 58 59 eqtr2di 
 |-  ( B e. Fin -> 1 = ( 1 x. ( ( # ` B ) _C 0 ) ) )
61 abn0 
 |-  ( { f | f : ( y u. { z } ) -1-1-> B } =/= (/) <-> E. f f : ( y u. { z } ) -1-1-> B )
62 f1domg 
 |-  ( B e. Fin -> ( f : ( y u. { z } ) -1-1-> B -> ( y u. { z } ) ~<_ B ) )
63 62 adantr 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( f : ( y u. { z } ) -1-1-> B -> ( y u. { z } ) ~<_ B ) )
64 hashunsng 
 |-  ( z e. _V -> ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) ) )
65 64 elv 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) )
66 65 adantl 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) )
67 66 breq1d 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` ( y u. { z } ) ) <_ ( # ` B ) <-> ( ( # ` y ) + 1 ) <_ ( # ` B ) ) )
68 simprl 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> y e. Fin )
69 snfi 
 |-  { z } e. Fin
70 unfi 
 |-  ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin )
71 68 69 70 sylancl 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( y u. { z } ) e. Fin )
72 simpl 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> B e. Fin )
73 hashdom 
 |-  ( ( ( y u. { z } ) e. Fin /\ B e. Fin ) -> ( ( # ` ( y u. { z } ) ) <_ ( # ` B ) <-> ( y u. { z } ) ~<_ B ) )
74 71 72 73 syl2anc 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` ( y u. { z } ) ) <_ ( # ` B ) <-> ( y u. { z } ) ~<_ B ) )
75 hashcl 
 |-  ( y e. Fin -> ( # ` y ) e. NN0 )
76 75 ad2antrl 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` y ) e. NN0 )
77 nn0p1nn 
 |-  ( ( # ` y ) e. NN0 -> ( ( # ` y ) + 1 ) e. NN )
78 76 77 syl 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` y ) + 1 ) e. NN )
79 78 nnred 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` y ) + 1 ) e. RR )
80 55 adantr 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` B ) e. NN0 )
81 80 nn0red 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` B ) e. RR )
82 79 81 lenltd 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( ( # ` y ) + 1 ) <_ ( # ` B ) <-> -. ( # ` B ) < ( ( # ` y ) + 1 ) ) )
83 67 74 82 3bitr3d 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( y u. { z } ) ~<_ B <-> -. ( # ` B ) < ( ( # ` y ) + 1 ) ) )
84 63 83 sylibd 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( f : ( y u. { z } ) -1-1-> B -> -. ( # ` B ) < ( ( # ` y ) + 1 ) ) )
85 84 exlimdv 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( E. f f : ( y u. { z } ) -1-1-> B -> -. ( # ` B ) < ( ( # ` y ) + 1 ) ) )
86 61 85 syl5bi 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( { f | f : ( y u. { z } ) -1-1-> B } =/= (/) -> -. ( # ` B ) < ( ( # ` y ) + 1 ) ) )
87 86 necon4ad 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` B ) < ( ( # ` y ) + 1 ) -> { f | f : ( y u. { z } ) -1-1-> B } = (/) ) )
88 87 imp 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> { f | f : ( y u. { z } ) -1-1-> B } = (/) )
89 88 fveq2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( # ` (/) ) )
90 hashcl 
 |-  ( ( y u. { z } ) e. Fin -> ( # ` ( y u. { z } ) ) e. NN0 )
91 71 90 syl 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` ( y u. { z } ) ) e. NN0 )
92 91 faccld 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ! ` ( # ` ( y u. { z } ) ) ) e. NN )
93 92 nncnd 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ! ` ( # ` ( y u. { z } ) ) ) e. CC )
94 93 adantr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( ! ` ( # ` ( y u. { z } ) ) ) e. CC )
95 94 mul01d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( ( ! ` ( # ` ( y u. { z } ) ) ) x. 0 ) = 0 )
96 19 89 95 3eqtr4a 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. 0 ) )
97 66 adantr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) )
98 97 oveq2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) = ( ( # ` B ) _C ( ( # ` y ) + 1 ) ) )
99 80 adantr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( # ` B ) e. NN0 )
100 78 adantr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( ( # ` y ) + 1 ) e. NN )
101 100 nnzd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( ( # ` y ) + 1 ) e. ZZ )
102 animorr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( ( ( # ` y ) + 1 ) < 0 \/ ( # ` B ) < ( ( # ` y ) + 1 ) ) )
103 bcval4 
 |-  ( ( ( # ` B ) e. NN0 /\ ( ( # ` y ) + 1 ) e. ZZ /\ ( ( ( # ` y ) + 1 ) < 0 \/ ( # ` B ) < ( ( # ` y ) + 1 ) ) ) -> ( ( # ` B ) _C ( ( # ` y ) + 1 ) ) = 0 )
104 99 101 102 103 syl3anc 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( ( # ` B ) _C ( ( # ` y ) + 1 ) ) = 0 )
105 98 104 eqtrd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) = 0 )
106 105 oveq2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. 0 ) )
107 96 106 eqtr4d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) )
108 107 a1d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( # ` B ) < ( ( # ` y ) + 1 ) ) -> ( ( # ` { f | f : y -1-1-> B } ) = ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) -> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) ) )
109 oveq2 
 |-  ( ( # ` { f | f : y -1-1-> B } ) = ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) -> ( ( ( # ` B ) - ( # ` y ) ) x. ( # ` { f | f : y -1-1-> B } ) ) = ( ( ( # ` B ) - ( # ` y ) ) x. ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) ) )
110 68 adantr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> y e. Fin )
111 72 adantr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> B e. Fin )
112 simplrr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> -. z e. y )
113 simpr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` y ) + 1 ) <_ ( # ` B ) )
114 110 111 112 113 hashf1lem2 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ( # ` B ) - ( # ` y ) ) x. ( # ` { f | f : y -1-1-> B } ) ) )
115 80 adantr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( # ` B ) e. NN0 )
116 115 faccld 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( # ` B ) ) e. NN )
117 116 nncnd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( # ` B ) ) e. CC )
118 76 adantr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( # ` y ) e. NN0 )
119 peano2nn0 
 |-  ( ( # ` y ) e. NN0 -> ( ( # ` y ) + 1 ) e. NN0 )
120 118 119 syl 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` y ) + 1 ) e. NN0 )
121 nn0sub2 
 |-  ( ( ( ( # ` y ) + 1 ) e. NN0 /\ ( # ` B ) e. NN0 /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) - ( ( # ` y ) + 1 ) ) e. NN0 )
122 120 115 113 121 syl3anc 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) - ( ( # ` y ) + 1 ) ) e. NN0 )
123 122 faccld 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) e. NN )
124 123 nncnd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) e. CC )
125 123 nnne0d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) =/= 0 )
126 117 124 125 divcld 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) e. CC )
127 120 faccld 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` y ) + 1 ) ) e. NN )
128 127 nncnd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` y ) + 1 ) ) e. CC )
129 127 nnne0d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` y ) + 1 ) ) =/= 0 )
130 126 128 129 divcan2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( ( # ` y ) + 1 ) ) x. ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ! ` ( ( # ` y ) + 1 ) ) ) ) = ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) )
131 115 nn0cnd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( # ` B ) e. CC )
132 118 nn0cnd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( # ` y ) e. CC )
133 131 132 subcld 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) - ( # ` y ) ) e. CC )
134 ax-1cn 
 |-  1 e. CC
135 npcan 
 |-  ( ( ( ( # ` B ) - ( # ` y ) ) e. CC /\ 1 e. CC ) -> ( ( ( ( # ` B ) - ( # ` y ) ) - 1 ) + 1 ) = ( ( # ` B ) - ( # ` y ) ) )
136 133 134 135 sylancl 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ( ( # ` B ) - ( # ` y ) ) - 1 ) + 1 ) = ( ( # ` B ) - ( # ` y ) ) )
137 1cnd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> 1 e. CC )
138 131 132 137 subsub4d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ( # ` B ) - ( # ` y ) ) - 1 ) = ( ( # ` B ) - ( ( # ` y ) + 1 ) ) )
139 138 122 eqeltrd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ( # ` B ) - ( # ` y ) ) - 1 ) e. NN0 )
140 nn0p1nn 
 |-  ( ( ( ( # ` B ) - ( # ` y ) ) - 1 ) e. NN0 -> ( ( ( ( # ` B ) - ( # ` y ) ) - 1 ) + 1 ) e. NN )
141 139 140 syl 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ( ( # ` B ) - ( # ` y ) ) - 1 ) + 1 ) e. NN )
142 136 141 eqeltrrd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) - ( # ` y ) ) e. NN )
143 142 nnne0d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) - ( # ` y ) ) =/= 0 )
144 126 133 143 divcan2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ( # ` B ) - ( # ` y ) ) x. ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ( # ` B ) - ( # ` y ) ) ) ) = ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) )
145 130 144 eqtr4d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( ( # ` y ) + 1 ) ) x. ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ! ` ( ( # ` y ) + 1 ) ) ) ) = ( ( ( # ` B ) - ( # ` y ) ) x. ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ( # ` B ) - ( # ` y ) ) ) ) )
146 66 adantr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) )
147 146 fveq2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( # ` ( y u. { z } ) ) ) = ( ! ` ( ( # ` y ) + 1 ) ) )
148 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
149 120 148 eleqtrdi 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` y ) + 1 ) e. ( ZZ>= ` 0 ) )
150 115 nn0zd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( # ` B ) e. ZZ )
151 elfz5 
 |-  ( ( ( ( # ` y ) + 1 ) e. ( ZZ>= ` 0 ) /\ ( # ` B ) e. ZZ ) -> ( ( ( # ` y ) + 1 ) e. ( 0 ... ( # ` B ) ) <-> ( ( # ` y ) + 1 ) <_ ( # ` B ) ) )
152 149 150 151 syl2anc 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ( # ` y ) + 1 ) e. ( 0 ... ( # ` B ) ) <-> ( ( # ` y ) + 1 ) <_ ( # ` B ) ) )
153 113 152 mpbird 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` y ) + 1 ) e. ( 0 ... ( # ` B ) ) )
154 bcval2 
 |-  ( ( ( # ` y ) + 1 ) e. ( 0 ... ( # ` B ) ) -> ( ( # ` B ) _C ( ( # ` y ) + 1 ) ) = ( ( ! ` ( # ` B ) ) / ( ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) x. ( ! ` ( ( # ` y ) + 1 ) ) ) ) )
155 153 154 syl 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) _C ( ( # ` y ) + 1 ) ) = ( ( ! ` ( # ` B ) ) / ( ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) x. ( ! ` ( ( # ` y ) + 1 ) ) ) ) )
156 146 oveq2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) = ( ( # ` B ) _C ( ( # ` y ) + 1 ) ) )
157 117 124 128 125 129 divdiv1d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ! ` ( ( # ` y ) + 1 ) ) ) = ( ( ! ` ( # ` B ) ) / ( ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) x. ( ! ` ( ( # ` y ) + 1 ) ) ) ) )
158 155 156 157 3eqtr4d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) = ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ! ` ( ( # ` y ) + 1 ) ) ) )
159 147 158 oveq12d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) = ( ( ! ` ( ( # ` y ) + 1 ) ) x. ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ! ` ( ( # ` y ) + 1 ) ) ) ) )
160 118 148 eleqtrdi 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( # ` y ) e. ( ZZ>= ` 0 ) )
161 peano2fzr 
 |-  ( ( ( # ` y ) e. ( ZZ>= ` 0 ) /\ ( ( # ` y ) + 1 ) e. ( 0 ... ( # ` B ) ) ) -> ( # ` y ) e. ( 0 ... ( # ` B ) ) )
162 160 153 161 syl2anc 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( # ` y ) e. ( 0 ... ( # ` B ) ) )
163 bcval2 
 |-  ( ( # ` y ) e. ( 0 ... ( # ` B ) ) -> ( ( # ` B ) _C ( # ` y ) ) = ( ( ! ` ( # ` B ) ) / ( ( ! ` ( ( # ` B ) - ( # ` y ) ) ) x. ( ! ` ( # ` y ) ) ) ) )
164 162 163 syl 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) _C ( # ` y ) ) = ( ( ! ` ( # ` B ) ) / ( ( ! ` ( ( # ` B ) - ( # ` y ) ) ) x. ( ! ` ( # ` y ) ) ) ) )
165 elfzle2 
 |-  ( ( # ` y ) e. ( 0 ... ( # ` B ) ) -> ( # ` y ) <_ ( # ` B ) )
166 162 165 syl 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( # ` y ) <_ ( # ` B ) )
167 nn0sub2 
 |-  ( ( ( # ` y ) e. NN0 /\ ( # ` B ) e. NN0 /\ ( # ` y ) <_ ( # ` B ) ) -> ( ( # ` B ) - ( # ` y ) ) e. NN0 )
168 118 115 166 167 syl3anc 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) - ( # ` y ) ) e. NN0 )
169 168 faccld 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` B ) - ( # ` y ) ) ) e. NN )
170 169 nncnd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` B ) - ( # ` y ) ) ) e. CC )
171 118 faccld 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( # ` y ) ) e. NN )
172 171 nncnd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( # ` y ) ) e. CC )
173 169 nnne0d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` B ) - ( # ` y ) ) ) =/= 0 )
174 171 nnne0d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( # ` y ) ) =/= 0 )
175 117 170 172 173 174 divdiv1d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( # ` y ) ) ) ) / ( ! ` ( # ` y ) ) ) = ( ( ! ` ( # ` B ) ) / ( ( ! ` ( ( # ` B ) - ( # ` y ) ) ) x. ( ! ` ( # ` y ) ) ) ) )
176 164 175 eqtr4d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` B ) _C ( # ` y ) ) = ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( # ` y ) ) ) ) / ( ! ` ( # ` y ) ) ) )
177 176 oveq2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) = ( ( ! ` ( # ` y ) ) x. ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( # ` y ) ) ) ) / ( ! ` ( # ` y ) ) ) ) )
178 facnn2 
 |-  ( ( ( # ` B ) - ( # ` y ) ) e. NN -> ( ! ` ( ( # ` B ) - ( # ` y ) ) ) = ( ( ! ` ( ( ( # ` B ) - ( # ` y ) ) - 1 ) ) x. ( ( # ` B ) - ( # ` y ) ) ) )
179 142 178 syl 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` B ) - ( # ` y ) ) ) = ( ( ! ` ( ( ( # ` B ) - ( # ` y ) ) - 1 ) ) x. ( ( # ` B ) - ( # ` y ) ) ) )
180 138 fveq2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( ( # ` B ) - ( # ` y ) ) - 1 ) ) = ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) )
181 180 oveq1d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( ( ( # ` B ) - ( # ` y ) ) - 1 ) ) x. ( ( # ` B ) - ( # ` y ) ) ) = ( ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) x. ( ( # ` B ) - ( # ` y ) ) ) )
182 179 181 eqtrd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ! ` ( ( # ` B ) - ( # ` y ) ) ) = ( ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) x. ( ( # ` B ) - ( # ` y ) ) ) )
183 182 oveq2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( # ` y ) ) ) ) = ( ( ! ` ( # ` B ) ) / ( ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) x. ( ( # ` B ) - ( # ` y ) ) ) ) )
184 117 170 173 divcld 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( # ` y ) ) ) ) e. CC )
185 184 172 174 divcan2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( # ` y ) ) x. ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( # ` y ) ) ) ) / ( ! ` ( # ` y ) ) ) ) = ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( # ` y ) ) ) ) )
186 117 124 133 125 143 divdiv1d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ( # ` B ) - ( # ` y ) ) ) = ( ( ! ` ( # ` B ) ) / ( ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) x. ( ( # ` B ) - ( # ` y ) ) ) ) )
187 183 185 186 3eqtr4d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( # ` y ) ) x. ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( # ` y ) ) ) ) / ( ! ` ( # ` y ) ) ) ) = ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ( # ` B ) - ( # ` y ) ) ) )
188 177 187 eqtrd 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) = ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ( # ` B ) - ( # ` y ) ) ) )
189 188 oveq2d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ( # ` B ) - ( # ` y ) ) x. ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) ) = ( ( ( # ` B ) - ( # ` y ) ) x. ( ( ( ! ` ( # ` B ) ) / ( ! ` ( ( # ` B ) - ( ( # ` y ) + 1 ) ) ) ) / ( ( # ` B ) - ( # ` y ) ) ) ) )
190 145 159 189 3eqtr4d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) = ( ( ( # ` B ) - ( # ` y ) ) x. ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) ) )
191 114 190 eqeq12d 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) <-> ( ( ( # ` B ) - ( # ` y ) ) x. ( # ` { f | f : y -1-1-> B } ) ) = ( ( ( # ` B ) - ( # ` y ) ) x. ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) ) ) )
192 109 191 syl5ibr 
 |-  ( ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) /\ ( ( # ` y ) + 1 ) <_ ( # ` B ) ) -> ( ( # ` { f | f : y -1-1-> B } ) = ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) -> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) ) )
193 108 192 81 79 ltlecasei 
 |-  ( ( B e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` { f | f : y -1-1-> B } ) = ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) -> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) ) )
194 193 expcom 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( B e. Fin -> ( ( # ` { f | f : y -1-1-> B } ) = ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) -> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) ) ) )
195 194 a2d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( B e. Fin -> ( # ` { f | f : y -1-1-> B } ) = ( ( ! ` ( # ` y ) ) x. ( ( # ` B ) _C ( # ` y ) ) ) ) -> ( B e. Fin -> ( # ` { f | f : ( y u. { z } ) -1-1-> B } ) = ( ( ! ` ( # ` ( y u. { z } ) ) ) x. ( ( # ` B ) _C ( # ` ( y u. { z } ) ) ) ) ) ) )
196 27 36 45 54 60 195 findcard2s 
 |-  ( A e. Fin -> ( B e. Fin -> ( # ` { f | f : A -1-1-> B } ) = ( ( ! ` ( # ` A ) ) x. ( ( # ` B ) _C ( # ` A ) ) ) ) )
197 196 imp 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` { f | f : A -1-1-> B } ) = ( ( ! ` ( # ` A ) ) x. ( ( # ` B ) _C ( # ` A ) ) ) )