Metamath Proof Explorer

Theorem hashf1lem2

Description: Lemma for hashf1 . (Contributed by Mario Carneiro, 17-Apr-2015)

Ref Expression
Hypotheses hashf1lem2.1 
|- ( ph -> A e. Fin )
hashf1lem2.2 
|- ( ph -> B e. Fin )
hashf1lem2.3 
|- ( ph -> -. z e. A )
hashf1lem2.4 
|- ( ph -> ( ( # ` A ) + 1 ) <_ ( # ` B ) )
Assertion hashf1lem2 
|- ( ph -> ( # ` { f | f : ( A u. { z } ) -1-1-> B } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` { f | f : A -1-1-> B } ) ) )

Proof

Step Hyp Ref Expression
1 hashf1lem2.1 
 |-  ( ph -> A e. Fin )
2 hashf1lem2.2 
 |-  ( ph -> B e. Fin )
3 hashf1lem2.3 
 |-  ( ph -> -. z e. A )
4 hashf1lem2.4 
 |-  ( ph -> ( ( # ` A ) + 1 ) <_ ( # ` B ) )
5 ssid 
 |-  { f | f : A -1-1-> B } C_ { f | f : A -1-1-> B }
6 mapfi 
 |-  ( ( B e. Fin /\ A e. Fin ) -> ( B ^m A ) e. Fin )
7 2 1 6 syl2anc 
 |-  ( ph -> ( B ^m A ) e. Fin )
8 f1f 
 |-  ( f : A -1-1-> B -> f : A --> B )
9 2 1 elmapd 
 |-  ( ph -> ( f e. ( B ^m A ) <-> f : A --> B ) )
10 8 9 syl5ibr 
 |-  ( ph -> ( f : A -1-1-> B -> f e. ( B ^m A ) ) )
11 10 abssdv 
 |-  ( ph -> { f | f : A -1-1-> B } C_ ( B ^m A ) )
12 7 11 ssfid 
 |-  ( ph -> { f | f : A -1-1-> B } e. Fin )
13 sseq1 
 |-  ( x = (/) -> ( x C_ { f | f : A -1-1-> B } <-> (/) C_ { f | f : A -1-1-> B } ) )
14 eleq2 
 |-  ( x = (/) -> ( ( f |` A ) e. x <-> ( f |` A ) e. (/) ) )
15 noel 
 |-  -. ( f |` A ) e. (/)
16 15 pm2.21i 
 |-  ( ( f |` A ) e. (/) -> f e. (/) )
17 14 16 syl6bi 
 |-  ( x = (/) -> ( ( f |` A ) e. x -> f e. (/) ) )
18 17 adantrd 
 |-  ( x = (/) -> ( ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) -> f e. (/) ) )
19 18 abssdv 
 |-  ( x = (/) -> { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } C_ (/) )
20 ss0 
 |-  ( { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } C_ (/) -> { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } = (/) )
21 19 20 syl 
 |-  ( x = (/) -> { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } = (/) )
22 21 fveq2d 
 |-  ( x = (/) -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( # ` (/) ) )
23 hash0 
 |-  ( # ` (/) ) = 0
24 22 23 eqtrdi 
 |-  ( x = (/) -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = 0 )
25 fveq2 
 |-  ( x = (/) -> ( # ` x ) = ( # ` (/) ) )
26 25 23 eqtrdi 
 |-  ( x = (/) -> ( # ` x ) = 0 )
27 26 oveq2d 
 |-  ( x = (/) -> ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) = ( ( ( # ` B ) - ( # ` A ) ) x. 0 ) )
28 24 27 eqeq12d 
 |-  ( x = (/) -> ( ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) <-> 0 = ( ( ( # ` B ) - ( # ` A ) ) x. 0 ) ) )
29 13 28 imbi12d 
 |-  ( x = (/) -> ( ( x C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) ) <-> ( (/) C_ { f | f : A -1-1-> B } -> 0 = ( ( ( # ` B ) - ( # ` A ) ) x. 0 ) ) ) )
30 29 imbi2d 
 |-  ( x = (/) -> ( ( ph -> ( x C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) ) ) <-> ( ph -> ( (/) C_ { f | f : A -1-1-> B } -> 0 = ( ( ( # ` B ) - ( # ` A ) ) x. 0 ) ) ) ) )
31 sseq1 
 |-  ( x = y -> ( x C_ { f | f : A -1-1-> B } <-> y C_ { f | f : A -1-1-> B } ) )
32 eleq2 
 |-  ( x = y -> ( ( f |` A ) e. x <-> ( f |` A ) e. y ) )
33 32 anbi1d 
 |-  ( x = y -> ( ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) <-> ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) ) )
34 33 abbidv 
 |-  ( x = y -> { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } = { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } )
35 34 fveq2d 
 |-  ( x = y -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) )
36 fveq2 
 |-  ( x = y -> ( # ` x ) = ( # ` y ) )
37 36 oveq2d 
 |-  ( x = y -> ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) )
38 35 37 eqeq12d 
 |-  ( x = y -> ( ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) <-> ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) ) )
39 31 38 imbi12d 
 |-  ( x = y -> ( ( x C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) ) <-> ( y C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) ) ) )
40 39 imbi2d 
 |-  ( x = y -> ( ( ph -> ( x C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) ) ) <-> ( ph -> ( y C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) ) ) ) )
41 sseq1 
 |-  ( x = ( y u. { a } ) -> ( x C_ { f | f : A -1-1-> B } <-> ( y u. { a } ) C_ { f | f : A -1-1-> B } ) )
42 eleq2 
 |-  ( x = ( y u. { a } ) -> ( ( f |` A ) e. x <-> ( f |` A ) e. ( y u. { a } ) ) )
43 42 anbi1d 
 |-  ( x = ( y u. { a } ) -> ( ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) <-> ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) ) )
44 43 abbidv 
 |-  ( x = ( y u. { a } ) -> { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } = { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } )
45 44 fveq2d 
 |-  ( x = ( y u. { a } ) -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) )
46 fveq2 
 |-  ( x = ( y u. { a } ) -> ( # ` x ) = ( # ` ( y u. { a } ) ) )
47 46 oveq2d 
 |-  ( x = ( y u. { a } ) -> ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) )
48 45 47 eqeq12d 
 |-  ( x = ( y u. { a } ) -> ( ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) <-> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) ) )
49 41 48 imbi12d 
 |-  ( x = ( y u. { a } ) -> ( ( x C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) ) <-> ( ( y u. { a } ) C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) ) ) )
50 49 imbi2d 
 |-  ( x = ( y u. { a } ) -> ( ( ph -> ( x C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) ) ) <-> ( ph -> ( ( y u. { a } ) C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) ) ) ) )
51 sseq1 
 |-  ( x = { f | f : A -1-1-> B } -> ( x C_ { f | f : A -1-1-> B } <-> { f | f : A -1-1-> B } C_ { f | f : A -1-1-> B } ) )
52 f1eq1 
 |-  ( f = y -> ( f : A -1-1-> B <-> y : A -1-1-> B ) )
53 52 cbvabv 
 |-  { f | f : A -1-1-> B } = { y | y : A -1-1-> B }
54 53 eqeq2i 
 |-  ( x = { f | f : A -1-1-> B } <-> x = { y | y : A -1-1-> B } )
55 ssun1 
 |-  A C_ ( A u. { z } )
56 f1ssres 
 |-  ( ( f : ( A u. { z } ) -1-1-> B /\ A C_ ( A u. { z } ) ) -> ( f |` A ) : A -1-1-> B )
57 55 56 mpan2 
 |-  ( f : ( A u. { z } ) -1-1-> B -> ( f |` A ) : A -1-1-> B )
58 vex 
 |-  f e. _V
59 58 resex 
 |-  ( f |` A ) e. _V
60 f1eq1 
 |-  ( y = ( f |` A ) -> ( y : A -1-1-> B <-> ( f |` A ) : A -1-1-> B ) )
61 59 60 elab 
 |-  ( ( f |` A ) e. { y | y : A -1-1-> B } <-> ( f |` A ) : A -1-1-> B )
62 57 61 sylibr 
 |-  ( f : ( A u. { z } ) -1-1-> B -> ( f |` A ) e. { y | y : A -1-1-> B } )
63 eleq2 
 |-  ( x = { y | y : A -1-1-> B } -> ( ( f |` A ) e. x <-> ( f |` A ) e. { y | y : A -1-1-> B } ) )
64 62 63 syl5ibr 
 |-  ( x = { y | y : A -1-1-> B } -> ( f : ( A u. { z } ) -1-1-> B -> ( f |` A ) e. x ) )
65 64 pm4.71rd 
 |-  ( x = { y | y : A -1-1-> B } -> ( f : ( A u. { z } ) -1-1-> B <-> ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) ) )
66 65 bicomd 
 |-  ( x = { y | y : A -1-1-> B } -> ( ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) <-> f : ( A u. { z } ) -1-1-> B ) )
67 66 abbidv 
 |-  ( x = { y | y : A -1-1-> B } -> { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } = { f | f : ( A u. { z } ) -1-1-> B } )
68 54 67 sylbi 
 |-  ( x = { f | f : A -1-1-> B } -> { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } = { f | f : ( A u. { z } ) -1-1-> B } )
69 68 fveq2d 
 |-  ( x = { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( # ` { f | f : ( A u. { z } ) -1-1-> B } ) )
70 fveq2 
 |-  ( x = { f | f : A -1-1-> B } -> ( # ` x ) = ( # ` { f | f : A -1-1-> B } ) )
71 70 oveq2d 
 |-  ( x = { f | f : A -1-1-> B } -> ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` { f | f : A -1-1-> B } ) ) )
72 69 71 eqeq12d 
 |-  ( x = { f | f : A -1-1-> B } -> ( ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) <-> ( # ` { f | f : ( A u. { z } ) -1-1-> B } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` { f | f : A -1-1-> B } ) ) ) )
73 51 72 imbi12d 
 |-  ( x = { f | f : A -1-1-> B } -> ( ( x C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) ) <-> ( { f | f : A -1-1-> B } C_ { f | f : A -1-1-> B } -> ( # ` { f | f : ( A u. { z } ) -1-1-> B } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` { f | f : A -1-1-> B } ) ) ) ) )
74 73 imbi2d 
 |-  ( x = { f | f : A -1-1-> B } -> ( ( ph -> ( x C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. x /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` x ) ) ) ) <-> ( ph -> ( { f | f : A -1-1-> B } C_ { f | f : A -1-1-> B } -> ( # ` { f | f : ( A u. { z } ) -1-1-> B } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` { f | f : A -1-1-> B } ) ) ) ) ) )
75 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
76 2 75 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
77 76 nn0cnd 
 |-  ( ph -> ( # ` B ) e. CC )
78 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
79 1 78 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
80 79 nn0cnd 
 |-  ( ph -> ( # ` A ) e. CC )
81 77 80 subcld 
 |-  ( ph -> ( ( # ` B ) - ( # ` A ) ) e. CC )
82 81 mul01d 
 |-  ( ph -> ( ( ( # ` B ) - ( # ` A ) ) x. 0 ) = 0 )
83 82 eqcomd 
 |-  ( ph -> 0 = ( ( ( # ` B ) - ( # ` A ) ) x. 0 ) )
84 83 a1d 
 |-  ( ph -> ( (/) C_ { f | f : A -1-1-> B } -> 0 = ( ( ( # ` B ) - ( # ` A ) ) x. 0 ) ) )
85 ssun1 
 |-  y C_ ( y u. { a } )
86 sstr 
 |-  ( ( y C_ ( y u. { a } ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) -> y C_ { f | f : A -1-1-> B } )
87 85 86 mpan 
 |-  ( ( y u. { a } ) C_ { f | f : A -1-1-> B } -> y C_ { f | f : A -1-1-> B } )
88 87 imim1i 
 |-  ( ( y C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) ) -> ( ( y u. { a } ) C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) ) )
89 oveq1 
 |-  ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) -> ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) + ( ( # ` B ) - ( # ` A ) ) ) = ( ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) + ( ( # ` B ) - ( # ` A ) ) ) )
90 elun 
 |-  ( ( f |` A ) e. ( y u. { a } ) <-> ( ( f |` A ) e. y \/ ( f |` A ) e. { a } ) )
91 59 elsn 
 |-  ( ( f |` A ) e. { a } <-> ( f |` A ) = a )
92 91 orbi2i 
 |-  ( ( ( f |` A ) e. y \/ ( f |` A ) e. { a } ) <-> ( ( f |` A ) e. y \/ ( f |` A ) = a ) )
93 90 92 bitri 
 |-  ( ( f |` A ) e. ( y u. { a } ) <-> ( ( f |` A ) e. y \/ ( f |` A ) = a ) )
94 93 anbi1i 
 |-  ( ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) <-> ( ( ( f |` A ) e. y \/ ( f |` A ) = a ) /\ f : ( A u. { z } ) -1-1-> B ) )
95 andir 
 |-  ( ( ( ( f |` A ) e. y \/ ( f |` A ) = a ) /\ f : ( A u. { z } ) -1-1-> B ) <-> ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) \/ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) )
96 94 95 bitri 
 |-  ( ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) <-> ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) \/ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) )
97 96 abbii 
 |-  { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } = { f | ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) \/ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) }
98 unab 
 |-  ( { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } u. { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) = { f | ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) \/ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) }
99 97 98 eqtr4i 
 |-  { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } = ( { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } u. { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } )
100 99 fveq2i 
 |-  ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( # ` ( { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } u. { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) )
101 snfi 
 |-  { z } e. Fin
102 unfi 
 |-  ( ( A e. Fin /\ { z } e. Fin ) -> ( A u. { z } ) e. Fin )
103 1 101 102 sylancl 
 |-  ( ph -> ( A u. { z } ) e. Fin )
104 mapvalg 
 |-  ( ( B e. Fin /\ ( A u. { z } ) e. Fin ) -> ( B ^m ( A u. { z } ) ) = { f | f : ( A u. { z } ) --> B } )
105 2 103 104 syl2anc 
 |-  ( ph -> ( B ^m ( A u. { z } ) ) = { f | f : ( A u. { z } ) --> B } )
106 mapfi 
 |-  ( ( B e. Fin /\ ( A u. { z } ) e. Fin ) -> ( B ^m ( A u. { z } ) ) e. Fin )
107 2 103 106 syl2anc 
 |-  ( ph -> ( B ^m ( A u. { z } ) ) e. Fin )
108 105 107 eqeltrrd 
 |-  ( ph -> { f | f : ( A u. { z } ) --> B } e. Fin )
109 f1f 
 |-  ( f : ( A u. { z } ) -1-1-> B -> f : ( A u. { z } ) --> B )
110 109 adantl 
 |-  ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) -> f : ( A u. { z } ) --> B )
111 110 ss2abi 
 |-  { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } C_ { f | f : ( A u. { z } ) --> B }
112 ssfi 
 |-  ( ( { f | f : ( A u. { z } ) --> B } e. Fin /\ { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } C_ { f | f : ( A u. { z } ) --> B } ) -> { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } e. Fin )
113 108 111 112 sylancl 
 |-  ( ph -> { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } e. Fin )
114 113 adantr 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } e. Fin )
115 109 adantl 
 |-  ( ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) -> f : ( A u. { z } ) --> B )
116 115 ss2abi 
 |-  { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } C_ { f | f : ( A u. { z } ) --> B }
117 ssfi 
 |-  ( ( { f | f : ( A u. { z } ) --> B } e. Fin /\ { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } C_ { f | f : ( A u. { z } ) --> B } ) -> { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } e. Fin )
118 108 116 117 sylancl 
 |-  ( ph -> { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } e. Fin )
119 118 adantr 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } e. Fin )
120 inab 
 |-  ( { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } i^i { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) = { f | ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) /\ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) }
121 simprlr 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> -. a e. y )
122 abn0 
 |-  ( { f | ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) /\ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) } =/= (/) <-> E. f ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) /\ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) )
123 simprl 
 |-  ( ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) /\ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) -> ( f |` A ) = a )
124 simpll 
 |-  ( ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) /\ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) -> ( f |` A ) e. y )
125 123 124 eqeltrrd 
 |-  ( ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) /\ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) -> a e. y )
126 125 exlimiv 
 |-  ( E. f ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) /\ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) -> a e. y )
127 122 126 sylbi 
 |-  ( { f | ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) /\ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) } =/= (/) -> a e. y )
128 127 necon1bi 
 |-  ( -. a e. y -> { f | ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) /\ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) } = (/) )
129 121 128 syl 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> { f | ( ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) /\ ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) ) } = (/) )
130 120 129 syl5eq 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } i^i { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) = (/) )
131 hashun 
 |-  ( ( { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } e. Fin /\ { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } e. Fin /\ ( { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } i^i { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) = (/) ) -> ( # ` ( { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } u. { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) ) = ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) + ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) ) )
132 114 119 130 131 syl3anc 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( # ` ( { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } u. { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) ) = ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) + ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) ) )
133 100 132 syl5eq 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) + ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) ) )
134 simpr 
 |-  ( ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) -> ( y u. { a } ) C_ { f | f : A -1-1-> B } )
