Step | Hyp | Ref
| Expression |
1 | | hlhilset.l |
. 2
HLHil |
2 | | hlhilset.k |
. . . . 5
|
3 | | elex 3212 |
. . . . . 6
|
4 | 3 | adantr 481 |
. . . . 5
|
5 | 2, 4 | syl 17 |
. . . 4
|
6 | | hlhilset.h |
. . . . . 6
|
7 | | fvex 6201 |
. . . . . 6
|
8 | 6, 7 | eqeltri 2697 |
. . . . 5
|
9 | 8 | mptex 6486 |
. . . 4
Scalar sSet HGMap
HDMap |
10 | | nfcv 2764 |
. . . . 5
|
11 | | nfcv 2764 |
. . . . . 6
|
12 | | nfcsb1v 3549 |
. . . . . 6
Scalar sSet HGMap
HDMap |
13 | 11, 12 | nfmpt 4746 |
. . . . 5
Scalar sSet HGMap
HDMap |
14 | | fveq2 6191 |
. . . . . . 7
|
15 | 14, 6 | syl6eqr 2674 |
. . . . . 6
|
16 | | csbeq1a 3542 |
. . . . . 6
Scalar sSet HGMap
HDMap
Scalar sSet HGMap
HDMap |
17 | 15, 16 | mpteq12dv 4733 |
. . . . 5
Scalar sSet HGMap
HDMap
Scalar sSet HGMap
HDMap |
18 | | df-hlhil 37225 |
. . . . 5
HLHil
Scalar sSet HGMap
HDMap |
19 | 10, 13, 17, 18 | fvmptf 6301 |
. . . 4
Scalar sSet HGMap
HDMap HLHil
Scalar sSet HGMap
HDMap |
20 | 5, 9, 19 | sylancl 694 |
. . 3
HLHil
Scalar sSet HGMap
HDMap |
21 | 5 | adantr 481 |
. . . 4
|
22 | | fvexd 6203 |
. . . . 5
|
23 | | fvexd 6203 |
. . . . . 6
|
24 | | id 22 |
. . . . . . . . . 10
|
25 | | id 22 |
. . . . . . . . . . . . 13
|
26 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
27 | 26 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
28 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
29 | 27, 28 | fveq12d 6197 |
. . . . . . . . . . . . . 14
|
30 | | hlhilset.u |
. . . . . . . . . . . . . 14
|
31 | 29, 30 | syl6eqr 2674 |
. . . . . . . . . . . . 13
|
32 | 25, 31 | sylan9eqr 2678 |
. . . . . . . . . . . 12
|
33 | 32 | fveq2d 6195 |
. . . . . . . . . . 11
|
34 | | hlhilset.v |
. . . . . . . . . . 11
|
35 | 33, 34 | syl6eqr 2674 |
. . . . . . . . . 10
|
36 | 24, 35 | sylan9eqr 2678 |
. . . . . . . . 9
|
37 | 36 | opeq2d 4409 |
. . . . . . . 8
|
38 | 32 | adantr 481 |
. . . . . . . . . . 11
|
39 | 38 | fveq2d 6195 |
. . . . . . . . . 10
|
40 | | hlhilset.p |
. . . . . . . . . 10
|
41 | 39, 40 | syl6eqr 2674 |
. . . . . . . . 9
|
42 | 41 | opeq2d 4409 |
. . . . . . . 8
|
43 | 26 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
44 | 43, 28 | fveq12d 6197 |
. . . . . . . . . . . . 13
|
45 | | hlhilset.e |
. . . . . . . . . . . . 13
|
46 | 44, 45 | syl6eqr 2674 |
. . . . . . . . . . . 12
|
47 | 26 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
HGMap HGMap |
48 | 47, 28 | fveq12d 6197 |
. . . . . . . . . . . . . 14
HGMap HGMap |
49 | | hlhilset.g |
. . . . . . . . . . . . . 14
HGMap |
50 | 48, 49 | syl6eqr 2674 |
. . . . . . . . . . . . 13
HGMap |
51 | 50 | opeq2d 4409 |
. . . . . . . . . . . 12
HGMap
|
52 | 46, 51 | oveq12d 6668 |
. . . . . . . . . . 11
sSet HGMap sSet |
53 | | hlhilset.r |
. . . . . . . . . . 11
sSet
|
54 | 52, 53 | syl6eqr 2674 |
. . . . . . . . . 10
sSet HGMap |
55 | 54 | opeq2d 4409 |
. . . . . . . . 9
Scalar sSet HGMap Scalar |
56 | 55 | ad2antrr 762 |
. . . . . . . 8
Scalar sSet
HGMap Scalar |
57 | 37, 42, 56 | tpeq123d 4283 |
. . . . . . 7
Scalar sSet HGMap
Scalar |
58 | 38 | fveq2d 6195 |
. . . . . . . . . 10
|
59 | | hlhilset.t |
. . . . . . . . . 10
|
60 | 58, 59 | syl6eqr 2674 |
. . . . . . . . 9
|
61 | 60 | opeq2d 4409 |
. . . . . . . 8
|
62 | 26 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
HDMap HDMap |
63 | 62, 28 | fveq12d 6197 |
. . . . . . . . . . . . . . 15
HDMap HDMap |
64 | | hlhilset.s |
. . . . . . . . . . . . . . 15
HDMap |
65 | 63, 64 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
HDMap |
66 | 65 | ad2antrr 762 |
. . . . . . . . . . . . 13
HDMap |
67 | 66 | fveq1d 6193 |
. . . . . . . . . . . 12
HDMap |
68 | 67 | fveq1d 6193 |
. . . . . . . . . . 11
HDMap |
69 | 36, 36, 68 | mpt2eq123dv 6717 |
. . . . . . . . . 10
HDMap |
70 | | hlhilset.i |
. . . . . . . . . 10
|
71 | 69, 70 | syl6eqr 2674 |
. . . . . . . . 9
HDMap |
72 | 71 | opeq2d 4409 |
. . . . . . . 8
HDMap |
73 | 61, 72 | preq12d 4276 |
. . . . . . 7
HDMap
|
74 | 57, 73 | uneq12d 3768 |
. . . . . 6
Scalar sSet HGMap
HDMap Scalar |
75 | 23, 74 | csbied 3560 |
. . . . 5
Scalar sSet HGMap
HDMap Scalar |
76 | 22, 75 | csbied 3560 |
. . . 4
Scalar sSet HGMap
HDMap Scalar |
77 | 21, 76 | csbied 3560 |
. . 3
Scalar sSet HGMap
HDMap Scalar |
78 | 2 | simprd 479 |
. . 3
|
79 | | tpex 6957 |
. . . . 5
Scalar |
80 | | prex 4909 |
. . . . 5
|
81 | 79, 80 | unex 6956 |
. . . 4
Scalar |
82 | 81 | a1i 11 |
. . 3
Scalar |
83 | 20, 77, 78, 82 | fvmptd 6288 |
. 2
HLHil Scalar |
84 | 1, 83 | syl5eq 2668 |
1
Scalar |