Step Hyp Ref
Expression
1 oveq1 6303
. . . . . 6
2 1 fveq2d 5875
. . . . 5
3 fveq2 5871
. . . . . 6
4 3 oveq1d 6311
. . . . 5
5 2 , 4 eqeq12d 2479
. . . 4
6 5 imbi2d 316
. . 3
7 oveq2 6304
. . . . . . . 8
8 7 fveq2d 5875
. . . . . . 7
9 fveq2 5871
. . . . . . . 8
10 9 oveq2d 6312
. . . . . . 7
11 8 , 10 eqeq12d 2479
. . . . . 6
12 11 imbi2d 316
. . . . 5
13 oveq2 6304
. . . . . . . 8
14 13 fveq2d 5875
. . . . . . 7
15 fveq2 5871
. . . . . . . 8
16 15 oveq2d 6312
. . . . . . 7
17 14 , 16 eqeq12d 2479
. . . . . 6
18 17 imbi2d 316
. . . . 5
19 oveq2 6304
. . . . . . . 8
20 19 fveq2d 5875
. . . . . . 7
21 fveq2 5871
. . . . . . . 8
22 21 oveq2d 6312
. . . . . . 7
23 20 , 22 eqeq12d 2479
. . . . . 6
24 23 imbi2d 316
. . . . 5
25 oveq2 6304
. . . . . . . 8
26 25 fveq2d 5875
. . . . . . 7
27 fveq2 5871
. . . . . . . 8
28 27 oveq2d 6312
. . . . . . 7
29 26 , 28 eqeq12d 2479
. . . . . 6
30 29 imbi2d 316
. . . . 5
31 hashcl 12428
. . . . . . . . 9
32 31 nn0cnd 10879
. . . . . . . 8
33 32 exp0d 12304
. . . . . . 7
34 33 eqcomd 2465
. . . . . 6
35 vex 3112
. . . . . . . . . 10
36 map0e 7476
. . . . . . . . . 10
37 35 , 36 ax-mp 5
. . . . . . . . 9
38 df1o2 7161
. . . . . . . . 9
39 37 , 38 eqtri 2486
. . . . . . . 8
40 39 fveq2i 5874
. . . . . . 7
41 0ex 4582
. . . . . . . 8
42 hashsng 12438
. . . . . . . 8
43 41 , 42 ax-mp 5
. . . . . . 7
44 40 , 43 eqtri 2486
. . . . . 6
45 hash0 12437
. . . . . . 7
46 45 oveq2i 6307
. . . . . 6
47 34 , 44 , 46 3eqtr4g 2523
. . . . 5
48 oveq1 6303
. . . . . . . 8
49 vex 3112
. . . . . . . . . . . . 13
50 snex 4693
. . . . . . . . . . . . 13
51 49 , 50 , 35 3pm3.2i 1174
. . . . . . . . . . . 12
52 simprr 757
. . . . . . . . . . . . 13
53 disjsn 4090
. . . . . . . . . . . . 13
54 52 , 53 sylibr 212
. . . . . . . . . . . 12
55 mapunen 7706
. . . . . . . . . . . 12
56 51 , 54 , 55 sylancr 663
. . . . . . . . . . 11
57 simpl 457
. . . . . . . . . . . . 13
58 simprl 756
. . . . . . . . . . . . . 14
59 snfi 7616
. . . . . . . . . . . . . 14
60 unfi 7807
. . . . . . . . . . . . . 14
61 58 , 59 , 60 sylancl 662
. . . . . . . . . . . . 13
62 mapfi 7836
. . . . . . . . . . . . 13
63 57 , 61 , 62 syl2anc 661
. . . . . . . . . . . 12
64 mapfi 7836
. . . . . . . . . . . . . 14
65 64 adantrr 716
. . . . . . . . . . . . 13
66 mapfi 7836
. . . . . . . . . . . . . 14
67 57 , 59 , 66 sylancl 662
. . . . . . . . . . . . 13
68 xpfi 7811
. . . . . . . . . . . . 13
69 65 , 67 , 68 syl2anc 661
. . . . . . . . . . . 12
70 hashen 12420
. . . . . . . . . . . 12
71 63 , 69 , 70 syl2anc 661
. . . . . . . . . . 11
72 56 , 71 mpbird 232
. . . . . . . . . 10
73 hashxp 12492
. . . . . . . . . . . 12
74 65 , 67 , 73 syl2anc 661
. . . . . . . . . . 11
75 vex 3112
. . . . . . . . . . . . . 14
76 35 , 75 mapsnen 7613
. . . . . . . . . . . . 13
77 hashen 12420
. . . . . . . . . . . . . 14
78 67 , 57 , 77 syl2anc 661
. . . . . . . . . . . . 13
79 76 , 78 mpbiri 233
. . . . . . . . . . . 12
80 79 oveq2d 6312
. . . . . . . . . . 11
81 74 , 80 eqtrd 2498
. . . . . . . . . 10
82 72 , 81 eqtrd 2498
. . . . . . . . 9
83 hashunsng 12459
. . . . . . . . . . . . 13
84 75 , 83 ax-mp 5
. . . . . . . . . . . 12
85 84 adantl 466
. . . . . . . . . . 11
86 85 oveq2d 6312
. . . . . . . . . 10
87 32 adantr 465
. . . . . . . . . . 11
88 hashcl 12428
. . . . . . . . . . . 12
89 88 ad2antrl 727
. . . . . . . . . . 11
90 87 , 89 expp1d 12311
. . . . . . . . . 10
91 86 , 90 eqtrd 2498
. . . . . . . . 9
92 82 , 91 eqeq12d 2479
. . . . . . . 8
93 48 , 92 syl5ibr 221
. . . . . . 7
94 93 expcom 435
. . . . . 6
95 94 a2d 26
. . . . 5
96 12 , 18 , 24 , 30 , 47 , 95 findcard2s 7781
. . . 4
97 96 com12 31
. . 3
98 6 , 97 vtoclga 3173
. 2
99 98 imp 429
1