135 134 unssbd 
 |-  ( ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) -> { a } C_ { f | f : A -1-1-> B } )
136 vex 
 |-  a e. _V
137 136 snss 
 |-  ( a e. { f | f : A -1-1-> B } <-> { a } C_ { f | f : A -1-1-> B } )
138 135 137 sylibr 
 |-  ( ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) -> a e. { f | f : A -1-1-> B } )
139 f1eq1 
 |-  ( f = a -> ( f : A -1-1-> B <-> a : A -1-1-> B ) )
140 136 139 elab 
 |-  ( a e. { f | f : A -1-1-> B } <-> a : A -1-1-> B )
141 138 140 sylib 
 |-  ( ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) -> a : A -1-1-> B )
142 80 adantr 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( # ` A ) e. CC )
143 118 adantr 
 |-  ( ( ph /\ a : A -1-1-> B ) -> { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } e. Fin )
144 hashcl 
 |-  ( { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } e. Fin -> ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) e. NN0 )
145 143 144 syl 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) e. NN0 )
146 145 nn0cnd 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) e. CC )
147 142 146 pncan2d 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( ( ( # ` A ) + ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) ) - ( # ` A ) ) = ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) )
148 f1f1orn 
 |-  ( a : A -1-1-> B -> a : A -1-1-onto-> ran a )
149 148 adantl 
 |-  ( ( ph /\ a : A -1-1-> B ) -> a : A -1-1-onto-> ran a )
150 f1oen3g 
 |-  ( ( a e. _V /\ a : A -1-1-onto-> ran a ) -> A ~~ ran a )
151 136 149 150 sylancr 
 |-  ( ( ph /\ a : A -1-1-> B ) -> A ~~ ran a )
152 hasheni 
 |-  ( A ~~ ran a -> ( # ` A ) = ( # ` ran a ) )
153 151 152 syl 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( # ` A ) = ( # ` ran a ) )
154 1 adantr 
 |-  ( ( ph /\ a : A -1-1-> B ) -> A e. Fin )
155 2 adantr 
 |-  ( ( ph /\ a : A -1-1-> B ) -> B e. Fin )
156 3 adantr 
 |-  ( ( ph /\ a : A -1-1-> B ) -> -. z e. A )
157 4 adantr 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( ( # ` A ) + 1 ) <_ ( # ` B ) )
158 simpr 
 |-  ( ( ph /\ a : A -1-1-> B ) -> a : A -1-1-> B )
159 154 155 156 157 158 hashf1lem1 
 |-  ( ( ph /\ a : A -1-1-> B ) -> { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ~~ ( B \ ran a ) )
160 hasheni 
 |-  ( { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ~~ ( B \ ran a ) -> ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( # ` ( B \ ran a ) ) )
161 159 160 syl 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( # ` ( B \ ran a ) ) )
162 153 161 oveq12d 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( ( # ` A ) + ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) ) = ( ( # ` ran a ) + ( # ` ( B \ ran a ) ) ) )
163 f1f 
 |-  ( a : A -1-1-> B -> a : A --> B )
164 163 frnd 
 |-  ( a : A -1-1-> B -> ran a C_ B )
165 164 adantl 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ran a C_ B )
166 155 165 ssfid 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ran a e. Fin )
167 diffi 
 |-  ( B e. Fin -> ( B \ ran a ) e. Fin )
168 155 167 syl 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( B \ ran a ) e. Fin )
169 disjdif 
 |-  ( ran a i^i ( B \ ran a ) ) = (/)
170 169 a1i 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( ran a i^i ( B \ ran a ) ) = (/) )
171 hashun 
 |-  ( ( ran a e. Fin /\ ( B \ ran a ) e. Fin /\ ( ran a i^i ( B \ ran a ) ) = (/) ) -> ( # ` ( ran a u. ( B \ ran a ) ) ) = ( ( # ` ran a ) + ( # ` ( B \ ran a ) ) ) )
172 166 168 170 171 syl3anc 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( # ` ( ran a u. ( B \ ran a ) ) ) = ( ( # ` ran a ) + ( # ` ( B \ ran a ) ) ) )
173 undif 
 |-  ( ran a C_ B <-> ( ran a u. ( B \ ran a ) ) = B )
174 165 173 sylib 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( ran a u. ( B \ ran a ) ) = B )
175 174 fveq2d 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( # ` ( ran a u. ( B \ ran a ) ) ) = ( # ` B ) )
176 162 172 175 3eqtr2d 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( ( # ` A ) + ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) ) = ( # ` B ) )
177 176 oveq1d 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( ( ( # ` A ) + ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) ) - ( # ` A ) ) = ( ( # ` B ) - ( # ` A ) ) )
178 147 177 eqtr3d 
 |-  ( ( ph /\ a : A -1-1-> B ) -> ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( # ` B ) - ( # ` A ) ) )
179 141 178 sylan2 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( # ` B ) - ( # ` A ) ) )
180 179 oveq2d 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) + ( # ` { f | ( ( f |` A ) = a /\ f : ( A u. { z } ) -1-1-> B ) } ) ) = ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) + ( ( # ` B ) - ( # ` A ) ) ) )
181 133 180 eqtrd 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) + ( ( # ` B ) - ( # ` A ) ) ) )
182 hashunsng 
 |-  ( a e. _V -> ( ( y e. Fin /\ -. a e. y ) -> ( # ` ( y u. { a } ) ) = ( ( # ` y ) + 1 ) ) )
183 182 elv 
 |-  ( ( y e. Fin /\ -. a e. y ) -> ( # ` ( y u. { a } ) ) = ( ( # ` y ) + 1 ) )
184 183 ad2antrl 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( # ` ( y u. { a } ) ) = ( ( # ` y ) + 1 ) )
185 184 oveq2d 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( ( # ` y ) + 1 ) ) )
186 81 adantr 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( ( # ` B ) - ( # ` A ) ) e. CC )
187 simprll 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> y e. Fin )
188 hashcl 
 |-  ( y e. Fin -> ( # ` y ) e. NN0 )
189 187 188 syl 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( # ` y ) e. NN0 )
190 189 nn0cnd 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( # ` y ) e. CC )
191 1cnd 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> 1 e. CC )
192 186 190 191 adddid 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( ( ( # ` B ) - ( # ` A ) ) x. ( ( # ` y ) + 1 ) ) = ( ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) + ( ( ( # ` B ) - ( # ` A ) ) x. 1 ) ) )
193 186 mulid1d 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( ( ( # ` B ) - ( # ` A ) ) x. 1 ) = ( ( # ` B ) - ( # ` A ) ) )
194 193 oveq2d 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) + ( ( ( # ` B ) - ( # ` A ) ) x. 1 ) ) = ( ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) + ( ( # ` B ) - ( # ` A ) ) ) )
195 185 192 194 3eqtrd 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) = ( ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) + ( ( # ` B ) - ( # ` A ) ) ) )
196 181 195 eqeq12d 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) <-> ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) + ( ( # ` B ) - ( # ` A ) ) ) = ( ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) + ( ( # ` B ) - ( # ` A ) ) ) ) )
197 89 196 syl5ibr 
 |-  ( ( ph /\ ( ( y e. Fin /\ -. a e. y ) /\ ( y u. { a } ) C_ { f | f : A -1-1-> B } ) ) -> ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) -> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) ) )
198 197 expr 
 |-  ( ( ph /\ ( y e. Fin /\ -. a e. y ) ) -> ( ( y u. { a } ) C_ { f | f : A -1-1-> B } -> ( ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) -> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) ) ) )
199 198 a2d 
 |-  ( ( ph /\ ( y e. Fin /\ -. a e. y ) ) -> ( ( ( y u. { a } ) C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) ) -> ( ( y u. { a } ) C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) ) ) )
200 88 199 syl5 
 |-  ( ( ph /\ ( y e. Fin /\ -. a e. y ) ) -> ( ( y C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) ) -> ( ( y u. { a } ) C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) ) ) )
201 200 expcom 
 |-  ( ( y e. Fin /\ -. a e. y ) -> ( ph -> ( ( y C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) ) -> ( ( y u. { a } ) C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) ) ) ) )
202 201 a2d 
 |-  ( ( y e. Fin /\ -. a e. y ) -> ( ( ph -> ( y C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. y /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` y ) ) ) ) -> ( ph -> ( ( y u. { a } ) C_ { f | f : A -1-1-> B } -> ( # ` { f | ( ( f |` A ) e. ( y u. { a } ) /\ f : ( A u. { z } ) -1-1-> B ) } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` ( y u. { a } ) ) ) ) ) ) )
203 30 40 50 74 84 202 findcard2s 
 |-  ( { f | f : A -1-1-> B } e. Fin -> ( ph -> ( { f | f : A -1-1-> B } C_ { f | f : A -1-1-> B } -> ( # ` { f | f : ( A u. { z } ) -1-1-> B } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` { f | f : A -1-1-> B } ) ) ) ) )
204 12 203 mpcom 
 |-  ( ph -> ( { f | f : A -1-1-> B } C_ { f | f : A -1-1-> B } -> ( # ` { f | f : ( A u. { z } ) -1-1-> B } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` { f | f : A -1-1-> B } ) ) ) )
205 5 204 mpi 
 |-  ( ph -> ( # ` { f | f : ( A u. { z } ) -1-1-> B } ) = ( ( ( # ` B ) - ( # ` A ) ) x. ( # ` { f | f : A -1-1-> B } ) ) )